一句话：用 SMT 约束生成带已知安全性的程序作为测试预言，检测程序分析器自身的可靠性与精度缺陷。
程序分析器实现了复杂算法，其实现中同样可能存在缺陷：不精确的分析器无法验证本无不可达错误位置的安全程序，而不可靠的分析器则会把存在可达错误位置的不安全程序错误地证明为安全。本文提出为分析器生成基于约束的测试预言的方法，将用于 fuzzer 基准测试的 Fuzzle 改造并扩展为工具 Minotaur。Minotaur 从 SMT 约束生成 C 程序，并依据约束的可满足性推导所生成程序是安全还是不安全；据此判定被测分析器的结论是否正确，例如若分析器将不安全程序证明为安全，则说明其存在可靠性问题。作者用 Minotaur 测试了 11 个著名的、推理可达性属性的分析器，共发现 30 个独特的可靠性与精度问题。
Program analyzers implement complex algorithms and, as any software, can contain bugs. Bugs in their implementation may lead to analyzers being imprecise and failing to verify safe programs, i.e., programs with no reachable error locations; or worse, analyzer bugs may lead to reporting unsound results by verifying unsafe programs, i.e., programs with reachable error locations.In this paper, we propose a method to detect such bugs by generating constraint-based test oracles for analyzers. We re-purpose and extend Fuzzle, a tool for benchmarking fuzzers, in a tool called Minotaur. Minotaur generates C programs from SMT constraints, and based on the satisfiability of the constraints, derives whether the generated programs are safe or unsafe. For instance, for an unsafe program, an analyzer under test contains a soundness issue if it proves it safe. Using Minotaur, we found 30 unique soundness and precision issues in 11 well-known analyzers that reason about reachability properties.CCS Concepts• Software and its engineering → Software testing and debugging.
@inproceedings{FleischmannKIWC24,
title = {Constraint-Based Test Oracles for Program Analyzers},
author = {Markus Fleischmann and David Kaindlstorfer and Anastasia Isychev and Valentin Wüstholz and Maria Christakis},
booktitle = {ASE},
year = {2024},
doi = {10.1145/3691620.3695035}
}