Lifting Compiler Security Properties to Stronger Attackers: the Speculation Cas...
summary
A formal framework proves when a compiler countermeasure for Spectre-style leaks preserves security against stronger attacker models by modelling speculative primitives as labeled transition contracts and by requiring a compiler to be a well-formed translator. Security is RSNIP (robust speculative no-interference preservation). Independence means compilation does not introduce new speculative channels; syntactic Independence is a simple check when inserted instructions (e.g., fences) never overlap speculative opcodes. Applied to an indirect-jump mitigation that rewrites to a return trapped in a fenced self-loop, the method shows preservation for several combined attackers but finds gaps (some mitigations like SLS remain vulnerable).
AI-written summary · about
chapters (11)
- 0:00Introduction
- 0:23Spectre attacks and CPU speculation
- 2:51Compiler countermeasures
- 4:38Limitations of single-contract models
- 7:27Multi-contract security via waveform translators
- 9:41Case study: Red Pine compiler
- 11:08Fence-based compiler independence
- 13:14Stronger combined attackers
- 15:25Limitations and future work
- 16:49Q&A
- 18:41Closing remarks
related talks
19mDo You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
25mExorcising Spectres with Secure Compilers
24mSNIP: Speculative Execution and Non-Interference Preservation for Compiler(…)
22mSNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
18mPreservation of speculative constant-time by compilation
56mSpectre/C++
01h 28m“Spectre: Secrets, Side-Channels, Sandboxes, and Security”
16mMitigating Transient-Execution Attacks with CHERI Compartments