Type-directed Program Transformation for Constant-Time Enforcement
summary
Claims a relaxed information-flow type that distinguishes direct vs indirect flows and proves any program typable under it can be automatically transformed into a semantically equivalent constant-time program. Transformation uses CT-select, delayed predicated merging, and dynamic bounds checks to avoid unsafe out‑of‑bounds accesses. Algorithms are implemented in the jasmin compiler and validated on crafted representative examples; reported overhead is large preoptimization but shrinks after standard compiler passes, yielding practical constant-time code.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:22Side-channel attacks
- 2:07Timing attack mitigations
- 3:15Constant-time policy
- 5:23Existing enforcement tools
- 8:38Limitations of transformations
- 10:01New program transformation
- 14:43Safety in transformations
- 16:27Transformation process
- 18:56Secure type systems
- 21:45Indirect flow tracking
- 23:15Type system guarantees
- 24:20Experimental results
- 25:05Q&A
related talks
26mType-directed Program Transformation for Constant-Time Enforcement
56mOn Type-Based Techniques for Program Manipulation
21mWhen Obfuscations Preserve Cryptographic Constant-Time
29mA Flow-Insensitive-Complete Program Representation
32mVerifying Constant-Time Implementations
47mInformation Flow Types, Runtime Monitors, and Gradual Typing
19mDecompiling for Constant-Time Analysis
33mA Historical Perspective on Program Transformation and Recent Developments (Invi...