Andrew Bernard

Engineering Formal Security Policies for Proof-Carrying Code Degree Type: Ph.D. in Computer Science
Advisor(s): Peter Lee
Graduated: May 2004

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

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