foxdec-0.1.0.0: Formally Verified x86-64 Decompilation

foxdec-0.1.0.0: Formally Verified x86-64 Decompilation

This package contains tools for decompilation based on formal methods.

Modules

• Algorithm
Submodules
• Analysis
Submodules
• A Context stores all the information retrieved from the binary, as well as the command-line parameters passed to FoxDec.
• Contains functions pertaining to control flow graph generation.
• Provides functions to
• Functions for dealing with symbolic pointers and abstraction.
• Some base functions, imported by almost all other modules.
• Some customizable constants.
• Data
Submodules
• Provides a taxonomy for the generated output, as well as JSON functionality.
• Provides a taxonomy for the generated output.
• A datatype for resolving the operand of a jump/call
• A datatype for symbolic expressions and symbolic predicates.
• Generic
Submodules
• A generic abstract interpretation algorithm for propagating postcondition-transformations through a control flow graph.
• Instantiation
Submodules
• Provides an instantiation of all function necessary to do symbolic propagation
• OutputGeneration
Submodules
• X86
Submodules
• In this file, we eumerate assumptions made on calling conventions and over external functions.