Zhou S, Jiang M, Chen W, et al. WADIFF: A Differential Testing Framework for WebAssembly Runtimes[C]//2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 2023: 939-950.
Introduction
Wasm运行时的准确率和可靠性很重要
现有工作的不足：
- 测试用例非法，无法通过有效性测试
- 合法测试用例是随机生成的，无法探索复杂的runtime实现
- 无法系统的建模运行时的状态，语义相关的未触发crash的漏洞可能不会被报告
挑战
- 如何生成测试用例，尽可能多地覆盖spec的内容
- 使用wasm-spec来生成有效的测试用例：设计了DSL transformer将自然语言转化为DSL，基于转化的DSL，设计了符号执行引擎来生成测试用例
- 为了达到非法的测试用例，对测试用例进行变异
- 确定性的差分模糊测试框架：确定需要比对执行结果的哪些内容
- 增加了prologue语句来设置前置状态
- 建模wasm运行时，手动插桩哪些属性需要被丢弃，如果被丢弃的属性有difference，怎么存在不一致的指令
生成了1,395,091个测试用例，124,157触发了异常，417个指令触发了异常；仅发现了21个问题，8个被确认或修复了
贡献
- spec的transformer，将原来的语言转化为DSL，基于dsl进行程序分析
- 测试用例生成器：基于dsl采用符号执行生成wasm程序，设计了变异器对wasm进行变异
- wasm运行时的学习和建模
- 差分测试框架：测试用例生成+确定性测试引擎
Background
wasm运行时包括三个步骤
- decoding：字节码被翻译为模块module
- validation：wasm运行时检查module是否有效
- execution：有效后初始化模块，创建模块的实例，调用开始函数
Wasm操作码会有不同的控制流，需要生成可以覆盖到各个流的测试用例，方法是将SPEC转化为DSL
Methodlogy
测试用例生成器
差分测试引擎
比较变量的值来确定是否存在不一致性
差分测试的形式化定义
其他材料
开源仓库：https://github.com/erxiaozhou/WaDiff
展望
- 生成调用多个指令的测试用例
- 覆盖率不高
- 生成测试用例的模板较为单一