Submitted to ICFP 2010 Security-Typed Programming within Dependently-Typed Programming

Several recent security-typed programming languages, such as Aura, PCML5, and Fine, allow programmers to express and en-force access control and information flow policies. Most of these security-typed languages 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 depen-dently typed programming language, Agda. This language design strategy allows us to inherit both the metatheoretic properties, such as type safety, and the implementation of the host language. Our embedded language accounts for the major features of these ex-isting security-typed programming languages, including decentral-ized access control, stateful and dynamic policies, spatially dis-tributed and principaled computation, and information flow. Our embedding consists of the following ingredients: we represent the syntax and proofs of an authorization logic, Garg and Pfenning’s BL0, using dependent types, and implement a proof search proce-dure, based on a focused sequent calculus, to ease the burden of constructing proofs. Additionally, we represent computations as a monad indexed by pre- and post-conditions drawn from the autho-rization logic, which permits stateful policies that change during execution. Our work shows that a dependently typed language can be used to prototype a security-typed language with all of these features. 1