A Formal Model of Cache Speculation Side-Channels
summary
A TLA+ specification models speculative execution as two-CPU speculative model sharing memory and a single cached/not-cached bit per address, with non-deterministic instruction selection and separate speculative registers. TLC finds a counterexample: a Spectre v1 style trace where combining an untrusted offset with a high address yields different cache imprints and breaks confidentiality. The model maps Spectre variants and Meltdown to specific rule violations and validates mitigations like CSDB, SSBB, SB and kernel page table isolation at the abstract level.
AI-written summary · about
chapters (8)
- 0:00Introduction to talk
- 1:32Abstract CPU model
- 6:51Speculative execution model
- 9:24Security properties definition
- 12:58Model checking results
- 15:08Mapping vulnerabilities to model
- 17:41ARM barriers and workarounds
- 18:43Further reading and conclusion
related talks
01h 28m“Spectre: Secrets, Side-Channels, Sandboxes, and Security”
15mSpecSafe: Detecting Cache Side Channels in a Speculative World
01h 01mTutorial: Side-Channel Attacks and Transient Execution Vulnerab...
13mExposing Cache Timing Side-Channel Leaks through Out-of-Order Symbolic Execution
48mSpeculative execution vulnerabilities
14mCollapsing Towers for Side-Channel Security
15mI Know What You Said: Unveiling Hardware Cache Side-Channels in Local Large
24mSNIP: Speculative Execution and Non-Interference Preservation for Compiler(…)