Skip to content

Program Structure

Jump to bottom
Thomas-Malcolm edited this page Jul 3, 2023 · 12 revisions

ADT to BASIL IR

Analysis is performed over the tool's own internal IR, BASIL IR. To do so, we need a way to take a program (assumed: binary), and transform it into this IR. To do this we use a tool to lift the Binary into an ADT (Abstract Data Type) - BAP lifts the ARM binary into its own IR, which it can then output as an ADT. We parse this ADT into an internal representation of what BAP lifted, and then translate this into our IR. This is then what is used to perform analysis on, and later translate into Boogie. An overview of the translating processes is given here.

Parsing Phase

ANTLR is a tool which takes a grammar file (BilAdt.g4) and creates a parser in Java that exposes tokens of the grammar through classes. The parser is autogenerated at runtime here.

val adtLexer = BilAdtLexer(CharStreams.fromFileName(fileName))
val tokens = CommonTokenStream(adtLexer)
val parser = BilAdtParser(tokens)

Walking Phase

The parser object then stores the parsed ADT (Abstract Data Tree) of the program. We then walk the ADT in AdtStatementLoader, which happens here.

val program = AdtStatementLoader.visitProject(parser.project())

As the ADT is walked we transform tokenised ADT nodes into internal BAP IR structures, all defined here. For example, a parsed direct call, stored by the parser as a DirectCallContext, will be converted into a BAPDirectCall.

These are all collated into a BAPProgram, which is essentially a list of functions in the program, and known memory sections, as represented by BAP.

Translating Phase

We now have an internal representation of the program we want to analyse, stored as a mapping of how BAP lifted it. Instead of performing analysis on this, we translate this into our own IR. The BASIL IR was designed to be easily translated into Boogie, meaning any transformations of the program structure resulting from analyses should not hamper our ability to translate into Boogie.

With the ADT parsed, we then match up symbol names with procedures in the ADT via the output of readelf, stored in the associated .relf. This helps us identify external functions, internal functions, and global variables.

The BAPProgram is then translated into an IR Program via BAPToIR.

We then remove external functions that we wish to ignore for analysis (such as printf), and clean up some BAP naming artefacts. At this point we have a BASIL IR of the program which we can then perform analyses over, and later translate to Boogie IVL.

Derivation of the ADT grammar

The grammar of the parser is inspired by the existing parser found at BinaryAnalysisPlatform/bap-python, in particular, the nodes found in adt.py, br.py and bil.py. The grammar attempts to reflect the inheritance hierarchy - the alternatives of a token are its subclasses.

For example, exp and term are subclasses of ADT, and thus in the grammar we have adt : exp | term | ....

General Notes

  • Negative numbers are encoded somewhat strangely. It takes the 2's complement representation of the number, and interprets the binary string as if it were an unsigned integer.
    • For example, the number -2 in 64 bits is 1111111111111111111111111111111111111111111111111111111111111110, which is interpreted in the ADT as Int(18446744073709551614, 64).

BASIL IR

The internal IR is designed such that it will translate easily to Boogie's IVL. The structure of the IR is given:

Program

Similar to BAP, this simply stores a list of known functions (procedures) and memory regions.

Procedure

A procedure is a representation of a function call, e.g. __libc_start_main. It stores

  • name : the function's string representation (e.g. "__libc_start_main").
  • address : offset into the binary.
  • blocks : a list of blocks in the procedure. See Block for an explanation of what constitutes a block.
  • calls : a list of function calls made by blocks in this procedure.

Memory Section

Represents an abstract region of memory. It has an address and a number of bytes in size. It can also store a sequence of bytes, representing data in the memory region.

Block

A basic block. Basic blocks in the context of this IR are consecutive sequences of instructions without a jump.

  • label : unique identifier for this block. This is the label that BAP gave it which has propagated through (its effectively a "BAP Address").
  • address : offset of the start of this block in the binary.
  • statements : sequence of statements in the block.
  • jumps : a jump from this block to another block - because our blocks are basic blocks, this will either be a single (direct|indirect) call, one GoTo call representing a loop, or two GoTo calls representing a conditional branch.

These sets are calculated and stored in the block also:

  • calls : names of functions (jumps) from this block which have been resolved (i.e. direct calls).
  • modifies : memory regions that are modified within this block.
  • locals : registers accessed during this block.

Statement

An expression (rhs) which is evaluated and stored into a register (lhs). For example, R2 := 3bv32 + 20bv32 is a statement, with lhs: R2 and rhs: Expression(3bv32 + 20bv32).

  • modifies : memory regions that this statement modifies.
  • locals : registers that this statement accesses (writing or reading).

LocalAssign

Assigning a value to a local variable. Local in this context means local to the procedure scope.

  • lhs : variable (local) which stores the evaluation of the rhs is stored in
  • rhs : expression to be evaluated and stored in lhs
  • modifies : empty for local.
  • locals : registers that this statement accesses (writing or reading).

MemoryAssign

Assigning a value to some memory region. A memory region can be on the stack, in the heap, or global.

  • lhs : memory region that the evaluation of the rhs is stored in
  • rhs : MemoryStore expression to be evaluated and stored at memory region specified in lhs
  • modifies : Memory regions that this statement modifies (lhs of statement).
  • locals : registers that this statement accesses (writing or reading).

Jump

A jump from this point in the program to another part in the program.

  • modifies : currently unused. NOTE: is this deprecated?
  • locals : dependencies for this jump. For example, a goto instruction will depend on some expression involving CPU flags. For procedure calls, these are parameters passed to the function call.
  • calls : currently unused. NOTE: is this deprecated?

GoTo

A jump directly to a specified address (Block in this instance), without any form of stack preparation or function prologue. Used in loops and conditionals.

  • target : the Block to jump to.
  • condition : if this is a conditional jump, the expression being evaluated to decide whether to jump
  • modifies : currently unused.
  • locals : any Variable used by the conditional expression, if this is a conditional jump.

DirectCall

Call to a procedure which is known.

  • target : the Procedure to jump to.
  • condition : if this is a conditional jump, the expression being evaluated to decide whether to jump.
  • returnTarget: the Block to jump back to upon execution finish.
  • locals : any Variable used by the conditional expression, if this is a conditional jump.
  • calls : any Procedure that is called within the target of this call.

IndirectCall

Call to a procedure given by an expression which has not been resolved / evaluated yet.

  • target : the Variable storing the address to jump to.
  • condition : if this is a conditional jump, the expression being evaluated to decide whether to jump.
  • returnTarget: the Block to jump back to upon execution finish.
  • locals : any Variable used by the conditional expression, if this is a conditional jump.

Expressions

All the above then depend Expressions, which contain representations for instructions to be evaluated / left symbolic, such as literals and binary operations. Boogie uses BitVectors for register values, and so operations in the BASIL IR are also represented as BitVector operations.

CFG Construction

TODO: being refactored.

Analyses

TODO: this will change when the CFG is refactored.

Analysis and Solvers

Supported Analyses

Clone this wiki locally