Bridging the Gap between Real-World and Formal Binary Lifting through(…)
summary
Defines correctness as filtered-simulation and formalizes three concrete transformations: control flow graph reconstruction, abstract stack reconstruction, and function input/output identification. Implements FIBLE for x86-64 Linux on GDRA/okl, includes three IR layers, an interpreter and a validator, and reproduces results on Coreutils and CGC. It automatically infers assumptions for >70% of programs; validator shows correctness for all checked runs; most CGC lifts finish <10s and most Coreutils lifts finish in 1–2 minutes. Artifacts are available.
AI-written summary · about
chapters (8)
- 0:00Binary lifting research intro
- 1:05Capturing machine code behaviors
- 2:30Key transformations in lifters
- 4:15Formalizing correctness
- 7:48Fibble lifter implementation
- 9:14Real-world binary results
- 11:00Conclusion and future
- 11:20Q&A
related talks
20mSift: Using Refinement-guided Automation to Verify Complex Distributed Systems
17mLet It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow
20mAn Automated Scalable RISC-V Cache Coherency Verification Project
25mProperty-agnostic base case extension for scalable verification of distributed systems
22mTowards Modelling and Verification of Coupler Behaviour in Climate Models
18mDeriving Semantic Checkers from Tests to Detect Silent Failures in Production...
46mVerified Vector Clocks An Unexpected Journey
16mIgloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verifica