跳转至

符号执行原理

欢迎来到angr小课堂，接下来我们将通过这个系列教程来初步掌握angr的使用以及符号执行的一些原理和思想。

第一个问题：什么是angr呢？简单来说，angr是目前最好用的符号执行引擎之一，是逆向辅助分析的神器。符号执行是angr的核心功能，可以说如果不能充分理解符号执行背后原理，就很难灵活使用angr，所以angr这个系列的教程我们从符号执行原理讲起。

0x00. 前置知识与参考资料

阅读本系列教程读者需要具备以下基础：

  • 逆向基础
  • x86汇编基础
  • C/C++和Python编程基础

一些符号执行的科普资料：

0x01. 什么是符号执行

一般情况下，当我们运行一个程序并给定程序所需要的所有输入时，一个程序的执行路径是确定并且唯一的，这里用一个伪代码来说明：

int main(){
    x = input();
    y = input();
    z = 2 * y;
    if(x == z){
        if(x > y + 10){
            print("Path-1");
        }else{
            print("Path-2");
        }
    }else{
        print("Path-3");
    }
}

input函数表示获取用户输入，print函数就是字面意思，我们可以很容易地画出程序的控制流程图（Control Flow Graph）：

假设用户的输入是{x = 2, y = 1}，那么程序会沿着红色线条标记的路径执行，其路径是确定且唯一的，其他输入也同理，这里不再赘述。当程序的输入确定时，这种执行就叫做具体执行：

如果现在input函数不是获取用户的具体输入，而是直接获取一个对应的符号值呢？例如{x = xsym, y = ysym}。当程序的输入由具体的值变成了符号值之后，程序的运行由具体执行变成了符号执行（Symbolic Execution）。

为了解释符号执行，现在我要引入两个概念，第一个概念叫做符号状态（Symbolic State），并且用σ来表示，符号状态是原变量到符号值的一个映射，初始时符号状态σ为空，当执行完以下两个语句后：

x = input();
y = input();

即x和y获得了符号化的输入{x = xsym, y = ysym}，此时的符号状态σ = {x → xsym, y → ysym}。当执行完z = 2 * y之后，符号状态更新为σ = {x → xsym>, y → ysym, z → 2 * ysym}。

第二个概念叫做路径约束（Path Constraint），简称PC，PC表示到达当前路径需要满足的条件，PC的初始值为true，意为没有约束。例如达到Path-1需要满足条件x == z和x > y + 10，那么这条路径的路径约束PC就是(xsym == 2 * ysym) && (xsym > ysym + 10)。

符号执行需要为每一条路径维护一个符号状态σ和一个路径约束PC，让我们来模拟一下上述实例程序的符号执行过程，首先是初始状态，符号状态σ映射了x, y和z的符号值，此时路径约束PC = true：

假设符号执行的遍历策略是广度优先搜索BFS，那么经过第一个分支之后，符号执行分裂出了两条路径，两条路径的状态分别是：

分裂出来的两个路径唯一的不用是路径约束PC不同，不同的原因是因为分支条件的成立与否不同。分支条件成立就会执行左边的路径，PC = x_sym == 2 * y_sym表示达到左边的路径需要满足的约束条件；分支条件不成立就会执行右边的路径，PC = x_sym != 2 * y_sym表示达到右边的路径需要满足的约束条件。

右边这条路径已经执行到尽头了，而左边的路径还可以继续延伸，所以继续分裂出两条路径，更新路径约束PC：

所以该程序执行到最后有3个状态，对应3条不同的路径。讲到这里，相信大家对符号执行已经有一个初步的认识了，接下来我们进行下一步的学习。

0x02. 约束求解

假设现在有一个问题——我们输入的x和y的值分别是多少时，程序能够输出"Path-1"。在上一节中我们已经通过符号执行求解出了Path-1对应的路径约束PC，即PC = (xsym == 2 * ysym) && (xsym > ysym + 10)，那么我们只需要把xsym和ysym当做未知量，令PC == true，即可得到一个二元一次方程：(xsym == 2 * ysym) && (xsym > ysym + 10) == true，对这个方程求解即可得到一系列满足条件的x和y。

目前流行的符号执行引擎基本都会内置一个约束求解器（通俗点来说就是方程/方程组求解器），angr和miasm两个符号执行引擎使用的约束求解器都是z3，z3是微软开发的一款开源约束求解器，功能强大并且易用，之后我们会对z3专门进行讲解。简单用z3演示一下上述路径约束的求解：

from z3 import *

x = Int('x')
y = Int('y')
solver = Solver()
solver.add(x == 2 * y)
solver.add(x > y + 10)
print(solver.check())
print(solver.model())

输出：

sat
[y = 11, x = 22]

solver.check()用来检验方程是否有解，sat表示方程有解，unsat表示方程无解。[y = 11, x = 22]是求解出来方程的一个可行解。

除了用来求解具体值之外，约束求解也可以用来判断某条路径是否可行，如果一条路径的约束求解无解，则该条路径总是不会被执行，其后的分支也可以被忽略，节省符号执行的时间。

约束求解在某种程度上依然是符号执行的关键瓶颈之一，很多时候符号执行引擎跑不出结果来都是因为约束求解器的求解能力不足，这一点我们会在之后讨论。

0x03. 动态符号执行

上述的符号执行过程我们都是用类似于C语言的高级语言形式来描述的，显然真正的符号执行不可能是基于高级语言的，要么是汇编，要么是符号执行引擎内置的中间代码（IR），这些都属于低级语言。低级语言就会涉及内存、寄存器等一些概念，如果我们把内存和寄存器全部符号化，那么符号执行的路径约束就会显得非常复杂，并且一个包含各种符号的路径约束也没有什么实际使用价值。

由于纯符号执行的种种缺陷，现代的符号执行引擎基本上都是动态符号执行（Dynamic Symbloic Execution）或者叫做混合执行（Concolic Execution），以下统一称为动态符号执行。动态符号执行会维护一个实际状态和一个符号状态：实际状态将所有具有实际值的变量映射到实际值，符号状态只映射那些有非实际值的变量。以angr符号执行引擎为例，默认情况下，只有从标准输入流中读取的数据会被符号化，其他数据都是具有实际值的。

例如：

>>> state = proj.factory.entry_state()
<SimState @ 0x401120>
>>> state.regs.rax
<BV64 0x1c>

这里初始化了一个“状态”，这个状态维护了寄存器等一些变量，在这个状态中rax寄存器是具有实际值0x1c的。

好的，符号执行的入门知识讲到这就足够了，之后我们会在合适的时机进行拓展。

评论