Preservation of Speculative Constant-time by Compilation
summary
Shows that common compilers (GCC -O0 and -O1 and Jasmin) produce speculatively insecure binaries from speculatively constant-time sources, then builds a proof-of-concept compiler mechanized in Coq that implements nine compiler passes (constant folding, dead-branch elimination, array reuse, RTL gen, etc.) and formally proves preservation of speculative constant-time. Also patches Jasmin’s speculative-constant-time checker and demonstrates that all Jasmin cryptographic implementations can be fixed with minimal changes, so the prototype succeeds where GCC/Jasmin initially fail.
AI-written summary · about
chapters (10)
- 0:00Speculative constant-time preservation
- 1:50Speculation and side-channel leakage
- 3:56Constant-time semantics
- 6:48Speculative constant-time under adversary
- 8:53Compiler simulation with directives
- 10:20Compiler with nine passes
- 11:44Constant propagation for security
- 12:26Dead assignment elimination
- 13:31Summary
- 14:33Q&A
related talks
18mPreservation of speculative constant-time by compilation
23mSmooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs(…)
20mLifting Compiler Security Properties to Stronger Attackers: the Speculation Cas...
23mFormally Verified Speculation and Deoptimization in a JIT Compiler
29mTowards Formally Verified Just-In-Time Compilation
19mDo You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
23mRobust Constant-Time Cryptography
24mA CompCert Compiler that Preserves Cryptographic Constant-time