一句话：提出 HistFuzz，从历史缺陷触发公式提取骨架并用关联规则枚举原子公式，以模糊测试 SMT 求解器并发现大量新缺陷。
SMT 求解器广泛应用于软件验证、测试生成和程序合成等关键任务，其内部缺陷会严重误导下游应用，因此保障可靠性至关重要，但已有测试方法仍难高效发现缺陷。本文对 SMT 求解器缺陷跟踪系统中的历史触发缺陷公式进行实证研究，发现其中包含有价值的骨架（公式核心结构）以及显著影响触发缺陷能力的原子公式。基于此，作者提出提取历史触发公式的骨架，并在由历史公式导出的关联规则指导下枚举原子公式，实现模糊测试工具 HistFuzz。在 Z3 和 cvc5 上的广泛测试表明，HistFuzz 已发现 111 个确认的新缺陷，其中 108 个已被修复；23 个为默认模式下发现的 soundness bug 和 invalid model bug。实验还显示其在代码覆盖率和有效性上优于当前最优的 SMT 求解器模糊测试工具。
SMT solvers check the satisfiability of logic formulas over first-order theories, which have been utilized in a rich number of critical applications, such as software verification, test case generation, and program synthesis. Bugs hidden in SMT solvers would severely mislead those applications and further cause severe consequences. Therefore, ensuring the reliability and robustness of SMT solvers is of critical importance. Although many approaches have been proposed to test SMT solvers, it is still a challenge to discover bugs effectively. To tackle such a challenge, we conduct an empirical study on the historical bug-triggering formulas in SMT solvers' bug tracking systems. We observe that the historical bug-triggering formulas contain valuable skeletons (i.e., core structures of formulas) as well as associated atomic formulas which can cast significant impacts on formulas' ability in triggering bugs. Therefore, we propose a novel approach that utilizes the skeletons extracted from the historical bug-triggering formulas and enumerates atomic formulas under the guidance of association rules derived from historical formulas. In this study, we realized our approach as a practical fuzzing tool HistFuzz and conducted extensive testing on the well-known SMT solvers Z3 and cvc5. To date, HistFuzz has found 111 confirmed new bugs for Z3 and cvc5, of which 108 have been fixed by the developers. More notably, out of the confirmed bugs, 23 are soundness bugs and invalid model bugs found in the solvers' default mode, which are essential for SMT solvers. In addition, our experiments also demonstrate that HistFuzz outperforms the state-of-the-art SMT solver fuzzers in terms of achieved code coverage and effectiveness.
@inproceedings{SunYWWZJ23,
title = {Validating SMT Solvers via Skeleton Enumeration Empowered by Historical Bug-Triggering Inputs},
author = {Maolin Sun and Yibiao Yang and Ming Wen and Yongcong Wang and Yuming Zhou and Hai Jin},
booktitle = {ICSE},
year = {2023},
doi = {10.1109/icse48619.2023.00018}
}