Safe Kernel Extensions Without Run-Time Checking

9 years 12 months ago
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 ...
George C. Necula, Peter Lee
Added 02 Nov 2010
Updated 02 Nov 2010
Type Conference
Year 1996
Where OSDI
Authors George C. Necula, Peter Lee
Comments (0)