Verifying and Synthesizing Constant-Resource Implementations with Types

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.

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