[Paper] 无崩溃的演绎验证器

Source: arXiv - 2604.19448v1

概述

演绎式验证器的功能日益强大，已经可以超出原始开发者圈子的使用范围，但它们仍然存在可靠性问题，这些问题可能会吓跑新用户。本文提出了一种轻量且实用的解决方案：对验证器本身进行模糊测试。通过将验证器视为黑盒程序，并向其输入一系列自动生成的、格式错误的或边缘情况的输入，作者展示了如何在这些问题到达终端用户之前，捕捉到崩溃、误导性的错误信息以及其他稳健性问题。

关键贡献

• 用于演绎验证器的模糊测试框架 – 一种具体的方法论，将经典的覆盖引导模糊测试适配到验证工具的特殊性。
• 原型实现（AValAnCHE） – 与 VerCors 验证器集成，展示了只需适度的工程工作即可加入模糊测试。
• 实证评估 – 该原型在 VerCors 中发现了多个错误（包括崩溃、错误诊断以及隐藏的不可靠性），并表明相同的方法同样适用于其他最先进的验证器。
• 面向实践者的指南 – 一套针对验证工具的仪器化、种子生成和模糊测试结果解释的最佳实践。

方法论

1. 输入模型 – 验证器的命令行界面（或 API）被视为模糊测试的入口点。输入包括程序文件、注解文件和配置标志。
2. 仪器化 – 最小包装记录崩溃、超时和异常退出码，无需修改验证器内部。
3. 种子语料库 – 一小批真实的验证任务（例如带有 JML/VerCors 注解的小型 Java/Scala 程序）作为模糊测试的种子。
4. 变异引擎 – 标准的覆盖引导模糊测试器（如 AFL、libFuzzer）被扩展以理解源文件语法，使其能够注入语法噪声、删除注解或扰乱命令行选项。
5. 判定器 – “判定器”很简单：任何验证器崩溃、验证器内部的断言失败，或出现意外的 “verification succeeded/failed” 信息，都将标记为需要人工检查。

该过程全自动化：模糊测试器持续运行，报告崩溃，开发者对发现进行分流。

结果与发现

• 崩溃检测 – AValAnCHE 在为期 48 小时的模糊测试中触发了 VerCors 的 12 起不同的崩溃，其中许多可以通过单行测试用例复现。
• 误导性诊断 – 模糊测试工具暴露了 7 起 VerCors 对正确程序报告验证失败的情况，揭示了在处理某些注解模式时隐藏的不可靠性。
• 跨工具适用性 – 将相同的测试框架应用于 VeriFast 和 KeY 验证器，发现了 另外 3 个 bug（2 起崩溃，1 起错误报告），证实该方法并非针对特定验证器。
• 低开销 – 插桩仅增加了 < 5 % 的运行时开销，且模糊测试只需适度的计算资源（单个现代 CPU 核心）。

这些发现表明，即使是成熟的验证器也可能隐藏关键的鲁棒性问题，而这些问题在其自身的测试套件中是不可见的。

实际影响

• 更高的采用者信心 – 组织可以将模糊测试集成到验证工具的 CI 流水线中，在回归影响开发者之前捕获它们。
• 更好的用户体验 – 通过消除崩溃并改进错误信息，验证器对非验证专家的工程师更友好。
• 加速工具演进 – 及早发现边缘案例错误可减少开发者调试自有验证流水线的时间，使其能够专注于扩展验证器的功能。
• 标准化质量门槛 – 社区可以将模糊测试作为事实上的质量门槛，类似于编译器常规的模糊测试，从而提升验证生态系统的整体可靠性。

限制与未来工作

• 覆盖空白 – 模糊测试仅探索已执行的代码路径；需要特定逻辑输入的深层语义错误可能仍然隐藏。
• 判定器简易性 – 当前的判定器标记任何崩溃或意外结果，但需要更细致的正确性检查（例如，与可信基准进行比较）以实现彻底的可靠性验证。
• 对大型代码库的可扩展性 – 虽然在小型基准程序上效果显著，但将该方法扩展到庞大的工业代码库可能需要更智能的种子策略和领域特定的变异器。
• 工具特定的适配 – 每个验证器都有自己的输入语言和配置细节；未来工作应提供一个可重用的库来抽象这些差异，使模糊测试能够在验证领域即插即用。

作者

• Wander Nauta
• Marcus Gerhold
• Marieke Huisman

论文信息

• arXiv ID: 2604.19448v1
• 分类: cs.SE
• 出版日期: 2026年4月21日
• PDF: 下载 PDF