由 xiaoheshang404 
使用下来，个人感觉angr是一个帮助我们二进制、逆向分析的助手。主要是基于符号执行：把输入变为符号值，那么程序计算的输出值就是一个符号输入值的函数 ，我们计算出函数，也就计算出了输入应该的范围。
reverse练练手
我们用ida打开，一道很简单的reverse
angr可以帮我们快速高效地解决
import angr
proj = angr.Project('./02_angr_find_condition')
state = proj.factory.entry_state()
sm = proj.factory.simulation_manager()
addr = 0x0804900A
#explor(find = addr or function , avoid = )
sm=sm.explore(find=addr)
if sm.found:
#found[0] input found[1] output
final = sm.found[0]
final = final.posix.dumps(0)
print("[+] Success! Solution is: ",hex(addr),"resolve is",final)
另一种脚本
import angr
import sys
def main(argv):
bin_path = argv[1]
proj = angr.Project(bin_path)
init_state = proj.factory.entry_state()
sm = proj.factory.simulation_manager(init_state)
#函数判断下我们想要的输出是否存在
def is_good(state):
return b'Good Job' in state.posix.dumps(1)
def is_bad(state):
return b'Try again' in state.posix.dumps(1)
#explor(find = 地址或者函数 , avoid = )，find是想要去的地方，avoid是不去的地方
sm.explore(find=is_good,avoid = is_bad)#这里如果is_good = True，其实自动把find赋予输出GOOD Job的地址
if sm.found:
#found[0] input found[1] output
final = sm.found[0]
final = final.posix.dumps(0)
print("[+] Success! Solution is: ",format(final))
if __name__=='__main__':
main(sys.argv)
成功输出结果
符号化寄存器
可以看到这里输入是三个
官方文档里面讲述是不支持这种多个参数的
Angr doesn't currently support reading multiple things with scanf (Ex: scanf("%u %u).) You will have to tell the simulation engine to begin the program after scanf is called and manually inject the symbols into registers.但是其实现在新版本已经可以支持了(如下，之前有师傅问过）
我们可以把开始的地址设置到input函数之后start_addr = 0x008048980
我们要人为的给三个参数赋值
根据前面的分析我们这段三个参数之前是分别传到了eax，ebx，edx三个寄存器中，给寄存器赋值 #创建符号向量并且后面赋值给对应寄存器
para1 = claripy.BVS('para1',32)
para2 = claripy.BVS('para2',32)
para3 = claripy.BVS('para3',32)
init_state.regs.eax = para1
init_state.regs.ebx = para2
init_state.regs.edx = para3完整代码import angr
import sys
import claripy
def main(argv):
bin_path = argv[1]
proj = angr.Project(bin_path)
start_addr = 0x008048980
init_state = proj.factory.blank_state(addr = start_addr)
para1 = claripy.BVS('para1',32)
para2 = claripy.BVS('para2',32)
para3 = claripy.BVS('para3',32)
init_state.regs.eax = para1
init_state.regs.ebx = para2
init_state.regs.edx = para3
sm = proj.factory.simulation_manager(init_state)
def is_good(state):
return b'Good Job' in state.posix.dumps(1)
def is_bad(state):
return b'Try again' in state.posix.dumps(1)
#explor(find = addr or function , avoid = )
sm.explore(find=is_good,avoid = is_bad)
if sm.found:
#found[0] input found[1] output
found_state = sm.found[0]
end1 = found_state.solver.eval(para1)
end2 = found_state.solver.eval(para2)
end3 = found_state.solver.eval(para3)
print("[+] Success! Solution is: {} {} {}",hex(end1),hex(end2),hex(end3))
#这个时候如果打印found_state.posix.dumps(0)输入结果,结果是空的，因为我们之前没有进入scanf，直接从start_adrr开始了
if __name__=='__main__':
main(sys.argv)符号化栈内存
进入对应的汇编代码
我们先看scanf的调用过程
首先，我们要知道，lea和mov指令的区别：lea是直接取对应地址，mov是取地址对应的值
初始化栈之后，把两个参数的地址（！）push入栈
然后push offset aUU，这个主要是与scanf的格式化有关，几个参数就有几个U，本题即为“%u %u”，aUUUU只是方便程式师知道这里是个什么样式的变数,实际上它仍是一个地址仍然是push dword ptr [xxxxxx]
做好这些准备工作之后我们就可以call了
但是我们现在不调用scanf函数，初始化之后直接把我们的向量加到栈上
initial_state.regs.ebp = initial_state.regs.esp
padding_length_in_bytes = 8 #这里的padding根据实际情况修改，这道题是8
initial_state.regs.esp -= padding_length_in_bytes然后我们初始化向量
password1 = claripy.BVS('password1', 32)#本题为32位，所以为32
password2 = claripy.BVS('password2', 32)将向量push进栈
initial_state.stack_push(password1)
initial_state.stack_push(password2)之后就可以正常走下去到，利用angr完成计算
前后不同的栈布局如下
add esp,10h
这个是清除之前的栈布局，所以我们可以在这条指令之后开始执行
也就是 start_address = 0x8048697
完整脚本：
import angr
import claripy
import sys
def main(argv):
path_to_binary = './04_angr_symbolic_stack'
project = angr.Project(path_to_binary)
start_address = 0x8048697
initial_state = project.factory.blank_state(addr=start_address)
initial_state.stack_push(initial_state.regs.ebp)
initial_state.regs.ebp = initial_state.regs.esp
password1 = claripy.BVS('password1', 32) # :bitvector (claripy.BVS, claripy.BVV, claripy.BV)
password2 = claripy.BVS('password2', 32)# 本题为32位，所以为32
padding_length_in_bytes = 8
initial_state.regs.esp -= padding_length_in_bytes
initial_state.stack_push(password1)
initial_state.stack_push(password2)
simulation = project.factory.simgr(initial_state)
def is_successful(state):
return b'Good Job' in state.posix.dumps(1)
def should_abort(state):
return b'Try again' in state.posix.dumps(1)
simulation.explore(find=is_successful, avoid=should_abort)
if simulation.found:
solution_state = simulation.found[0]
solution1 = solution_state.solver.eval(password1)
solution2 = solution_state.solver.eval(password2)
print(str(solution1),str(solution2))
else:
raise Exception('Could not find the solution')
if __name__ == '__main__':
main(sys.argv)
上面脚本其实就是模拟压栈过程来进行压入符号，我们也可以直接强制加入符号
initial_state.mem[initial_state.regs.ebp-0xC].uint32_t = password1
initial_state.mem[initial_state.regs.ebp-0x10].uint32_t = password2符号化bss段内存
scanf函数把输入放在四个bss地址处
我们要把符号向量放在这四个bss里
看下汇编
跟之前一样，依旧是add esp，20h回收栈
我们在之后也就是
start_addr = 0x008048601关于内存地址写入我们要用到
init_state.memory.store(addr1,para1)创建state可以适当优化
load_options={"auto_load_libs":False})因为目前这个工具还不支持直接接收转化为str,所以我们必须
cast_to = bytesend1 = found_state.solver.eval(para1,cast_to=bytes).decode("utf-8")如果使用cast_to = str就会报错不支持
cast_to parameter <class 'str'> is not a valid cast target, currently supported are only int and bytes!完整脚本：
import angr
import sys
import claripy
def main(argv):
#bin_path = argv[1]
proj = angr.Project('./05_angr_symbolic_memory')
start_addr = 0x0008048601
init_state = proj.factory.blank_state(addr = start_addr,load_options={"auto_load_libs":False})
para1 = init_state.solver.BVS('para1',64) #8*8
para2 = init_state.solver.BVS('para2',64)
para3 = init_state.solver.BVS('para3',64)
para4 = init_state.solver.BVS('para4',64)
addr1 = 0xA1BA1C0
addr2 = 0xA1BA1C8
addr3 = 0xA1BA1D0
addr4 = 0xA1BA1D8
init_state.memory.store(addr1,para1)
init_state.memory.store(addr2,para2)
init_state.memory.store(addr3,para3)
init_state.memory.store(addr4,para4)
sm = proj.factory.simulation_manager(init_state)
def is_good(state):
return b'Good Job' in state.posix.dumps(1)
def is_bad(state):
return b'Try again' in state.posix.dumps(1)
#explor(find = addr or function , avoid = )
sm.explore(find=is_good,avoid = is_bad)
if sm.found:
#found[0] input found[1] output
found_state = sm.found[0]
end1 = found_state.solver.eval(para1,cast_to=bytes).decode("utf-8")
end2 = found_state.solver.eval(para2,cast_to=bytes).decode("utf-8")
end3 = found_state.solver.eval(para3,cast_to=bytes).decode("utf-8")
end4 = found_state.solver.eval(para4,cast_to=bytes).decode("utf-8")
# found_state=found_state.posix.dumps(0)
print("[+] Success! Solution is: ",end1,end2,end3,end4)
# print("solution is",found_state)
else:
print("failed")
if __name__=='__main__':
main(sys.argv)符号化堆内存
malloc两个chunk，地址分别赋值给buffer1，buffer2
我们需要伪造两个chunk，并且将我们的符号向量放进去
start_addr = 0x08048699
buffer1和buffer2的地址
我们需要伪造（其实就是找）chunk，把地址写在buffer处，把向量写在chunk处
init_state.memory.store(buffer1,heap_addr1,endness = proj.arch.memory_endness)
init_state.memory.store(buffer2,heap_addr2,endness = proj.arch.memory_endness)
init_state.memory.store(heap_addr1,para1)
init_state.memory.store(heap_addr2,para2)因为angr默认是大端序，所以要加上endness = proj.arch.memory_endness转化为小端序
完整代脚本：
import angr
import sys
import claripy
def main(argv):
#bin_path = argv[1]
proj = angr.Project('./06_angr_symbolic_dynamic_memory')
start_addr = 0x008048699
init_state = proj.factory.blank_state(addr = start_addr,load_options={"auto_load_libs":False})
para1 = init_state.solver.BVS('para1',64)
para2 = init_state.solver.BVS('para2',64)
buffer1 = 0x0ABCC8A4
buffer2 = 0x0ABCC8AC
heap_addr1 = 0x7ffefffc-0x100
heap_addr2 = 0x7ffefffc-0x200
init_state.memory.store(buffer1,heap_addr1,endness = proj.arch.memory_endness)
init_state.memory.store(buffer2,heap_addr2,endness = proj.arch.memory_endness)
init_state.memory.store(heap_addr1,para1)
init_state.memory.store(heap_addr2,para2)
sm = proj.factory.simulation_manager(init_state)
def is_good(state):
return b'Good Job' in state.posix.dumps(1)
def is_bad(state):
return b'Try again' in state.posix.dumps(1)
#explor(find = addr or function , avoid = )
sm.explore(find=is_good,avoid = is_bad)
if sm.found:
#found[0] input found[1] output
found_state = sm.found[0]
end1 = found_state.solver.eval(para1,cast_to=bytes).decode("utf-8")
end2 = found_state.solver.eval(para2,cast_to=bytes).decode("utf-8")
# found_state=found_state.posix.dumps(0)
print("[+] Success! Solution is: ",end1,end2)
# print("solution is",found_state)
else:
print("failed")
if __name__=='__main__':
main(sys.argv)