baby-re(DEFCON 2016 quals)

angr学习
题目链接 https://github.com/angr/angr-doc/tree/master/examples/defcon2016quals_baby-re

IDA打开分析，程序要求输入12个数字，经过CheckSolution进行检查
请添加图片描述
进入CheckSolution，发现函数非常复杂且无法反编译，编写符号执行脚本解题。

1
2
3
4
5
6
import angr
p=angr.Project("baby-re")
s=p.factory.simulation_manager(p.factory.full_init_state())
s.one_active.options.add(angr.options.LAZY_SOLVES)
s.explore(find=0x40292C,avoid=0x402941)
print(s.found[0].posix.dumps(0))

运行结果
请添加图片描述

得到flag
请添加图片描述

总结：虽然成功解题但脚本运行效率太低，官方脚本中hook了库函数来提高效率，将在以后学习。

官方脚本

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
#!/usr/bin/env python2
from __future__ import print_function

# Authors: David Manouchehri <manouchehri@protonmail.com>
#          P1kachu <p1kachu@lse.epita.fr>
#          Audrey Dutcher <audrey@rhelmot.io>
# DEFCON CTF Qualifier 2016
# Challenge: baby-re
# Write-up: http://hack.carleton.team/2016/05/21/defcon-ctf-qualifier-2016-baby-re/
# Runtime: ~15 seconds (thanks lazy solves!)

import angr
import claripy

def main():
    proj = angr.Project('./baby-re', 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 range(13)]
    class my_scanf(angr.SimProcedure):
        def run(self, fmt, ptr): # pylint: disable=arguments-differ,unused-argument
            self.state.mem[ptr].dword = flag_chars[self.state.globals['scanf_count']]
            self.state.globals['scanf_count'] += 1

    proj.hook_symbol('__isoc99_scanf', my_scanf(), replace=True)

    sm = proj.factory.simulation_manager()
    sm.one_active.options.add(angr.options.LAZY_SOLVES)
    sm.one_active.globals['scanf_count'] = 0

    # 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(main())