|
USENIX 2nd Symposium on
OS Design and Implementation (OSDI '96)
Safe Kernel Extensions Without Run-Time Checking
Best Paper Award
George C. Necula and
Peter Lee
Carnegie Mellon University
Abstract
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.
|
Need help? Use our Contacts page.
Conference Index