CMU-CS-02-130
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-02-130

Temporal Logic for Proof-Carrying Code

Andrew Bernard, Peter Lee

August 2002

CMU-CS-02-130.ps
CMU-CS-02-130.pdf

Keywords: Proof-carrying code, temporal logic, formal methods


Proof-carrying code (PCC) is a framework for ensuring that untrusted programs are safe to install and execute. When using PCC, untrusted programs are required to contain a proof that allows the program text to be checked efficiently for safe behavior. In this paper, we lay the foundation for a potential engineering improvement to PCC. Specifically, we present a practical approach to using temporal logic to specify security policies in such a way that a PCC system can enforce them.

39 pages


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

This page maintained by reports@cs.cmu.edu