多态松弛非干涉
Polymorphic Relaxed Noninterference
摘要：
信息流安全类型通过强制不干扰静态地保持机密性。为了解决选择性和灵活的解密机密信息的实际需要，几种方法已经开发了一种宽松的不干涉的概念，其中安全标签是函数或类型。标签作为类型的方法宽松的不干涉支持表达解密政策，包括递归的，通过一个简单的基于子类型的排序，并提供了一个本地的，模块化的推理原则。在这项工作中，我们扩展了这种表达解密方法，以支持多态解密。首先，我们通过具体的例子确定有界多态性的需要。然后，我们形式化多态放松不干涉类型面向对象的演算，使用一个步骤索引的逻辑关系，证明所有类型良好的条款是安全的。最后，我们解决了原始类型的情况，这需要一种特殊的多态性。因此，这项工作解决了实际的障碍，提供控制和表达解密的信息流安全系统的建设。
英文摘要：
Information-flow security typing statically preserves confidentiality by enforcing noninterference. To address the practical need of selective and flexible declassification of confidential information, several approaches have developed a notion of relaxed noninterference, where security labels are either functions or types. The labels-as-types approach to relaxed noninterference supports expressive declassification policies, including recursive ones, via a simple subtyping-based ordering, and provides a local, modular reasoning principle. In this work, we extend this expressive declassification approach in order to support polymorphic declassification. First, we identify the need for bounded polymorphism through concrete examples. We then formalize polymorphic relaxed noninterference in a typed object-oriented calculus, using a step-indexed logical relation to prove that all well-typed terms are secure. Finally, we address the case of primitive types, which requires a form of ad-hoc polymorphism. Therefore, this work addresses practical hurdles to providing controlled and expressive declassification for the construction of information-flow secure systems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
