PCAL: Language Support for Proof-Carrying Authorization Systems

Avik Chaudhuri and Deepak Garg

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.


    author = {Avik Chaudhuri and Deepak Garg},
    title = {{PCAL}: Language Support for Proof-Carrying Authorization Systems},
    booktitle = {Proceedings of the 14th European Symposium on
                 Research in Computer Security (ESORICS'09)},
    year = {2009},
    pages = {184--199},
    publisher = {Springer}