CTF-All-In-One/doc/5.3_symbolic_execution.md

5.3 符号执行

• 符号执行的历史
• 什么是符号执行

符号执行的历史

或者进入https://github.com/enzet/symbolic-execution查看SVG大图。

什么是符号执行

符号执行起初应用于基于源代码的安全检测中，它通过符号表达式来模拟程序的执行，将程序的输出表示成包含这些符号的逻辑或数学表达式，从而进行语义分析。

符号执行可分为过程内分析和过程间分析（或全局分析）。过程内分析是指只对单个函数的代码进行分析，过程间分析是指在当前函数入口点要考虑当前函数的调用信息和环境信息等。当符号执行用于代码漏洞静态检测时，更多的是进行程序全局的分析且更侧重代码的安全性相关的检测。将符号执行与约束求解器结合使用来产生测试用例是一个比较热门的研究方向。（关于约束求解我们会在另外的章节中详细讲解）

符号执行具有代价小、效率高的有点，但缺点也是很明显的。比如路径状态空间的爆炸问题，由于每一个条件分支语句都可能会使当前路径再分出一条新的路径，特别是遇到循环分支时，每增加一次循环都将增加一条新路径，因此这种增长是指数级的。在实践中，通常采用一些这种的办法来解决路径爆炸问题，比如规定每个过程内的分析路径的数目上限，或者设置时间上限和内存上限等来进行缓解。

动态符号执行

动态符号执行将符号执行和具体执行结合起来，并交替使用静态分析和动态分析，在具体执行的同时堆执行到的指令进行符号化执行。