3 ms·

Sound C Code Decompilation for a Subset of x86-64 Binaries [pdf]

22 points by matt_d 6y ago

sounds 6y ago
More info available here: https://ssrg-vt.github.io/FoxDec/ https://ssrg-vt.github.io/FoxDec/
speps 6y ago
https://llrm-project.org/ https://llrm-project.org/
peter_d_sherman 6y ago
>"The FoxDec (for Formal x86-64 Decompilation) project is investigating decompilation of x86-64 binaries into C code that is sound as well as fully recompilable. Soundness ensures that the decompiled C code is functionally equivalent to the input binary. Recompilability ensures that the decompiled C code can be successfully compiled to generate an executable binary for x86-64 architectures. Formally verified decompilation Decompilation to a high-level language involves multiple phases. At a high-level, the phases usually include disassembly that lifts assembly code from binary, control flow graph (CFG) recovery that extracts program CFG from assembly, extraction of high-level program constructs (e.g., statements, variables, references) from assembly, and type assignment. FoxDec is investigating techniques for the decompilation phases that are formally verified. FoxDec’s decompilation phases include disassembly; CFG recovery; extraction of an abstract code that models a program as a CFG of basic blocks; converting basic blocks into sequential code that models the program’s corresponding state changes over memory, registers, and flags; variable analysis that maps memory regions to variables and references; and type analysis that assigns types. Converting basic blocks into sequential code that captures program state changes requires a formal model of the underlying machine (i.e., formal semantics of x86-64 instructions). The project leverages the Chum project’s formal x86-64 machine model for this purpose. Central to formally verified decompilation is the notion of sound decompilation. FoxDec defines soundness for each of these decompilation phases (sound disassembly is explored in a different project) and formally verifies them: algorithms for each phase are formalized in the Isabelle/HOL theorem prover and proven correct."

22 points by matt_d 6y ago

sounds 6y ago

More info available here: https://ssrg-vt.github.io/FoxDec/ https://ssrg-vt.github.io/FoxDec/

speps 6y ago

https://llrm-project.org/ https://llrm-project.org/

peter_d_sherman 6y ago

>"The FoxDec (for Formal x86-64 Decompilation) project is investigating decompilation of x86-64 binaries into C code that is sound as well as fully recompilable. Soundness ensures that the decompiled C code is functionally equivalent to the input binary. Recompilability ensures that the decompiled C code can be successfully compiled to generate an executable binary for x86-64 architectures. Formally verified decompilation Decompilation to a high-level language involves multiple phases. At a high-level, the phases usually include disassembly that lifts assembly code from binary, control flow graph (CFG) recovery that extracts program CFG from assembly, extraction of high-level program constructs (e.g., statements, variables, references) from assembly, and type assignment. FoxDec is investigating techniques for the decompilation phases that are formally verified. FoxDec’s decompilation phases include disassembly; CFG recovery; extraction of an abstract code that models a program as a CFG of basic blocks; converting basic blocks into sequential code that models the program’s corresponding state changes over memory, registers, and flags; variable analysis that maps memory regions to variables and references; and type analysis that assigns types. Converting basic blocks into sequential code that captures program state changes requires a formal model of the underlying machine (i.e., formal semantics of x86-64 instructions). The project leverages the Chum project’s formal x86-64 machine model for this purpose. Central to formally verified decompilation is the notion of sound decompilation. FoxDec defines soundness for each of these decompilation phases (sound disassembly is explored in a different project) and formally verifies them: algorithms for each phase are formalized in the Isabelle/HOL theorem prover and proven correct."