Hardware Verification of Timing Side Channel Freedom in the Spectre Era
summary
Claim: a synthesizable, pipelined two-core RISC-V design plus a hardware security monitor enforces strong timing isolation and is proven equivalent to an air‑gapped specification. The development uses cycle-accurate semantics formalized in Coq, a verified Koika→Circus compiler down to circuits, and a top-level theorem of trace-equivalence of MMIO. Proofs sidestep full processor correctness by only requiring purge-on-context-switch properties; prototype verification succeeds as a modular, replaceable proof approach.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 0:10Motivation
- 1:13Microtiming side channels
- 2:45Our proposal
- 4:35Outline
- 5:45Implementation
- 11:10Conclusion
related talks
17mSecuring High-performance RISC V-Processors from Time Speculation
33mGhosting the Spectre
14mCollapsing Towers for Side-Channel Security
24mDemocratising Formal Verification of RISC V Processors
18mCPU Security in the Context of RISC-V
16mMitigating Transient-Execution Attacks with CHERI Compartments
28mSanctum: Minimal Hardware Extensions for Strong Software Isolation
25mRISC-V Zkt: Portable Timing Attack Resistance (via Dynamic Taint Analys...