Enhancing Symbolic Execution with Machine-Checked Safety Proofs
summary
Generates machine-checked safety proofs per-analysis so an exhaustive symbolic run yields a Rocq-verified proof tying symbolic to concrete LLVM IR semantics; implements a KLEE-based prototype that instruments KLEE to emit proofs and a ~20k-line Rocq formalization of concrete and symbolic semantics. Validation times are reasonable but unoptimized proofs hit huge sizes and some proof compilations run out of memory. The prototype finds previously unknown semantic implementation issues in KLEE and incurs only minor runtime overhead.
AI-written summary · about
chapters (11)
- 0:00Machine-checked safety proofs
- 2:06Unverified symbolic execution limits
- 4:55Translation validation with proofs
- 6:18Proof structure in Rocq
- 8:46Safety for execution trees
- 10:11Automated proof generation
- 13:25Proof compilation in Rocq
- 16:38Generalizing instruction proofs
- 17:18Implementation and evaluation
- 18:47Summary and future work
- 19:08Q&A
related talks
31mSound Symbolic Execution via Abstract Interpretation and its Application to Sec...
01h 17mProof-Carrying Code For the Age of AI: Machine-Checked Guarantees from(…)
28mForward Symbolic Execution for Trustworthy Automation of Binary Code Verification
01h 00mAI Safety through Programming?
21mFormal Methods for Everyone: Practical Tools for Computer-Aided Reasoning
11mFormally Verifying YUL Level Static Analyses and Optimization with Coq
32mVerifying Constant-Time Implementations
26mEndangered by the Language But Saved by the Compiler: Robust Safety via Semantic(…)