Programming with Flow-Limited Authorization: Coarser is Better

Applications that handle sensitive information need to express and reason about the trust relationships between security principals. Such reasoning is difficult because the trust relationships are dynamic, and must thus be reasoned about at runtime when discovering and reasoning about trust relationships might inadvertently reveal confidential information and be subject to manipulation by untrusted principals. The Flow-Limited Authorization Model (FLAM) by Arden et al. exactly meets these needs. However, previous attempts to use FLAM in a programming language have not reaped the full benefits of the model. We present Flamio, an instantiation of FLAM in a language with coarse-grained dynamic information-flow control (IFC) which naturally lends itself to dynamic enforcement techniques. In our implementation of Flamio, the FLAM proof search rules for deriving trust relationships are implemented as regular Flamio computations: the IFC requirements for FLAM proof rules are a natural fit with coarse-grained information-flow mechanisms. Flamio even supports remote procedure calls, and thus seamlessly supports FLAM's distributed proof search. We have implemented Flamio as a Haskell library, and proved that a calculus based on Flamio enforces a noninterference-based security guarantee. We have implemented several case studies, demonstrating the expressiveness and usefulness of Flamio in distributed settings, as well as our novel approach to control label creep during proof search.