符号执行（）是一种计算机科学领域的程序分析技术，通过采用抽象的符号代替精确值作为程序输入变量，得出每个路径抽象的输出结果。这一技术在硬件、底层程序测试中有一定的应用，能够有效的发现程序中的漏洞。

这一思想最初由IBM托马斯·J·华森研究中心的詹姆斯·C.金（James C. King） 于1976年6月在论文Symbolic Execution and Program Testing中提出，文中“解析程序的路径后，用符号模拟通过路径并获得输出”的方法如今被称为“经典符号执行”。由于20世纪80年代的研究追求分析的完备性，而大型程序的路径复杂，不可能完全遍历，符号执行这一研究领域遇冷。21世纪后，该领域研究有了新的进展：2006年，克里斯蒂安·卡达尔（Cristian Cadar）在论文中设计了一种“先进行符号执行，后根据符号执行结果生成测试用例”的“执行生成测试”技术，并随后将其发展为应用在GNU/Linux内核错误检查中的KLEE；2007年，库希克·森（Koushik Sen）在当年的软件工程自动化（Automated Software Engineering）会议提出将符号执行和实际执行结合的“混合执行（Concolic testing）”方法；2009年，维塔利·奇波诺夫（Vitaly Chipounov）提出“选择性符号执行”方法，通过选择“对程序设计者有意义”的执行分支进行符号执行测试来提高对大型程序应用符号执行测试的可行性。

符号模拟技术（）则把类似的思想用于电路分析；符号计算（）则用于数学表达式分析。

符号执行引擎
符号执行引擎是符号执行技术的实现产物，可以用于对程序进行符号执行。一个基本的符号执行引擎由下列部分组成：

状态信息存储器：存储下列符号执行所需状态信息。

pc：指向需要处理的下一条程序语句,其可以是赋值语句、条件分支语句或者是跳转语句；

\pi：指代路径约束信息,表示为执行到程序特定语句需要经过的条件分支，以及各分支处关于符号值a_i的表达式;

\sigma：表示与程序变量相关的符号值集.

语句执行器：执行每一条语句来获取该程序的控制流程。

约束解算器（）：用于在一条路径的符号执行结束后解算路径约束与符号执行结果，为开发者提供一个可供实际执行（）的值

实例
對於下列代码：
int f() {
y = read();
z = y * 2;
if(z == 12){
fail();
}else{
printf("OK");
}
}

实际执行时，该方法读入一个值存储于变量y。当z的值为12（即y的值为6）时，该方法调用fail()，反之打印OK。

在符号执行时，程序读入一个符号值λ，并将 λ 2 赋值给 z。当运行到 if 条件判断语句，由于无法判断 λ 2 == 12是否为真，符号执行引擎将执行“为真”与“为假”两种分支。执行时，引擎将判断语句处的程序环境与路径约束复制一份并应用于两条分支。本例中， fail() 分支的路径约束指的是判断条件 λ 2 == 12 ，而print("OK")分支的路径约束为 λ 2 != 12。路径结束时，约束解算器计算并得出一个对此路径有意义（即能够完成该分支的）输入变量实际值。该值可供帮助开发者复现错误时进行实际执行使用。本例中，fail()分支的一个约束结算结果是6。

局限性
路径爆炸
大多数符号执行方法不适用于大型程序：随着程序规模的扩大，程序中有意义的路径成指数级扩大。有些程序中存在无尽循环或递归调用，这更大大增加了有意义路径，提高了符号执行难度。为解决此问题，马健强（音译，Kin-Keung Ma）等人提出使用启发式路径搜索算法提高代码覆盖率；马特·斯塔特斯（Matt Staats）等人提出并行执行独立路径的方法来降低符号执行耗时； 库兹涅佐夫等人则提出了合并相似分支的方法缓解路径爆炸问题。

待测程序输入变量的特点
由于利用路径分析进行程序分析，对于输入变量范围大，但程序分支较少的程序，符号执行方法比对输入变量进行分析的方法（如动态程序分析）具有较强优势。但是对于输入变量变化范围小，程序分支多的程序，符号执行的效率较低。

内存地址存在别名
由于符号执行根据内存地址分析变量及其变化，对于有内存地址别名的程序，符号执行引擎将难以区分不同别名，因此执行结果可能有偏差。需要使用进行处理。

数组的处理
由于数组是大量不同值（如内存地址）的集合，符号执行引擎需要选择将数组作为一个单独的完整变量处理还是将每一个数组元素作为单独的变量处理。由于引擎无法得知程序中每个数组的意义，动态确定每个数组的类型十分具有挑战性。、Cloud9和Otter等工具通过实现文件系统操作、套接字、IPC等模型采用了这种方法。

创建整个运行环境的状态分支：基于虚拟机技术的符号执行工具通过创建整个VM状态的分支来解决环境问题。比如S2E中，每个符号执行状态都是一个独立的虚拟机快照。这种方法的空间复杂度较高，对内存的消耗很大。

注释
参考文献