foxdec-0.1.0.0: Formally Verified x86-64 Decompilation

This package contains tools for decompilation based on formal methods.

Modules

Algorithm
Submodules
- Algorithm.Dominance
- Algorithm.L0_Lifting
Analysis
Submodules
- Analysis.Context A Context stores all the information retrieved from the binary, as well as the command-line parameters passed to FoxDec.
- Analysis.ControlFlow Contains functions pertaining to control flow graph generation.
- Analysis.FunctionNames Provides functions to
- Analysis.Pointers Functions for dealing with symbolic pointers and abstraction.
Base Some base functions, imported by almost all other modules.
Config Some customizable constants.
Data
Submodules
- Data.JSON Provides a taxonomy for the generated output, as well as JSON functionality.
- Data.JSON_Taxonomy Provides a taxonomy for the generated output.
- Data.JumpTarget A datatype for resolving the operand of a jump/call
- Data.SPointer
- Data.SValue
- Data.SValue2
- Data.SymbolicExpression A datatype for symbolic expressions and symbolic predicates.
- Data.Variable
Generic
Submodules
- Generic.Address
- Generic.Binary
- Generic.HasSize
- Generic.Instruction
- Generic.Operand
- Generic.SymbolicConstituents
- Generic.SymbolicPropagation A generic abstract interpretation algorithm for propagating postcondition-transformations through a control flow graph.
Instantiation
Submodules
- Instantiation.BinaryElf
- Instantiation.BinaryMacho
- Instantiation.SymbolicPropagation Provides an instantiation of all functions necessary to do symbolic propagation
- Instantiation.SymbolicPropagation2 Provides an instantiation of all function necessary to do symbolic propagation
NASM
Submodules
- NASM.L0ToNASM Lift the L0 representation of the binary to symbolized and recompilable NASM.
OutputGeneration
Submodules
X86
Submodules
- X86.Address
- X86.Conventions In this file, we eumerate assumptions made on calling conventions and over external functions.
- X86.Flag
- X86.Instruction
- X86.Opcode
- X86.Operand
- X86.Prefix
- X86.Register