Validated Binary Decompilation Without Tears

Abstract

Binaries are an attractive target for formal verification—they describe a precise and deterministic semantics that closely conforms to the execution. However, binary verification entails a decompilation process, and the credibility of the verification hinges on the correctness of the decompiler. In this paper, we present a translation validation approach to decompiler assurance. We define a simple and compositional formalisation of decompiler correctness that is strong enough to preserve safety properties as well as security hyperproperties, thereby enabling verification results of the decompiled code to transfer to the executable code. Our notion, termed conditional trace-equivalence, allows the decompilation to leverage heuristics by embedding them within the program semantics. Our translation validation approach is implemented in the AArch64 decompiler Basil. Its evaluation showcases that translation validation is well-suited to verifying binary decompilation that scales to real-world C binaries. Our encoding exemplifies that the approach incurs minimal engineering overhead.