SpecSafe: Detecting Cache Side Channels in a Speculative World
summary
SpecSafe detects cache side channels by defining Speculative-Aware noninterference (SANI), applying a program transformation that encodes speculative traces so existing cache-aware symbolic executors can check soundly. A taint pass selects 29/340 libgcrypt functions for symbolic analysis; symbolic execution removes five false positives and reveals three previously unknown code patterns that can leak up to 65 kilobits. The tool flags two potential Spectre-style leaks in ChaCha20 and Salsa20, and the paper proves the transformation’s soundness.
AI-written summary · about
chapters (10)
- 0:00Intro
- 0:13Side Channel Attacks
- 3:07What Can Go Wrong?
- 4:58Limitations of Existing Work
- 6:20New Speculative Execution Leakage
- 8:12Identifying Speculative Leakage (Speculative Aware Non-Interference)
- 9:15Capturing Speculative Behavior
- 10:53Program Transformation
- 13:13SpecSafe Evaluation
- 14:09Conclusion
related talks
01h 28m“Spectre: Secrets, Side-Channels, Sandboxes, and Security”
20mA Formal Model of Cache Speculation Side-Channels
13mExposing Cache Timing Side-Channel Leaks through Out-of-Order Symbolic Execution
20mAutomatic and Incremental Repair for Speculative Information Leaks
24mSNIP: Speculative Execution and Non-Interference Preservation for Compiler(…)
25mTowards Understanding Spectre-PHT in Memory-Safe Languages
56mSpectre/C++
25mExorcising Spectres with Secure Compilers