可满足性模理论 (SMT) 求解器是许多技术的核心引擎,例如符号执行。因此,确保 SMT 求解器的稳健性和正确性至关重要。虽然模糊测试是一种确保 SMT 求解器质量的有效方法,但我们观察到之前的模糊测试工作仅侧重于生成各种一阶公式作为输入,而忽略了 SMT 求解器的算法配置空间,这导致许多深藏不露的错误未被及时报告。在本文中,我们提出了 Falcon,一种同时探索公式空间和配置空间的模糊测试技术。将这两个空间结合起来会显著扩大搜索空间,使有效检测错误变得更加困难。我们通过利用两个空间之间的相关性来减少搜索空间,并引入自适应变异策略来提高搜索效率,从而解决了这个问题。经过六个月的广泛测试,Falcon 在两款最先进的 SMT 求解器 CVC4 和 Z3 中发现了 518 个已确认的错误,其中 469 个已经修复。与两款最先进的模糊测试器相比,Falcon 在 24 小时的测试中检测到了 38 个和 44 个以上的错误,并且覆盖率大幅提高。
主要关键词