GuoXB's Blog

Reverse Engineering 3201-Symbolic Analysis

发表于 分类于
本文字数： 3.6k 阅读时长 ≈ 13 分钟

Reverse Engineering 3201: Symbolic Analysis

课程链接：https://p.ost2.fyi/courses/course-v1:OpenSecurityTraining2+RE3201_symexec+2021_V1/course/

该套课程从Z3到SAT，再到angr，比较系统的介绍了符号执行的大致发展和思想，但是相对来说比较简略，其习题设置需要一定的逆向基础，否则做起来会比较花时间去理解。主要内容是以 binary bomb 程序为例来讲解angr的各种基础用法。

Binary Bomb

接下来通过对这个例子的讲解来简要介绍angr常见的一些基础用法：符号化寄存器、栈、内存等
首先看一下 bomb 程序的整体流程：

image-20231129203456418

binary 总共有6个阶段，每个阶段都需要单独来解，这里也侧面教了如何对一个程序中的片段做符号执行。

phase_1

接下来我们先看 phase_1:

![image-20231129203553171](D:\Program Files (x86)\Typora\typora-user-images\image-20231129203553171.png)

可以看到，a1 是我们第一阶段的输入，通过逆向分析，可以看到 phase_1 通过 strings_not_equal 函数来判断我们的输入a1 和 “I am just a renegade hockey mom.” 这个字符串作比较：

![image-20231129205541477](D:\Program Files (x86)\Typora\typora-user-images\image-20231129205541477.png)

从上反编译后的代码可以看到，如果不相等则返回 1 从而在下面进入 explode_bomb() 函数引爆炸弹。我们要做的（整个过程）都是避免程序调用explode_bomb函数。

phase_1 并不需要符号执行，我们能直接看到应该输入的字符串，但这里还是应用符号执行来做，我们首先通过反汇编代码来分析确定一下我们要开始符号执行的位置。

phase_1：

![image-20231129205844139](D:\Program Files (x86)\Typora\typora-user-images\image-20231129205844139.png)

strings_not_equal：

![image-20231129205820091](D:\Program Files (x86)\Typora\typora-user-images\image-20231129205820091.png)

我们以 phase_1 函数的开头 0x15a7 作为符号分析的起始地址（也可以直接进入strings_not_equal函数，但这样的话就需要手动对函数参数做设置，比较麻烦），a1是我们的输入，从反编译的代码可以看到，strings_not_equal函数的第一个参数与phase_1的参数一样，而在x64中第一个参数都是用 rdi 来传递的，所以在反汇编里没有体现。rdi 存储的就是存放我们输入字符串的地址。接下来结合代码来解释：

我们首先做一下全局变量设置：

1
2
3
4
import angr,claripy
proj = angr.Project('./bomb',auto_load_libs=False)
BASE_ADDR = proj.loader.main_object.min_addr
BOMB = BASE_ADDR + 0x1be5

BASE_ADDR 是程序加载后的基地址，BOMB是我们要避免的函数地址。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
# phase 1 
phase_1 = BASE_ADDR + 0x15a7 
# target_1 = BASE_ADDR + 0x15bf
target_1 = BASE_ADDR + 0x1b19

state = proj.factory.blank_state(addr=phase_1)
sim = proj.factory.simgr(state)
sim.explore(find=target_1,avoid=BOMB)

found = sim.found[0]
flag1_addr = found.regs.rbx
mem_addr_1 = found.memory.load(flag1_addr, 32)

print(found.solver.eval(mem_addr_1, cast_to=bytes))

target_1 不能是上面 0x15bf 的原因是，如果到那里，ebx已经改变，edi也已经改变，已经没有寄存器能够指向我们的输入，就不能进行求解了。

进行求解是内存是ebx所指向的内存，而不是最开始的edi，是因为在strings_not_equal函数开头，0x1AD9处将edi赋值给rbx，在0x1AE7处又将rbp赋值给rdi，此时rdi已经改变了，而且在后续都保持这个值，所以我们不能用这个。而ebx在target_1之前，始终保持指向我们的输入（在target之后会恢复原来的值），所以可以用。

执行后可以得到phase_1阶段的结果：

1
b'I am just a renegade hockey mom.'

phase_2

接下来看phase_2：

![image-20231129212457797](D:\Program Files (x86)\Typora\typora-user-images\image-20231129212457797.png)

同样，参数a1是我们的输入，read_six_numbers函数对我们的输入进行一些处理，具体为：

![image-20231129212616442](D:\Program Files (x86)\Typora\typora-user-images\image-20231129212616442.png)

从我们输入的字符串 a1 中，通过 sscanf 来获取 6 个int型整数。但由于涉及到比较复杂的sscanf函数，对输入做符号化比较麻烦，所以采用hook来简化其操作。

反汇编代码如下：

phase_2：

![image-20231129212359884](D:\Program Files (x86)\Typora\typora-user-images\image-20231129212359884.png)

首先对 read_six_numbers函数做一下hook：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
class read_six_numbers(angr.SimProcedure):
    answer_inits = []
    int_addrs = []
    #run函数的参数, 就是要hook的函数的参数，顺序和数量要一致。
    def run(self, str_addr, int_addr):
        # self.int_addrs.append(int_addr) //不知道干嘛用的，目前在phase2中没影响
        for i in range(6):
            bvs = self.state.solver.BVS("phase_2_int_%d" % i, 32)
            self.answer_inits.append(bvs)
            self.state.mem[int_addr].int.array(6)[i] = bvs
        return 6

# hook 函数
READ_SIX_NUMBERS = BASE_ADDR + 0x1c11
proj.hook(READ_SIX_NUMBERS, read_six_numbers())

首先还是确定第二阶段符号分析的入口位置，同样选择函数入口处。但是在target地址的选择上，官方选择了不直接执行到结尾，而是在中间断开，分两部分进行，在这里并没有理解为什么要这么做，可能是为了避免状态爆炸？这个还不是很清楚。但其他部分并没有什么注意的，都是常规流程，代码如下：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
phase_2 = BASE_ADDR + 0x15cb
target_2_A = BASE_ADDR + 0x15f3
target_2_B = BASE_ADDR + 0x1633

state = proj.factory.blank_state(addr=phase_2, remove_options={angr.options.LAZY_SOLVES})
sim = proj.factory.simulation_manager(state)
while len(sim.active) > 0:
    sim.explore(find=target_2_A, avoid=BOMB)

founds = sim.found
for found in founds:
    sim = proj.factory.simulation_manager(found)
    sim.explore(find=target_2_B, avoid=BOMB)
    if len(sim.found) > 0:
        found = sim.found[0]
        break
flag2 = " ".join([str(found.solver.eval(i)) for i in read_six_numbers.answer_inits])
print(flag2)

phase_3

接下来看phase_3：

![image-20231129214413724](D:\Program Files (x86)\Typora\typora-user-images\image-20231129214413724.png)

同样，参数a1是我们输入的字符串，这里通过sscanf来从我们输入的字符串中提取两个整数，这里的sscanf并不复杂，其参数是存放在栈上的，所以我们选择对栈上的数据进行符号化处理。通过反编译对sscanf函数参数看的不清楚，我们通过汇编代码来看：

![image-20231129214705410](D:\Program Files (x86)\Typora\typora-user-images\image-20231129214705410.png)

可以看到，第一个参数rdi被省略了，因为rdi没有变化，第二个参数rsi为格式化字符串 %d %d，第三个字符串rdx就是取出的第一个整数的地址，等于rsp也就是在栈顶，第四个参数rcx为[rsp+18h-14h]刚好是栈顶下一个。这里注意下汇编指令，lea和mov，指令虽然不同，但最终都是传递的地址。

对于sscanf稍微复杂些的函数，我们的起始位置就不能是开头了，如果还是开头，那么angr不能很好的处理sscanf得到的输入，所以我们把起始位置定位到sscanf下一条指令处 0x1665，cmp eax,1处，手动对sscanf参数（栈上的数据）做符号化处理。

注：压栈时，要注意，x64 栈指针 rsp 一次减 8 的整数倍，所以不能通过压两入两个32位符号值来分别取这两个整数，而要压入一个64位的，之后再进行划分。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
phase_3 = BASE_ADDR + 0x1665 #在 sscanf 之后
target_3 = BASE_ADDR + 0x16cc #0x16d2也可以，因为我这里求解的时候用了变量名，所以跟堆栈位置无关，如果求解使用教程里的stack_pop(),那么就需要保证栈指针rsp不被破坏，即只能是0x16cc
phase_3_flag = claripy.BVS('phase_3_flag',64) # 这里不能用两个32位，因为64位栈 栈帧 rsp-8，否则会报错
state = proj.factory.blank_state(addr=phase_3, remove_options={angr.options.LAZY_SOLVES})
# state.regs.rsp = state.regs.rbp
# state.regs.rsp -= 0x10
# 这里不对栈做处理也能成功得到结果，可能是因为刚好是参数刚好存放在栈顶吧，或者按照之前的思路对rsp和rbp做设置也可以得到结果。
# 将符号化变量压入栈
state.stack_push(phase_3_flag)
sim = proj.factory.simgr(state)
sim.explore(find=target_3, avoid=BOMB, enable_veritesting=True) # 不太明白这个veritesting是干嘛的，不加对于这个程序也能求解出结果
found = sim.found[0]
flag3 = []
# temp = found.solver.eval(found.stack_pop())
temp = found.solver.eval(phase_3_flag)
# 将高位和低位分开
low = temp & 0xffffffff
flag3.append(str(low))
high = temp >> 32 & 0xffffffff
flag3.append(str(high))
print(" ".join(flag3))

phase_4

接下来看phase_4：

![image-20231129220051220](D:\Program Files (x86)\Typora\typora-user-images\image-20231129220051220.png)

v2就是从我们输入字符串中提取的第一个整数，v3是第二个整数。同样，我们选择起始位置时跳过sscanf，在后面手动进行符号化值的设置。下面出现了func4，我们先来看看func4函数的内容：

![image-20231129220358229](D:\Program Files (x86)\Typora\typora-user-images\image-20231129220358229.png)

可以看到是一个递归函数，大概作用是从a2和a3之间找到a1（V2，也就是第一个整数）。而根据phase_4函数流程分析可以看到，第二个整数必须要等于10，随意我们只用对第一个值进行符号化即可。而第一个值对于func4来说是其第一个参数，通过rdi寄存器来传递，所以我们将起始位置定位到func4函数开头，手动为相应传参寄存器赋值来传递参数，并符号化rdi寄存器来获取第一个整数值。

func4汇编代码如下：

![image-20231129220925573](D:\Program Files (x86)\Typora\typora-user-images\image-20231129220925573.png)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
phase_4 = BASE_ADDR + 0x1715
target_4 = BASE_ADDR + 0x1732

phase_4_flag = claripy.BVS('phase_4_flag', 32)
state = proj.factory.blank_state(addr=phase_4, remove_options={angr.options.LAZY_SOLVES})
state.regs.edi = phase_4_flag
state.regs.esi = 0
state.regs.edx = 0x0e

sim = proj.factory.simgr(state)
sim.explore(find=target_4,avoid=BOMB)
found = sim.found[0]
flag = 10 - found.solver.eval(phase_4_flag) #结合程序分析，但是看不懂那个逆向后的程序算法
print(flag)

这里要注意的一点就是，func4函数返回值应该等于 10，但是符号执行求解得到的 7 其实就是直接让a1等于v3，并没有进行递归就推出了，此时func4的返回值是7而不是10，所以需要再做进一步处理，课程中的题解的方法是用 10 - 7，还不太能明白这么做的原理是什么，但是确实是对的，而且就算不是10，改成20和11也是对的，很神奇。猜测很算法有关，回头问问师弟。

phase_5

接下来看phase_5：

跟phase_3相似，所以直接放代码了：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
phase_5 = BASE_ADDR + 0x17f5
target_5 = BASE_ADDR + 0x184E
phase_5_flag = claripy.BVS('phase_3_flag',64)

state = proj.factory.blank_state(addr=phase_5, remove_options={angr.options.LAZY_SOLVES})
state.stack_push(phase_5_flag)
sim = proj.factory.simgr(state)
sim.explore(find=target_5, avoid=BOMB)
found = sim.found[0]
flag5 = []
# temp = found.solver.eval(found.stack_pop())
temp = found.solver.eval(phase_5_flag)
# 将高位和低位分开
low = temp & 0xffffffff
flag5.append(str(low))
high = temp >> 32 & 0xffffffff
flag5.append(str(high))
print(" ".join(flag5))

phase_6

接下来看phase_6：

跟phase_2比较类似，但是比2更加复杂，做法是一样的，都是将符号执行分成两步完成，可能是为了防止路径爆炸导致内存不够吧。

代码如下：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
phase_6 = BASE_ADDR + 0x185B
target_6_A = BASE_ADDR + 0x1906
target_6_B = BASE_ADDR + 0x1971 # add rsp, 60h

READ_SIX_NUMBERS = BASE_ADDR + 0x1c11

class read_six_numbers(angr.SimProcedure):
    answer_inits = []
    # int_addrs = []
    # run函数的参数, 就是要hook的函数的参数，顺序和数量要一致。
    def run(self, str_addr, int_addr):
        # self.int_addrs.append(int_addr) # 不知道干嘛用的，目前在phase2中没影响
        for i in range(6):
            bvs = self.state.solver.BVS("phase_6_int_%d" % i, 32)
            self.answer_inits.append(bvs)
            self.state.mem[int_addr].int.array(6)[i] = bvs

        return 6
    
proj.hook(READ_SIX_NUMBERS,read_six_numbers())

state = proj.factory.blank_state(addr=phase_6, remove_options={angr.options.LAZY_SOLVES})
sim = proj.factory.simgr(state)

# while len(sim.active)>0:
sim.explore(find=target_6_A,avoid=BOMB)
print(sim)
# print(sim.found)
founds = sim.found
for found in founds:
    sim = proj.factory.simgr(found)
    sim.explore(find=target_6_B, avoid=BOMB)
    if len(sim.found) >0 :
        found = sim.found[0]
        break
flag6 = [str(found.solver.eval(i)) for i in read_six_numbers.answer_inits]
flag6 = " ".join(flag6)
print(flag6)

总结

课程还是很好的，但是需要有一定的逆向基础，并且对汇编代码比较熟悉（甚至应该对angr有一些初步的了解，做过angr_CTF更好）。讲课的老师直接在反汇编得到的汇编代码上进行讲解，有些地方对汇编不熟悉的话，就需要取IDA中分析一下才能跟上老师的思路（IDA真好用），然后就是对于一些步骤仍然没有讲为什么要那么做，怎么发现的，可能是我的基础不好吧，自己探索了好一阵子。但总的来说课程还是可以的，尤其是bomb这个程序，综合联系了符号执行angr的一些常见基本操作，并且让我对blank_state()这个状态有了新的理解，也对如何进行复杂程序某一段指令的符号执行有了初步的认识。

附 Binary Bomb 的完整解题代码，solution.py:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
import angr,claripy

proj = angr.Project('./bomb',auto_load_libs=False)

BASE_ADDR = proj.loader.main_object.min_addr
BOMB = BASE_ADDR + 0x1be5
# print(hex(BASE_ADDR))

# phase 1 从寄存器中获取地址处的值
phase_1 = BASE_ADDR + 0x15a7
# target_1 = BASE_ADDR + 0x15bf
target_1 = BASE_ADDR + 0x1b19

state = proj.factory.blank_state(addr=phase_1)
sim = proj.factory.simgr(state)
sim.explore(find=target_1,avoid=BOMB)

found = sim.found[0]
flag1_addr = found.regs.rbx
mem_addr_1 = found.memory.load(flag1_addr, 32)

print(found.solver.eval(mem_addr_1, cast_to=bytes))


# phase 2
# 如何 hook 函数

# hook
class read_six_numbers(angr.SimProcedure):
    answer_inits = []
    int_addrs = []
    #run函数的参数, 就是要hook的函数的参数，顺序和数量要一致。
    def run(self, str_addr, int_addr):
        # self.int_addrs.append(int_addr) //不知道干嘛用的，目前在phase2中没影响
        for i in range(6):
            bvs = self.state.solver.BVS("phase_2_int_%d" % i, 32)
            self.answer_inits.append(bvs)
            self.state.mem[int_addr].int.array(6)[i] = bvs
        return 6

phase_2 = BASE_ADDR + 0x15cb
READ_SIX_NUMBERS = BASE_ADDR + 0x1c11
target_2_A = BASE_ADDR + 0x15f3
target_2_B = BASE_ADDR + 0x1633
# hook 函数
proj.hook(READ_SIX_NUMBERS, read_six_numbers())

state = proj.factory.blank_state(addr=phase_2, remove_options={angr.options.LAZY_SOLVES})
sim = proj.factory.simulation_manager(state)
while len(sim.active) > 0:
    sim.explore(find=target_2_A, avoid=BOMB)
print(sim)
founds = sim.found
for found in founds:
    sim = proj.factory.simulation_manager(found)
    sim.explore(find=target_2_B, avoid=BOMB)
    if len(sim.found) > 0:
        found = sim.found[0]
        break
flag2 = " ".join([str(found.solver.eval(i)) for i in read_six_numbers.answer_inits])
print(flag2)

# phase 3
# 符号化栈上的数据
phase_3 = BASE_ADDR + 0x1665 #在 sscanf 之后
target_3 = BASE_ADDR + 0x16cc #0x16d2也可以，因为我这里求解的时候用了变量名，所以跟堆栈位置无关，如果求解使用教程里的stack_pop(),那么就需要保证栈指针rsp不被破坏
phase_3_flag = claripy.BVS('phase_3_flag',64) # 这里不能用两个32位，因为64位栈 栈帧 rsp-8，否则会报错
state = proj.factory.blank_state(addr=phase_3, remove_options={angr.options.LAZY_SOLVES})
# state.regs.rsp = state.regs.rbp
# state.regs.rsp -= 0x10
# 将符号化变量压入栈
state.stack_push(phase_3_flag)
sim = proj.factory.simgr(state)
sim.explore(find=target_3, avoid=BOMB, enable_veritesting=True) # 不太明白这个veritesting是干嘛的，不加对于这个程序也能求解出结果
found = sim.found[0]
flag3 = []
# temp = found.solver.eval(found.stack_pop())
temp = found.solver.eval(phase_3_flag)
# 将高位和低位分开
low = temp & 0xffffffff
flag3.append(str(low))
high = temp >> 32 & 0xffffffff
flag3.append(str(high))
print(" ".join(flag3))

# phase 4
# 配合程序理解，来符号化执行程序
phase_4 = BASE_ADDR + 0x1715
target_4 = BASE_ADDR + 0x1732

phase_4_flag = claripy.BVS('phase_4_flag', 32)
state = proj.factory.blank_state(addr=phase_4, remove_options={angr.options.LAZY_SOLVES})
state.regs.edi = phase_4_flag
state.regs.esi = 0
state.regs.edx = 0x0e

sim = proj.factory.simgr(state)
sim.explore(find=target_4,avoid=BOMB)
found = sim.found[0]
flag = 10 - found.solver.eval(phase_4_flag) #结合程序分析，但是看不懂那个逆向后的程序算法
print(flag)

# phase 5
phase_5 = BASE_ADDR + 0x17f5
target_5 = BASE_ADDR + 0x184E
phase_5_flag = claripy.BVS('phase_3_flag',64)

state = proj.factory.blank_state(addr=phase_5, remove_options={angr.options.LAZY_SOLVES})
state.stack_push(phase_5_flag)
sim = proj.factory.simgr(state)
sim.explore(find=target_5, avoid=BOMB)
found = sim.found[0]
flag5 = []
# temp = found.solver.eval(found.stack_pop())
temp = found.solver.eval(phase_5_flag)
# 将高位和低位分开
low = temp & 0xffffffff
flag5.append(str(low))
high = temp >> 32 & 0xffffffff
flag5.append(str(high))
print(" ".join(flag5))

# phase 6
phase_6 = BASE_ADDR + 0x185B
target_6_A = BASE_ADDR + 0x1906
target_6_B = BASE_ADDR + 0x1971 # add rsp, 60h

READ_SIX_NUMBERS = BASE_ADDR + 0x1c11

class read_six_numbers(angr.SimProcedure):
    answer_inits = []
    # int_addrs = []
    # run函数的参数, 就是要hook的函数的参数，顺序和数量要一致。
    def run(self, str_addr, int_addr):
        # self.int_addrs.append(int_addr) # 不知道干嘛用的，目前在phase2中没影响
        for i in range(6):
            bvs = self.state.solver.BVS("phase_6_int_%d" % i, 32)
            self.answer_inits.append(bvs)
            self.state.mem[int_addr].int.array(6)[i] = bvs

        return 6
    
proj.hook(READ_SIX_NUMBERS,read_six_numbers())

state = proj.factory.blank_state(addr=phase_6, remove_options={angr.options.LAZY_SOLVES})
sim = proj.factory.simgr(state)

# while len(sim.active)>0:
sim.explore(find=target_6_A,avoid=BOMB)
print(sim)
# print(sim.found)
founds = sim.found
for found in founds:
    sim = proj.factory.simgr(found)
    sim.explore(find=target_6_B, avoid=BOMB)
    if len(sim.found) >0 :
        found = sim.found[0]
        break
flag6 = [str(found.solver.eval(i)) for i in read_six_numbers.answer_inits]
flag6 = " ".join(flag6)
print(flag6)