一句话：提出 MCFuzz 模糊测试技术，通过合成分支可达性性质自动发现软件模型检查器中的 62 个真实缺陷。
软件模型检查（SMC）是验证安全攸关软件的重要自动程序验证技术，因此模型检查器自身的可靠性至关重要，但此前少有工作对其进行验证。本文提出一种实用、自动化的模糊测试技术，聚焦控制流可达性（如某分支是否或多少次被到达），并针对有效 fuzzing 的两个关键挑战——测试预言（oracle）与可扩展性——给出解决方案：对确定性程序，利用其具体执行合成合法且有效的分支可达性性质，从而解决 oracle 问题；再将这些单独性质融合为单一安全性质，以提升 fuzzing 的可扩展性并减少人工检查负担。作者实现了工具 MCFuzz，并对三个主流 C 软件模型检查器 CPAchecker、CBMC 和 SeaHorn 进行了广泛测试，共发现 62 个独特缺陷，其中 58 个已被确认、20 个已被修复。论文进一步分析并分类了这些多样化的缺陷，总结了构建可靠鲁棒模型检查器的若干经验，测试工作也获得开发者认可，并促进了工具可用性与文档的改进。
Software Model Checking (SMC) is a well-known automatic program verification technique and frequently adopted for checking safety-critical software. Thus, the reliability of SMC tools themselves (i.e., software model checkers) is critical. However, little work exists on validating software model checkers, an important problem that this paper tackles by introducing a practical, automated fuzzing technique. For its simplicity and generality, we focus on control-flow reachability (e.g., whether or how many times a branch is reached) and address two specific challenges for effective fuzzing: oracle and scalability. Given a deterministic program, we (1) leverage its concrete executions to synthesize valid branch reachability properties (thus solving the oracle problem) and (2) fuse such individual properties into a single safety property (thus improving the scalability of fuzzing and reducing manual inspection). We have realized our approach as the MCFuzz tool and applied it to extensively test three state-of-the-art C software model checkers, CPAchecker, CBMC, and SeaHorn. MCFuzz has found 62 unique bugs in all three model checkers -- 58 have been confirmed, and 20 have been fixed. We have further analyzed and categorized these bugs (which are diverse), and summarized several lessons for building reliable and robust model checkers. Our testing effort has been well-appreciated by the model checker developers, and also led to improved tool usability and documentation.
DOI 原文 ·
@inproceedings{paperbot5143,
title = {Finding and understanding bugs in software model checkers},
author = {Chengyu Zhang and Ting Su and Yichen Yan and Fuyuan Zhang and Geguang Pu and Zhendong Su},
booktitle = {FSE},
year = {2019},
doi = {10.1145/3338906.3338932}
}