Proving Memory Access Violations in Isabelle/HOL
summary
Verifies memory isolation for SmuV and TrustLite by translating compiled C through BAP and BIL into Isabelle/HOL theories, extending the pipeline to produce adversary models and conformance predicates, and automatically generating litmus programs that cover every case where an assembly instruction could violate a predicate. Builds and runs the toolchain on real attestation implementations, produces concrete failing programs, mechanizes proofs that violations are detected, and uncovers ambiguous TrustLite control-flow rules that the predicates resolve and tighten.
AI-written summary · about
chapters (10)
- 0:00Memory access verification intro
- 1:24Memory isolation in attestation
- 3:52Verifying microvisor implementations
- 8:49C to Isabelle/HOL toolchain
- 13:19Adversary model for isolation
- 17:57Proving conformance predicates
- 19:22TrustLite architecture
- 21:50Discovering TrustLite ambiguities
- 22:54Control flow conformance
- 28:00Q&A
related talks
28mForward Symbolic Execution for Trustworthy Automation of Binary Code Verification
28mMemory simulations, security and optimization in a verified compiler
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
14mCollapsing Towers for Side-Channel Security
12mMemory-Safety Verification of Open Programs With Angelic Assumptions
28mLightweight Hypervisor Verification: Putting the Hardware Burger on a Diet
34mFormally verified hardening of C programs against hardware fault injection
01h 00mAI Safety through Programming?