CacheD: Identifying Cache-Based Timing Channels in Production Software
summary
CacheD applies symbolic execution and constraint solving over a cache-line model to decide whether memory loads differ for distinct secrets, produces concrete counterexample key pairs that trigger different cache lines, and confirms timing effects in a hardware simulator. It analyzes nine crypto implementations (over 120 million instructions) in under 17 CPU hours, reproduces prior findings and discovers new vulnerabilities in OpenSSL and Botan, reporting precise program points and memory-access formulas that indicate exploitable cache-timing channels.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:54Secret Dependent Memory Access
- 4:45Run Model
- 5:35Existing Research
- 6:45Structure of CacheD
- 7:58CacheD Example
- 15:37Symbolic Inscription
- 16:22Identify Independent Oneball Points
- 19:47Evaluation
- 22:16Case Study
- 24:01Summary
- 24:30Questions
related talks
13mExposing Cache Timing Side-Channel Leaks through Out-of-Order Symbolic Execution
15mI Know What You Said: Unveiling Hardware Cache Side-Channels in Local Large
17mQuantifying and Mitigating Cache Side Channel Leakage with Differential Set
14mProtecting cryptography code from timing vulnerabilities
15mSpecSafe: Detecting Cache Side Channels in a Speculative World
20mA Formal Model of Cache Speculation Side-Channels
35mShowTime: CPU Timing Attacks With the Human Eye
35mPage Cache Attacks: Microarchitectural Attacks on Flawless Hardware