本文共 760 字，大约阅读时间需要 2 分钟。

符号执行最初应用于源代码安全检测领域，通过模拟程序执行，使用符号表达式表示变量取值，进而进行语义分析。该技术将路径条件转化为符号约束，结合约束求解器，用于检测程序漏洞和生成测试用例。

基本原理

符号执行分为过程内分析和过程间分析。过程内分析仅处理单个函数，而过程间分析则考虑函数调用链和环境信息。这种方法在漏洞检测中更为常用，侧重于全局安全性检测。符号执行与约束求解器结合使用，生成测试用例是热门研究方向。

符号执行的优势在于效率高、代价低，但面临路径状态空间爆炸问题。每个条件分支增加新路径，尤其循环时，路径数呈指数增长。解决方法包括限制路径数或设置时间、内存上限。

动态符号执行结合静态分析与具体执行，交替符号化和动态执行指令。每条路径用true/false序列表示，第i个条件语句对应第i个true/false。

检测程序漏洞

漏洞表现为变量取值不符合约束。通过符号执行，变量取值表示为符号表达式，条件转化为约束，判断路径可行性。例如，数组越界可用约束求解器验证。

构造测试用例

符号执行过程中收集输入约束，分析异常条件，构造满足约束的输入触发漏洞。精心设计测试用例可引发程序异常。

实现方法

符号执行包含符号执行和约束求解。正向分析全面处理程序，逆向分析针对漏洞部分。过程内分析逐句处理，记录变量存储空间和全局变量，检查赋值和控制转移。过程间分析按深度优先或广度优先顺序处理。

动态符号执行

动态符号执行与具体执行交替，符号化未执行指令。路径状态用σ表示变量映射，PC表示不含量词表达式。

实例分析

缓冲区溢出漏洞例子：数组访问检查点，符号约束可检测越界。正向分析生成约束，逆向分析从漏洞语句逆推路径条件。

通过符号执行，可发现变量取值范围，判断漏洞是否存在。结合调用图分析，发现漏洞约束可满足时，程序存在漏洞。