Class Central is learner-supported. When you buy through links on our site, we may earn an affiliate commission.

YouTube

Verifying and Synthesizing Constant-Resource Implementations with Types

IEEE via YouTube

Overview

Explore a 19-minute IEEE conference talk on verifying and synthesizing constant-resource implementations using types. Delve into a novel type system for ensuring programs maintain constant-resource behavior, crucial for preventing side-channel attacks. Learn about the extension of automatic amortized resource analysis (AARA) techniques, achieving compositionality, precision, and automation. Discover how information flow tracking is incorporated into resource analysis, allowing for certification of programs that may violate constant-time requirements without leaking confidential information. Understand the concept of resource-aware noninterference and its enforcement. Examine the application of type inference algorithms in synthesizing constant-time implementations and repairing insecure programs automatically. Explore a second AARA system for computing lower bounds on resource usage and deriving quantitative bounds on information leakage. Gain insights into the practical applications of this approach in encryption, decryption routines, database queries, and other resource-aware functionalities.

Syllabus

Intro
Classic non-interference
Example: Sequential search
Solution: Quantitative language-based approach
Overview
Security type system
Examples
Global and local reasoning
Proving constant-resource
Evaluation
Summary

Taught by

IEEE Symposium on Security and Privacy

Reviews

Start your review of Verifying and Synthesizing Constant-Resource Implementations with Types

Never Stop Learning.

Get personalized course recommendations, track subjects and courses with reminders, and more.

Someone learning on their laptop while sitting on the floor.