Abstract
We present BIRD: A Binary Intermediate Representation for formally verified Decompilation of x86-64 binaries. BIRD is a generic language capable of representing a binary program at various stages of decompilation. Decompilation can consist of various small translation passes, each raising the abstraction level from assembly to source code. Where most decompilation frameworks do not guarantee that their translations preserve the program’s operational semantics or even provide any formal semantics, translation passes built on top of BIRD must prove their output to be bisimilar to their input. This work presents the mathematical machinery needed to define BIRD. Moreover, it provides two instantiations - one representing x86-64 assembly, and one where registers have been replaced by variables—as well as a formally proven correct translation pass between them. This translation serves both as a practical first step in trustworthy decompilation as well as a proof of concept that semantic preserving translations of low-level programs are feasible. The entire effort has been formalized in the Coq theorem prover. As such, it does not only provide a mathematical formalism but can also be exported as executable code to be used in a decompiler. We envision BIRD to be used to define provably correct binary-level analyses and program transformations.
Original language | English |
---|---|
Title of host publication | Tests and Proofs |
Subtitle of host publication | 17th International Conference, TAP 2023, Leicester, UK, July 18–19, 2023, Proceedings |
Editors | Virgile Prevosto, Cristina Seceleanu |
Publisher | Springer, Cham |
Pages | 3-20 |
Number of pages | 18 |
Edition | 1 |
ISBN (Electronic) | 9783031388286 |
ISBN (Print) | 9783031388279 |
DOIs | |
Publication status | Published - Jul 2023 |
Event | 17th International Conference, Tests and Proofs 2023 - Leicester, United Kingdom Duration: 18 Jul 2023 → 19 Jul 2023 https://conf.researchr.org/home/tap-2023 |
Publication series
Series | Lecture Notes in Computer Science (LNCS) series |
---|---|
Volume | 14066 |
ISSN | 0302-9743 |
Conference
Conference | 17th International Conference, Tests and Proofs 2023 |
---|---|
Abbreviated title | TAP 2023 |
Country/Territory | United Kingdom |
City | Leicester |
Period | 18/07/23 → 19/07/23 |
Internet address |
Keywords
- Decompilation
- Formal Methods
- Static Analysis