×

Access control in a core calculus of dependency. (English) Zbl 1277.03008

Cardelli, Luca (ed.) et al., Computation, meaning, and logic. Articles dedicated to Gordon Plotkin. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 172, 5-31 (2007).
Summary: The dependency core calculus (DCC) is an extension of the computational lambda calculus that was designed in order to capture the notion of dependency that arises in information-flow control, partial evaluation, and other programming-language settings. We show that, unexpectedly, DCC can also be used as a calculus for access control in distributed systems. Initiating the study of DCC from this perspective, we explore some of its appealing properties.
For the entire collection see [Zbl 1273.68018].

MSC:

03B40 Combinatory logic and lambda calculus
68N18 Functional programming and lambda calculus

Keywords:

authorization; types
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Martín Abadi. Logic in access control. In Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer Science; Martín Abadi. Logic in access control. In Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer Science
[2] Martín Abadi. Access control in a core calculus of dependency. In Proceedings of the 11th ACM International Conference on Functional Programming (ICFP 2006); Martín Abadi. Access control in a core calculus of dependency. In Proceedings of the 11th ACM International Conference on Functional Programming (ICFP 2006) · Zbl 1321.68134
[3] Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. A core calculus of dependency. In Proceedings of the 26th ACM Symposium on Principles of Programming Languages; Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. A core calculus of dependency. In Proceedings of the 26th ACM Symposium on Principles of Programming Languages
[4] Abadi, Martín; Burrows, Michael; Lampson, Butler; Plotkin, Gordon, A calculus for access control in distributed systems, ACM Transactions on Programming Languages and Systems, 15, 4, 706-734 (October 1993)
[5] Andrew W. Appel and Edward W. Felten. Proof-carrying authentication. In Proceedings of the 5th ACM Conference on Computer and Communications Security; Andrew W. Appel and Edward W. Felten. Proof-carrying authentication. In Proceedings of the 5th ACM Conference on Computer and Communications Security
[6] Lujo Bauer, Scott Garriss, and Michael K. Reiter. Distributed proving in access-control systems. In Proceedings of the 2005 IEEE Symposium on Security and Privacy; Lujo Bauer, Scott Garriss, and Michael K. Reiter. Distributed proving in access-control systems. In Proceedings of the 2005 IEEE Symposium on Security and Privacy
[7] Cardelli, Luca, Type systems, (Tucker, Allen B., The Computer Science and Engineering Handbook (1997), CRC Press: CRC Press Boca Raton, FL), 2208-2236, chapter 103
[8] Denning, Dorothy E., Cryptography and Data Security (1982), Addison-Wesley: Addison-Wesley Reading, Mass. · Zbl 0573.68001
[9] John DeTreville. Binder, a logic-based security language. In Proceedings of the 2002 IEEE Symposium on Security and Privacy; John DeTreville. Binder, a logic-based security language. In Proceedings of the 2002 IEEE Symposium on Security and Privacy
[10] Fairtlough, Matt; Mendler, Michael, Propositional lax logic, Information and Computation, 137, 1, 1-33 (1997) · Zbl 0889.03015
[11] Deepak Garg and Frank Pfenning. Non-interference in constructive authorization logic. A revised version of this paper appears in the Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW 19); Deepak Garg and Frank Pfenning. Non-interference in constructive authorization logic. A revised version of this paper appears in the Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW 19)
[12] Gasser, Morrie, Building a Secure Computer System (1988), Van Nostrand Reinhold Company Inc.: Van Nostrand Reinhold Company Inc. New York
[13] Jean-Yves Girard. Interprétation Fonctionnelle et Elimination des Coupures de l’Arithmétique d’Ordre Supérieur; Jean-Yves Girard. Interprétation Fonctionnelle et Elimination des Coupures de l’Arithmétique d’Ordre Supérieur
[14] Hudak, Paul; Jones, Simon Peyton; Wadler, Philip; Boutel, Brian; Fairbairn, Jon; Fasel, Joseph; Guzmán, María M.; Hammond, Kevin; Hughes, John; Johnsson, Thomas; Kieburtz, Dick; Nikhil, Rishiyur; Partain, Will; Peterson, John, Report on the programming language Haskell: a non-strict, purely functional language, ACM SIGPLAN Notices, 27, 5, 1-164 (1992), Version 1.2
[15] Trevor Jim. SD3: A trust management system with certified evaluation. In Proceedings of the 2001 IEEE Symposium on Security and Privacy; Trevor Jim. SD3: A trust management system with certified evaluation. In Proceedings of the 2001 IEEE Symposium on Security and Privacy
[16] Lampson, Butler; Abadi, Martín; Burrows, Michael; Wobberm, Edward, Authentication in distributed systems: Theory and practice, ACM Transactions on Computer Systems, 10, 4, 265-310 (November 1992)
[17] Lampson, Butler W., Computer security in the real world, IEEE Computer, 37, 6, 37-46 (June 2004)
[18] David Langworthy. Private communication. February 2006; David Langworthy. Private communication. February 2006
[19] Li, Ninghui; Grosof, Benjamin N.; Feigenbaum, Delegation logic: A logic-based approach to distributed authorization, ACM Transactions on Information and System Security, 6, 1, 128-171 (February 2003)
[20] Li, Ninghui; Mitchell, John C., Datalog with constraints: A foundation for trust-management languages, (Proceedings of the Fifth International Symposium on Practical Aspects of Declarative Languages. Proceedings of the Fifth International Symposium on Practical Aspects of Declarative Languages, (PADL 2003). Proceedings of the Fifth International Symposium on Practical Aspects of Declarative Languages. Proceedings of the Fifth International Symposium on Practical Aspects of Declarative Languages, (PADL 2003), Lecture Notes in Computer Science, volume 2562 (January 2003), Springer-Verlag), 58-73 · Zbl 1026.68793
[21] Mitchell, John C., Foundations for Programming Languages (1996), The MIT Press: The MIT Press Cambridge, Mass.
[22] Moggi, Eugenio, Notions of computation and monads, Information and Control, 93, 1, 55-92 (1991) · Zbl 0723.68073
[23] Andrew C. Myers. JFlow: Practical mostly-static information flow control. In Proceedings of the 26th ACM Symposium on Principles of Programming Languages; Andrew C. Myers. JFlow: Practical mostly-static information flow control. In Proceedings of the 26th ACM Symposium on Principles of Programming Languages
[24] Plotkin, Gordon D., Call-by-name, call-by-value and the \(λ\)-calculus, Theoretical Computer Science, 1, 125-159 (1975) · Zbl 0325.68006
[25] François Pottier and Sylvain Conchon. Information flow inference for free. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming; François Pottier and Sylvain Conchon. Information flow inference for free. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming · Zbl 1321.68158
[26] Pottier, François; Simonet, Vincent, Information flow inference for ML, ACM Transactions on Programming Languages and Systems, 25, 1, 117-158 (January 2003)
[27] Stephen Tse and Steve Zdancewic. Translating dependency into parametricity. Journal of Functional Programming; Stephen Tse and Steve Zdancewic. Translating dependency into parametricity. Journal of Functional Programming · Zbl 1323.68168
[28] Philip Wadler. The marriage of effects and monads. In Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming; Philip Wadler. The marriage of effects and monads. In Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming · Zbl 1370.68050
[29] Wallach, Dan S.; Appel, Andrew W.; Felten, Edward W., Safkasi: A security mechanism for language-based systems, ACM Transactions on Software Engineering and Methodology, 9, 4, 341-378 (2000)
[30] Wobber, Edward; Abadi, Martín; Burrows, Michael; Lampson, Butler, Authentication in the Taos operating system, ACM Transactions on Computer Systems, 12, 1, 3-32 (February 1994)
[31] Steve Zdancewic. Private communication. August 2006; Steve Zdancewic. Private communication. August 2006
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.