PCAL: Language Support for Proof-Carrying Authorization Systems

  • Avik Chaudhuri
  • Deepak Garg
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5789)


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.


Access Control Theorem Prover Command Line System Interface Access Control Policy 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    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 PlotkinMathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    Avijit, K., Datta, A., Harper, R.: PCML5: A language for ensuring compliance with access control policies (2009); Draft, personal communicationGoogle Scholar
  5. 5.
    Bauer, L.: Access Control for the Web via Proof-Carrying Authorization. PhD thesis, Princeton University (2003)Google Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    Chaudhuri, A., Garg, D.: PCAL: Language support for proof-carrying authorization systems. Technical Report CMU-CS-09-141, Carnegie Mellon University (2009)Google Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    Flanagan, C.: Hybrid type checking. In: ACM Symposium on Principles of Programming Languages (POPL 2006), pp. 245–256. ACM, New York (2006)Google Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    Garg, D.: Proof search in an authorization logic. Technical Report CMU-CS-09-121, Carnegie Mellon University (2009)Google Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    Garg, D., Pfenning, F.: A proof-carrying file system. Technical Report CMU-CS-09-123, Carnegie Mellon University (2009)Google Scholar
  18. 18.
    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)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Avik Chaudhuri
    • 1
  • Deepak Garg
    • 2
  1. 1.University of MarylandCollege Park
  2. 2.Carnegie Mellon UniversityUSA

Personalised recommendations