符号执行（Symbolic Execution）

符号执行是一种程序分析技术，它不用具体数值而是用符号变量作为程序输入，在执行过程中沿每条路径积累关于这些符号的约束，从而系统性地探索程序的所有可能行为。

概述

符号执行的思想在二十世纪七十年代由詹姆斯·金（James King）等人提出，近年随着约束求解技术的成熟而重新兴起。它介于静态分析与动态测试之间：既像执行那样跟随程序控制流，又像静态分析那样处理抽象的符号而非具体值。

核心原理

• 符号状态：程序变量的值用关于输入符号的表达式表示，而非具体数字。
• 路径条件：沿某条执行路径上所有分支判断累积而成的约束公式，刻画走到该路径需要满足的输入条件。
• 约束求解：借助可满足性理论求解器判断路径条件是否可满足，可满足则路径可达并可生成具体测试输入。
• 路径爆炸：分支数量随程序规模指数增长，是符号执行面临的最大挑战。

应用场景

符号执行广泛用于自动测试用例生成、软件漏洞挖掘、程序验证与调试。混合式的动态符号执行结合具体执行与符号执行，能穿透复杂的外部调用。许多知名的自动化漏洞发现工具都以符号执行为核心引擎。

常见问题

问：路径爆炸问题如何缓解？答：常见手段包括路径合并、启发式搜索优先探索高价值路径、函数摘要复用、以及与具体执行结合的动态符号执行，用具体值绕过难以求解的部分，从而控制路径数量的膨胀。

问：符号执行和模糊测试有何区别？答：模糊测试随机变异输入靠概率触发缺陷，快速但盲目；符号执行通过约束求解精确构造能进入特定路径的输入，深入但代价高。两者常结合使用，取长补短。