中间验证器的鲁棒性测试
软件工程
2018-05-10 v1
摘要
程序验证器也无法免于影响几乎每一段软件的缺陷。此外，它们常常表现出脆弱行为：其性能会随着输入程序表达方式细节的变动而显著变化——这些细节本应无关紧要，例如独立声明的顺序。这种鲁棒性的缺失令用户感到困扰，他们不得不花费大量时间去弄清单工具的特性才能有效使用。本文提出一种检测程序验证器鲁棒性缺失的技术；该技术轻量且完全自动化，因为它基于测试方法（如变异测试和蜕变测试）。其核心思想是生成许多最初通过验证的程序的简单变体。所有变体在构造上均与原程序等价；因此，任何验证失败的变体都表明验证器存在鲁棒性缺失。我们在一款名为“mugie”的工具中实现了该技术，该工具作用于以流行的 Boogie 验证语言编写的程序——Boogie 被用作众多程序验证器的中间表示。针对 135 个 Boogie 程序的实验表明，脆弱行为出现得相当频繁（16 个程序）且不难触发。基于这些结果，本文讨论了脆弱行为的主要来源并提出了提升鲁棒性的手段。
引用
@article{arxiv.1805.03296,
title = {Robustness Testing of Intermediate Verifiers},
author = {Yu-Ting Chen and Carlo A. Furia},
journal= {arXiv preprint arXiv:1805.03296},
year = {2018}
}