CMU-CS-04-124
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-04-124

Engineering Formal Security Policies
for Proof-Carrying Code

Andrew Bernard

April 2004

Ph.D. Thesis

CMU-CS-04-124.ps
CMU-CS-04-124.pdf


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 reports@cs.cmu.edu