题目分析
获取输入
v1 = sys_read(0, byte_412000, 0x40uLL);
中间计算
byte_412000[42] = __ROR1__(byte_412000[42], 4);
*(_DWORD *)&byte_412000[44] ^= 0x4EC10FC6u;
*(_WORD *)&byte_412000[15] ^= 0xEBFFu;
*(_DWORD *)&byte_412000[38] -= 1698263770;
// 以下省略
最后的验证
v9 = byte_412000;
v10 = byte_412050;
v11 = 64LL;
v12 = 0;
do
{
v12 |= *v10++ ^ *v9++;
--v11;
}
while ( v11 );
Angr求解
还是很容易看懂的,主要是如何求解
一种思路是把汇编反过来,pizza爷用的是这种做法,于是就写了个Angr喝茶去了
Angr用的是手动往全局变量注入符号,然后在验证前停止,手动添加约束,wp中的写法是直接用程序中的验证,并添加了 LAZY_SOLVES
参数,学到了
之前用自己脚本跑的适合发现一直是 unsat
,以为Angr会有问题,但后来发现有个wp就是用的Angr
于是掏出了之前写的脚本做了一些尝试
from angr import *
import claripy
import binascii
input_length = 56
base_addr = 0x400000
proj = Project('runofthemill', main_opts={"base_addr": base_addr})
start_addr = 0x401054
state = proj.factory.blank_state(addr = start_addr, add_options={options.LAZY_SOLVES})
# state.regs.rdi = 0x412000
user_input = [claripy.BVS('input_%d' % i, 8) for i in range(input_length)]
mem_addr = 0x412000
for i in range(input_length):
state.memory.store(mem_addr + i, user_input[i])
state.add_constraints(state.memory.load(mem_addr, 6) == int(binascii.hexlify(b"DrgnS{"), 16))
simgr = proj.factory.simgr(state)
find_addr = 0x4117FF
simgr.explore(find = find_addr)
ans = [
0xB5, 0x9C, 0x9A, 0x08, 0x68, 0x91, 0x29, 0x0F, 0xBD, 0x1E,
0xFB, 0x71, 0xF4, 0x93, 0x5C, 0xDA, 0x0D, 0x94, 0x10, 0x77,
0x6C, 0x41, 0x8D, 0xE2, 0x5E, 0x26, 0xA5, 0x0A, 0x95, 0xE1,
0x14, 0xDB, 0x25, 0x0B, 0x09, 0xE4, 0x7B, 0xE7, 0x07, 0x71,
0x4E, 0xD3, 0xF2, 0xC1, 0x5C, 0xB2, 0xB4, 0x17, 0x30, 0xAA,
0x3D, 0x35, 0x1E, 0x98, 0xC4, 0x92, 0xF4, 0x33, 0x69, 0xCC,
0x11, 0xB0, 0xCE, 0xCC
]
if simgr.found:
print ("end state found")
end_state = simgr.found[0]
for i in range(64):
end_state.add_constraints(end_state.memory.load(mem_addr + i, 1) == ans[i])
for i in range(input_length):
print (end_state.solver.eval(user_input[i], cast_to=bytes).decode(), end='')
print ()
else:
print ("No result")
最后发现只要把 input_length
设置为56及以下就可以,其他的都是 unsat
capstone学习
TODO
后续学习一下再来补