Computer Science Department
School of Computer Science, Carnegie Mellon University


Engineering Formal Security Policies
for Proof-Carrying Code

Andrew Bernard

April 2004

Ph.D. Thesis

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

Thesis statement: 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).

310 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by