Automatically Eliminating Speculative Leaks with Blade
summary
Blade is a static detector for speculative leaks that combines a transient-flow type system with an automatic repair pass that inserts a provably minimal set of fences. It models transient sources and sinks, turns the program into a flow graph and runs max-flow min-cut to find optimal cuts, and exposes a fine-grained protector primitive that converts transient to stable. Soundness is proved via the speculative interference property and evaluation on co-star shows SLH uses almost twice as many fences.
AI-written summary · about
chapters (6)
related talks
16mAutomatically Eliminating Speculative Leaks from Cryptographic Code with Blade
20mAutomatic and Incremental Repair for Speculative Information Leaks
20mFSLH: Flexible Mechanized Speculative Load Hardening
22mSNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
24mSNIP: Speculative Execution and Non-Interference Preservation for Compiler(…)
56mSpectre/C++
20mLifting Compiler Security Properties to Stronger Attackers: the Speculation Cas...
15mSpecSafe: Detecting Cache Side Channels in a Speculative World