Aura: A programming language for authorization and audit

Limin Jia, Jeffrey Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr and Steve Zdancewic

The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP 2008)
Victoria, British Columbia, Canada, September 22-24, 2008

---

Abstract

This paper presents AURA, a programming language for access control that treats ordinary programming constructs (e.g., integers and recursive functions)

and authorization logic constructs (e.g., principals and access control policies) in a uniform way. AURA is based on polymorphic DCC and uses dependent types to permit assertions that refer directly to AURA values while keeping computation out of the assertion level to ensure tractability. The main technical results of this paper paper include a proof of decidability for AURA's type system, a fully mechanically verified proof of soundness, and a prototype typechecker and interpreter.

---

START Conference Manager (V2.54.6)