Leakage models are a leaky abstraction (...)
summary
They verify timing by symbolically executing gate‑level RTL instead of assuming leakage models, translating circuits to Rosette and running a symbolic RTL simulator to prove cycle‑counts independent of secrets. Experiments include Ed25519 on a 7‑stage pipeline and code on tiny RISC‑V cores and OTBN, showing exact constant‑cycle bounds. Tool requires per‑target verification, occasional developer annotations for symbolic branching, and currently cannot modularly certify library fragments or scale to complex out‑of‑order speculative cores.
AI-written summary · about
chapters (10)
- 0:00Hardware crypto verification
- 0:44Leakage models limits
- 1:45Direct hardware timing
- 3:49RTL simulation with Rosette
- 5:58End-to-end timing verification
- 7:02Advantages over leakage models
- 8:27Case studies complexity
- 9:30Branching secrets timing
- 10:13Symbolic execution scaling
- 11:15Challenges future directions
related talks
20mPantomime: Constructive Leakage Proofs via Simulation
15mInterpretable Noninterference Measurement and its Application to Processor Designs
14mCollapsing Towers for Side-Channel Security
53mLightweight Resource Leak Verification and Inference
24mSystem Level Security Verification of RISC V Based SoCs
13mExposing Cache Timing Side-Channel Leaks through Out-of-Order Symbolic Execution
27mAutomated Learning and Verification of Embedded Security Architectures
01h 33mRISC V Verification for Processor Cores and Optional Custom Extensions