AURA: a programming language for authorization and audit

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 include fully mechanically verified proofs of the decidability and soundness for AURA's type system, and a prototype typechecker and interpreter. Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory; D.4.6 [Operating Systems]: Security and Protection ? Access controls; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic ? Lambda calculus and related systems General Terms Design, Language, Security Keywords Access control, Authorization logic, Aud...

• Type: Conference
• Year: 2008
• Where: ICFP
• Authors: Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, Steve Zdancewic
• Keywords: Authorization Logic, ICFP 2008, Keywords Access Control, Ordinary Programming Constructs, Programming Languages