符号执行框架


符号执行框架

符号执行介绍

随着时代的发展,程序的流程越来越复杂,如果我们继续像以前那样在 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_?}

文章作者: W3nL0u
版权声明: 本博客所有文章除特別声明外,均采用 CC BY 4.0 许可协议。转载请注明来源 W3nL0u !
  目录