VERONICA：富有表达力且精确并发信息流安全（含技术附录的扩展版）
计算机科学中的逻辑
2020-01-31 v1
摘要
证明并发软件不泄露其秘密的方法在过去至少四十年中一直是活跃的研究课题。尽管已有大量工作，现状仍高度不尽如人意。当代的组合证明方法迫使人们在表达力（对广泛安全策略进行推理的能力）与精确性（对复杂线程交互与程序行为进行推理的能力）之间做出选择。二者兼得至关重要，且我们认为这需要一种新型的组合推理风格。我们提出 VERONICA，这是首个用于证明并发程序信息流安全的程序逻辑，支持对广泛安全策略与程序行为（例如富有表达力的去密、值依赖分类、秘密依赖分支）进行组合式、高精度的推理。同样重要的是，VERONICA 体现了一类可复用于他处的工程化此类逻辑的新方法，称为解耦功能正确性(DFC)。DFC 带来了简洁清晰的逻辑，同时实现了这一前所未有的特性组合。我们通过验证一系列超越既有方法能力的示例程序，展示了 VERONICA 的优点与通用性。
引用
@article{arxiv.2001.11142,
title = {VERONICA: Expressive and Precise Concurrent Information Flow Security (Extended Version with Technical Appendices)},
author = {Daniel Schoepe and Toby Murray and Andrei Sabelfeld},
journal= {arXiv preprint arXiv:2001.11142},
year = {2020}
}