Encoding secure information flow with restricted delegation and revocation in Haskell

Distributed applications typically involve many components, each with unique security and privacy requirements. Such applications require fine-grained access control mechanisms that allow dynamic delegation and revocation of access rights. Embedding such domain-specific requirements in a functional language like Haskell puts all the expressiveness of the host language at the disposal of the domain user. Using a custom monad, we design and implement an embedded Haskell library that embraces the decentralized label model, allowing mutually-distrusting principals to express individual confidentiality and integrity policies. Our language includes first-class references, higher-order functions, declassification and endorsement of policies, and user authority in the presence of global unrestricted delegation. Then, building on previous work by the first author, we extend the language to enable fine-grained dynamic delegation and revocation of access rights. The resulting language generalizes, extends, and simplifies various libraries for expressing and reasoning about information flow.