Secure Composition of SPECTRE Mitigations
summary
Formal framework proves when compiler passes that add Spectre mitigations compose safely and when they do not, using robust preservation and a cross-language trace relation to project target-level no-leak properties back to intermediate levels. Results include composition theorems showing security preserved for intersected/projected classes, a concrete counterexample where swapping a barrier pass and a bounds-check pass reintroduces leakage, and a mechanized proof plan that builds a graph of compatible mitigation compositions.
AI-written summary · about
chapters (11)
- 0:00Spectre mitigation intro
- 1:44Speculative execution flaws
- 2:50Mitigation strategies limits
- 3:52Modular compiler security
- 5:39Composition pitfalls in pipelines
- 6:21Secure compilation preservation
- 9:32Cross-language trace relations
- 11:19Composing secure compilers
- 13:06Proving Spectre compositions
- 14:29Summary and future work
- 14:50Q&A
related talks
19mDo You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
25mExorcising Spectres with Secure Compilers
56mSpectre/C++
25mComposing Secure Compilers
01h 28m“Spectre: Secrets, Side-Channels, Sandboxes, and Security”
16mMitigating Transient-Execution Attacks with CHERI Compartments
46mRethinking Architectures and Abstraction for a World Where Security Improvements Matter More than Performance Gains
18mHardware-Software Codesign for Mitigating Spectre