符号执行框架
符号执行介绍
随着时代的发展,程序的流程越来越复杂,如果我们继续像以前那样在 ida 里仔细分析,肯定是太累了,所以有些科学家想要用自动化的算法来进行逆向工程,然后,他们就提出了符号执行这个算法。
符号执行算法听起来很高端,其实内部算法却并不难理解,接下来就介绍一下符号执行的核心理念。
假如有这样一个程序:
1 | int main() { |
我们现在想要知道为了让程序到达 puts(‘Success.’) 这一行,需要的输入条件是什么,那我们要怎么得出到达这一行的条件呢?首先我们来看看执行这个程序的时候,user_input 都经历了什么。
user_input 经过了一个判断语句,其中 user_input - 10>= 0 就是成功的条件。所以很显然,我们只
要将这个不等式解出来,就能知道需要的条件了。
那么接下来假如说有一个这样的程序呢:
1 | int main() { |
这个程序稍微复杂了那么一点。但是这不是问题,我们照着解决上一个程序的方法,先看看
user_input 都经历了什么:
不难看出, user_input 经历了个两个判断条件,所以这回我们为了得出输出成功的条件,我们得解一
个方程组:
不难发现,就算 if 语句再多,只要能够一个个收集齐全,将这些条件形成一个(不)等式组,然后解出
这个(不)等式组,就可以得到我们想要的输出了。
但是现实生活中的程序不可能这么简单,单凭人力是无法收集全的,那么我们自然是要用程序来收集。
这个时候就该我们的 angr 登场了。
angr 作为一个二进制分析的工具包,但它通常作为符号执行工具更为出名。
符号执行就是给程序传递一个符号而不是具体的值,让这个符号伴随程序运行,当碰见分支时,符号会
进入哪个分支呢?
angr 的回答是全都进入。angr 会保存所有分支,以及分支后的所有分支,并且在分支时,保存进入该
分支时的判断条件,通常这些判断条件时对符号的约束。
当 angr 运行到目标状态时,就可以调用求解器对一路上收集到的约束进行求解,最终得到某个符号能
够到达当前状态的值。
angr 核心概念
顶层接口
Project 类是 angr 的主类,也是 angr 的开始,通过初始化该类的对象,可以将你想要分析的二进制文
件加载进来,就像这样:
1 | import angr |
参数为待分析的文件路径,它是唯一必须传入的参数,此外还有一个比较常用的参数 load-options,它
指明加载的方式,如下
State
Project 实际上只是将二进制文件加载进来了,要执行它,实际上是对 SimState 对象进行操作,它是程
序的状态。
要创建状态,需要使用 Project 对象中的 factory,它还可以用于创建模拟管理器和基本块,如下:
1 | state = p.factory.entry_state() |
预设状态有四种方式如下:
状态包含了程序运行时的一切信息,寄存器、内存的值、文件系统以及符号变量等,这些信息的使用等
用到时再进一步说明。
entry_state 和 blank_state 是常用的两种方式,后者通常用于跳过一些极大降低 angr 效率的指令,它
们间的对比如下:
1 | >> state = p.factory.entry_state() |
在 blank_state 方式中,我们仍将地址设定为程序的入口点,然而 rax 中的值由于没有初始化,它现在
是一个名字,也即符号变量,这是符号执行的基础。此外,可以看到寄存器中的数据类型并不是 int,
而是 BV64,它是一个位向量(Bit Vector)。
Simulation Manager
上述方式只是预设了程序开始分析时的状态,我们要分析程序就必须要让它到达下一个状态,这就需要
模拟管理器的帮助(简称 SM)。
使用以下指令能创建一个 SM,它需要传入一个 state 或者 state 的列表作为参数:
默认情况下,state 会被存放在 active 中。
可以通过 step() 方法来让处于 active 的 state 执行一个基本块,这种操作不会改变 state 本身(类比
docker):
Explorer
可以使用 explorer 方法去执行某个状态,直到找到目标指令或者 active 中没有状态为止,它有如下参
数:
find:传入目标指令的地址或地址列表,或者一个用于判断的函数
avoid:传入要避免的指令的地址或地址列表,或者一个用于判断的函数,用于减少路径
angr 会沿着分支按照某种策略(默认DFS)进行状态搜索,当达到目标状态时,使用约束求解器
(claripy)对收集到的约束进行求解。
因此,使用 angr 一般分为如下步骤:
\1. 创建 Project,预设 state
\2. 创建位向量和符号变量,保存在内存/寄存器/文件或其他地方
\3. 将 state 添加到 SM 中
\4. 运行,探索满足条件的路径
\5. 约束求解获取执行结果
angr 入门练习
1 | pearl{d1d_y0u_aut0m4t3_0r_4r3_y0u_h4rdw0rk1ng_?} |
1 | pearl{d1d_y0u_aut0m4t3_0r_4r3_y0u_h4rdw0rk1ng_?} |