Nonmalleable Information Flow Control
Nonmalleable Information Flow Control
复制标题
DOI：
10.1145/3133956.3134054
复制
发表时间：
2017-08
期刊：
影响因子：
--
通讯作者：
Ethan Cecchetti;A. Myers;Owen Arden
中科院分区：
文献类型：
--
作者：
Ethan Cecchetti;A. Myers;Owen Arden
非干预是一种流行的语义安全条件，因为它提供了强大的端到端保证，它本质上是组成的，并且可以使用简单的安全类型系统执行。不幸的是，对于实际系统来说，它太过限制了。需要降低信息的机制来捕获现实世界的安全要求，但降级可以消除非脱位的强大组成安全保证。我们介绍了无易信息流，这是一种新的正式安全状况，概括了非干预以允许控制机密性和完整性的降级。尽管以前关于强大解密的工作阻止了对手利用机密性的降低，但我们的主要见解是透明的认可，这是降级完整性的机制，同时捍卫了对抗性剥削。强大的解密似乎通过使机密性取决于诚信，从而打破了机密性和完整性的双重性，但是透明的认可使完整性取决于机密性，从而恢复了这一双重性。我们展示了如何以透明的认可扩展安全性的编程语言，并证明该静态类型系统会强制执行不可宽图的信息流，这是一种涵盖强大的解密和透明认可的新安全属性。最后，我们描述了这种类型系统在Flame的上下文中的实现，这是Glasgow Haskell编译器的流量限制授权插件。
Noninterference is a popular semantic security condition because it offers strong end-to-end guarantees, it is inherently compositional, and it can be enforced using a simple security type system. Unfortunately, it is too restrictive for real systems. Mechanisms for downgrading information are needed to capture real-world security requirements, but downgrading eliminates the strong compositional security guarantees of noninterference. We introduce nonmalleable information flow, a new formal security condition that generalizes noninterference to permit controlled downgrading of both confidentiality and integrity. While previous work on robust declassification prevents adversaries from exploiting the downgrading of confidentiality, our key insight is transparent endorsement, a mechanism for downgrading integrity while defending against adversarial exploitation. Robust declassification appeared to break the duality of confidentiality and integrity by making confidentiality depend on integrity, but transparent endorsement makes integrity depend on confidentiality, restoring this duality. We show how to extend a security-typed programming language with transparent endorsement and prove that this static type system enforces nonmalleable information flow, a new security property that subsumes robust declassification and transparent endorsement. Finally, we describe an implementation of this type system in the context of Flame, a flow-limited authorization plugin for the Glasgow Haskell Compiler.