Dynamic Analysis and Debugging of Binary Code for Security Applications - Runtime Verification - page 409

3 Cross-Platform Binary Symbolic Execution System (CBASS)

In contrast to existing symbolic execution tools, where the core analysis algorithms
are tied to specific DBI tools or whole-system emulators, CBASS performs symbolic
execution on the platform independent REIL IR. This is advantageous because any
enhancement to the core analysis algorithms would automatically benefit all platforms.

3.1 The REIL IR

REIL stands for Reverse Engineering Intermediate Language [16]. It is a platform in-
dependent intermediate representation of disassembled code, originally designed for
supporting static code analysis. We adopt REIL in our system for three reasons:

- Translators for statically mapping the native instruction set to REIL IR are readily
available for most of the ISAs, including x86, ARM, PowerPC, and MIPS.
- The REIL instructions are sufficiently close to native instructions on most platforms
and therefore can be used to preserve the native register state easily.
- The semantics of REIL instructions can be encoded in SMT formulas precisely by
using the bit-vector theory, and therefore is amendable to symbolic analysis.

REIL has only seventeen instructions, each of which has a simple effect on the program
state. Each REIL instruction has three operands. The first two operands are always the
source operands and the last operand is always the destination operand. One or more of
the operands can be empty. Table 2 summarizes the seventeen REIL instructions. For a
more detailed description of REIL, please refer to the online document [17].
Designed for reverse engineering purposes, REIL provides the support to statically
translate native instructions in x86, ARM, PowerPC, and MIPS to their IR equivalents
for an instruction, a function, or the entire program. More importantly, REIL provides

Ta b l e 2 . The REIL Instructions and Their Semantics

Category REIL Instruction Semantics

Arithmetic ADD s1, s2, d d=s1+ s2

SUB s1, s2, d d = s1 s2

MUL s1, s2, d d=s1 ∗ s2

DIV s1, s2, d d=s1 / s2

MOD s1, s2, d d=s1mods2

if s2 > 0d=s1 ∗ 2 s 2
else d = s1 /2 −s 2

BSH s1, s2, d

Bitwise AND s1, s2, d d=s1&s2

OR s1, s2, d d=s1 | s2

XOR s1, s2, d d = s1 xor s2

Logical BISZ s1, ,d ifs1=0,d=1elsed=0

JCC s1, ,d iff s1 =0, set eip = d

Transfer LDM s1, ,d d=mem[s1]

STM s1, ,d mem[d] =s1

STR s1, ,d d=s1

Other NOP, , , No op

UNDEF , ,d Undefined instruction

UNKN , , Unknown instruction