符号执行 （Symbolic Execution）是一种程序分析技术。其可以通过分析程序来得到让特定代码区域执行的输入。

使用符号执行分析一个程序时，该程序会使用符号值作为输入，而非一般执行程序时使用的具体值。在达到目标代码时，分析器可以得到相应的路径约束，然后通过约束求解器来得到可以触发目标代码的具体值。

符号执行技术是一种白盒的静态分析技术。即，分析程序可能的输入需要能够获取到目标源代码的支持。同时，它是静态的，因为并没有实际的执行程序本身，而是分析程序的执行路径。

符号执行就是把程序的执行用符号化的公式进行表示，直到最后才求解出满足约束的输入值，从而达到遍历程序所有约束的目的。那么，首先，什么是符号？

通过类比来理解：

那什么是执行路径？

程序可能的从头到尾的执行流程（ It’s a possible way to travel through the program.）

该例子有两条执行路径：

而执行路径如何像约束变量的方程那样对符号起作用？

输入不使用一个具体值，而是把输入符号化，这个例子中，也就是把输入a符号化为λ。如果想要Path1被执行，那么，符号λ，必须大于1，否则，就会执行另外的路径。

下面介绍如何对这个例子进行简单的符号执行。

首先，我们注入符号，把输入 a 符号化：将 a 定义为一个符号化的int值，其大小为32位，这32位的每一位都是符号化的。

当运行到一个由符号决定的if判断的时候，怎么做？branch ，分支，也就是分为可能的不同执行路径。这里会分出两个分支：

如果我们想要程序能够走到两条路径，达到100%执行覆盖率，那很简单，求解器会随便取两个值，一个是大于1的值，另一个是小于等于1的值，这两个输入就足够覆盖两条路径。

如果我们想要b输出一个特定值，也很简单。

假如我们想要b输出一个值“2”，那么我们有两条约束：

可计算出结果：

也就说约束求解器会给出两个答案：a=0或a=3。又如我们想让b输出0，那么两条约束：

这就只能算出一个答案a=-1。

下面这个例子来自angr_ctf的ppt。

这段代码有哪些可能的路径？可以把这些路径表示成一个树，然后使用搜索算法来找到return 1节点。广度优先遍历是个好选择，angr默认使用的也是它。

一旦我们选择了一条执行路径，那么就可以构建一个SMT公式来求解符号。当然，在现实世界中，二进制文件会更复杂，随之，符号也就会更多，路径也会更多。二进制文件的复杂性呈指数增长是符号执行的最大问题。

SMT:

SAT（satisfiability）问题指的是命题逻辑公式的可满足性问题。但是 SAT 在表达能力上有很大的局限性，需要比 SAT 更强的表达方式。在这种形势下，将SAT问题扩展为SMT，经过扩展，SMT 能比 SAT 更好地表达一些人工智能和形式化方法领域内的问题，比如在资源规划、时序推理、编译器优化等很多方面用到了SMT。

SMT 的全称是 Satisfiability Modulo Theories，可被翻译为“可满足性模理论”、“多理论下的可满足性问题”或者“特定（背景）理论下的可满足性问题”，其判定算法被称为 SMT 求解器。简单地说，一个 SMT公式是结合了理论背景的逻辑公式，其中的命题变量可以代表理论公式。

这里举个例子，命题逻辑公式是这样：

即只允许出现变量、变量的否定和逻辑连接词

而SMT公式可以是这样：

即可以出现非逻辑符号，比如函数g(a)、f(g(a))和常量c、d，其中g(a) = c 这些理论公式可以替代命题变量。

P.S. 希望看雪的md编辑器能加上latex公式的功能。

那么怎么去遍历程序，找到我们想要的执行路径，然后求解出符号λ呢？ 正在学习angr，那这里肯定就是用angr了。angr是一个符号执行引擎。它能1）遍历程序并找到所有分支；2）搜索程序里符合给定条件的状态；3）通过给定路径约束，求解符号变量。

符号执行有两个基础：执行路径和符号。从这两者入手来学习。

一条执行路径代表程序从某处开始执行，再到某处结束的一个执行流程。在angr中，执行路径的节点由SimState对象表示，它存储程序的状态以及之前状态的历史。将这些SimState连接起来就会创建一条执行路径。

但是我们关注的不仅仅是一条路径，而应该关注多条路径以搜索到我们需要的路径。在angr中如何表示以及构建一组路径呢？

angr存储和操作给定程序的一组路径是通过Simulation Manager（SM）对象完成的。SM提供了函数去遍历程序以生成可能的路径和状态。生成一组路径的过程如下：

angr可以在指定的位置启动程序，此时是第一个active状态；

在每个active（未终止）状态下执行指令，直到到达分支点或者该状态终止；

生成了路径，那么其中如何搜索我们想要的呢？在生成路径过程中，搜索是否有哪个active状态符合我们的条件，这个条件可以是指令的地址，也可以是任何确定我们是否已达到所需状态的函数。

关于执行路径，符号执行中有一个很大的问题，就是状态爆炸（State Explosion）。对于每个if语句，分支路径可能会加倍，路径的增长与程序的“大小”呈指数关系。当前并没有非常好的解决方案。

一个好的方案是：如果可以确定继续运行不太可能到达成功状态的条件，则可以立即终止那部分路径并舍弃状态图的大部分。至于如何确定可能会失败的状态，可以使用各种启发式算法，比如：Veritesting。

接着，我们小结一下搜索和避免路径的方法

最后，我们看看angr中关于这部分的函数：explore函数。它会将所有符合条件的状态放到simulation.found列表中。

另外，搜索或者避开一个特定指令的地址很常用，所以，find和void参数都可以是地址：

当用户输入是从标准输入（stdin）中获得，比如简单调用scanf函数的时候，angr会自动注入符号进行符号化；然而，当用户输入更复杂，比如scanf函数的格式化字符串很复杂，或者从文件、网络或者UI中获取输入的时候，angr则不会自动注入符号，这时我们需要手动在需要的地方进行注入符号。

angr中的符号是由bitvector（位向量）表示的。位向量具有大小（size），即它们的位数。位向量最常表示的数据是n位整数或字符串。位向量和典型变量之间的区别在于：典型变量仅仅存储一个值，但是位向量存储满足某些约束的每个值。比如：设位向量λ为8位，并受以下约束：

上面是位向量的存储方式。但是，如果我们要具体化位向量，则它可以取以下任意值：2、4或1。

按我自己的理解，这个位向量应该是这样：[00010110]。如有错误欢迎指正^_^。

关于位向量的一些定义：

angr为开源约束求解器z3提供了一个不错的前端，用它来求解符号约束。它具有如下功能（不止）：

只要位向量的大小等于变量的大小，我们就可以把符号注入变量中。引擎在执行给定路径的时候，会自动生成约束（例如，对于下面的程序，如果要执行Success那条路径， λ= 'hunter2'，或者对于另外一条路径就是 λ 不等于 'hunter2'）。如果需要，可以在程序执行期间的任何时候手动将约束添加到任何位向量。

前面学习了符号的注入和表示，接下来我们看看符号的传播（Symbol Propagation），直接用一个例子来学习。

下图代表内存，其中变量user_input和encrypted_inputX都已经标注；所有符号都用绿色表示。很明显，变量encrypted_inputX的值完全由user_input决定，如箭头所示。传输值的时候，符号也可以传播。

约束也是可以随着符号值进行传播的（Constraint Propagation）。如果添加约束λ= 10，那么我们可以求解出encrypted_input2。

而逆过来的话，即约束逆向传播（Constraint Reverse-Propagation）也是当然可以的，比如我们给传播的符号值添加约束：encrypted_input2 = 14，那么可以求解出λ= -10。也就是我们通过给定的结果求解出了初始条件。

前面对于执行路径，符号执行有个大问题就是路径爆炸。那么对于符号，这里也有个大问题，那就是符号执行依赖于解决复杂的约束系统——约束满足问题是NP完全问题。

在ang r_ctf项目的solutions目录下都给出了解题脚本，在注释中也对这些文件进行了说明：

IDA graph界面中指令前显示地址的方法：Options->General->Disassembly->勾选 Line prefixes(graph)

解题脚本：修改一下原有脚本，把python2改成python3。

运行结果：

标准输入相关：

状态构造函数：

project.factory.entry_state()是project factory上可用的状态构造函数之一。构造函数主要有这些：

使用IDA一打开程序，main函数太大，不能显示图形化界面，也不能反编译成C伪代码。往下翻，发现调用了很多avoid_me函数，如下图所示。

那么查看avoid_me函数，功能就是给should_succeed变量赋值0，没有别的了，那么我们在符号执行的时候可以在explore函数里指定avoid参数以避免执行它。

边上还有个函数maybe_me，这里面有我们想要的东西。

那么这题的思路和上一题差不多，只不过对explore函数加个参数avoid。

解题脚本：修改一下原有脚本，把python2改成python3。

运行结果：

这一题和第0题差不多，都是对输入和一个字符串进行比较，改一下第1题的脚本，也可以用。

但是这题的本意是让我们学会如何根据程序本身的输出来告诉angr应避免或搜索的内容，而不需要用IDA来找地址。也就是说，可以先各写一个函数来判断输出中是否有“Good Job.”和“Try again.”，然后分别把他们当作explore函数的find参数和avoid参数。两个参数的值不再是一个想要执行到的地址，而是一个判断state是否满足条件的函数。

解题脚本：将python2改成python3，除了修改print，还有给is_successful和should_abort里的stdout_output加上str()函数。

运行结果：

什么是SMT

angr官方文档 - Core Concepts - Simulation Managers

angr_ctf - solutions

[注意]传递专业知识、拓宽行业人脉——看雪讲师团队等你加入！