前言

符号执行 (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的三个变量的和。我们这里设置的条件是想看看什么样的输入向量的情况下，得到的三个输出变量的和等于3.

符号执行

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

静态符号执行具体流程

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

过程内分析流程

程序全局分析流程

动态符号执行(concolic)(混合符号执行)

符号执行在发展过程中出现了一种叫做动态符号执行的方法(concrete and symbolic， concolic)。动态符号执行是以具体数值作为输入来模拟执行程序代码，与传统静态符号执行相比，其输入值的表示形式不同。动态符号执行使用具体值作为输入，同时启动代码模拟执行器，并从当前路径的分支语句的谓词中搜集所有符号约束。然后修改该符号约束内容构造出一条新的可行的路径约束，并用约束求解器求解出一个可行的新的具体输入，接着符号执行引擎对新输入值进行一轮新的分析。通过使用这种输入迭代产生变种输入的方法，理论上所有可行的路径都可以被计算并分析一遍。

动态符号执行相对于静态符号执行的优点是每次都是具体输入的执行，在模拟执行这个过程中，符号化的模拟执行比具体化的模拟执行的开销大很多；并且模拟执行过程中所有的变量都为具体值，而不必使用复杂的数据结构来表达符号值，使得模拟执行的花销进一步减少。但是动态符号执行的结果是对程序的所有路径的一个下逼近，即其最后产生路径的集合应该比所有路径集合小，其实concolic执行使用了深度优先的搜索策略。

参考：

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