Deepak Garg

Proof Theory for Authorization Logic and Its Application to a Practical File System Degree Type: Ph.D. in Computer Science
Advisor(s): Frank Pfenning
Graduated: December 2009

Abstract:

In most computer systems, users’ access to resources is controlled using authorization policies. Logic is an appropriate medium for representing, understanding, and enforcing authorization policies, yet despite several years of pragmatic work on the subject, the foundations of relevant logics remain unexplored and poorly understood. It is in this realm that the work of this thesis lies; the thesis explores the theory of logics for expressing authorization policies as well as applications of the theory in practice. In doing so, it makes three foundational and technically challenging contributions.

First, the thesis introduces proof theory and metatheory in the context of authorization logics, illustrated through a new logic BL. In particular, structural proof-theoretic systems of natural deduction and sequent calculus are investigated and their importance explained. Pragmatic problems like proof verification and automatic proof search are then addressed using the sound foundations of proof theory.

Second, the thesis considers a logical treatment of dynamism in authorization policies and, in particular, logical constructs for representing authorizations depending on system state, consumable credentials, and explicit time are presented. Further, a practical, efficient, and provably correct mechanism for their enforcement is developed. The mechanism is based on a combination of proofs and cryptographic capabilities.

Third, the practical usefulness of the proof theory and the enforcement mechanism is demonstrated through an implementation of the same in a file system, PCFS. It is shown through measurements that file access in PCFS is very efficient.

In addition, the thesis includes a detailed case study that formalizes in BL policies used to control access to classified information in the U.S., and explains how the policies may be enforced using PCFS.

Thesis Committee:
Frank Pfenning (Chair)
Martín Abadi
Lujo Bauer
Anupam Datta
Robert Harper

Peter Lee, Head, Computer Science Department
Randy Bryant, Dean, School of Computer Science

Keywords:
Proof theory, access control, file system, formal logic, modal logic, computer security