@inproceedings{936edd02357245679cccacebf5753cc1,
title = "Sound C Code Decompilation for a Subset of x86-64 Binaries",
abstract = "We present FoxDec: an approach to C code decompilation that aims at producing sound and recompilable code. Formal methods are used during three phases of the decompilation process: control flow recovery, symbolic execution, and variable analysis. The use of formal methods minimizes the trusted code base and ensures soundness: the extracted C code behaves the same as the original binary. Soundness and recompilablity enable C code decompilation to be used in the contexts of binary patching, binary porting, binary analysis and binary improvement, with confidence that the recompiled code{\textquoteright}s behavior is consistent with the original program. We demonstrate that FoxDec can be used to improve execution speed by recompiling a binary with different compiler options, to patch a memory leak with a code transformation tool, and to port a binary to a different architecture. FoxDec can also be leveraged to port a binary to run as a unikernel, a minimal and secure virtual machine usually requiring source access for porting.",
author = "F. Verbeek and Pierre Olivier and Binoy Ravindran",
year = "2020",
doi = "10.1007/978-3-030-58768-0_14",
language = "English",
isbn = "978-3-030-58768-0",
series = "Lecture Notes in Computer Science (LNCS) series",
publisher = "Springer Nature Switzerland AG",
pages = "247--264",
editor = "{de Boer}, Frank and Antonio Cerone",
booktitle = "Software Engineering and Formal Methods",
address = "Switzerland",
note = "18th International Conference on Software Engineering and Formal Methods, SEFM 2020 ; Conference date: 14-09-2020 Through 18-09-2020",
url = "https://event.cwi.nl/sefm2020/",
}