ZESTI论文阅读笔记

A. 彻底对敏感操作进行测试

ZESTI将程序输入替换成符号值, 并在同时记录相应的具体输入值, 在遇到分支时使用具体输入来导向程序执行流程. 在执行程序时, ZESTI会收集路径条件并用于验证潜在的错误操作. 例如, 只要程序访问符号内存地址, ZESTI就会检查对于所有满足当前路径条件的输入而言, 该操作是否安全.

1: int v[100];
2: void f ( int x) {
3:  if (x > 99)
4:      x = 99;
5:   v[x] = 0;
6 : }

上例代码存在bug: 当输入的x是负数时是可以访问非法内存的. 测试套件可以使用不同的参数调用此函数并验证函数行为, 试图以此来最大化测试效果, 比如代码行覆盖率. 符号执行在第3行收集路径约束x \leq 99 然后在第5行检查是否有任何可能的x值是的缓冲区v溢出. 更具体的就是ZESTI会检查公式 x \leq 99 \Rightarrow (x \geq 0 \land x \leq 99) 是否有效, 并立即以x的负整数值找到一个反例.

为了兼容所有的测试框架, ZESTI将测试和测试脚本视为黑盒子. 对原始程序重命名, 并将其替换为能够调用ZESTI解释器的脚本, 再将院士程序和任何命令行参数都作为参数传递给脚本执行.

ZESTI自动检查几个输入类, 即命令行参数和读取文件的操作, 并将其视为符号数据的来源.

B. 探索敏感操作的额外路径

为了缓解路径爆炸问题, ZESTI通过两种机制仔细选择不同的路径.

  1. 它只偏向敏感指令, 即可能包含错误的指令
  2. 它根据敏感指令的距离按升序选择分歧点

这种方法的关键思想是在一个稍微不同的路径上执行敏感指令, 目的是为了能在相应指令包含bug时及时触发. 选择一个合适的分歧点可以不费功夫地再次到达相同的指令.

ZESTI动态识别敏感指令. 当它执行具体的程序路径时, 它会跟踪所有可能导致替代执行(alternative execution)出错的指令. 我们考虑两种类型的敏感指令: 内存访问和除法. 我们将所有的指针解引用视为敏感操作, 而对于除法, 我们只考虑那些将符号作为分母的敏感操作. 在LLVM层级, ZESTI把对符号地址的所有内存访问, 以及GetElementPtr指令前面的那些(具体或符号)的内存访问, 以及将符号作为分母的所有除法和模运算视为敏感操作.

为了全面地使用不同的输入执行敏感指令, ZESTI尝试遵循达到这些敏感指令的替代执行路径. 为此, ZESTI会识别沿着执行可能遇到分支的具体路径的所有点, 例如取决于符号输入的分支. 然后ZESTI会根据与敏感指令的距离以升序对分支点进行排序, 并将它们作为符号执行的起始点.

figure2.png

上图概述了ZESTI所使用的策略.

  • 第1行遍历从1到用户指定的最大距离
  • 第2行遍历所有的敏感指令
  • 如果在距当前指令的当前距离处发现任何分支点, 则将其用于运行深度受限的符号执行, 界定函数为f(D).

函数f应适当高估分支点和替代路径上的敏感指令之间的距离. 低估这个距离会使得SE深度限制太小而无法到达敏感指令, 然而过于高估也能增加不必要的开销.(要注意, 并非所有ZESTI探索的额外路径都能保证到达敏感指令). 我们根据经验发现线性函数表现良好, 在试验中我们采用f(D) = 2 *D

作为优化, 算法的第2行以, 与程序起始位置距离递减的顺序, 考虑敏感指令. 这有利于有限探索更深层的状态, 前提是:

  • 更深层的状态更有意义, 因为它们与测试套件所执行的功能相关, 而不是通常与命令行解析或输入验证相关的浅状态
  • 由于路径保证问题, 标准符号执行不太可能在合理的时间内到达这些状态.

直观说, ZESTI用来测量两个执行点距离的度量需要评估符号执行从一个点到另一个点所需要的工作量. 为此, ZESTI将两条指令之间的距离定义为它们之间的分支数, 要求这些分支能使得输入可以在分支任意一侧执行. 使用该度量标准可以确定程序可能采用的不同路径(以及ZESTI可探索的路径)的分支点数, 并且对于仅使用具体具体数据的大型代码块在本质上是不敏感的.

This entry was posted in papers, symbolic execution. Bookmark the permalink.

Leave a Reply

Your email address will not be published. Required fields are marked *

This site uses Akismet to reduce spam. Learn how your comment data is processed.