Automatic and Incremental Repair for Speculative Information Leaks
summary
CureSpec is a model-checking framework that either proves a program free of speculative side‑channel leaks or inserts concrete mitigations (fences) and emits a checkable certificate. It runs over LLVM IR inside SeaHorn with Z3, reuses an over‑approximation incrementally to avoid full rechecks, and automatically fixes real code including AES from OpenSSL. Experiments show dramatic fence reductions versus a naive “fence everywhere” baseline, but several large benchmarks hit a two‑hour timeout and some repaired binaries incur up to ~50% runtime overhead.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 0:23Spectre attack explained
- 2:13Speculative leaks problem
- 3:42TSpec tool overview
- 4:50Making speculation visible
- 5:31Fence positions marking
- 6:17SeaHorn for vulnerability checking
- 7:20Incremental repair process
- 8:51Final program guarantees
- 9:33Fence position strategies
- 10:39Evaluation setup
- 12:13Baseline results
- 13:42Fences impact on performance
- 15:07Conclusion
- 15:36Q&A
related talks
15mSpecSafe: Detecting Cache Side Channels in a Speculative World
04mAutomatically Eliminating Speculative Leaks with Blade
24mSNIP: Speculative Execution and Non-Interference Preservation for Compiler(…)
25mExorcising Spectres with Secure Compilers
20mLifting Compiler Security Properties to Stronger Attackers: the Speculation Cas...
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)
18mHardware-Software Codesign for Mitigating Spectre
16mAutomatically Eliminating Speculative Leaks from Cryptographic Code with Blade