简单的尝试angr

0x00:前言

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

0x01:关于符号执行

以下来自维基百科:

1
符号执行 (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来测试一些执行路径也是可以的…不过还是不能太依赖,更多的时候还是要人肉分析+调试。

文章目录
  1. 1. 0x00:前言
  2. 2. 0x01:关于符号执行
  3. 3. 0x02:简单的使用
  4. 4. 0x03:其他
  5. 5. 0x04:
,