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
CMU-CS-04-124.ps
CMU-CS-04-124.pdf
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 This page maintained by reports@cs.cmu.edu
School of Computer Science homepage