Information Technology Reference
In-Depth Information
To detect vulnerabilities, the taint sinks are usually the unexplored branches. When
we encounter a branch instruction, we create a path condition if the branch predicate
is tainted by a symbolic input.
As shown in Table 2, there are four categories of REIL instructions directly related
to symbolic execution. Mathematical and logical instructions perform the correspond-
ing operations on constants, registers, or memory. Memory instructions handle memory
read or write operations, which propagate values between registers and memory. Con-
trol instructions decide where to jump if the branch conditions are true. During symbolic
execution, we use a
concrete and symbolic memory (CSM)
map to represent the memory
state. It has both the concrete value and the symbolic value. For memory instructions, if
the address is symbolic, also called a symbolic pointer, we have to under-approximate
it by using the concrete value derived from the actual execution trace.
3.3
The Running Example
We use the instructions in Table 1 to demonstrate how to construct a path condition
during symbolic execution and how to generate the SMT formula. As the IR instructions
are fed to the symbolic execution engine, CBASS creates symbolic variables for the
taint sources and constructs the symbolic expressions. For each IR instruction, it creates
a new symbolic expression for the destination operand if any of the source operands is
symbolic. If all the source operands have concrete values, then it uses the concrete value
for the destination operand.
Ta b l e 3 .
Example: The REIL IR based Symbolic Execution
Native
Instruc-
REIL Instructions
Symbolic Execution, with ebp = 0x12ff84
and mem[12ff74] = INPUT
tions
00401073
movsx edx, byte
ss:[ebp-10]
40107300: add [DWORD FFFFFFF0, DWORD ebp,
QWORD t0]
t0 = 0x12ff84+0xfffffff0 = 10012ff74
40107301: and [QWORD t0, DWORD FFFFFFFF,
DWORD t1]
t1 = t0 and 0xffffffff =0x12ff74
40107302: ldm [DWORD t1, EMPTY , BYTE t2] t2 = mem[t1] =INPUT VA R [ 8 ]
40107303: xor [BYTE t2, BYTE 0x80, BYTE t3] t3 = INPUT VAR[8] xor 0x80
40107304: sub [BYTE t3, BYTE 0x80, DWORD t4] t4 = (INPUT VAR[8] xor 0x80) -0x80
40107305:
t5 = ((INPUT VAR[8] xor 0x80) -0x80)
and 0xffffffff
40107306: str [DWORD t5, EMPTY , DWORD edx] edx = ((INPUT VAR[8] xor 0x80) -0x80)
and 0xffffffff
and
[DWORD
t4,
BYTE
FFFFFFFF,
BYTE t5]
00401077
cmp
40107700:
and
[DWORD
edx,
DWORD
t0 = (((INPUT VAR[8] xor 0x80) -0x80)
and 0xffffffff)and 0x80000000
edx, 0x62
0x80000000, DWORD t0]
40107701: and [DWORD 98, DWORD 0x80000000,
DWORD t1]
t1 = 98 and 0x80000000 = 98
40107702:
sub
[DWORD
edx,
DWORD
98,
t2 = (((INPUT VAR[8] xor 0x80) -0x80)
and 0xffffffff) - 98
QWORD t2]
Ignore irrelevant temps ...
...
4010770B: and [QWORD t2, QWORD FFFFFFFF,
DWORD t8]
t8= ((((INPUT VAR[8] xor 0x80) -0x80)
and 0xffffffff) 98) and 0xffffffff
4010770C: bisz [DWORD t8, EMPTY , BYTE ZF]
ZF = ite(t8==0,1,0)
0040107a
jnz
40107A00: bisz [BYTE ZF, EMPTY , BYTE t0]
t0 = ite(ZF==0,1,0)
loc 40108e
40107A01:
jcc
[BYTE
t0,
EMPTY
,
DWORD
eip = ite(t0==1,0x40108e,0x40107c)
0x40108e]
