Lifter

The second step in the symbolic execution pipeline is to lift the assembly to the (extended) Reverse Engineering Intermediate Language (REIL)**. REIL is an intermediate language created by Zynamics for use in their binary analysis IDE, BinNavi. The specification for REIL can be found here. Relief utilizes an open source x86 to REIL binary lifter, the REIL Translation Library found here. This is a barebones implementation of a lifter, and a more complete lifter called openreil can be found here. I chose to use the REIL Translation Library because frankly, openreil was too complete and I wanted to build the fun parts myself.

Example:

>>> from loader import *
>>> my_bin = load_elf("tests/jmp_test")
>>> lifted_bin = my_bin.lift()
>>> for instructions in lifted_bin:
...     for il in instructions.il_instructions:
...             print il
... 
str (1, 32), (t00, 64)
str (t00, 64), (rax, 64)
str (rax, 64), (t00, 32)
str (rax, 64), (t01, 32)
and (t00, 32), (t01, 32), (t02, 32)

There would be no real reason for the end user to directly interact with the lifter however since binary loading and lifting is abstracted away into bin_to_cfg() in the top level api.

** If you are not familiar with intermediate languages, this is done in order to be able to perform system-independent analyses on binaries as well as increase the tractability of these analyses since intermediate languages often have much simpler syntax and semantics than assembly languages. For example x86 has ~1500 instructions (likely more) while REIL has 23, and REIL's 3 address syntax is very easy to parse. Another advantage of intermediate languages is that their instructions typically have no side effects, for example, the ADD instruction in x86 both moves the new value into the destination register and sets flags, an intermediate language would break this into multiple instructions, one to add source registers and move the result to the destination register, and several others to move the appropriate values into each individual flag register.