AURA: a programming language for authorization and audit

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 include fully mechanically verified proofs of the decidability and soundness for AURA's type system, and a prototype typechecker and interpreter.

REFERENCES

• 1: Martín Abadi, Logic in Access Control, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.228, June 22-25, 2003
• 2: Martín Abadi, Access control in a core calculus of dependency, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 3: Martín Abadi, Access Control in a Core Calculus of Dependency, Electronic Notes in Theoretical Computer Science (ENTCS), 172, p.5-31, April, 2007 [doi>10.1016/j.entcs.2007.02.002]
• 4: Martín Abadi , Anindya Banerjee , Nevin Heintze , Jon G. Riecke, A core calculus of dependency, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.147-160, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292555]
• 5: Martín Abadi , Michael Burrows , Butler Lampson , Gordon Plotkin, A calculus for access control in distributed systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.4, p.706-734, Sept. 1993 [doi>10.1145/155183.155225]
• 6: Andrew W. Appel , Edward W. Felten, Proof-carrying authentication, Proceedings of the 6th ACM conference on Computer and communications security, p.52-62, November 01-04, 1999, Kent Ridge Digital Labs, Singapore [doi>10.1145/319709.319718]
• 7: Aslan Askarov, Daniel Hedin, and Andrei Sabelfeld. Cryptographically masked information flows. In Proceedings of the International Static Analysis Symposium, LNCS, Seoul, Korea, August 2006.
• 8: Lennart Augustsson, Cayenne—a language with dependent types, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.239-250, September 26-29, 1998, Baltimore, Maryland, United States
• 9: Brian Aydemir , Arthur Charguéraud , Benjamin C. Pierce , Randy Pollack , Stephanie Weirich, Engineering formal metatheory, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 10: H. P. Barendregt, Lambda calculi with types, Handbook of logic in computer science (vol. 2): background: computational structures, Oxford University Press, Inc., New York, NY, 1993
• 11: Lujo Bauer, Scott Garriss, Jonathan M. McCune, Michael K. Reiter, Jason Rouse, and Peter Rutenbar. Device-enabled authorization in the Grey system. In Information Security: 8th International Conference, ISC 2005, pages 431--445, September 2005.
• 12: Matt Bishop. Computer Security: Art and Science. Addison-Wesley Professional, 2002.
• 13: Matt Blaze , Joan Feigenbaum , Angelos D. Keromytis, KeyNote: Trust Management for Public-Key Infrastructures (Position Paper), Proceedings of the 6th International Workshop on Security Protocols, p.59-63, April 15-17, 1998
• 14: J. G. Cederquist , R. Corin , M. A. C. Dekker , S. Etalle , J. I. den Hartog, An Audit Logic for Accountability, Proceedings of the Sixth IEEE International Workshop on Policies for Distributed Systems and Networks, p.34-43, June 06-08, 2005 [doi>10.1109/POLICY.2005.5]
• 15: Tom Chothia, Dominic Duggan, and Jan Vitek. Type based distributed access control. In Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW'03), Asilomar, Ca., USA, July 2003.
• 16: Yang-Hua Chu , Joan Feigenbaum , Brian LaMacchia , Paul Resnick , Martin Strauss, REFEREE: trust management for Web applications, Computer Networks and ISDN Systems, v.29 n.8-13, p.953-964, Sep. 1997
• 17: The Coq Development Team, LogiCal Project. The Coq Proof Assistant Reference Manual, 2006.
• 18: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• 19: Haskell B. Curry, Robert Feys, and William Craig. Combinatory Logic, volume 1. North-Holland, Amsterdam, 1958.
• 20: Henry DeYoung , Deepak Garg , Frank Pfenning, An Authorization Logic With Explicit Time, Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium, p.133-145, June 23-25, 2008 [doi>10.1109/CSF.2008.15]
• 21: Cedric Fournet, Andrew D. Gordon, and Sergio Maffeis. A type discipline for authorization policies. In Proc. of the 14th European Symposium on Programming, April 2005.
• 22: Cedric Fournet , Andrew Gordon , Sergio Maffeis, A Type Discipline for Authorization in Distributed Systems, Proceedings of the 20th IEEE Computer Security Foundations Symposium, p.31-48, July 06-08, 2007 [doi>10.1109/CSF.2007.7]
• 23: Peter Hancock , Anton Setzer, Interactive Programs in Dependent Type Theory, Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic, p.317-331, August 21-26, 2000
• 24: W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindly, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus, and Formalism, pages 479--490. Academic Press, New York, 1980.
• 25: Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, and Steve Zdancewic. Aura: A programming language for authorization and audit, preliminary technical results. Technical Report MS-CIS-08-10, U. Pennsylvania, 2008.
• 26: Simon Peyton Jones and Erik Meijer. Henk: A typed intermediate language. In Proceedings of the Types in Compilation Workshop, Amsterdam, June 1997.
• 27: Peeter Laud, On the computational soundness of cryptographically masked flows, ACM SIGPLAN Notices, v.43 n.1, January 2008
• 28: Peeter Laud and Varmo Vene. A type system for computationally secure information flow. In Proceedings of the 15th International Symposium on Fundamentals of Computational Theory, volume 3623, pages 365--377, Lübeck, Germany, 2005.
• 29: Daniel K. Lee , Karl Crary , Robert Harper, Towards a mechanized metatheory of standard ML, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 30: Conor McBride. The Epigram Prototype: a nod and two winks, April 2005. Available from http://www.e- pig.org/downloads/epigram-system.pdf.
• 31: Andrew C. Myers, Stephen Chong, Nathaniel Nystrom, Lantian Zheng, and Steve Zdancewic. Jif: Java information flow. 1999.
• 32: Aleksandar Nanevski , Greg Morrisett , Lars Birkedal, Polymorphism and separation in hoare type theory, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 33: Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden, September 2007.
• 34: Simon Peyton Jones , Dimitrios Vytiniotis , Stephanie Weirich , Geoffrey Washburn, Simple unification-based type inference for GADTs, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 35: François Pottier , Vincent Simonet, Information flow inference for ML, ACM Transactions on Programming Languages and Systems (TOPLAS), v.25 n.1, p.117-158, January 2003 [doi>10.1145/596980.596983]
• 36: Geoffrey Smith, Secure information flow with random assignment and encryption, Proceedings of the fourth ACM workshop on Formal methods in security, p.33-44, November 03-03, 2006, Alexandria, Virginia, USA [doi>10.1145/1180337.1180341]
• 37: Martin Sulzmann , Manuel M. T. Chakravarty , Simon Peyton Jones , Kevin Donnelly, System F with type equality coercions, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France [doi>10.1145/1190315.1190324]
• 38: Nikhil Swamy , Brian J. Corcoran , Michael Hicks, Fable: A Language for Enforcing User-defined Security Policies, Proceedings of the 2008 IEEE Symposium on Security and Privacy (sp 2008), p.369-383, May 18-21, 2008 [doi>10.1109/SP.2008.29]
• 39: Don Syme. ILX: Extending the .NET Common IL for functional language interoperability. Electronic Notes in Theoretical Computer Science, 59(1), 2001.
• 40: Jeffrey A. Vaughan , Limin Jia , Karl Mazurak , Steve Zdancewic, Evidence-Based Audit, Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium, p.177-191, June 23-25, 2008 [doi>10.1109/CSF.2008.24]
• 41: Jeffrey A. Vaughan , Steve Zdancewic, A Cryptographic Decentralized Label Model, Proceedings of the 2007 IEEE Symposium on Security and Privacy, p.192-206, May 20-23, 2007 [doi>10.1109/SP.2007.5]
• 42: Philip Wadler, Monads for Functional Programming, Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques-Tutorial Text, p.24-52, May 24-30, 1995
• 43: Philip Wadler and Robert Bruce Findler. Well-typed programs can't be blamed. In Workshop on Scheme and Functional Programming, pages 15--26, 2007.
• 44: Edwin Westbrook , Aaron Stump , Ian Wehrman, A language-based approach to functionally correct imperative programming, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 45: Edward Wobber , Martín Abadi , Michael Burrows , Butler Lampson, Authentication in the Taos operating system, ACM Transactions on Computer Systems (TOCS), v.12 n.1, p.3-32, Feb. 1994 [doi>10.1145/174613.174614]
• 46: Hongwei Xi. Applied Type System (extended abstract). In post-workshop Proceedings of TYPES 2003, pages 394--408. Springer-Verlag LNCS 3085, 2004.
• 47: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Access controls

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Design, Languages, Security

Keywords:
access control, audit, authorization logic, type systems