符号执行
維基百科,自由的 encyclopedia
符号执行(英語:symbolic execution)是一种计算机科学领域的程序分析技术,通过采用抽象的符号代替精确值作为程序输入变量,得出每个路径抽象的输出结果。这一技术在硬件、底层程序测试中有一定的应用[1],能够有效的发现程序中的漏洞。[2]
这一思想最初由IBM托马斯·J·华森研究中心的詹姆斯·C.金(James C. King) 于1976年6月在论文Symbolic Execution and Program Testing中提出[3],文中“解析程序的路径后,用符号模拟通过路径并获得输出”的方法如今被称为“经典符号执行”。由于20世纪80年代的研究追求分析的完备性,而大型程序的路径复杂,不可能完全遍历,符号执行这一研究领域遇冷。21世纪后,该领域研究有了新的进展:2006年,克里斯蒂安·卡达尔(Cristian Cadar)在论文中设计了一种“先进行符号执行,后根据符号执行结果生成测试用例”的“执行生成测试”技术[4],并随后将其发展为应用在GNU/Linux内核错误检查中的KLEE[5];2007年,库希克·森(Koushik Sen)在当年的软件工程自动化(Automated Software Engineering)会议提出将符号执行和实际执行结合的“混合执行(Concolic testing)”方法[6];2009年,维塔利·奇波诺夫(Vitaly Chipounov)提出“选择性符号执行”方法,通过选择“对程序设计者有意义”的执行分支进行符号执行测试来提高对大型程序应用符号执行测试的可行性。
符号模拟技术(symbolic simulation)则把类似的思想用于电路分析[7];符号计算(Symbolic computation)则用于数学表达式分析[8]。