Andrew Bernard

Engineering Formal Security Policies for Proof-Carrying Code

Degree Type: Ph.D. in Computer Science
Advisor(s): Peter Lee
Graduated: May 2004

Keywords: Proof-carrying code, temporal logic, formal verification, proof engineering, security policies

Abstract

It is practical to engineer a system for proof-carrying code (PCC) in which policy is separated from mechanism. In particular, I exhibit a generic implementation of the PCC infrastructure that accepts a wide variety of security properties encoded in a formal specification language. I approach the problem by addressing two distinct subproblems: enforcement (checking programs and proofs) and certification (constructing programs and proofs).

Thesis Committee

Peter Lee (Chair)
Karl Crary
Frank Pfenning
Fred B,. Schneider (Cornell)

Randy Bryant, Head, Computer Science Department
James Morris, Dean, School of Computer Science

Thesis Document

CMU-CS-04-124.pdf (2.47 MB) (310 pages)