A Proof-Carrying File System
Deepak Garg, Frank Pfenning · 2009
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.