利用黑盒变异模糊检测SMT求解器中的关键缺陷
Detecting Critical Bugs in SMT Solvers Using Blackbox Mutational Fuzzing
摘要：
形式化方法广泛地使用SMT求解器来确定公式的可满足性，例如，在软件验证、系统测试生成和程序合成中。然而，由于其复杂的实现，求解器可能包含导致不合理结果的关键错误。鉴于求解器在软件可靠性方面的广泛适用性，依赖这种不合理的结果可能会产生有害的后果。在本文中，我们提出了风暴，一种新的黑盒突变模糊技术，用于检测SMT求解器中的关键错误。我们在7个成熟的求解器上运行模糊器，发现了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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
