PCFS is an implementation of proof-carrying authorization (PCA)
inside a file system. Through a combination of proofs and
cryptographic capabilities, PCFS rigorously enforces complex
user-defined 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 step-by-step 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.
Papers and Reports
- Proof theory for
authorization logic and its application to a practical
file system. Ph.D. Thesis, Technical Report
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 Proof-Carrying
File System. IEEE Symposium on Security and Privacy
(Oakland), 2010. [Expanded, outdated
version: Technical Report CMU-CS-09-123]
Description of the design of PCFS, its use, perfomance
evaluation, and briefly, the logic BL.
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.
representation of common rules for controlling access to
classified information. Technical Report
A case study for the use of PCFS and BL.
an authorization logic. Technical Report
Two methods for automatic proof search in
BL. Generalization of one of these methods with time is
implemented in PCFS.