Fleischmann, M., Kaindlstorfer, D. M., Isychev, A., Wüstholz, V., & Christakis, M. (2024). Constraint-Based Test Oracles for Program Analyzers. In V. Filkov, B. Ray, & M. Zhou (Eds.), ASE ’24: Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering (pp. 344–355). Association for Computing Machinery. https://doi.org/10.1145/3691620.3695035
ASE '24: 39th IEEE/ACM International Conference on Automated Software Engineering
en
Event date:
27-Oct-2024 - 1-Nov-2024
-
Event place:
Sacramento, United States of America (the)
-
Number of Pages:
12
-
Publisher:
Association for Computing Machinery, New York, NY, USA
-
Peer reviewed:
Yes
-
Keywords:
constraint-based test oracles; program analyzers; unsoundness; imprecision
en
Abstract:
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.
en
Project title:
Testing Program Analyzers Ad Absurdum: 101076510 (European Commission)
CC BY-SA 4.0
