SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
summary
Introduces a speculative semantics that models attacker-controlled microarchitectural directives and leakage and proves a proof method (a new simulation relation) that preserves non-interference (SNIP) across compilation. Shows dead‑code elimination is SNIP, finds a previously unknown register‑allocation weakness that leaks secrets, reproduces it on LLVM using libsodium code, and builds a static product analysis plus an automated fix for register allocation. Provides machine‑checked proofs that the fixed allocator satisfies SNIP via simulation square and simulation cube.
AI-written summary · about
chapters (7)
- 0:00SNIP and speculative execution
- 3:39Spectre attacks in new semantics
- 7:12Safety in speculative semantics
- 13:53Simulation cube for SNIP
- 17:44Proving SNIP for dead code
- 18:27SNIP approach summary
- 18:50Q&A
related talks
24mSNIP: Speculative Execution and Non-Interference Preservation for Compiler(…)
20mLifting Compiler Security Properties to Stronger Attackers: the Speculation Cas...
25mExorcising Spectres with Secure Compilers
26mNon-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
01h 28m“Spectre: Secrets, Side-Channels, Sandboxes, and Security”
56mSpectre/C++
16mMitigating Transient-Execution Attacks with CHERI Compartments
15mSpecSafe: Detecting Cache Side Channels in a Speculative World