Kumar Avijit
Robert Harper
ABSTRACT
We propose a programming language, called PCML5, for building distributed applications with distributed access control. Target applications include web-based systems in which programs must compute with stipulated resources at different sites. In such a setting, access control policies are decentralized (each site may impose restrictions on access to its resources without the knowledge of or cooperation with other sites) and spatially distributed each site may store its policies locally). To enforce such policies PCML5 employs a distributed proof-carrying authorization framework in which sensitive resources are governed by reference monitors that authenticate principals and demand logical proofs of compliance with site-specific access control policies. The language provides primitive operations for authentication, and acquisition of proofs from local policies. The type system of PCML5 enforces locality restrictions on resources, ensuring that they can only be accessed from the site at which they reside, and enforces the authentication and authorization obligations required to comply with local access control policies. This ensures that a well-typed PCML5 program cannot incur a runtime access control violation at a reference monitor for a controlled resource.
- Martín Abadi. Access control in a core calculus of dependency. In ICFP, pages 263--273, 2006. Google Scholar
Digital Library
- Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. A core calculus of dependency. In Proceedings 26th ACM Symp. on Principles of Programming Languages (POPL), pages 147--160, 1999. Google ScholarDigital Library
- 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, 1999. Google ScholarDigital Library
- Kumar Avijit, Anupam Datta, and Robert Harper. Distributed programming with distributed authorization, 2009. Available at http://www.cs.cmu.edu/kavijit/papers/pcml5-full.pdf.Google Scholar
- Lujo Bauer, Michael A. Schneider, and Edward W. Felten. A proof-carrying authorization system. Technical Report TR-638-01, Princeton University, April 2001. URL http://www.ece.cmu.edu/lbauer/papers/pcaprototr.pdf.Google Scholar
- Lujo Bauer, Scott Garriss, Jonathan M. Mccune, Michael K. Reiter, Jason Rouse, and Peter Rutenbar. Device-enabled authorization in the grey system. In Proceedings of the 8th Information Security Conference (ISC'05, pages 431--445, 2005. Google ScholarDigital Library
- Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, and Sergio Maffeis. Refinement types for secure implementations. In Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium, pages 17--32, 2008. Google ScholarDigital Library
- M. Blaze, J. Feigenbaum, and J. Lacy. Decentralized trust management. In Proceedings of the IEEE Symposium on Security and Privacy, pages 164--173, May 1996. Google ScholarDigital Library
- Avik Chaudhuri and Deepak Garg. PCAL: Language support for proof-carrying authorization systems. In Proceedings of the European Symposium on Research in Computer Security, pages 184--199, 2009. Google ScholarDigital Library
- Dwaine E. Clarke, Jean-Emile Elien, Carl M. Ellison, Matt Fredette, Alexander Morcos, and Ronald L. Rivest. Certificate chain discovery in SPKI/SDSI. Journal of Computer Security, 9 (4): 285--322, 2001. Google ScholarDigital Library
- Cedric Fournet, Andrew Gordon, and Sergio Maffeis. A type discipline for authorization in distributed systems. In CSF '07: Proceedings of the 20th IEEE Computer Security Foundations Symposium, pages 31--48, 2007. Google ScholarDigital Library
- Deepak Garg. Proof Theory for Authorization Logic and its Application to a Practical File System. PhD thesis, School of Computer Science, Carnegie Mellon University, 2009. Available as Technical Report CMU-CS-09-123.Google Scholar
- Deepak Garg and Frank Pfenning. Non-interference in constructive authorization logic. In Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW 19), pages 283--296, 2006. Google ScholarDigital Library
- Robert Harper and Daniel R. Licata. Mechanizing metatheory in a logical framework. Journal of Functional Programming, 17 (4--5): 613--673, July 2007. Google ScholarDigital Library
- Robert Harper, John C. Mitchell, and Eugenio Moggi. Higher-order modules and the phase distinction. In POPL '90: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 341--354, 1990. Google ScholarDigital Library
- Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40 (1): 143--184, 1993. Google ScholarDigital Library
- Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, and Steve Zdancewic. Aura: a programming language for authorization and audit. In ICFP '08: Proceeding of the 13th ACM SIGPLAN International Conference on Functional programming, pages 27--38, 2008. Google ScholarDigital Library
- Neel Krishnaswami and Jonathan Aldrich. Permission-based ownership: encapsulating state in higher-order typed languages. SIGPLAN Notices, 40 (6): 96--106, 2005. Google ScholarDigital Library
- Butler W. Lampson, Martín Abadi, Michael Burrows, and Edward Wobber. Authentication in distributed systems: Theory and practice. ACM Transactions on Computer Systems, 10 (4): 265--310, 1992. Google ScholarDigital Library
- Ninghui Li, John C. Mitchell, and William H. Winsborough. Design of a role-based trust-management framework. In Proceedings of the 2002 IEEE Symposium on Security and Privacy, pages 114--130, 2002. Google ScholarDigital Library
- Tom Murphy, VII. Modal Types for Mobile Code. PhD thesis, Carnegie Mellon, January 2008. Available as technical report CMU-CS-08-126. Google ScholarDigital Library
- Tom Murphy, VII, Karl Crary, Robert Harper, and Frank Pfenning. A symmetric modal lambda calculus for distributed computing. In Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), pages 286--295,, 2004. Google ScholarDigital Library
- Tom Murphy, VII, Karl Crary, and Robert Harper. Type-safe distributed programming with ML5. In Trustworthy Global Computing 2007, November 2007. Google ScholarDigital Library
- B. C. Neuman and T. Ts'o. Kerberos: An authentication service for computer networks. Communications Magazine, IEEE, 32 (9): 33--38, 1994.Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Jeffrey A. Vaughan, Limin Jia, Karl Mazurak, and Steve Zdancewic. Evidence-based audit. In CSF '08: Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium, pages 177--191, 2008. Google ScholarDigital Library
- Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework I: Judgments and properties. Technical Report CMU-CS-02-101, Carnegie Mellon University, School of Computer Science, 2002.Google Scholar
- Edward Wobber, Martín Abadi, Michael Burrows, and Butler Lampson. Authentication in the taos operating system. ACM Transactions on Computer Systems, 12: 256--269, 1994. Google ScholarDigital Library
Index Terms
- Distributed programming with distributed authorization
Recommendations
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 ...
Flow-Limited Authorization
CSF '15: Proceedings of the 2015 IEEE 28th Computer Security Foundations SymposiumBecause information flow control mechanisms often rely on an underlying authorization mechanism, their security guarantees can be subverted by weaknesses in authorization. Conversely, the security of authorization can be subverted by information flows ...
Nexus authorization logic (NAL): Design rationale and applications
Nexus Authorization Logic (NAL) provides a principled basis for specifying and reasoning about credentials and authorization policies. It extends prior access control logics that are based on “says” and “speaks for” operators. NAL enables authorization ...
Comments