Flow-Limited Authorization
Owen Arden

Ph.D. dissertation, Cornell University
January 2017


Enforcing the confidentiality and integrity of information is critical in distributed applications. Production systems typically use some form of authorization mechanism to protect information, but these mechanisms do not typically provide end-to-end information security guarantees. Information flow control mechanisms provide end-to-end security, but their guarantees break down when trust relationships may change dynamically, a common scenario in production environments. This dissertation presents flow-limited authorization, a new foundation for enforcing information security. Flow-limited authorization is an approach to authorization in that it can be used to reason about whether a principal is permitted to perform an action. It is an approach to information flow control in that it can be used to reason about whether a flow of information is secure.

This dissertation presents the theoretical foundation of this approach, the Flow-Limited Authorization Model (FLAM). FLAM uses a novel principal algebra that unifies authority and information flow policies and a logic for making secure authorization and information flow decisions. This logic ensures that such decisions cannot be influenced by attackers or leak confidential information.

We embed the FLAM logic in a core programming model, the Flow-Limited Authorization Calculus (FLAC). FLAC programs selectively enable flows of information; the type system ensures that attackers cannot create unauthorized flows. A well-typed FLAC not only ensures proper authorization, but also secure information flow.

The FLAC approach to secure programming is instantiated in , a library and compiler plugin for enforcing flow-limited authorization in Haskell programs. Flame uses type-level constraints and monadic effects to statically enforce flow-limited authorization for Haskell programs in a modular way.

0 Because information flow control mechanisms often rely on an underlying authorization mechanism, their security guarantees can be subverted by weaknesses in authorization. Conversely, the security of authorization can be subverted by information flows that leak information or that influence how authority is delegated between principals. We argue that interactions between information flow and authorization create security vulnerabilities that have not been fully identified or addressed in prior work. We explore how the security of decentralized information flow control (DIFC) is affected by three aspects of its underlying authorization mechanism: first, delegation of authority between principals; second, revocation of previously delegated authority; third, information flows created by the authorization mechanisms themselves. It is no surprise that revocation poses challenges, but we show that even delegation is problematic because it enables unauthorized downgrading. Our solution is a new security model, the Flow-Limited Authorization Model (FLAM), which offers a new, integrated approach to authorization and information flow control. FLAM ensures robust authorization, a novel security condition for authorization queries that ensures attackers cannot influence authorization decisions or learn confidential trust relationships. We discuss our prototype implementation and its algorithm for proof search.

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. 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 programs and explore the expressiveness of FLAC with several examples.