Security-typed programming within dependently typed programming

Several recent security-typed programming languages, such as Aura, PCML5, and Fine, allow programmers to express and enforce 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 dependently 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 existing security-typed programming languages, including decentralized access control, stateful and dynamic policies, spatially distributed 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 implem...

• Type: Conference
• Year: 2010
• Where: ICFP
• Authors: Jamie Morgenstern, Daniel R. Licata
• Keywords: ICFP 2010, Language Design, Programming Languages, Security-typed Programming Languages, Stand-alone Language Designs