We consider the problem of specifying and proving the security of non-trivial, concurrent programs that intentionally leak information. We present a method that decomposes the problem into (a) proving that the program only leaks information it has declassified via assume annotations already widely used in deductive program verification; and (b) auditing the declassifications against a declarative security policy. We show how condition (a) can be enforced by an extension of the existing program logic SecCSL, and how (b) can be checked by proving a set of simple entailments. Part of the challenge is to define respective semantic soundness criteria and to formally connect these to the logic rules and policy audit. We support our methodology in an auto-active program verifier, which we apply to verify the implementations of various case study programs against a range of declassification policies.

翻译：我们研究了在非平凡并发程序中规范并证明其故意泄露信息的安全性问题。提出了一种方法，将问题分解为：(a) 通过已在形式化验证中广泛使用的假设标注，证明程序仅泄露了经过去分类的信息；(b) 根据声明式安全策略审核去分类操作。我们展示了如何通过扩展现有程序逻辑SecCSL来保证条件(a)，以及如何通过证明一组简单蕴含关系来实施条件(b)。部分挑战在于定义相应的语义可靠性准则，并将其与逻辑规则和安全策略审核建立形式化关联。我们在一款自动主动程序验证器中实现了该方法，并通过多款案例研究程序对一系列去分类策略的实现进行了验证。