前言

符号执行（Symbolic Execution）是一种程序分析技术，它可以通过分析程序来得到让特定代码区域执行的输入。顾名思义，使用符号执行分析一个程序时，该程序会使用符号值作为输入，而非一般执行程序时使用的具体值。在达到目标代码时，分析器可以得到相应的路径约束，然后通过约束求解器来得到可以触发目标代码的具体值。

符号执行理解

以下面的源代码为例子：

int m=M, n=N, q=Q; 
int x1=0,x2=0,x3=0;
if(m!=0)
{
    x1=-2;
}
if(n<12)
{
    if(!m && q)
    {
        x2=1;
    }
    x3=2;
}
assert(x1+x2+x3!=3)

上述代码是一个简单的c语言分支结构代码，它的输入是M,N,Q三个变量；输出是x1,x2,x3的三个变量的和。我们这里设置的条件是想看看什么样的输入向量<M,N,Q>的情况下，得到的三个输出变量的和等于3.

符号执行

如果把结果条件更改为漏洞条件，理论上也是能够进行漏洞挖掘了。对于如何根据最终得到的结果求解输入向量，已经有很多现成的数学工具可以使用。上述问题其实可以规约成约束规划的求解问题（更详细的介绍看这里：Constraint_programming ）。比较著名的工具比如SMT（Satisfiability Modulo Theory，可满足性模理论）和SAT。

静态符号执行具体流程

符号执行分为过程内分析和过程间分析（又称全局分析）。过程内分析是指只对单个过程的代码进行分析，全局分析指对整个软件代码进行上下文敏感的分析。所谓上下文敏感分析是指在当前函数入口点要考虑当前的函数间调用信息和环境信息等。程序的全局分析是在过程内分析的基础上进行的，如果过程内分析中包含了函数调用，就引入了过程间分析，因此两者之间是相对独立又相互依赖的关系

过程内分析流程

程序全局分析流程

动态符号执行（concolic）（混合符号执行）

动态符号执行，也叫dynamic symbolic execution（DSE）， concolic testing（concrete + symbolic）, directed automated random testing（DART）等
符号执行在发展过程中出现了一种叫做动态符号执行的方法（concrete and symbolic， concolic）。动态符号执行是以具体数值作为输入来模拟执行程序代码，与传统静态符号执行相比，其输入值的表示形式不同。动态符号执行使用具体值作为输入，同时启动代码模拟执行器，并从当前路径的分支语句的谓词中搜集所有符号约束。然后修改该符号约束内容构造出一条新的可行的路径约束，并用约束求解器求解出一个可行的新的具体输入，接着符号执行引擎对新输入值进行一轮新的分析。通过使用这种输入迭代产生变种输入的方法，理论上所有可行的路径都可以被计算并分析一遍。
动态符号执行相对于静态符号执行的优点是每次都是具体输入的执行，在模拟执行这个过程中，符号化的模拟执行比具体化的模拟执行的开销大很多；并且模拟执行过程中所有的变量都为具体值，而不必使用复杂的数据结构来表达符号值，使得模拟执行的花销进一步减少。但是动态符号执行的结果是对程序的所有路径的一个下逼近，即其最后产生路径的集合应该比所有路径集合小，其实concolic执行使用了深度优先的搜索策略。

image.png

符号执行相比于具体执行（concrete execution，对变量赋值进行测试）的好处是，它生成的测试用例虽然也是一个具体的数值，但是这些数据代表的是一类数据输入（class of inputs）。因此，通过符号执行，对于比较小的问题，可以在有限的时间完成覆盖完全的测试。

存在挑战：
1.内存。符号分析如何处理指针、数组等复杂对象？
2.环境。对库和系统代码的调用可能会有副作用，如创建文件，对用户代码的调用等。但是不可能对所有的交互都进行评估。
3.路径爆炸。分支以及循环会导致路径指数级增长。
4.约束求解。SMT可以对多达上百个参数的约束求解，但是非线性的情况无能为力。

基础知识：

可靠性（soundness）

可靠性的意思是防止false negative假阴性，也即保证所有不安全的输入都能够找出来

完备性（completeness）

完备性是防止假阳性false positive，也即找出来的不安全的输入确实都是不安全的。

STMT

stmt是下一个要评估的语句，可以是赋值，条件分支或跳转。
对于每一个在静态分析中不能确定值的变量，都使用符号 $\alpha$ 来表示；代码中的所有分支条件都通过 $\pi$ 来表示，这些条件就构成了约束（constraint）；然后和下一步执行的代码stmt，构成了符号执行树上的一个节点。

SMT

当符号执行树构造好了之后，接下来的便是对约束进行求解，这里是SMT（satisfiability modula theory）的范畴了。通过对每一个非叶节点的条件求解，可以获得满足条件的变量的具体值。

参考：
https://www.k0rz3n.com/2019/02/28/%E7%AE%80%E5%8D%95%E7%90%86%E8%A7%A3%E7%AC%A6%E5%8F%B7%E6%89%A7%E8%A1%8C%E6%8A%80%E6%9C%AF/
https://zhuanlan.zhihu.com/p/26927127
https://zhuanlan.zhihu.com/p/42831910
https://blog.csdn.net/wcventure/article/details/86773290

简述符号执行