PCAL: Language Support for Proof-Carrying Authorization Systems

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, the authors 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.