Abstract
By shifting the burden of proofs to the user, a proof-carrying authorization (PCA) system can automatically enforce complex access control policies. Unfortunately, managing those proofs can be a daunting task for the user. In this paper we develop a Bash-like language, PCAL, that can automate correct and efficient use of a PCA interface. Given a PCAL script, the PCAL compiler tries to statically construct the proofs required for executing the commands in the script, while re-using proofs to the extent possible and rewriting the script to construct the remaining proofs dynamically. We obtain a formal guarantee that if the policy does not change between compile time and run time, then the compiled script cannot fail due to access checks at run time.
Chapter PDF
References
Abadi, M.: Access control in a core calculus of dependency. Electronic Notes in Theoretical Computer Science 172, 5–31 (2007); Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin
Abadi, M., Burrows, M., Lampson, B., Plotkin, G.: A calculus for access control in distributed systems. ACM Transactions on Programming Languages and Systems 15(4), 706–734 (1993)
Appel, A.W., Felten, E.W.: Proof-carrying authentication. In: ACM Conference on Computer and Communications Security (CCS 2009), pp. 52–62. ACM Press, New York (1999)
Avijit, K., Datta, A., Harper, R.: PCML5: A language for ensuring compliance with access control policies (2009); Draft, personal communication
Bauer, L.: Access Control for the Web via Proof-Carrying Authorization. PhD thesis, Princeton University (2003)
Bauer, L., Garriss, S., McCune, J.M., Reiter, M.K., Rouse, J., Rutenbar, P.: Device-enabled authorization in the grey system. In: Zhou, J., López, J., Deng, R.H., Bao, F. (eds.) ISC 2005. LNCS, vol. 3650, pp. 431–445. Springer, Heidelberg (2005)
Becker, M.Y., Fournet, C., Gordon, A.D.: Design and semantics of a decentralized authorization language. In: IEEE Computer Security Foundations Symposium (CSF 2007), pp. 3–15. IEEE Computer Society Press, Los Alamitos (2007)
Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A., Maffeis, S.: Refinement types for secure implementations. In: IEEE Computer Security Foundations Symposium (CSF 2008), pp. 17–32. IEEE, Los Alamitos (2008)
Chaudhuri, A., Abadi, M.: Secrecy by typing and file-access control. In: IEEE Computer Security Foundations Workshop (CSFW 2006), pp. 112–123. IEEE, Los Alamitos (2006)
Chaudhuri, A., Garg, D.: PCAL: Language support for proof-carrying authorization systems. Technical Report CMU-CS-09-141, Carnegie Mellon University (2009)
Chaudhuri, A., Naldurg, P., Rajamani, S.: A type system for data-flow integrity on Windows Vista. In: ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS 2008), pp. 89–100. ACM, New York (2008)
DeTreville, J.: Binder, a logic-based security language. In: IEEE Symposium on Security and Privacy (S&P 2002), pp. 105–113. IEEE, Los Alamitos (2002)
Flanagan, C.: Hybrid type checking. In: ACM Symposium on Principles of Programming Languages (POPL 2006), pp. 245–256. ACM, New York (2006)
Fournet, C., Gordon, A., Maffeis, S.: A type discipline for authorization in distributed systems. In: IEEE Computer Security Foundations Symposium (CSF 2007), pp. 31–48. IEEE, Los Alamitos (2007)
Garg, D.: Proof search in an authorization logic. Technical Report CMU-CS-09-121, Carnegie Mellon University (2009)
Garg, D., Pfenning, F.: Non-interference in constructive authorization logic. In: IEEE Computer Security Foundations Workshop (CSFW 2006), pp. 283–293. IEEE, Los Alamitos (2006)
Garg, D., Pfenning, F.: A proof-carrying file system. Technical Report CMU-CS-09-123, Carnegie Mellon University (2009)
Jia, L., Vaughan, J.A., Mazurak, K., Zhao, J., Zarko, L., Schorr, J., Zdancewic, S.: Aura: A programming language for authorization and audit. In: ACM International Conference on Functional Programming (ICFP 2008). ACM, New York (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chaudhuri, A., Garg, D. (2009). PCAL: Language Support for Proof-Carrying Authorization Systems. In: Backes, M., Ning, P. (eds) Computer Security – ESORICS 2009. ESORICS 2009. Lecture Notes in Computer Science, vol 5789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04444-1_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-04444-1_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04443-4
Online ISBN: 978-3-642-04444-1
eBook Packages: Computer ScienceComputer Science (R0)