Computer Science Department
School of Computer Science, Carnegie Mellon University


A Proof-Carrying File System

Deepak Garg, Frank Pfenning

June 2009


Keywords: Access control, proof carrying authorization, file system

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.

46 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by