符号执行

符号执行

简单的来说，符号执行就是在运行程序时，用符号来替代真实值。符号执行相较于真实值执行的优点在于，当使用真实值执行程序时，我们能够遍历的程序路径只有一条，而使用符号进行执行时，由于符号是可变的，我们就可以利用这一特性，尽可能的将程序的每一条路径遍历，这样的话，必定存在至少一条能够输出正确结果的分支，每一条分支的结果都可以表示为一个离散关系式，使用约束求解引擎即可分析出正确结果，这就是符号执行的简单阐述。

angr

angr是适用范围最广的符号执行工具，pip install angr即可安装。

defcamp_r100

请添加图片描述
请添加图片描述
请添加图片描述
程序的逻辑是输入一个字符串，在sub_4006FD中检验
官方脚本

1
2
3
4
5
6
7
8
9
10
11
12
13
14
import angr

def main():
    p = angr.Project("r100")
    simgr = p.factory.simulation_manager(p.factory.full_init_state())
    simgr.explore(find=0x400844, avoid=0x400855)

    return simgr.found[0].posix.dumps(0).strip(b'\0\n')

def test():
    assert main().startswith(b'Code_Talkers')

if __name__ == '__main__':
    print(main())

p = angr.Project(“r100”)
装载需要分析的程序，这样操作之后，p就是你的主二进制文件以及它依赖的所有库的代表。

simgr = p.factory.simulation_manager(p.factory.full_init_state())
创建一个simulation_manager用来模拟执行并设置好状态

simgr.explore(find=0x400844, avoid=0x400855)
让程序运行到0x400844(“Nice”)处，避免运行到0x400844(“Incorrect password!”)处。使用explore方法寻找到达到目标的路径。

return simgr.found[0].posix.dumps(0).strip(b’\0\n’)
found成员是一个表，存储着所有找到的路径，成员数据类型是SimState，代表程序的状态，posix代表程序通过POSIX规范中的接口获取的数据。posix.dumps(0)获取的是标准输入中的数据。