A Calculus for Flow-Limited Authorization
A Calculus for Flow-Limited Authorization
复制标题
DOI：
10.1109/csf.2016.17
复制
发表时间：
2016-06
期刊：
影响因子：
--
通讯作者：
Owen Arden;A. Myers
中科院分区：
文献类型：
--
作者：
Owen Arden;A. Myers
现实世界的应用程序通常根据动态计算做出授权决策。推理动态计算的权限是具有挑战性的。如果攻击者能够不当影响授权计算，系统的完整性可能会受到损害。授权也会损害机密性，因为授权决策通常基于成员列表和密码等敏感数据。以前的正式授权模型没有完全解决允许信任关系更改的安全隐患，这限制了它们推理动态计算所派生的权限的能力。我们的目标是一种构建不违反机密性或完整性的动态授权机制的方法。我们引入了流量限制授权演算（FLAC），它既是用于推理动态授权的简单、富有表现力的模型，也是用于安全地实现各种授权机制的信息流控制语言。 FLAC 结合了之前两个模型的见解：它通过流量限制授权模型实现的功能扩展了依赖核心演算。即使对于合并和实施丰富的动态授权机制的程序，FLAC 也可以提供强大的端到端信息安全保证。这些保证包括不干扰和强大的解密，防止攻击者以未经授权的方式影响信息披露。我们为所有 FLAC 程序正式证明了这些安全属性，并通过几个示例探讨了 FLAC 的表达能力。
Real-world applications routinely make authorization decisions based on dynamic computation. Reasoning about dynamically computed authority is challenging. Integrity of the system might be compromised if attackers can improperly influence the authorizing computation. Confidentiality can also be compromised by authorization, since authorization decisions are often based on sensitive data such as membership lists and passwords. Previous formal models for authorization do not fully address the security implications of permitting trust relationships to change, which limits their ability to reason about authority that derives from dynamic computation. Our goal is a way to construct dynamic authorization mechanisms that do not violate confidentiality or integrity. We introduce the Flow-Limited Authorization Calculus (FLAC), which is both a simple, expressive model for reasoning about dynamic authorization and also an information flow control language for securely implementing various authorization mechanisms. FLAC combines the insights of two previous models: it extends the Dependency Core Calculus with features made possible by the Flow-Limited Authorization Model. FLAC provides strong end-to-end information security guarantees even for programs that incorporate and implement rich dynamic authorization mechanisms. These guarantees include noninterference and robust declassification, which prevent attackers from influencing information disclosures in unauthorized ways. We prove these security properties formally for all FLAC programs and explore the expressiveness of FLAC with several examples.