Exorcising Spectres with Secure Compilers
summary
Ongoing work builds a formal semantics that pairs a standard non‑speculative semantics with a prediction oracle–driven speculative semantics and an attacker model that sees memory access locations, branch targets and speculative begin/end events. It formalizes three concrete security criteria—strict speculative safety, speculative safety and speculative non‑interference—and uses them to reason whether compiler countermeasures (fences or masking) actually prevent extra leakage; work is a roadmap toward secure compilation guarantees, not final proofs.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:59Compiler-level countermeasures
- 1:59Speculative execution + branch prediction
- 4:51Spectre V1
- 8:46Injecting speculation barriers
- 9:23Speculative load-hardening (SLH)
- 11:12How to capture leakage?
- 13:24Notation
- 15:49Strict speculative safety
- 18:15Speculative non-interference
- 19:29A hierarchy of security conditions
- 22:11Secure compilation for Spectre
related talks
20mLifting Compiler Security Properties to Stronger Attackers: the Speculation Cas...
19mDo You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
24mSNIP: Speculative Execution and Non-Interference Preservation for Compiler(…)
23mSecure Composition of SPECTRE Mitigations
22mSNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
01h 28m“Spectre: Secrets, Side-Channels, Sandboxes, and Security”
33mGhosting the Spectre
56mSpectre/C++