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

F. Verbeek*, Pierre Olivier, Binoy Ravindran

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference Article in proceedingAcademicpeer-review


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’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.
Original languageEnglish
Title of host publicationSoftware Engineering and Formal Methods
Subtitle of host publication18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings
EditorsFrank de Boer, Antonio Cerone
Place of PublicationCham
PublisherSpringer Nature Switzerland AG
Number of pages18
ISBN (Electronic)978-3-030-58767-3
ISBN (Print)978-3-030-58768-0
Publication statusPublished - 2020
Event18th International Conference on Software Engineering and Formal Methods - Online, Amsterdam, Netherlands
Duration: 14 Sept 202018 Sept 2020

Publication series

SeriesLecture Notes in Computer Science (LNCS) series
SeriesTheoretical Computer Science and General Issues (LNCS subseries)


Conference18th International Conference on Software Engineering and Formal Methods
Abbreviated titleSEFM 2020
Internet address


Dive into the research topics of 'Sound C Code Decompilation for a Subset of x86-64 Binaries'. Together they form a unique fingerprint.

Cite this