Computer Science Department
School of Computer Science, Carnegie Mellon University


Temporal Logic for Proof-Carrying Code

Andrew Bernard, Peter Lee

August 2002

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