Symbolic Execution for Software Testing: Three Decades Later 翻译

摘要

近年来, 由于其能够生成高覆盖率的测试套件并能够在复杂的软件应用程序中发现深层错误, 因此对软件测试的符号执行产生了浓厚的兴趣. 在本文中, 我们该市了现代符号执行技术, 讨论了他们在路径探索, 约束解决和内存建模方面的主要挑战, 并讨论了主要从作者自己的工作中得出的几种解决方案.

引言

近年来，符号执行作为一种用于生成高覆盖率测试套件并在复杂软件应用程序中查找深层错误的有效技术，引起了广泛关注。尽管符号执行背后的关键思想是在三十年多以前引入的，但由于约束可满足性的重大进步以及结合了具体和符号执行的可伸缩性更强的动态方法，才使它成为现实。在本文中，我们概述了现代符号执行技术，并讨论了它们在路径探索，约束解决和内存建模方面的挑战。请注意，我们的目的不是在此提供对该地区现有工作的全面调查，而是选择使用主要来自作者自己的工作的示例来说明一些关键挑战和建议的解决方案。
在软件测试中，符号执行的主要目标是在给定的时间内探索尽可能多的不同程序路径，并为每个路径生成一组行使该路径的具体输入值，并检查是否存在各种错误，包括声明冲突，未捕获的异常，安全漏洞和内存损坏。生成具体测试输入的能力是符号执行的主要优势之一：从测试生成的角度来看，它允许创建高覆盖率的测试套件，而从错误查找的角度来看，它为开发人员提供了触发错误的具体输入，可独立于生成错误的符号执行工具来用于确认和调试错误。
此外，请注意，就查找给定程序路径上的错误而言，符号执行比传统的动态执行技术（如由诸如Valgrind或Purify之类的流行工具所实现的那些技术）更强大，后者取决于触发错误的具体输入的可用性。最后，与某些其他程序分析技术不同，符号执行不限于查找诸如缓冲区溢出之类的通用错误，而是可以推断出更高级别的程序属性，例如复杂的程序断言。

古典符号执行概述

符号执行的关键思想是使用符号值而不是具体的数据值作为输入，并在符号输入值上将程序变量的值表示为符号表达式。结果，程序计算的输出值表示为符号输入值的函数。在软件测试中，符号执行用于为程序的每个执行路径生成测试输入。执行路径是一个true和false的序列，其中序列中第i个位置的true（分别为false）值表示沿执行路径遇到的第i个条件语句采用了“ then”（分别为“else”）科。可以使用称为执行树的树来表示程序的所有执行路径。例如，图1中的函数testme（）具有三个执行路径，它们形成了图2所示的执行树。例如，可以通过在输入{x = 0，y = 1上运行程序）来执行这些路径。 }，{x = 2，y = 1}和{x = 30，y = 15}。目的是生成这样的一组输入，以便通过在这些输入上运行程序，可以完全探究一次取决于符号输入值（或在给定时间预算内尽可能多）的所有执行路径。