Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
summary
A sound, proof-producing symbolic execution framework is formalized and implemented in HOL4 theorem prover and HolBA, instantiated for the BIR intermediate language and tied to ISA models for RISC‑V and ARM Cortex‑M0. Core inference rules mirror symbolic-executor operations, with pruning and merging strategies that trade precision for scalability; all rules carry machine-checked soundness proofs. Automated runs prove functional contracts and compute interval time bounds for medium binaries (hundreds of instructions take ~seconds–minutes, larger ciphers up to ~10–60 minutes) — progress structures witness the results.
AI-written summary · about
chapters (14)
- 0:00Binary code verification intro
- 1:07Unstructured binary challenges
- 3:12Symbolic execution theory
- 5:00Concrete vs symbolic states
- 7:31Symbolic soundness structure
- 10:02Execution rules and ops
- 13:18HOL4 and Beer impl
- 15:49Proof automation arch
- 17:34Functional correctness workflow
- 20:04Case studies
- 21:27Cortex-M0 time bounds
- 23:14Tool comparison
- 24:20Summary and future
- 24:46Q&A
related talks
28mProving Memory Access Violations in Isabelle/HOL
31mSound Symbolic Execution via Abstract Interpretation and its Application to Sec...
21mEnhancing Symbolic Execution with Machine-Checked Safety Proofs
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
28mLightweight Hypervisor Verification: Putting the Hardware Burger on a Diet
24mQSYM : A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing
14mScaling Instruction-Selection Verification against Authoritative ISA Semantics
24mInception: System-Wide Security Testing of Real-World Embedded Systems Software