Date: December 5, 1996
Speaker: George Ciprian Necula, CMU
Proof-Carrying Code
Abstract:
This talk describes Proof-Carrying Code (PCC), a software mechanism that allows a host system to determine with certainty that it is safe to execute a program supplied by an untrusted source. For this to be possible, the untrusted code supplier must provide with the code a safety proof that attests to the code's safety properties. The code consumer can easily and quickly validate the proof without using cryptography and without consulting any external agents.
In order to gain preliminary experience with proof-carrying code, we have performed a series of case studies. In one case study, we write safe assembly-language network packet filters. These filters can be executed with no run-time overhead, beyond a one-time cost of 1 to 3 milliseconds for validating the attached safety 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. We also present two experiments that show how PCC can be used to enforce safety aspects other than memory safety. In one experiment we use PCC to guarantee that assembly language extensions to a simplified version of the Standard ML runtime system preserve data abstraction boundaries and the representation invariants. In another experiment we show how PCC can be used to make resource usage about extensions that are permitted to acquire and release resources and send network packets.
SDI / LCS Seminar Questions?
Karen Lindenfelser, 86716, or visit www.pdl.cmu.edu/SDI/