AURA

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.

This software is also peer reviewed by journal TOMS.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 7 articles , 1 standard article )

Showing results 1 to 7 of 7.
Sorted by year (citations)

  1. Lepigre, Rodolphe: A classical realizability model for a semantical value restriction (2016)
  2. Casinghino, Chris; Sjöberg, Vilhelm; Weirich, Stephanie: Combining proofs and programs in a dependently typed language (2014)
  3. Amir-Mohammadian, Sepehr; Fallah, Mehran S.: Noninterference in a predicative polymorphic calculus for access control (2013)
  4. Charguéraud, Arthur: The locally nameless representation (2012)
  5. Morgenstern, Jamie; Licata, Daniel R.: Security-typed programming within dependently typed programming (2010)
  6. Abadi, Martín: Logic in access control (tutorial notes) (2009)
  7. Jia, Limin; Vaughan, Jeffrey A.; Mazurak, Karl; Zhao, Jianzhou; Zarko, Luke; Schorr, Joseph; Zdancewic, Steve: AURA: a programming language for authorization and audit (2008)