Formally Verified Lifting of C-compiled x86-64 Binaries
summary
A disassembler is built that lifts C‑compiled x86‑64 binaries into horograph outputs: graphs whose edges are Hoare triples and whose nodes are state predicates, exported to Isabelle proofs. It scales to hundreds of thousands of instructions and typically generates 250–300k Hoare triples per large binary. Applied to real code (Coreutils, Firefox, Xen hypervisor: 63 binaries, ~2,100 functions) it verifies most functions but annotates low‑level assumptions and reports 32 functions it cannot prove and 4 that time out (3‑hour limit).
AI-written summary · about
chapters (5)
- 0:00Start
- 1:25Disassembly Is Not a Solved Problem
- 1:52Existing Disassemblers
- 2:17Challenge behind Disassembly
- 4:31Monolithic Approach
related talks
21mDemystify Today's Binary Disassembling and How Modern ABI Makes it Easier
23mAn In-Depth Analysis of Disassembly on Full-Scale x86/x64 Binaries
24m(Ab)using Compiler Tools
28mForward Symbolic Execution for Trustworthy Automation of Binary Code Verification
01h 15mReliable Stack Traces, the Reality of Myth
51mReverse Engineering Binaries
53mFrom Within: Compiler Testing and Validation via Compilers
57mCode Genome - Fingerprinting Code to Build Trustworthy SBOMs