Safe Kernel Extensions Without Run-Time Checking

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 rst de nes 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 PCC 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 di culty of PCC is in generating the safety proofs. In order to gain some preliminary experience with this, we have written several network packet lters in hand-tuned DEC Alpha assembly language, and then generated PCC binaries for them using a special prototype assembler. The PCC ...

• Type: Conference
• Year: 1996
• Where: OSDI
• Authors: George C. Necula, Peter Lee
• Keywords: Operating System, OSDI 1996, Packet Lters, PCC Binaries, Safety Policy