Proving LTL Properties of Bitvector Programs and Decompiled Binaries
summary
Introduces a source transformation that replaces bitvector operators with extra linear-case splits and uses integer interpolation to let SMT-backed tools reason in the integer domain, claiming bitwise branching adds branching with negligible overhead, improves reachability, enables previously failing termination proofs, and yields the first practical LTL verification for bitvector code; implements the pipeline as DarkSea to lift binaries and reports that Ultimate/CPAchecker with the technique proves most benchmarks and verifies the lifted binaries; highlights use of integer interpolation.
AI-written summary · about
chapters (13)
- 0:00Intro
- 0:19Background
- 1:15Problems
- 3:23Example 1: Reachability
- 4:12Key Idea
- 5:11Example: Source-translation bitwise branching
- 6:29Transformation with bitwise branching
- 7:58Experiments: Reachability
- 8:46Weakening Rules and Termination
- 11:20Tools and Benchmarks
- 12:18Binary Decompilation
- 13:07LTL Experiments on Decompiled Binaries
- 13:52Reachability. Termination and LTL
related talks
28mProving Memory Access Violations in Isabelle/HOL
58mAutomating Relational Verification of Infinite-State Programs
40mSafe Coding with LLMs - Verifiable Scala Silver Bullet
21mFormal Methods for Everyone: Practical Tools for Computer-Aided Reasoning
15mOn Temporal Verification of Stateful P4 Programs
27mProofs of proofs: incremental verifiability from recursion and accumulation
28mForward Symbolic Execution for Trustworthy Automation of Binary Code Verification
34mFormally verified hardening of C programs against hardware fault injection