Sciweavers

ICFP
2010
ACM

Security-typed programming within dependently typed programming

13 years 4 months ago
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...
Jamie Morgenstern, Daniel R. Licata
Added 09 Nov 2010
Updated 09 Nov 2010
Type Conference
Year 2010
Where ICFP
Authors Jamie Morgenstern, Daniel R. Licata
Comments (0)