Pantomime: Constructive Leakage Proofs via Simulation
summary
Claims a constructive alternative to non-interference: build a simulator circuit that reproduces all attacker-observable timing using only the censored secret, then check equivalence. Implementation Pantomime is in Haskell, verifies a 5‑stage in‑order AIMCore (≈800 LOC) with a 300‑line leakage spec and a 200‑line simulator, and finishes checks in ~30–40s using a local SMT back end. Leakages are executable and found two CVEs in WolfSSL. The refinement mapping is a Haskell function and artifacts are available.
AI-written summary · about
chapters (6)
- 0:00Pantomime introduction
- 3:21Hardware constant-time proofs
- 6:55Simulating timing via circuits
- 9:55Adder fast path case
- 13:39Pantomime evaluation
- 16:49Q&A
related talks
12mLeakage models are a leaky abstraction (...)
14mCollapsing Towers for Side-Channel Security
26mNon-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
01h 08mTutorial: Security
32mBlack box side-channel leakage verification using statistical approach
12mHardware Verification of Timing Side Channel Freedom in the Spectre Era
24mSNIP: Speculative Execution and Non-Interference Preservation for Compiler(…)
22mSNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations