一句话：提出类型与文法感知的生成式变异策略，用于 SMT 求解器测试，发现 Z3/CVC4 中 158 个 bug。
SMT 求解器是程序分析与验证等安全关键软件的核心组件，其正确性至关重要。自 2009 年以来已有多种面向不同逻辑的模糊测试活动，但现有方法多依赖算子变异或随机生成。本文提出生成式类型感知变异（generative type-aware mutation），它是类型感知算子变异的推广，将变异建立在类型与文法结构之上，以更有效地生成合法且多样的 SMT 公式。作者实现了该策略，并针对 Z3 与 CVC4 开展为期五个月的测试，共报告 158 个 bug，其中包括可追溯到 2016 年早期版本的缺陷。该工作表明类型与文法引导的生成式变异能显著提升 SMT 求解器测试的缺陷发现能力。
Satisfiability Modulo Theories (SMT) solvers are at the core of many software advances such as program analysis and verification which are highly safety-critical. Hence, to ensure the correctness of the solvers, there have been multiple fuzzing campaigns targeting different logics since 2009. In this paper, we propose a generative type-aware mutation strategy, which is a generalization of a type-aware operator mutation. We have realized the generative type-aware mutation and reported 158 bugs in Z3 and CVC4 including bugs from the versions released as early as 2016 in five months.
DOI 原文 ·
@inproceedings{paperbot6378,
title = {SMT solver testing with type and grammar based mutation},
author = {Jiwon Park},
booktitle = {FSE},
year = {2021},
doi = {10.1145/3468264.3473497}
}