Andrew Bernard
Carnegie Mellon University

Temporal Logic for Proof-Carrying Code


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.

Principles of Programming Seminars

POP Seminar
July 12, 2002
3:30 p.m.
Wean Hall 8220