1.符号执行总结简单来说，符号执行就是在运行程序时用符号代替真实值。符号执行相对于实值执行的优势在于，当使用实值执行程序时，我们可以遍历的程序路径只有一条，而当使用符号执行时，由于符号是可变的，我们可以利用这一特性，尽可能遍历程序的每条路径。在这种情况下，必须至少有一个分支可以输出正确的结果。每个分支的结果可以表示为离散的关系表达式，使用约束求解引擎可以分析出正确的结果，这是一种简单的符号执行形式。Angr是python开发的二进制程序分析框架。我们可以使用这个工具来尝试对一些CTF题进行符号执行来寻找正确答案，即flag。当然需要注意的是，符号执行的路径选择问题还是一个大问题。也就是说，当我们的程序有循环时，由于符号执行会尝试遍历所有路径，所以每次循环后至少会形成两个分支。当循环次数足够多时，路径就会爆炸，整个机器的内存就会被耗尽。2.使用Angr我个人觉得Angr在解决REVERSE问题上很有用，但是在处理PWN问题时，多用于一些辅助的位置，比如寻找strcmp等敏感函数。本次我们将简单介绍一下如何使用Angr进行REVERSE分析以及问题的解决。我会先讲解一下Angr在实践中的几个关键操作，然后再用一道简单的CTF题进行练习。建议大家使用ipython进行简单练习。ipython的tab补全让你看到了Angr的很多精彩功能。1.运行程序当我们得到一个程序后，首先需要为该程序创建一个Angr工程。p=angr.Project('program')我们可以通过这个项目得到程序的一些信息，比如程序名p.filename等。然后我们需要运行这个程序并处理程序的一些输入。前面提到，符号执行时，我们使用的不是真正的值，而是单个的符号，可以简单理解为变量，所以我们需要在Angr中构造一个符号作为程序的输入。(1)命令行参数当程序需要命令行参数时，我们首先需要使用claripy模块来定义抽象数据。importclaripyclaripy的BVS函数可以创建一个指定长度的抽象数据。BVS函数需要两个参数，第一个参数是变量名，第二个参数是变量长度。argv=[p.filename,]arg=claripy.BVS('arg1',8)argv.append(arg1)这样我们就创建了一个命令行参数，我们现在可以运行程序到程序入口，并且获取当前状态。state=p.factory.entry_state(args=argv)p.factory是工厂函数的集合，在工厂函数中可以调用各种函数进行符号执行，其中entry_state()函数接收一个列表作为程序的命令行参数并返回程序入口的状态（这个状态将在2.2节中解释）。(2)标准输入当程序需要从标准输入中读取数据时，需要使用read_from()函数。需要注意的是，这个函数位于状态中，我们可以对输入施加一些约束，以减少符号执行所遍历的路径。for_inxrange(5):k=state.posix.files[0].read_from(1)state.se.add(k!=10)这意味着我们从标准输入读取5个字节，每个字节都不换行。2、Angr中程序的几种状态前面我们提到了程序入口点的状态。Angr中的状态表示程序符号执行后的几个结果。在Angr中，当获取到程序入口点的状态后，我们需要使用Angr的Simgr模拟器进行符号执行sm=p.factory.simgr(state)表示从入口点创建一个模拟器进行符号执行。在Angr寻找路径的同时，程序的当前状态有多种表示。step()表示向下执行一个block(42bytes)，step()函数产生一个active状态，表示该分支正在执行；run()表示运行结束，run()函数产生deadended状态，表示分支结束；explore()可以限制地址以减少符号执行所经过的路径。比如sm.explore(find=0x400676,avoid=[0x40073d])explore()产生一个found状态，表示探索的结果等，在这些状态下找到我们需要的路径。我们可以得到当前状态程序的输出printsm.found.posix.dumps(1)命令行参数printsm.found.solver.eval(arg1,cast_to=str)标准输入inp=sm.found.posix.files[0].all_bytes()printsm.found.solver.eval(inp,cast_to=str)z在求解命令行参数和标准输入值时，我们使用约束求解引擎求解3??.angr练习bin(re50)下载：http//oj.xctf.org.cn/web/practice/defensetrain/465f6bb8f4ad4d65a70cce2bd69dfacf/scriptingimportangrimportsysprint[*]start-------------------------------------"p=angr.Project(sys.argv[1])#创建项目初始化二进制文件state=p.factory.entry_state()#获取入口点的状态'''state。posix.files[0].read_from(1)表示从标准输入中读取一个字节'''for_inxrange(int(sys.argv[2])):#对输入的简单约束（不是回车）k=state.posix.files[0].read_from(1)state.se.add(k!=10)k=state.posix.files[0].read_from(1)state.se.add(k==10)#输入是终结符state.posix.files[0].seek(0)state.posix.files[0].length=int(sys.argv[2])+1#约束输入长度（大于实际长度也可以)打印[*]simgrstart----------------------------"sm=p.factory.simgr(state)#初始化进程模拟器sm.explore(find=lambdas:"correct!"ins.posix.dumps(1))#在运行进程中寻找“correc”吨！"，并丢弃其他路径print"[*]programexcuted------------------------"forppinsm.found:out=pp.posix。dumps(1)#表示程序的输出printoutinp=pp.posix.files[0].all_bytes()#得到输入变量printpp.solver.eval(inp,cast_to=str)#使用约束求解引擎求解输入操作root@kali:~#pythonre50.pyppp4[*]start----------------------------------/usr/local/lib/python2.7/dist-packages/cle/loader.py:729:UnicodeWarning:Unicode相等比较未能将两个参数转换为Unicode-解释themas是不合格的libname.strip('.0123456789')==spec.strip('.0123456789'):[*]simgrstart------------------------------[*]programexcuted------------------------pleaseinputthekey:correct!9563root@kali:~#Wegotthecorrectkeyvalue9563
