Preservation of speculative constant-time by compilation
summary
Shows that mainstream compilers (GCC -O0/-O1 and Jasmin) can break speculative constant-time by removing or introducing Spectre-v1 leaks, gives concrete counterexamples, and builds a mechanized proof-of-concept compiler (nine simplified passes) verified in Coq to preserve speculative constant-time. The work isolates directive and observation transformers for simulation, finds and patches a Jasmin type-checker bug that caused a memory-sharing vulnerability, and fixes all Jasmin cryptographic implementations with minimal impact.
AI-written summary · about
chapters (11)
- 0:00Intro to speculative CT preservation
- 1:13Key takeaways
- 3:00Spectre v1 recap
- 4:46Compiler security challenges
- 5:50Semantics under speculation
- 8:25Preservation via simulation
- 10:52Equivalence of conditions
- 11:34Constant propagation analysis
- 12:39Assignment elimination analysis
- 14:07Compiler pass preservation summary
- 15:12Q&A on register allocation
related talks
18mPreservation of Speculative Constant-time by Compilation
20mLifting Compiler Security Properties to Stronger Attackers: the Speculation Cas...
25mExorcising Spectres with Secure Compilers
23mFormally Verified Speculation and Deoptimization in a JIT Compiler
24mSNIP: Speculative Execution and Non-Interference Preservation for Compiler(…)
14mCollapsing Towers for Side-Channel Security
23mRobust Constant-Time Cryptography
29mTowards Formally Verified Just-In-Time Compilation