A Proof-Carrying File System

Abstract

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 06, 2009
Accession Number
ADA507095

Entities

People

  • Deepak Garg
  • Frank Pfenning

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Abstracts
  • Authentication
  • Case Studies
  • Computer Access Control
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Construction
  • Control Systems
  • Denial Of Service Attack
  • Directories
  • Information Operations
  • Language
  • Operating Systems
  • Time Intervals
  • Verification

Fields of Study

  • Computer science

Readers

  • Computer Science.
  • Cybersecurity.
  • Mathematical Modeling and Probability Theory.