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. 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.
[Download PCFS]
Papers and Reports
- Proof theory for
authorization logic and its application to a practical
file system. Ph.D. Thesis, Technical Report
CMU-CS-09-168, 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 Proof-Carrying
File System. With Frank Pfenning. 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.
-
A logical
representation of common rules for controlling access to
classified information. Technical Report
CMU-CS-09-139, 2009.
A case study for the use of PCFS and BL.
-
Proof-search in an authorization logic. Technical Report
CMU-CS-09-121, 2009.
Two methods for automatic proof search in
BL. Generalization of one of these methods with time is
implemented in PCFS.
Related Papers
|