VERONICA：可表达和精确的并发信息流安全（扩展版及技术附录）
VERONICA: Expressive and Precise Concurrent Information Flow Security (Extended Version with Technical Appendices)
摘要：
证明并发软件不会泄露其秘密的方法至少在过去的四十年里一直是一个活跃的研究课题。尽管开展了一系列令人印象深刻的工作，但目前的情况仍然非常不令人满意。使用当代的组合证明方法，人们被迫在表达性（推理各种安全策略的能力）和精确性（推理复杂线程交互和程序行为的能力）之间做出选择。实现这两个是必不可少的，我们认为，需要一种新的风格的组合推理。我们提出了VERONICA，第一个程序逻辑证明并发程序信息流安全，支持组合，高精度的推理范围广泛的安全策略和程序行为（例如，表达去分类，值相关的分类，秘密相关的分支）。同样重要的是，VERONICA体现了一种新的方法，用于工程这样的逻辑，可以在其他地方重用，称为解耦功能正确性（DFC）。DFC导致了一个简单而清晰的逻辑，即使在实现这种前所未有的功能组合的同时。我们证明了VERONICA的优点和多功能性，通过验证一系列的例子程序，超出了以前的方法。
英文摘要：
Methods for proving that concurrent software does not leak its secrets has remained an active topic of research for at least the past four decades. Despite an impressive array of work, the present situation remains highly unsatisfactory. With contemporary compositional proof methods one is forced to choose between expressiveness (the ability to reason about a wide variety of security policies), on the one hand, and precision (the ability to reason about complex thread interactions and program behaviours), on the other. Achieving both is essential and, we argue, requires a new style of compositional reasoning. We present VERONICA, the first program logic for proving concurrent programs information flow secure that supports compositional, high-precision reasoning about a wide range of security policies and program behaviours (e.g. expressive de-classification, value-dependent classification, secret-dependent branching). Just as importantly, VERONICA embodies a new approach for engineering such logics that can be re-used elsewhere, called decoupled functional correctness (DFC). DFC leads to a simple and clean logic, even while achieving this unprecedented combination of features. We demonstrate the virtues and versatility of VERONICA by verifying a range of example programs, beyond the reach of prior methods.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
