PCFS is an implementation of proofcarrying authorization (PCA)
inside a file system. Through a combination of proofs and
cryptographic capabilities, PCFS rigorously enforces complex
userdefined access policies that are expressed as logical
formulas. The current release of PCFS is v2.1.1. This release
includes all source code, and a stepbystep tutorial on setting
up the file system and using it. Also included is a sample
scenario, complete with policies. The logic for representing
policies in PCFS is called BL. Links to papers describing both
PCFS and BL can be found below.
[Download PCFS]
Papers and Reports
 Proof theory for
authorization logic and its application to a practical
file system. Ph.D. Thesis, Technical Report
CMUCS09168, 2009.
Description of the design of
PCFS, its use, performance evaluation, and the proof
theory and implementation of the logic BL. Superset of
all other papers and reports listed here.
 A ProofCarrying
File System. IEEE Symposium on Security and Privacy
(Oakland), 2010. [Expanded, outdated
version: Technical Report CMUCS09123]
Description of the design of PCFS, its use, perfomance
evaluation, and briefly, the logic BL.
 Stateful
Authorization Logic  Proof Theory and A Case
Study. In the International Workshop on Security and
Trust Management (STM), 2010.
Treatment of system
state in the logic BL.

A logical
representation of common rules for controlling access to
classified information. Technical Report
CMUCS09139, 2009.
A case study for the use of PCFS and BL.

Proofsearch in an authorization logic. Technical Report
CMUCS09121, 2009.
Two methods for automatic proof search in
BL. Generalization of one of these methods with time is
implemented in PCFS.
Related Papers
