Context
可靠程序的大规模生产是将计算机应用于当今具有挑战性的问题的基本要求之一。现行的方法基于测试, 工作焦点在选择数据集, 但无法证明程序是正确的. 一劳永逸的程序证明存在难以在短期内克服的困难, 所以难以应用到实际.
Objectives
这篇文章的目标是设计在这两个极端中的一个实际的程序测试方法(符号执行).
Methods
向程序提供代表任意值的符号值而不是真实的输入, 随后”正常地”执行程序, 唯一的区别是, 程序里的值是在输入符号上的公式(在这篇paper中被限制为整数的多项式). 程序执行的每个结果会对应到一大类普通的测试数据. 结果可以之后检查是否满足程序员的期望.
符号执行是由普通执行通过将执行语义扩展到符号上扩展而来. 作者在简化的假设下讨论了符号执行. 符号值全部通过输入来引入. 表达式的计算通过将变量值替换成对应的符号值自然地扩展了. goto语句不需要任何更改. 通过将pc引入执行状态来扩展定义if语句的执行语义. pc是在符号输入上的一个布尔表达式, 不包含任何程序内的变量. pc是为了以某个路径运行, 程序必须满足的特性. 遇见if语句时, 通过当前pc和if包含的表达式q的关系, 来确定走哪条路径或是分裂执行(forking execution), 同时更新pc.
作者实现了一个符号执行工具EFFIGY, 它解释执行一个比上面的假设更复杂的PL/I风格语言, 提供了常规的debugger功能. 作者展示了如何利用这些功能处理符号执行中比较棘手的问题, 例如无限执行树问题.
Results
作者在论文中给出了对于多个实际程序，EFFIGY的处理. EFFIGY提供了标准的debugger功能, 并能使用符号解释执行程序, 并将变量用符号上的整数多项式表示. 对于执行树无限的程序, EFFIGY能利用状态保存和恢复, 交互式地探索不同的执行路径. 这证明了作者所提出的测试方法是实际有效的.
利用EFFIGY提供的PROVE,ASSERT和ASSUME语句, 可以验证和证明程序的性质.
也存在一些不足. 例如, 对数组的处理天然的存在模糊性, 机器运算的离散性和不精确性(溢出)会违反可交换性, 使一些优化无法进行. 一个自动推导因为能力限制会错误的认为一些条件无法确定, 导致系统沿着一条和真实世界完全不一样的路径执行.
Conclusion
作者提出符号执行的技术, 能用符号化的输入代替真实数据的输入执行程序, 用一组符号值代表一类真实的测试数据. 作者实现了EFFIGY交互式符号执行工具, 提供了标准debugger功能, 能在一个简单的语言上进行测试, 证明正确性等操作. 但符号执行仍然存在执行树无限, 内存地址引用模糊性, 计算溢出导致违背可交换性等等问题, 使其仍然只是较为理想情况下的工具.
Comments
这篇文章是最早的符号执行的文章, 其中提到的符号执行由于路径爆炸问题、约束求解困难集内存建模等问题, 难以在现实中达到很好的效果.