Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
summary
Paper introduces a lifting framework that upgrades compiler guarantees proved for weaker speculative semantics to stronger ones without redoing full secure compilation proofs. The analysis covers 9 compiler countermeasures across 5 Spectre classes and models 5 speculation mechanisms; fence- and retpoline-based defenses successfully lift to the strongest semantics under study, while speculative load hardening fails when indirect-jump speculation is allowed. Proof effort drops by using syntactic independence and trapped speculation criteria to derive Independence and safe nesting.
AI-written summary · about
chapters (10)
- 0:00Spectre attacks overview
- 2:07Compiler countermeasures limits
- 4:15Combined speculative attacks
- 6:25Nested transaction security
- 8:53Conditional security preservation
- 11:03Lifting theorem for compilers
- 12:28Lifting guarantees results
- 13:31Reducing proof burden
- 15:15Summary and future directions
- 15:47Q&A: Compiler chaining
related talks
20mLifting Compiler Security Properties to Stronger Attackers: the Speculation Cas...
25mExorcising Spectres with Secure Compilers
23mSecure Composition of SPECTRE Mitigations
56mSpectre/C++
24mSNIP: Speculative Execution and Non-Interference Preservation for Compiler(…)
01h 28m“Spectre: Secrets, Side-Channels, Sandboxes, and Security”
20mFSLH: Flexible Mechanized Speculative Load Hardening
16mMitigating Transient-Execution Attacks with CHERI Compartments