Assuring that fielded software is free of vulnerabilities exploitable by adversaries is critically important in military applications deployed by the Department of Defense (DoD). For systems that include binary-only software components, existing analysis solutions are limited, and any warnings of potential vulnerabilities would require significant manual effort by experts to investigate. Repairing binary code is even more difficult and expensive.

It is typically much easier to work with decompiled code than with raw machine code or assembly code, so using decompilation has the potential to greatly decrease the cost of finding and fixing vulnerabilities in binary code and to enable the DoD to fix potential vulnerabilities that might otherwise be cost prohibitive to investigate or repair. However, existing decompilers often do not produce code that is completely semantically faithful to the original binary.

To address this challenge, we launched this project to develop and implement techniques for automated semantic-equivalence checking. Our tool can identify which decompiled functions are likely to be semantically equivalent to the original binary function and which are unlikely to be equivalent. Our ultimate goal is to make it practical for DoD to use existing source-code static analyzers and repair tools on decompiled code, thereby increasing trust in the software. The figure below shows a pipeline for using our tool in practice. The binary code is decompiled with Ghidra, and the resulting decompiled code is compared for semantic equivalence to the LLVM produced by an independent binary lifter such as RetDec. Only those functions that are semantically equivalent are passed along for static analysis and repair.

This collaborative effort was informed by work with personnel who have significant experience in software assurance at the DoD and who are familiar with the types of issues that DoD faces when performing software assurance on binary code.