AURA: a programming language for authorization and audit. (English) Zbl 1323.68078
Proceedings of the 13th ACM SIGPLAN international conference on functional programming, ICFP ’08, Victoria, BC, Canada, September 20–28, 2008. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-59593-919-7). ACM SIGPLAN Notices 43, No. 9, 27-38 (2008).
MSC:
| 68N15 | Theory of programming languages |
| 68N18 | Functional programming and lambda calculus |
| 68Q55 | Semantics in the theory of computing |
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. |
| [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. 10.1145/1159803.1159839 · Zbl 1321.68134 |
| [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. 10.1016/j.entcs.2007.02.002 · Zbl 1277.03008 |
| [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. 10.1145/292540.292555 |
| [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. 10.1145/155183.155225 |
| [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. 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. In Proc. 3rd ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 239-250, September 1998. 10.1145/289423.289451 · Zbl 1428.68094 |
| [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. 10.1145/1328438.1328443 · Zbl 1295.68052 |
| [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. |
| [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. 10.1007/11556992_31 · Zbl 1159.68431 |
| [12] | Matt Bishop. Computer Security: Art and Science. Addison-Wesley Professional, 2002. |
| [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. |
| [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. 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, and Martin Strauss. REFEREE: Trust management for web applications. Computer Networks and ISDN Systems, 29:953-964, 1997. 10.1016/S0169-7552(97)00009-3 |
| [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. 10.1016/0890-5401(88)90005-3 · Zbl 0654.03045 |
| [19] | Haskell B. Curry, Robert Feys, and William Craig. Combinatory Logic, volume 1. North-Holland, Amsterdam, 1958. · Zbl 0081.24104 |
| [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. 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. 10.1007/978-3-540-31987-0_11 |
| [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. 10.1109/CSF.2007.7 |
| [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. · Zbl 0973.68041 |
| [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. 10.1145/1328897.1328479 · Zbl 1295.68152 |
| [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. 10.1007/11537311_32 · Zbl 1123.68034 |
| [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. 10.1145/1190216.1190245 · Zbl 1295.68088 |
| [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. 10.1145/1159803.1159812 · Zbl 1321.68351 |
| [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. 10.1145/1159803.1159811 |
| [35] | François Pottier and Vincent Simonet. Information flow inference for ML. ACM Trans. Program. Lang. Syst., 25(1):117-158, 2003. 10.1145/596980.596983 |
| [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. 10.1145/1180337.1180341 |
| [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. 10.1145/1190315.1190324 |
| [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. 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, 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. 10.1109/CSF.2008.24 |
| [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. 10.1109/SP.2007.5 |
| [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. |
| [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. 10.1145/1086365.1086400 · Zbl 1302.68095 |
| [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. 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. · Zbl 1100.03518 |
| [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. 10.1145/292540.292560 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
