Poster: Formally Verified Binary Lifting to P-Code

Analysis of binary software plays a critical role in software security. Reverse engineers analyze binaries to discover vulnerabilities, patch legacy software, and detect malware. Most of the reverse engineering tools have been developed from a practical point of view, and do not provide any guarantees with their results. Recently, formally verified reverse engineering and decompilation have gained traction. These formal tools are for the most part proof-of-concept systems not yet suitable for real-world reverse-engineering tasks. In this poster, we explore the idea of formalizing part of an existing decompilation tool instead. We focus on the lifting from assembly to the IR P-Code in one of the most popular decompilers, Ghidra. This step occurs immediately after disassembly. We are developing a proof system inside the Isabelle theorem prover, to automatically prove semantical equivalence between the assembly and P-Code instructions. We leverage machine-learned x86-64 semantics, to stay as close as possible to actual CPU behavior. This approach has uncovered several shortcomings in Ghidra's P-Code and the lifting it performs. By using a theorem prover, we obtain guarantees that our system of formal semantics and lifting is internally consistent. This work brings the powerful guarantees that formal methods provide in reverse engineering research to the real world.