Information Technology Reference
In-Depth Information
Table 3 shows the symbolic execution of the REIL instructions of the three native
x86 instructions. Notice that each native instruction is mapped to a sequence of REIL
instructions. The REIL instructions take the native registers and memory values as in-
put, transform them by using intermediate registers, and return the results back to the
native registers and memory. For example, the instruction at
0x401073
has the native
register
ebp
and memory value at address
0x12ff74
as input, and the native regis-
ter
edx
as output. Just before executing the instruction, the concrete value of
ebp
is
assumedtobe
0x12ff84
and the memory at the address
0x12ff74
has a symbolic
value. From the first two REIL instructions, we have
t1 = 0x12ff74
.The
ldm
in-
struction sets
t2 = mem[0x12ff74]
, which contains a symbolic value, and then
t2
= INPUT VAR[8]
.
After carrying out the symbolic execution as shown in Table 3, the branch condition
before executing
0040107a jnz loc 40108e
becomes
ite(ite(((((INPUT VAR[8]
xor 0x80) -0x80) and 0xffffffff) 98) and 0xffffffff)
. This is equiv-
alent to the SMT formula shown in Fig. 3. By negating the path condition and asking
the SMT solver for a satisfying solution, we can compute the new input value to be
98
,
which corresponds to
sBigBuf[0] == b
in the original code in Fig. 2.
Fig. 3.
Example: The Path Constraints in Z3 SMT Formula
4
Taint-Enabled Reverse Engineering Environment (TREE)
To unleash the analysis power of CBASS in security practice, we need to support
in-
teractive
analysis. Toward this end, we have developed the infrastructure that can (1)
generate REIL traces on demand, (2) visualize the analysis results on demand, (3) per-
form taint tracking on demand. Together, these new features form the basis of our taint-
enabled reverse engineering environment (TREE).
4.1
Interactive Trace Generation
TREE leverages existing features of IDA, a popular reverse engineering tool, to support
on-demand trace generation. IDA is a widely used tool in mainstream security prac-
tice. It has become the
de facto
standard tool for conducting vulnerability and malware
analysis. IDA can statically disassemble binary code on more than 50 processors and
support a wide range of operating systems.