Decompiling for Constant-Time Analysis
summary
Claims that mainstream decompilers can hide timing leaks by turning branches into conditional moves, tests five popular decompilers and finds unsoundness for constant‑time (CT) analysis, and formalizes CT transparency as the property that transformations neither remove nor introduce CT violations. Proves that making leakage transformers injective leakage transformer yields transparency, implements a pragmatic variant called CT-redec by removing nontransparent passes, and shows it recovers all vulnerabilities in the evaluation set (RedecK had removed 45).
AI-written summary · about
chapters (8)
- 0:00Constant-time analysis intro
- 2:50Binary analysis for constant time
- 3:53Decompilation removes leaks
- 6:18Formal properties for transformations
- 9:27Proving reflection and preservation
- 11:34Injectivity enables transformations
- 12:40RedDeck constant-time aware
- 14:05Summary and future
related talks
32mVerifying Constant-Time Implementations
14mCollapsing Towers for Side-Channel Security
21mWhen Obfuscations Preserve Cryptographic Constant-Time
28mType-directed Program Transformation for Constant-Time Enforcement
18mPreservation of speculative constant-time by compilation
22mReconciling Progress-Intensive Noninterference and Declassification
12mLeakage models are a leaky abstraction (...)
54mLost and Found in Translation