[开发测试][fuzz论文阅读] Symbolic execution for software testing: three decades later

Symbolic execution for software testing: three decades later

背景介绍

技术难点

1. 路径探索
2. 约束求解
3. 内存建模

关键目标

1. 生成一组具体的测试用例,执行该路径
2. 检查是否存在各种错误,包括内存断言冲突、未捕获的异常、安全漏洞和内存损坏

符号执行的优点

1. 比传统的动态执行技术更强大,不仅能够发现一般性的错误,还能够对复杂程序进行推理
2. 从测试生成来说,能够生成高覆盖率的测试用例
3. 从BUG寻找来说,能够提供具体的测试用例,方便确认和调试错误

符号执行的缺点

1. 如果判断条件是一个输入符号,会产生路径爆炸(限制搜索的时间、路径的深度、循环迭代的次数以及路径的数量)
2. 纯静态的符号执行,可能存在约束路径不能由求解器高效求解,比如判断函数的原函数实现咋不到

联合执行

1. 随机产生输入数据,得到响应的路径约束,然后取反得到对立的路径约束
2. 如此反复
3. 联合执行,可能会带来路径丢失,原因一样,路径约束不能求解
4. 联合执行,还需要区分实际状态和符号状态

面临的挑战

1. 路径选择

   1. 使用启发式函数对路径进行探索,先探索最值得探索的路径
   2. 使用一些可靠的程序分析的技术减少路径探索的复杂度

2. 约束求解

   1. 不相关约束消除(取反路径后面的约束)
   2. 增量求解(在前面的基础上)

3. 内存建模

   1. 程序语句如何翻译为符号化约束
      • 别名分析
   2. 符号化跳转
      • 联合执行,探索实际路径
      • SMT求解器,效率低
      • 使用静态分析

4. 并发执行

   1. 考虑动态符号执行

开源的符号执行工具

KLEE

KLEE结构图

组成

1. 解释模块
   1. 将被测程序翻译成LLVM(类似于RISC-V的精简指令集),LLVM实际上是一种汇编语言。通过在翻译好的LLVM指令中,加入一些功能函数的调用,在程序执行时,KLEE可以控制指令的执行过程,保存程序执行过程中的所有状态,包括内存信息、寄存器值以及程序计数器等。
2. 符号表示模块
   1. 将程序的输入变量全部用符号表示, 程序对变量操作统统体现在符号表上。当程序走到分支时,KLEE会将现有的信息进行复制,采用(COW(copy on write)的方式),复制只是对原对象的标记,只在对象发生变化时,才复制该对象并反映出变化。
3. 约束求解模块
   1. KLEE在使用符号执行时,会收集当前路径的约束条件。KLEE会对这些约束进行求解,得到具体的测试用例,在分支语句中,也可以用用例进行判断。
4. 路径选择模块
   1. 在路径执行时,KLEE将会保存所有经过约束求解但尚未执行的可行路径信息(state),在一条路径完成之后,该state会被标记为完成,被标记过的路径将不再被选择执行。路径的选择,有两种方法包括随机选择和基于覆盖率优化算法。
5. 错误检测模块
   1. 当程序遇到读写错误或者崩溃时,KLEE会根据约束条件,生成会导致该错误的测试用例,并终止此次执行。特别的当遇到除数为0时,KLEE会添加路径约束条件除数非0,继续执行。在遇到读写指令时,KLEE将变量地址和变量大小作为约束条件,检测是否存在内存越界。

ANGR

项目框架

组成

1. CLE模块(cle loads everything)
   1. 将可执行程序加载进内存空间,它可以从ELF/PE文件中识别文件头提取架构、代码段、数据段等信息,接着会继续加载程序的依赖文件,如so或者dll文件。
2. archinfo模块
   1. 保存针对不同架构的指令集,例如x86、arm、mips以及powerc等,提供专用的类,包含对应的CPU架构模型，包括寄存器、位宽、大小端等数据结构
3. pyVEX模块
   1. 将机器码转换为开源二进制插桩工具Valgrind所使用的中间语言VEX,这是因为angr可以处理不同架构的程序,因此需要一个中间语言进行分析
4. SimEngine
   1. 对VEX程序进行解释和执行,支持具体值执行和符号值执行，执行时支持自定义函数Hook和断点，支持自定义路径探索策略
5. Claripy
   1. 将符号执行中生成的路径约束转化成SMT公式，使用Z3进行求解
6. SimOS
   1. 用于模拟程序与系统环境交互，提供了许多模拟的libc函数和系统调用，用户也可以自行编写Hook函数进行模拟