FSLH: Flexible Mechanized Speculative Load Hardening
summary
Presents FSLH, a middle-ground Spectre v1 mitigation that uses a static information‑flow analysis plus selective masking and a semantics that inserts masks (an ideal semantics) to prove relative security — compiled code under speculation leaks no more than the sequential source. Mechanized proofs (~4,300 lines of Coq/Rocq) and a backwards compiler‑correctness step tie the model to code; it generalizes Selective SLH and Ultimate SLH (the latter measured at ~150% overhead), but there is no practical implementation or real‑world evaluation yet.
AI-written summary · about
chapters (8)
- 0:00FSLH introduction and goals
- 1:48Spectre mitigation shortcomings
- 3:11Selective and ultimate SLH overview
- 5:19Flexible mechanized SLH
- 8:07Static and dynamic analysis combo
- 11:57FSLH advantages and proof
- 12:40Future work and challenges
- 13:42Q&A
related talks
56mSpectre/C++
19mDo You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
20mLifting Compiler Security Properties to Stronger Attackers: the Speculation Cas...
01h 28m“Spectre: Secrets, Side-Channels, Sandboxes, and Security”
16mAutomatically Eliminating Speculative Leaks from Cryptographic Code with Blade
04mAutomatically Eliminating Speculative Leaks with Blade
24mSNIP: Speculative Execution and Non-Interference Preservation for Compiler(…)
23mSecure Composition of SPECTRE Mitigations