Automated soundness testing of program analyzers

Abstract

Program analyzers are commonly used to ensure that programs do not contain errors. Cases where they miss an error (soundness bugs), are therefore especially critical. Past techniques for testing program analyzers have either relied on differential testing, or focused mainly on precision issues. We present a technique that generates unsafe programs using satisfiable SMT formulas. These can be used to test soundness of program analyzers in an automated fashion, without the need for differential testing. In order to test the technique, we implemented it in a tool called Minotaur, and used it to look for soundness bugs in 8 state-of-the-art program analyzers. We found bugs in 5 of the tools, which we explain and categorize in order to analyze the types of bugs our technique can find.

Programmanalysestools werden häufig eingesetzt, um sicherzustellen, dass Programme fehlerfrei sind. Fälle, in denen diese Tools mögliche Fehler übersehen (Fehlschlüsse), sind daher besonders kritisch. Frühere Methoden, Programmanalysetools zu testen, verließen sich auf entweder auf differentielles Testen, oder testeten hauptsächlich die Genauigkeit dieser Tools. Wir präsentieren einen Ansatz, der es ermöglicht fehlerhafte Programme mit Hilfe von erfüllbaren SMT Formeln zu generieren. Diese Programme eignen sich wiederum um automatisiert zu testen, ob Programanalysetools mögliche Fehler erkennen, ohne dass dadurch differentielles testen erforderlich wird. Um zu prüfen, ob unser Ansatz Fehlschlüsse findet, implementierten wir ihn in einem Tool namens Minotaur und verwendeten dieses, um Fehler in 8 moderne Programanalysetools zu suchen. Über die letzten 9 Monaten haben wir Fehlschlüsse in 5 dieser Tools gefunden. Wir erklären und kategorisieren diese, um zu verstehen welche Art von Fehlern unsere Technik finden kann.