Exposing Cache Timing Side-Channel Leaks through Out-of-Order Symbolic Execution

on YouTube ↗13m

" summary

Claims a practical symbolic-execution tool that models CPU out-of-order and speculative scheduling to expose cache-timing leaks. Implements Out-of-Order Symbolic Execution with four components: Out-of-Order generation, Necessity Analysis, Reorder Modeling, and SMT-backed cache-leak checking. Evaluates 24 real-world crypto/compute kernels under different cache associativities and reorder-buffer sizes, finds 5 programs leak under some settings while 19 remain leak-free, shows larger reorder buffers raise traces/leaks, and reports SymO3+ (speculation model) finds more leaks at roughly +3 hours per leaky benchmark.

AI-written summary · about

" chapters (19)

1. 0:00Intro
2. 0:11Cache Timing Side-channel
3. 0:32Cache Timing Leak
4. 1:07Our key insight
5. 1:24Motivating Example
6. 2:04In order execution - cache behavior
7. 2:56A potential out-of-order execution case
8. 3:30The out-of-order execution case-cache behavior
9. 4:06Observation - new leak due to out-of-order execution
10. 4:31Challenges for the leak detection
11. 5:56Out-of-Order Generation
12. 7:25Reorder Necessity Analysis (RNA)
13. 8:22Reorder Modeling
14. 9:13Cache leak Analysis
15. 10:01Benchmarks
16. 10:15Leak detection - overall result
17. 10:57The impact of compiler optimization levels
18. 11:52The compound analysis with Speculation
19. 12:34Conclusions

" related talks

• 15mSpecSafe: Detecting Cache Side Channels in a Speculative WorldDanfeng Zhang, Gang Tan, Mahmut Taylan Kandemir, Robert Brotzman-Smith · OOPSLA 2021
• 27mCacheD: Identifying Cache-Based Timing Channels in Production SoftwarePei Wang, Xiao Liu, Danfeng Zhang, Shuai Wang, Dinghao Wu · 26th USENIX Security Symposium (USENIX Security '17)
• 15mI Know What You Said: Unveiling Hardware Cache Side-Channels in Local LargeZibo Gao, Junjie Hu, Feng Guo, Yixin Zhang, Yinglong Han, Siyuan Liu, Haiyang Li, Zhiqiang Lv · USENIX Security '25
• 20mA Formal Model of Cache Speculation Side-ChannelsCatalin Marinas · TLA+ Community Event 2020
• 01h 28m“Spectre: Secrets, Side-Channels, Sandboxes, and Security”Chandler Carruth · CppCon 2018
• 14mProtecting cryptography code from timing vulnerabilitiesTim McLean · StarCon 2018
• 14mCollapsing Towers for Side-Channel SecurityNada Amin, Adam Chlipala, Cameron Wong, Muhammad Abdullah, Yuheng Yang, Mengjia Yan · PEPM 2025
• 01h 01mTutorial: Side-Channel Attacks and Transient Execution Vulnerab...Allison Randal, Giorgos Christou · RISC-V Summit 2022