论文标题
使用BlackBox突变模糊检测SMT求解器中的关键错误
Detecting Critical Bugs in SMT Solvers Using Blackbox Mutational Fuzzing
论文作者
论文摘要
正式方法将SMT求解器广泛用于确定公式的满意度，例如在软件验证，系统测试生成和程序合成中。但是，由于其复杂的实现，求解器可能包含导致不符合结果的关键错误。鉴于求解器在软件可靠性中的广泛适用性，依靠这种不符合的结果可能会带来不利的后果。在本文中，我们提出了Storm，这是一种新型的黑盒突变模糊技术，用于检测SMT求解器中的关键错误。我们在七个成熟的求解器上运行fuzzer，并找到29个以前未知的关键错误。在部署之前，Storm已经用于测试流行求解器的新功能。
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.
