用例源码以及二进制文件链接:https://github.com/angr/angr-doc/tree/master/examples/defcon2016quals_baby-re
执行二进制文件,发现需要输入13个字符,然后通过一系列计算判断输入字符是否满足约束条件。
在IDA里非常清晰可以看见输入错误的字符串及其调用地址:
所以avoid_addr=0x402941
而正确的字符串以及地址为:
可以看出,flag将作为程序输出,所以find_addr地址可以设置为0x40292c(亲测有效)。
不过这一次就又对scanf函数进行了hook,用来创建13个符号变量。
这次是一定要hook scanf函数的。因为它默认会返回一个无约束的一个符号变量(是否是同一个符号变量还不确定),在scanf函数前面存在fflush函数,它的功能是清空缓冲区,将输入写入stream。
而且hook的函数,也出现了新的知识点:
class my_scanf(angr.SimProcedure):
def run(self, fmt, ptr):
if 'scanf_count' not in self.state.globals:
self.state.globals['scanf_count'] = 0
c = self.state.globals['scanf_count']
self.state.mem[ptr].dword = flag_chars[c]
self.state.globals['scanf_count'] = c + 1
在符号执行的过程中,是可以创建变量的,存储在state.globals里面。这里面就创建了一个变量scanf_count是记录scanf函数的数目,使得第i个scanf函数的state.mem赋值第i个符号变量。
用例源码:
#!/usr/bin/env python2
"""
Author: David Manouchehri <[email protected]>
DEFCON CTF Qualifier 2016
Challenge: baby-re
Team: hack.carleton
Write-up: http://hack.carleton.team/2016/05/21/defcon-ctf-qualifier-2016-baby-re/
Runtime: ~8 minutes (single threaded E5-2650L v3 @ 1.80GHz on DigitalOcean)
DigitalOcean is horrible for single threaded applications, I would highly suggest using something else.
"""
import angr
import claripy
def main():
proj = angr.Project('./baby-re', load_options={'auto_load_libs': False})
# let's provide the exact variables received through the scanf so we don't have to worry about parsing stdin into a bunch of ints.
flag_chars = [claripy.BVS('flag_%d' % i, 32) for i in xrange(13)]
class my_scanf(angr.SimProcedure):
def run(self, fmt, ptr):
if 'scanf_count' not in self.state.globals:
self.state.globals['scanf_count'] = 0
c = self.state.globals['scanf_count']
self.state.mem[ptr].dword = flag_chars[c]
self.state.globals['scanf_count'] = c + 1
proj.hook_symbol('__isoc99_scanf', my_scanf(), replace=True)
sm = proj.factory.simulation_manager()
# search for just before the printf("%c%c...")
# If we get to 0x402941, "Wrong" is going to be printed out, so definitely avoid that.
sm.explore(find=0x4028E9, avoid=0x402941)
# evaluate each of the flag chars against the constraints on the found state to construct the flag
flag = ''.join(chr(sm.one_found.solver.eval(c)) for c in flag_chars)
return flag
def test():
assert main() == 'Math is hard!'
if __name__ == '__main__':
print(repr(main()))