感谢 https://github.com/jakespringer/angr_ctf/blob/master/SymbolicExecution.pptx 这篇 PPT 和 https://www.bilibili.com/video/BV167411o7WK?t=1043 这个视频，本文章的出现和我能入门angr，这两个教程功不可没，如果你们有兴趣也可以看看。angr 官方项目地址：https://github.com/angr/angr
这篇文章主要是带大家入门如何用 angr 进行符号执行。
符号执行介绍
随着时代的发展，程序的流程越来越复杂，如果我们继续像以前那样在 ida 里仔细分析，肯定是太累了，所以有些科学家想要用自动化的算法来进行逆向工程，然后，他们就想到了符号执行这个算法。
符号执行算法听起来很高端，其实内部算法却并不难理解。接下来就介绍一下这个符号执行的内部算法：
假如有这样一个程序
这里采用 Python 只是为了方便理解。。。事实上符号执行可以解决所有语言的程序，这个算法和程序所采用的语言没啥关系
user_input = int(input())
if user_input - 10 >= 0:
print('Success.')
else:
print('Try again.')
我们现在想要知道为了让程序到达 print('Success.')这一行，需要的输入条件是什么，那我们要怎么得出到达这一行的条件呢？首先我们来看看执行这个程序的时候，user_input 都经历了什么。
user_input 经过了一个判断语句，其中 user_input - 10>= 0 就是成功的条件。所以很显然，我们只要将这个不等式接出来，就能知道需要的条件了。
那么接下来假如说有一个这样的程序呢：
user_input = int(input())
if user_input - 10 >= 0:
if user_input <= 20:
print('Success.')
else:
print('Try again.')
else:
print('Try again.')
这个程序稍微复杂了那么一点。但是这不是问题，我们照着解决上一个程序的方法，先看看 user_input 都经历了什么：
不难看出，user_input经历了个两个判断条件，所以这回我们为了得出输出成功的条件，我们得解一个方程组：
然后我们只要愉快的解出这个不等式组，就可以得到可能的输出了。
不难发现，就算你if语句再多，只要我能够一个个收集齐全，然后将这些条件形成一个不等式组，然后解出这个不等式组，就可以得到我们想要的输出了。
但是现实生活中的程序不可能这么简单，单凭人力是无法收集全的，那么我们自然是要用程序来收集。这个时候就该我们的angr登场了。
接下来我们通过一个程序来看看angr的使用方法和大概的工作流程。
angr 的安装
在用之前，我们得先安装这个东西。安装这个十分的简单，为了避免 python 库版本混乱的问题。我们在使用这个库之前将这个库装进 python 虚拟环境里隔离起来。如何建立虚拟环境这个可以自行百度，毕竟这属于python的基础知识。建立好以后，我们在终端中激活这个虚拟环境，然后用 pip3 install angr 安装 angr即可。
angr 上手教程
样例程序下载：
百度网盘链接: https://pan.baidu.com/s/1tdL3RmAm9VZz5wsR-IGA6g 密码: 6tf2
Github 链接: https://github.com/jakespringer/angr_ctf/blob/master/dist/00_angr_find
由于这个程序比较简单，因此我们这次用 ipython 来操作。（没装的自己百度哦）
首先进入 python 虚拟环境的 ipython，然后我们 import angr，如果没有问题，那就是安装好了。如果有报错，建议自行百度。其实 angr 官方有一个打包好的 docker 镜像，如果本机因为各种问题没法正常使用，就用这个docker环境吧。
接下来我们要新建一个 angr 工程：
>>> proj = angr.Project('程序的路径') # 相对路径和绝对路径均可
接下来我们就要新建一个模拟运行管理器，然后让angr搜索需要的分支信息。
>>> sm = proj.factory.simulation_manager()
>>> sm = sm.explore(find=0x08048675) # 探索到达 0x08048678 的路径
其中 factory 这个对象是用来生成和项目有关的一些分析工具，然后我们用这个对象生成了一个SimulationManager对象，存储在变量 sm 中。然后将这个变量那么什么是模拟运行管理器呢。那就要涉及到angr是如何收集所有的分支信息了。
用过 ida 的人，应该都相当熟悉这个画面
可以说，这个图中的一个个代码块就是 angr 框架中所谓的 state（这只是方便说明的说辞，实际上angr的一个state还存储了执行这个代码块后的寄存器状态，内存状态等信息），这一个一个state组合在一起，就形成了执行路径，然后我们用 SimulationManager 来生成，管理执行路径。
然后 angr 会将入口点那块 state 作为起点，将find的值对应的那块汇编代码作为终点，进行宽度优先搜索（还是要了解一下这个算法，这样才能理解其他的一些参数设置，如avoid参数的含义）。找到一条从起点到达终点的可行路径，然后将这条路上的所有if条件收集起来。最后自动对收集起来的条件形成的不等式组进行求解。（貌似具体的方法较为复杂，这里可以稍微这样简单理解一下）
其实我们还可以用 proj.factory.entry_state()来生成一个关于该程序入口点的state。然后将这个state作为proj.factory.simulation_manager()的参数，实际上proj.factory.simulation_manager()的默认参数就是proj.factory.entry_state()所以我就不手动指定了。
如果这步执行结束了，那么我们就可以导出能够让程序到达成功状态的输入了，
>>> final_state = sm.found[0] # 0 代表找到的第一个结果
>>> final_state.posix.dumps(0) # 导出结果
其中 posix 表示终点状态中存储的系统接口信息，然后通过dumps函数来导出系统输入，系统输出等信息。
final_state.posix.dumps(0) 表示导出输入，final_state.posix.dumps(1)表示导出输出。
然后我们就可以找到angr爆破出来的输出 b'JXWVXRKX'。
如何进阶
1: 学习一下宽度优先搜索。
2: https://github.com/jakespringer/angr_ctf 这个项目的 dist 文件夹中存着难度从易到难的题目。完成这些水平就会有不小的提升。
3: https://space.bilibili.com/386563875 这个 UP 有关于上面这个题库的题解视频，上面的这些题目完全没必要自己先做，可以先看一下这个 UP 如何操作，然后在吸收 angr 的不同用法。
[复制链接]
发表于 2021-2-14 23:49
|
发表于 2021-2-15 15:18
