符号执行Angr

突然发现记录一些简单题的做题过程只会浪费时间,以后就不记录特别简单的题了(虽然难的题也不会写XD

今天在做whalectf上面的题目时,有两道类型差不多的题,但是一道用爆破解出来了,另一道)却解不出来,查找writeup的时候找不到一样的题目,但是找到了类似的题目,并且发现了符号执行这个东西,学习后掌握了新的解题技巧。

首先要安装angr库,具体操作方法可以百度。

解题脚本:

1
2
3
4
5
6
7
8
import angr 
import claripy
p = angr.Project("./ais3_crackme")
argv1=claripy.BVS('argv1',24*8)
state=p.factory.entry_state(args=['./ais3_crackme',argv1])
simgr=p.factory.simgr(state)
simgr.explore(find=0x400602,avoid=0x40060e)
print simgr.found[0].solver.eval(argv1,cast_to=str)

其中:

p = angr.Project("./ais3_crackme")

为每一个angr脚本必备

argv1=claripy.BVS('argv1',24*8)

是以二进制形式设一个参数,ida分析程序得知参数长度为24

state=p.factory.entry_state(args=['./ais3_crackme',argv1])

获取程序的初始状态

simgr=p.factory.simgr(state)

遍历路径

simgr.explore(find=0x400602,avoid=0x40060e)

设定成功与失败的路径结果,地址由ida分析得

print simgr.found[0].solver.eval(argv1,cast_to=str)

以字符串形式输出结果

这一题几乎是照抄着写了一遍,因此再把之前那道简单的题)拿出来练一下手。

脚本如下:

1
2
3
4
5
6
import angr 
p = angr.Project("./r100")
state=p.factory.entry_state(args=['./r100'])
simgr=p.factory.simgr(state)
simgr.explore(find=0x400844,avoid=0x400855)
print simgr.found[0].posix.dumps(0)

但还是不太熟练,可至少拥有了两个简单的模版XD

再摘录一下freebuf上的较通用脚本

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
import angr
import sys
print "[*]start------------------------------------"
p = angr.Project(sys.argv[1]) # 建立工程初始化二进制文件
state = p.factory.entry_state() # 获取入口点处状态

'''
state.posix.files[0].read_from(1)表示从标准输入读取一个字节
'''

for _ in xrange(int(sys.argv[2])): # 对输入进行简单约束(不为回车)
k = state.posix.files[0].read_from(1)
state.se.add(k!=10)

k = state.posix.files[0].read_from(1)
state.se.add(k==10) # 回车为结束符

state.posix.files[0].seek(0)
state.posix.files[0].length = int(sys.argv[2])+1 # 约束输入长度(大于实际长度也可)

print "[*]simgr start-------------------------------"

sm = p.factory.simgr(state) # 初始化进程模拟器
sm.explore(find=lambda s:"correct!" in s.posix.dumps(1)) # 寻找运行过程中存在 “correct!”的路径,并丢弃其他路径
print "[*]program excuted---------------------------"

for pp in sm.found:
out = pp.posix.dumps(1) # 表示程序的输出
print out
inp = pp.posix.files[0].all_bytes() # 取输入的变量
print pp.solver.eval(inp,cast_to = str) # 利用约束求解引擎求解输入
文章目录
|