快速测试非干涉性
编程语言
2016-04-13 v2
摘要
信息流控制机制既难以设计也难以证明其正确性。为了减少因定义错误而在注定失败的证明尝试上浪费的时间，我们主张在设计过程中使用现代随机测试技术来寻找反例。我们展示了如何使用 QuickCheck（一种基于属性的随机测试工具）来指导日益复杂的信息流抽象机的设计，直至构建出一个具有新颖且高度宽松的流敏感动态执行机制的复杂寄存器机，该机制在存在一阶公共标签的情况下是可靠的。我们发现，生成分布良好的随机程序的复杂策略以及易于证伪的非干涉性属性表述，对于高效测试至关重要。我们提出了几种方法，并在一系列注入的不同微妙程度的错误上评估了它们的有效性。我们还提出了一种将大型反例缩减为最小且易于理解的反例的有效技术。综上所述，我们最好的方法使我们能够快速自动地为超过 45 个错误生成简单的反例。此外，我们展示了测试如何指导发现我们最复杂机器的非干涉性证明所需的复杂不变量。
引用
@article{arxiv.1409.0393,
title = {Testing Noninterference, Quickly},
author = {Catalin Hritcu and Leonidas Lampropoulos and Antal Spector-Zabusky and Arthur Azevedo de Amorim and Maxime Dénès and John Hughes and Benjamin C. Pierce and Dimitrios Vytiniotis},
journal= {arXiv preprint arXiv:1409.0393},
year = {2016}
}