Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
summary
Blade automatically finds data-flow paths from memory reads that can speculatively carry secrets to cache-leaking sinks, models them with a transient vs stable type system, and solves a max-flow/min-cut problem to synthesize a minimal set of fine‑grained protect insertions. Protect is implemented with either fences or speculative‑load‑hardening masks, integrated into the Cranelift WebAssembly backend. Evaluation on verified crypto shows an order‑of‑magnitude fewer protects than a load‑everywhere baseline and reported costs of ~1.7, ~5, and 15–27% in different configurations.
AI-written summary · about
chapters (9)
- 0:00Start
- 2:25Taming Speculation with protect
- 2:47Mitigation Approach
- 3:19A Type System for Speculation Static approximation of the runtime propagation of speculative secrets
- 8:01JIT-Step Semantics for Speculation
- 8:49Fetch Stage Move commands from the stack to the instruction buffer
- 9:39Formal Guarantees
- 10:36How do you implement protect?
- 12:28Blade Implementation
related talks
04mAutomatically Eliminating Speculative Leaks with Blade
56mSpectre/C++
01h 28m“Spectre: Secrets, Side-Channels, Sandboxes, and Security”
15mSpecSafe: Detecting Cache Side Channels in a Speculative World
20mFSLH: Flexible Mechanized Speculative Load Hardening
33mGhosting the Spectre
46mRethinking Architectures and Abstraction for a World Where Security Improvements Matter More than Performance Gains
20mAutomatic and Incremental Repair for Speculative Information Leaks