On the Decidability of Disassembling Binaries

The general consensus is that disassembly of binaries is undecidable. The cause lies in distinguishing instructions from data, and resolving indirections. Furthermore, binaries can behave in “weird” ways which have no counterpart in assembly languages, e.g., instructions may overlap, or use other instructions as data. Yet, the general consensus is that, for a large part of production binaries, disassembly works sufficiently well for the use cases at hand. This paper aims to address the question: for which binaries is disassembly decidable? For which binaries can disassembly become decidable if an external oracle, e.g., provides the set of instruction addresses, or resolves indirections? We present a set of five theorems on decidability of disassembly; each theorem corresponding to a use case. All five theorems are accompanied by a proof of correctness based on bisimilarity between the input binary and the output assembly program, and have been formalized in the Isabelle/HOL theorem prover.