We have described proof-carrying code, a mechanism that allows a kernel or server to interact safely with binaries supplied by an untrusted source. does not incur any run-time overhead for the kernel. Instead, the code producer is required to generate a formal proof that the code obeys the safety policy. The kernel can easily check the proofs for validity, after which it is absolutely certain that the code respects the safety policy. Furthermore, binaries are completely tamper-proof; any attempt to alter either the native code or safety proof in a binary is either detected or harmless. Our experiments with network packet filters show that can lead to significant performance advantages over existing approaches to safe code, including code-editing techniques such as Software Fault Isolation.
Proof-carrying code has the potential to free the system designer from relying on run-time checking as the sole means of ensuring safety. Traditionally, system designers have always viewed safety simply in terms of memory protection, achieved through the use of rather expensive run-time mechanisms such as hardware-enforced memory protection and extensive run-time checking of data. By being limited to memory protection and run-time checking, the designer must impose substantial restrictions on the structure and implementation of the entire system, for example by requiring the use of a restricted application-kernel interaction model (such as a fixed system call or application-program interface.)
Proof-carrying code, on the other hand, allows the safety policy to be defined by the kernel designer and then certified by each application. Not only does this provide greater flexibility for designers of both the system and applications, but also allows safety policies to be used that are more abstract and fine-grained than memory protection. We believe that this has the potential to lead to great improvements in the robustness and end-to-end performance of systems.