符号执行框架

符号执行介绍

随着时代的发展，程序的流程越来越复杂，如果我们继续像以前那样在 ida 里仔细分析，肯定是太累了，所以有些科学家想要用自动化的算法来进行逆向工程，然后，他们就提出了符号执行这个算法。

符号执行算法听起来很高端，其实内部算法却并不难理解，接下来就介绍一下符号执行的核心理念。

假如有这样一个程序：

1
2
3
4
5
6
7
8
int main() {
int user_input;
scanf("%d", &user_input);
if (user_input - 10 >= 0)
puts("Success");
else
puts("Try again");
}

我们现在想要知道为了让程序到达 puts(‘Success.’) 这一行，需要的输入条件是什么，那我们要怎么得出到达这一行的条件呢？首先我们来看看执行这个程序的时候，user_input 都经历了什么。

image-20240216232938209

user_input 经过了一个判断语句，其中 user_input - 10>= 0 就是成功的条件。所以很显然，我们只

要将这个不等式解出来，就能知道需要的条件了。

那么接下来假如说有一个这样的程序呢：

1
2
3
4
5
6
7
8
9
10
11
int main() {
int user_input;
scanf("%d", &user_input);
if (user_input - 10 >= 0)
if (user_input <= 20)
puts("Success");
else
puts("Try again");
else
puts("Try again");
}

这个程序稍微复杂了那么一点。但是这不是问题，我们照着解决上一个程序的方法，先看看

user_input 都经历了什么：

image-20240216233010717

不难看出， user_input 经历了个两个判断条件，所以这回我们为了得出输出成功的条件，我们得解一

个方程组：image-20240216233023177

不难发现，就算 if 语句再多，只要能够一个个收集齐全，将这些条件形成一个（不）等式组，然后解出

这个（不）等式组，就可以得到我们想要的输出了。

但是现实生活中的程序不可能这么简单，单凭人力是无法收集全的，那么我们自然是要用程序来收集。

这个时候就该我们的 angr 登场了。

angr 作为一个二进制分析的工具包，但它通常作为符号执行工具更为出名。

符号执行就是给程序传递一个符号而不是具体的值，让这个符号伴随程序运行，当碰见分支时，符号会

进入哪个分支呢？

angr 的回答是全都进入。angr 会保存所有分支，以及分支后的所有分支，并且在分支时，保存进入该

分支时的判断条件，通常这些判断条件时对符号的约束。

当 angr 运行到目标状态时，就可以调用求解器对一路上收集到的约束进行求解，最终得到某个符号能

够到达当前状态的值。

angr 核心概念

顶层接口

Project 类是 angr 的主类，也是 angr 的开始，通过初始化该类的对象，可以将你想要分析的二进制文

件加载进来，就像这样：

1
2
import angr
p = angr.Project("./test")

参数为待分析的文件路径，它是唯一必须传入的参数，此外还有一个比较常用的参数 load-options，它

指明加载的方式，如下

image-20240216233058337

image-20240216233105524

State

Project 实际上只是将二进制文件加载进来了，要执行它，实际上是对 SimState 对象进行操作，它是程

序的状态。

要创建状态，需要使用 Project 对象中的 factory，它还可以用于创建模拟管理器和基本块，如下：

1
state = p.factory.entry_state()

预设状态有四种方式如下：

image-20240216233150939

状态包含了程序运行时的一切信息，寄存器、内存的值、文件系统以及符号变量等，这些信息的使用等

用到时再进一步说明。

entry_state 和 blank_state 是常用的两种方式，后者通常用于跳过一些极大降低 angr 效率的指令，它

们间的对比如下：

1
2
3
4
5
6
>> state = p.factory.entry_state()
>>> print(state.regs.rax, state.regs.rip)
<BV64 0x1c> <BV64 0x4023c0>
>>> state = p.factory.blank_state(addr=0x4023c0)
>>> print(state.regs.rax, state.regs.rip)
<BV64 reg_rax_42_64{UNINITIALIZED}> <BV64 0x4023c0>

在 blank_state 方式中，我们仍将地址设定为程序的入口点，然而 rax 中的值由于没有初始化，它现在

是一个名字，也即符号变量，这是符号执行的基础。此外，可以看到寄存器中的数据类型并不是 int，

而是 BV64，它是一个位向量（Bit Vector）。

Simulation Manager

上述方式只是预设了程序开始分析时的状态，我们要分析程序就必须要让它到达下一个状态，这就需要

模拟管理器的帮助（简称 SM）。

使用以下指令能创建一个 SM，它需要传入一个 state 或者 state 的列表作为参数：

image-20240216233228867

默认情况下，state 会被存放在 active 中。

可以通过 step() 方法来让处于 active 的 state 执行一个基本块，这种操作不会改变 state 本身（类比

docker）：image-20240216233245331

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_?}