SNIP: Speculative Execution and Non-Interference Preservation for Compiler(…)
summary
Proposes a new directive-based simulation that models attacker-controlled microarchitectural choices and proves dead‑code elimination preserves speculative non‑interference; finds a concrete weakness in register allocation that leads to SNI violations and reproduces it across all four LLVM register allocators on code derived from libsodium (e.g., salsa). Builds a static poison‑analysis on a synchronized source/target product that locates poisoned leaks and inserts speculative‑load‑hardening mitigations iteratively to a fixpoint; the patched allocations are proven secure (fix not yet upstreamed to LLVM).
AI-written summary · about
chapters (13)
- 0:00SNIP and speculative execution
- 1:05Spectre attacks and leakage
- 5:03Spectre mitigations and limits
- 6:07Non-interference and SNI property
- 6:51Register allocation fails SNI
- 8:37SNIP goals: proving and fixing passes
- 10:03Simulation relations under semantics
- 12:29Poisoned states and refinement
- 14:13Fixing register allocation with poison
- 15:36Static poison analysis technique
- 18:49SNIP summary and guarantees
- 19:35Q&A: SNI vs constant time
- 20:44Q&A: Other optimizations and evaluation
related talks
22mSNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
20mLifting Compiler Security Properties to Stronger Attackers: the Speculation Cas...
56mSpectre/C++
25mExorcising Spectres with Secure Compilers
01h 28m“Spectre: Secrets, Side-Channels, Sandboxes, and Security”
19mDo You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
15mSpecSafe: Detecting Cache Side Channels in a Speculative World
16mMitigating Transient-Execution Attacks with CHERI Compartments