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.
This software is also peer reviewed by journal TOMS.
Keywords for this software
References in zbMATH (referenced in 10 articles , 1 standard article )
Showing results 1 to 10 of 10.
Sorted by year (- Lepigre, Rodolphe: A classical realizability model for a semantical value restriction (2016)
- Casinghino, Chris; Sjöberg, Vilhelm; Weirich, Stephanie: Combining proofs and programs in a dependently typed language (2014)
- Amir-Mohammadian, Sepehr; Fallah, Mehran S.: Noninterference in a predicative polymorphic calculus for access control (2013)
- Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean: Secure distributed programming with value-dependent types (2013)
- Backes, Michael; Maffei, Matteo; Pecina, Kim; Reischuk, Raphael M.: G2C: cryptographic protocols from goal-driven specifications (2012)
- Charguéraud, Arthur: The locally nameless representation (2012)
- Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean: Secure distributed programming with value-dependent types (2011)
- Morgenstern, Jamie; Licata, Daniel R.: Security-typed programming within dependently typed programming (2010)
- Abadi, Martín: Logic in access control (tutorial notes) (2009)
- Jia, Limin; Vaughan, Jeffrey A.; Mazurak, Karl; Zhao, Jianzhou; Zarko, Luke; Schorr, Joseph; Zdancewic, Steve: AURA: a programming language for authorization and audit (2008)