一句话：提出 Falcon，同时探索公式空间与配置空间，利用二者关联和自适应变异高效发现 SMT 求解器深层缺陷。
现有 SMT 求解器模糊测试主要关注生成不同的一阶公式作为输入，却忽视求解器的算法配置空间，导致许多深层隐藏缺陷难以被触发。Falcon 将公式空间与配置空间视为二维输入空间进行联合探索，利用两个空间之间的相关性缩小搜索范围，并引入自适应变异策略提高搜索效率。作者在 CVC4 和 Z3 上进行了六个月测试，共确认 518 个缺陷，其中 469 个已被修复；与两个当前最优模糊测试器相比，Falcon 在 24 小时内分别多发现 38 和 44 个缺陷，并大幅提升覆盖率。
Satisfiability Modulo Theories (SMT) solvers serve as the core engine of many techniques, such as symbolic execution. Therefore, ensuring the robustness and correctness of SMT solvers is critical. While fuzzing is an efficient and effective method for validating the quality of SMT solvers, we observe that prior fuzzing work only focused on generating various first-order formulas as the inputs but neglected the algorithmic configuration space of an SMT solver, which leads to under-reporting many deeply-hidden bugs. In this paper, we present Falcon, a fuzzing technique that explores both the formula space and the configuration space. Combining the two spaces significantly enlarges the search space and makes it challenging to detect bugs efficiently. We solve this problem by utilizing the correlations between the two spaces to reduce the search space, and introducing an adaptive mutation strategy to boost the search efficiency. During six months of extensive testing, Falcon finds 518 confirmed bugs in CVC4 and Z3, two state-of-the-art SMT solvers, 469 of which have already been fixed. Compared to two state-of-the-art fuzzers, Falcon detects 38 and 44 more bugs and improves the coverage by a large margin in 24 hours of testing.
DOI 原文 ·
@inproceedings{paperbot6655,
title = {Fuzzing SMT solvers via two-dimensional input space exploration},
author = {Peisen Yao and Heqing Huang and Wensheng Tang and Qingkai Shi and Rongxin Wu and Charles Zhang},
booktitle = {ISSTA},
year = {2021},
doi = {10.1145/3460319.3464803}
}