School of Computer Science
Carnegie Mellon University
Pittsburgh, Pennsylvania 15213-3891
{necula,petel}@cs.cmu.edu
This paper describes a mechanism by which an
operating system kernel can determine with certainty that it is safe to
execute a binary supplied by an untrusted source. The kernel first defines a
safety policy and makes it public. Then, using this policy, an application can
provide binaries in a special form called proof-carrying code, or simply
PCC. Each binary contains, in addition to the native code, a formal proof
that the code obeys the safety policy. The kernel can easily validate the
proof without using cryptography and without consulting any external
trusted entities. If the validation succeeds, the code is guaranteed to respect
the safety policy without relying on run-time checks.
The main practical difficulty of is in generating the safety proofs. In
order to gain some preliminary experience with this, we have written several
network packet filters in hand-tuned DEC Alpha assembly language, and then
generated binaries for them using a special prototype assembler. The
binaries can be executed with no run-time overhead, beyond a one-time cost
of 1 to 3 milliseconds for validating the enclosed proofs. The net
result is that our packet filters are formally guaranteed to be safe and are
faster than packet filters created using Berkeley Packet Filters, Software
Fault Isolation, or safe languages such as Modula-3.
This research was sponsored in part by the Advanced Research Projects Agency CSTO under the title ``The Fox Project: Advanced Languages for Systems Software,'' ARPA Order No. C533, issued by ESC/ENS under Contract No. F19628-95-C-0050. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the Advanced Research Projects Agency or the U.S. Government.
To appear at the Second Symposium on Operating Systems Design and
Implementation (OSDI '96), Seattle, Washington, October 28-31, 1996.