0x00:前言

之前接触到了符号执行，可以用于程序的自动化分析，感觉还是比较神奇，工业上的具体用法不是很清楚，不过在CTF中这个东西慢慢在流行...从defcon 2016就可以看出(有很多人解re用符号执行)。常用的库有angr、z3，我只尝试了angr。

0x01:关于符号执行

以下来自维基百科：

符号执行 （Symbolic Execution）是一种程序分析技术。其可以通过分析程序来得到让特定代码区域执行的输入。使用符号执行分析一个程序时，该程序会使用符号值作为输入，而非一般执行程序时使用的具体值。在达到目标代码时，分析器可以得到相应的路径约束，然后通过约束求解器来得到可以触发目标代码的具体值。[1]符号模拟技术（symbolic simulation）则把类似的思想用于硬件分析。符号计算（Symbolic computation）则用于数学表达式分析。

这个东西的详细资料可以google得到，github上也有一些介绍和demo。

0x02:简单的使用

对于CTF中的re题目来说，一些流程繁琐，代码量大的题目简直是体力活，做的人心力交瘁...举个简单的例子，之前听chxx表哥分享过一种代码混淆的技术叫控制流平坦化，用IDA打开视图简直是噩梦...如果是那种很复杂的，真的是爆炸，这里只用一个很简单的文件来演示。

其实这段代码没多长，几十行，判断的逻辑也很简单，但是就是利用几个变量在控制程序流程，跳来跳去，分析起来十分麻烦。

如果使用符号执行去解决就会使问题变得很简单

跑符号执行的机器配置要好些，这个东西太吃内存了,程序的复杂度和你代码约束条件写的如何，将决定你能不能跑出结果，因为这个程序很简单，所以很快就跑出来了。

大概 几十秒...

0x03:其他

个人感觉，angr的官方文档还不错，结合文档和官方给出的example应该可以学会使用这个库。但是符号执行也是有局限性的，不能盲目地去跑(如果你以为随便设定find 和 avoid 就可以跑出结果，那就太naive了)根据程序获取输入的方式不同，angr有不同的处理，还有一些筛选功能，这部分就可以看看文档啦，都比较容易懂。研究深入的话，这个东西还是很复杂的，我现在只想会使用这个工具就好，还有很多要学TAT。

0x04:

最近发现一个其他的用途，在分析pwn类型题目的二进制文件的时候，适当的使用angr来测试一些执行路径也是可以的...不过还是不能太依赖，更多的时候还是要人肉分析+调试。