Security-typed programming within dependently typed programming

Abstract

Abstract. Several recent security-typed programming languages allow programmers to express and enforce authorization policies governing access to controlled resources. Policies are expressed as propositions in an authorization logic, and enforced by a type system that requires each access to a sensitive resource to be accompanied by a proof. The securitytyped languages described in the literature, such as Aura and PCML5, have been presented as new, stand-alone language designs. In this paper, we instead show how to embed a security-typed programming language within an existing dependently typed programming language, Agda. This language-design strategy allows us to inherit both the metatheoretic results, such as type safety, and the implementation of the host language. Our embedding consists of the following ingredients: First, we represent the syntax and proofs of an authorization logic, Garg and Pfenning’s BL0, using dependent types. Second, we implement a proof search procedure, based on a focused sequent calculus, to ease the burden of constructing proofs. Third, we define an indexed monad of computations on behalf of a principal, with proof-carrying primitive operations. Our work shows that a dependently typed language can be used to prototype a security-typed language, and contributes to the growing body of literature on using dependently typed languages to construct domain-specific type systems. 1