Detecting Critical Bugs in SMT Solvers Using Blackbox Mutational Fuzzing
This addresses a reliability issue for users of SMT solvers in software verification and related fields, with incremental improvements in bug detection.
The paper tackled the problem of critical bugs in SMT solvers, which can cause unsound results in formal methods applications, and presented STORM, a blackbox mutational fuzzing technique that detected 29 previously unknown critical bugs in seven mature solvers.
Formal methods use SMT solvers extensively for deciding formula satisfiability, for instance, in software verification, systematic test generation, and program synthesis. However, due to their complex implementations, solvers may contain critical bugs that lead to unsound results. Given the wide applicability of solvers in software reliability, relying on such unsound results may have detrimental consequences. In this paper, we present STORM, a novel blackbox mutational fuzzing technique for detecting critical bugs in SMT solvers. We run our fuzzer on seven mature solvers and find 29 previously unknown critical bugs. STORM is already being used in testing new features of popular solvers before deployment.