foxdec-0.1.0.0: Formally Verified x86-64 Decompilation
Safe HaskellNone
LanguageHaskell2010

Data.JSON_Taxonomy

Contents

Description

Provides a taxonomy for output generated by FoxDec. The output is a JSON object, whose schema is defined by the JSON datatype below. That datatype provides its fields, such as instructions and control_flow. This is an overview of some of the information retrievable from FoxDec. For example, we have omitted control flow graphs and per-instruction invariants to keep the size of the JSON object manageable. However, if more information is required, or if there is a request for information in a different form, then let us know.

On the right hand side, unfold the synopsis for an overview.

Synopsis

Taxonomy

data JSON Source #

The top-level JSON datastructure consists of the following fields:

  • instructions: All instructions with their addresses and sizes.
  • control_flow: For each instruction address, this provides the set of successor instruction addresses. This includes indirections, if they were resolved.
  • function_boundaries: For each function entry address, this provides an overview of all instruction addresses belonging to that function.
  • function_summaries: For each function entry address, this provides a pre- and postcondition.
  • invariants: For each each instruction address, for each function address that contains the instruction, this provides an invariant.
  • pointer_domains: For each each instruction address, for each function address that contains the instruction, this provides a symbolic expression for the pointer of each memory operand.

Example of the entire JSON output:

{ "instructions": [...], "control_flow": [...], ... }

Constructors

JSON 

Fields

Instances

Instances details
Generic JSON Source # 
Instance details

Defined in Data.JSON_Taxonomy

Associated Types

type Rep JSON :: Type -> Type #

Methods

from :: JSON -> Rep JSON x #

to :: Rep JSON x -> JSON #

type Rep JSON Source # 
Instance details

Defined in Data.JSON_Taxonomy

type ControlFlow = [(Word64, [Word64])] Source #

The ControlFlow is provided as a mapping from instruction addresses to lists of instruction addresses.

Example of JSON output:

[5907,[5909,5929]]

This states the instruction at address 5907 has two possible successor instruction addresses (5909 and 5929).

type FunctionBoundary = String Source #

The FunctionBoundary is provided as a pretty-printed representation of all instruction addresses covered by the function.

Example of JSON output:

"1200-->1238 ; 1280-->1284"

This Function Boundary states that the function spans two non-consecutive ranges of instruction addresses.

data FunctionSummary Source #

A FunctionSummary contains:

  • a preconditon: a Predicate that holds whenever the function is called within the binary.
  • a postconditon: a Postcondition that holds whenever the function is returning, if the function returns normally.

Example of JSON output:

{"precondition" : [...], "postcondition" : [...]}

Instances

Instances details
Generic FunctionSummary Source # 
Instance details

Defined in Data.JSON_Taxonomy

Associated Types

type Rep FunctionSummary :: Type -> Type #

type Rep FunctionSummary Source # 
Instance details

Defined in Data.JSON_Taxonomy

type Rep FunctionSummary = D1 ('MetaData "FunctionSummary" "Data.JSON_Taxonomy" "foxdec-0.1.0.0-KhdyLJGQiCJLT7iSdXA91t" 'False) (C1 ('MetaCons "FunctionSummary" 'PrefixI 'True) (S1 ('MetaSel ('Just "precondition") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Predicate) :*: S1 ('MetaSel ('Just "postcondition") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Postcondition)))

type Invariant = (Word64, Predicate) Source #

An Invariant contains:

  • the entry address of the function in which the instruction occurs. Note that (rarely) the same instruction can occur in multiple functions. Therefore, we provide an invariant per entry.
  • an invariant: a Predicate.

Example of JSON output:

 [4320,[[{"SP_Reg":"RIP"},{"SE_Immediate":4324}],[{"SP_Reg":"RAX"},...]]]

The instruction occurs in the function with entry address 4320. Register RIP is set to 4324. Register RAX is always equal to iths initial value.

data Postcondition Source #

A Postcondition provides information on the return status of a function.

Example of JSON output:

{"Terminating" : [] }

Constructors

Terminating

The function does never return

ReturningWith Predicate

The function returns in a state satisfying the Predicate

UnknownRetBehavior

It is unknown whether the function returns or not

Instances

Instances details
Generic Postcondition Source # 
Instance details

Defined in Data.JSON_Taxonomy

Associated Types

type Rep Postcondition :: Type -> Type #

type Rep Postcondition Source # 
Instance details

Defined in Data.JSON_Taxonomy

type Rep Postcondition = D1 ('MetaData "Postcondition" "Data.JSON_Taxonomy" "foxdec-0.1.0.0-KhdyLJGQiCJLT7iSdXA91t" 'False) (C1 ('MetaCons "Terminating" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ReturningWith" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Predicate)) :+: C1 ('MetaCons "UnknownRetBehavior" 'PrefixI 'False) (U1 :: Type -> Type)))

type Predicate = Map StatePart SimpleExpr Source #

A Predicate is a mapping from state parts (registers, memory, flags) to symbolic expressions.

Example of JSON output:

[
  [{"SP_Reg":"RDI"},{"Bottom":{"FromPointerBases":[{"Malloc":[4420,""]}]}}],
  [{"SP_Reg":"RSI"},{"SE_Immediate":8217}]
]

This predicate states that register RDI is a pointer with as base the return value of malloc, called at address 4420. Register RSI contains an immediate value.

data Instruction Source #

An Instruction has an address, a prefix (which may also be null), a mnemonic/opcode, a list of operands (possibly empty) and a size in bytes.

Example of JSON output:

{"size":7,"prefix":"BND","addr":4420,"opcode":"JMP","operands":[{"Memory":[{"AddressImm":11869},8]}]}

Constructors

Instruction 

Fields

Instances

Instances details
Generic Instruction Source # 
Instance details

Defined in Data.JSON_Taxonomy

Associated Types

type Rep Instruction :: Type -> Type #

type Rep Instruction Source # 
Instance details

Defined in Data.JSON_Taxonomy

data Operand Source #

An Operand is either a memory operand, an effective address (in case of LEA), a register or an immediate value.

Example of JSON output:

{"Memory":[{"AddressPlus":[{"AddressRegister":"RIP"},{"AddressImm":11869}]},8]}

Constructors

Memory Address Int

A region in memory, with an Address and a size in bytes

EffectiveAddress Address

An address itself, but not the value stored at the address.

Register Register

A storage location such as a register or a variable

Immediate Word64

An immediate value

Instances

Instances details
Generic Operand Source # 
Instance details

Defined in Data.JSON_Taxonomy

Associated Types

type Rep Operand :: Type -> Type #

Methods

from :: Operand -> Rep Operand x #

to :: Rep Operand x -> Operand #

type Rep Operand Source # 
Instance details

Defined in Data.JSON_Taxonomy

data Address Source #

An Address is the unresolved address computation in the memory operand of an instruction.

Example of JSON output:

{"AddressPlus":[{"AddressRegister":"RIP"},{"AddressImm":11869}]}

Constructors

AddressRegister Register

Reading a pointer from a storage

AddressImm Word64

Immediate value

AddressPlus Address Address

Plus

AddressMinus Address Address

Minus

AddressTimes Address Address

Times

Instances

Instances details
Generic Address Source # 
Instance details

Defined in Data.JSON_Taxonomy

Associated Types

type Rep Address :: Type -> Type #

Methods

from :: Address -> Rep Address x #

to :: Rep Address x -> Address #

type Rep Address Source # 
Instance details

Defined in Data.JSON_Taxonomy