Taxonomy

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": [...], ... }

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).

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.

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" : [...]}

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.

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

Example of JSON output:

{"Terminating" : [] }

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

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.

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]}]}

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]}

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

Example of JSON output:

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