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

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’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
Chapter14
Pages247-264
Number of pages18
ISBN (Electronic)978-3-030-58767-3
ISBN (Print)978-3-030-58768-0
DOIs
Publication statusPublished - 2020
Event18th International Conference on Software Engineering and Formal Methods - Online, Amsterdam, Netherlands
Duration: 14 Sep 202018 Sep 2020
https://event.cwi.nl/sefm2020/

Publication series

SeriesLecture Notes in Computer Science (LNCS) series
Volume12310
ISSN0302-9743
SeriesTheoretical Computer Science and General Issues (LNCS subseries)
Volume12310

Conference

Conference18th International Conference on Software Engineering and Formal Methods
Abbreviated titleSEFM 2020
Country/TerritoryNetherlands
CityAmsterdam
Period14/09/2018/09/20
Internet address

Fingerprint

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