Automatically Identifying Soundness and Completeness Errors in Program Analysis Tools

Abstract

Program analysis tools (such as static analyzers, SMT solvers, and program verifiers) are extremely important for ensuring the correctness of a large variety of software systems. Very often, these tools are assumed to be sound (i.e., do not miss errors) and complete (i.e., have a low rate of false positives), otherwise their results are not reliable. However, these assumptions do not always hold in practice. Even if their theoretical designs have been proven correct, the actual implementations can still contain issues. We thus propose through this dissertation systematic techniques for automatically identifying soundness and completeness errors in the implementations of program analysis tools. Other types of bugs, such as performance or convergence issues, can be also detected as by-products. Our first contribution is a novel combination of automatic test case generation approaches for identifying soundness, precision, and termination issues in the implementations of numerical abstract domains, the main components of static analyzers based on abstract interpretation. We show that our technique effectively detects errors in widely-used libraries for numerical analyses, outperforming dynamic symbolic execution and grey-box fuzzing. Our work applies also to abstract domains that rely on machine learning to improve the performance of the analysis. Our second contribution is an automated approach for synthesizing SMT formulas that are satisfiable or unsatisfiable by construction. Together with the known ground truth, these are used to test the implementations of SMT solvers. We generate satisfiable formulas together with models, and unsatisfiable formulas together with unsat cores; being incrementally complex, they facilitate debugging and faster error localization. We evaluated our work on three widely-used SMT solvers, Z3-seq, Z3str3, and CVC4 and on the automata-based solver MT-ABC. Our experimental results show that our approach effectively detects soundness, performance, completeness, and precision problems. It is applicable also to MAX-SMT solvers. Our third contribution is an automated technique that allows the developers to detect completeness issues in SMT-based program verifiers and soundness errors in their axiomatizations. Moreover, our approach helps them devise better triggering strategies for all future runs of their tool with E-matching. We developed a novel algorithm for synthesizing the triggering terms necessary to complete unsatisfiability proofs using E-matching.We evaluated our work on benchmarks with known triggering issues from four program verifiers. Our experiments show that it successfully synthesized the missing triggering terms in the majority of the cases, and can significantly reduce the human effort in localizing and fixing the errors.