BIRD: A Binary Intermediate Representation for Formally Verified Decompilation of X86-64 Binaries

Daniel Engel*, Freek Verbeek, Binoy Ravindran

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference Article in proceedingAcademicpeer-review

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 languageEnglish
Title of host publicationTests and Proofs
Subtitle of host publication17th International Conference, TAP 2023, Leicester, UK, July 18–19, 2023, Proceedings
EditorsVirgile Prevosto, Cristina Seceleanu
PublisherSpringer, Cham
Pages3-20
Number of pages18
Edition1
ISBN (Electronic)9783031388286
ISBN (Print)9783031388279
DOIs
Publication statusPublished - Jul 2023
Event17th International Conference, Tests and Proofs 2023 - Leicester, United Kingdom
Duration: 18 Jul 202319 Jul 2023
https://conf.researchr.org/home/tap-2023

Publication series

SeriesLecture Notes in Computer Science (LNCS) series
Volume14066
ISSN0302-9743

Conference

Conference17th International Conference, Tests and Proofs 2023
Abbreviated titleTAP 2023
Country/TerritoryUnited Kingdom
CityLeicester
Period18/07/2319/07/23
Internet address

Keywords

  • Decompilation
  • Formal Methods
  • Static Analysis

Fingerprint

Dive into the research topics of 'BIRD: A Binary Intermediate Representation for Formally Verified Decompilation of X86-64 Binaries'. Together they form a unique fingerprint.

Cite this