Computer Science Department
School of Computer Science, Carnegie Mellon University
A Proof-Carrying File System
Deepak Garg, Frank Pfenning
This paper presents the design and implementation of PCFS, a file system that uses formal proofs and capabilities to efficiently enforce access policies expressed in a rich logic. Salient features include backwards compatibility with existing programs and automatic enforcement of access rules that depend on both time and system state. We rigorously prove that enforcement using capabilities is correct, and evaluate the file system's performance.