![](https://csd.cmu.edu/sites/default/files/styles/full_width_focal_point/public/graduate.png.webp?itok=Wsy3nMEH)
Andrew Bernard
Thesis Title:
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
CMU-CS-04-124.pdf (2.47 MB) ( 310 pages)Copyright Notice