research-article

AURA: a programming language for authorization and audit

Authors:

Jeffrey A. Vaughan,

Steve ZdancewicAuthors Info & Claims

ICFP '08: Proceedings of the 13th ACM SIGPLAN international conference on Functional programming

Pages 27 - 38

https://doi.org/10.1145/1411204.1411212

Published: 20 September 2008 Publication History

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.

Supplementary Material

JPG File (1411212.jpg)

Download
19.33 KB

index.html (index.html)

Slides from the presentation

Download
.93 KB

ZIP File (p27-slides.zip)

Supplemental material for: AURA: a programming language for authorization and audit

Download
16.88 MB

Audio only (1411212.mp3)

Download
10.24 MB

Video (1411212.mp4)

Download
140.89 MB

References

[1]

Martín Abadi. Logic in access control. In Proceedings of the 18th Annual Symposium on Logic in Computer Science (LICS'03), pages 228--233, June 2003.

Digital Library

[2]

Martín Abadi. Access control in a core calculus of dependency. In Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, Portland, Oregon, USA, September 16-21, 2006, pages 263--273. ACM, 2006.

Digital Library

[3]

Martín Abadi. Access control in a core calculus of dependency. Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin ENTCS, 172:5--31, April 2007.

Digital Library

[4]

Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon Riecke. A core calculus of dependency. In Proc. 26th ACM Symp. on Principles of Programming Languages (POPL), pages 147--160, San Antonio, TX, January 1999.

Digital Library

[5]

Martín Abadi, Michael Burrows, Butler W. Lampson, and Gordon D. Plotkin. A calculus for access control in distributed systems. Transactions on Programming Languages and Systems, 15(4):706--734, September 1993.

Digital Library

[6]

Andrew W. Appel and Edward W. Felten. Proof-carrying authentication. In CCS '99: Proceedings of the 6th ACM conference on Computer and communications security, pages 52--62, New York, NY, USA, 1999. ACM.

Digital Library

[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. In Proc. 3rd ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 239--250, September 1998.

Digital Library

[9]

Brian E. Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering formal metatheory. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, 2008.

Digital Library

[10]

Henk P. Barendregt. Lambda calculi with types. In Samson Abramsky, Dov M. Gabbay, and Thomas S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 117--309. Clarendon Press, Oxford, 1992.

Digital Library

[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.

Digital Library

[12]

Matt Bishop. Computer Security: Art and Science. Addison-Wesley Professional, 2002.

Digital Library

[13]

Matt Blaze, Joan Feigenbaum, and Angelos D. Keromytis. KeyNote: Trust management for public-key infrastructures (position paper). Lecture Notes in Computer Science, 1550:59--63, 1999.

Digital Library

[14]

J.G. Cederquist, R. Corin, M.A.C. Dekker, S. Etalle, and J.I. den Hartog. An audit logic for accountability. In The Proceedings of the 6th IEEE International Workshop on Policies for Distributed Systems and Networks, 2005.

Digital Library

[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, and Martin Strauss. REFEREE: Trust management for web applications. Computer Networks and ISDN Systems, 29:953--964, 1997.

Digital Library

[17]

The Coq Development Team, LogiCal Project. The Coq Proof Assistant Reference Manual, 2006.

[18]

T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76, 1988.

Digital Library

[19]

Haskell B. Curry, Robert Feys, and William Craig. Combinatory Logic, volume 1. North-Holland, Amsterdam, 1958.

[20]

Henry DeYoung, Deepak Garg, and Frank Pfenning. An authorization logic with explicit time. In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF-21), Pittsburgh, June 2008.

Digital Library

[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.

Digital Library

[22]

Cedric Fournet, Andrew D. Gordon, and Sergio Maffeis. A type discipline for authorization in distributed systems. In Proc. of the 20th IEEE Computer Security Foundations Symposium, July 2007.

Digital Library

[23]

Peter Hancock and Anton Setzer. Interactive programs in dependent type theory. In Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic, pages 317--331, London, UK, 2000. Springer-Verlag.

Digital Library

[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. SIGPLAN Not., 43(1):337--348, 2008.

Digital Library

[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.

Digital Library

[29]

Daniel K. Lee, Karl Crary, and Robert Harper. Towards a mechanized metatheory of Standard ML. In POPL '07: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 173--184, 2007.

Digital Library

[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]

A. Nanevski, G. Morrisett, and L. Birkedal. Polymorphism and separation in Hoare Type Theory. In Proc. 11th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2006.

Digital Library

[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, and Geoffrey Washburn. Simple unification-based type inference for GADTs. In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, 2006.

Digital Library

[35]

François Pottier and Vincent Simonet. Information flow inference for ML. ACM Trans. Program. Lang. Syst., 25(1):117--158, 2003.

Digital Library

[36]

Geoffrey Smith and Rafael Alpízar. Secure information flow with random assignment and encryption. In Proceedings of The 4th ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FSME'06), pages 33--43, November 2006.

Digital Library

[37]

Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones, and Kevin Donnelly. System F with type equality coercions. In TLDI '07: Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, pages 53--66, New York, NY, USA, 2007. ACM.

Digital Library

[38]

Nikhil Swamy, Brian J. Corcoran, and Michael Hicks. Fable: A language for enforcing user-defined security policies. In Proceedings of the IEEE Symposium on Security and Privacy (Oakland), May 2008.

Digital Library

[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, and Steve Zdancewic. Evidence-based audit. In Proc. of the IEEE Computer Security Foundations Symposium, 2008. Extended version available as U. Pennsylvania Technical Report MS-CIS-08-09.

Digital Library

[41]

Jeffrey A. Vaughan and Steve Zdancewic. A cryptographic decentralized label model. In IEEE Symposium on Security and Privacy, pages 192--206, Berkeley, California, 2007.

Digital Library

[42]

Philip Wadler. Monads for functional programming. In J. Jeuring and E. Meijer, editors, Advanced Functional Programming, volume 925 of LNCS. Springer Verlag, 1995. Some errata fixed August 2001.

Digital Library

[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]

E. Westbrook, A. Stump, and I. Wehrman. A language-based approach to functionally correct imperative programming. In B. Pierce, editor, 10th ACM SIGPLAN International Conference on Functional Programming, Tallinn, Estonia, 2005.

Digital Library

[45]

Edward Wobber, Martín Abadi, Michael Burrows, and Butler Lampson. Authentication in the Taos operating system. ACM Trans. Comput. Syst., 12(1):3--32, 1994.

Digital Library

[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 and Frank Pfenning. Dependent types in practical programming. In Proc. 26th ACM Symp. on Principles of Programming Languages (POPL), San Antonio, Texas, September 1998.

Digital Library

Cited By

Gollamudi AChong SRanise SCarbone RTakabi D(2023)Expressive Authorization Policies using Computation PrincipalsProceedings of the 28th ACM Symposium on Access Control Models and Technologies10.1145/3589608.3593834(107-119)Online publication date: 24-May-2023
https://dl.acm.org/doi/10.1145/3589608.3593834
Berger BNguempnang RSohr KKoschke R(2020)Static Extraction of Enforced Authorization Policies SeeAuthz2020 IEEE 20th International Working Conference on Source Code Analysis and Manipulation (SCAM)10.1109/SCAM51674.2020.00026(187-197)Online publication date: Sep-2020
https://doi.org/10.1109/SCAM51674.2020.00026
Hirsch AAmorim PCecchetti ETate RArden O(2020)First-Order Logic for Flow-Limited Authorization2020 IEEE 33rd Computer Security Foundations Symposium (CSF)10.1109/CSF49147.2020.00017(123-138)Online publication date: Jun-2020
https://doi.org/10.1109/CSF49147.2020.00017
Show More Cited By

Index Terms

AURA: a programming language for authorization and audit

Recommendations

AURA: a programming language for authorization and audit
ICFP '08

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. ...
Encoding information flow in AURA

Two of the main ways to protect security-sensitive resources in computer systems are to enforce access-control policies and information-flow policies. In this paper, we show how to enforce information-flow policies in AURA, which is a programming ...
Encoding information flow in Aura
PLAS '09: Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security

Two of the main ways to protect security-sensitive resources in computer systems are to enforce access-control policies and information-flow policies. In this paper, we show how to enforce information-flow policies in Aura, which is a programming ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '08: Proceedings of the 13th ACM SIGPLAN international conference on Functional programming

September 2008

422 pages

ISBN:9781595939197

DOI:10.1145/1411204

General Chair:
James Hook
Portland State University, USA
,
Program Chair:
Peter Thiemann
Universität Freiburg, Germany

ACM SIGPLAN Notices Volume 43, Issue 9
ICFP '08
September 2008
399 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1411203
Issue’s Table of Contents

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 September 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP08

Sponsor:

ICFP08: ACM SIGPLAN International Conference on Functional Programming

September 20 - 28, 2008

BC, Victoria, Canada

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

98
Total Citations
View Citations
453
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)4

Reflects downloads up to 14 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Gollamudi AChong SRanise SCarbone RTakabi D(2023)Expressive Authorization Policies using Computation PrincipalsProceedings of the 28th ACM Symposium on Access Control Models and Technologies10.1145/3589608.3593834(107-119)Online publication date: 24-May-2023
https://dl.acm.org/doi/10.1145/3589608.3593834
Berger BNguempnang RSohr KKoschke R(2020)Static Extraction of Enforced Authorization Policies SeeAuthz2020 IEEE 20th International Working Conference on Source Code Analysis and Manipulation (SCAM)10.1109/SCAM51674.2020.00026(187-197)Online publication date: Sep-2020
https://doi.org/10.1109/SCAM51674.2020.00026
Hirsch AAmorim PCecchetti ETate RArden O(2020)First-Order Logic for Flow-Limited Authorization2020 IEEE 33rd Computer Security Foundations Symposium (CSF)10.1109/CSF49147.2020.00017(123-138)Online publication date: Jun-2020
https://doi.org/10.1109/CSF49147.2020.00017
Zhao JOliveira BSchrijvers T(2019)A mechanical formalization of higher-ranked polymorphic type inferenceProceedings of the ACM on Programming Languages10.1145/33417163:ICFP(1-29)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341716
Pédrot PTabareau NFehrmann HTanter É(2019)A reasonably exceptional type theoryProceedings of the ACM on Programming Languages10.1145/33417123:ICFP(1-29)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341712
Lewchenko NRadhakrishna AGaonkar AČerný P(2019)Sequential programming for replicated data storesProceedings of the ACM on Programming Languages10.1145/33417103:ICFP(1-28)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341710
Eremondi JTanter ÉGarcia R(2019)Approximate normalization for gradual dependent typesProceedings of the ACM on Programming Languages10.1145/33416923:ICFP(1-30)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341692
Li PZhang D(2018)A derivation framework for dependent security label inferenceProceedings of the ACM on Programming Languages10.1145/32764852:OOPSLA(1-26)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276485
Ahmed ZAlizai MSyed A(2018)InKeVACM SIGCOMM Computer Communication Review10.1145/3243157.324316146:3(1-6)Online publication date: 27-Jul-2018
https://dl.acm.org/doi/10.1145/3243157.3243161
Ricciotti WCheney J(2018)Explicit AuditingTheoretical Aspects of Computing – ICTAC 201810.1007/978-3-030-02508-3_20(376-395)Online publication date: 15-Oct-2018
https://doi.org/10.1007/978-3-030-02508-3_20
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten