| ||||||||||||||||||||||||||||||||||||||||||||||||||||
USENIX 2nd Symposium on
OS Design and Implementation (OSDI '96)
[Technical Program]
   Next: Introduction
Safe Kernel Extensions Without Run-Time CheckingGeorge C. Necula Peter Lee
This research was sponsored in part by the Advanced Research Projects Agency CSTO under the title ``The Fox Project: Advanced Languages for Systems Software,'' ARPA Order No. C533, issued by ESC/ENS under Contract No. F19628-95-C-0050. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the Advanced Research Projects Agency or the U.S. Government. Submitted to the Second Symposium on Operating Systems Design and Implementation (OSDI '96), Seattle, Washington, October 28-31, 1996.
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.
Next: Introduction
Peter Lee Tue Sep 17 15:37:44 EDT 1996 |
|
This paper was originally published in the
proceedings of The Second Symposium on Operating Systems Design and Implementation (OSDI '96), October 28–31, 1996,
Seattle, Washington, USA
Last changed: 10 Jan 2003 aw |
|
Technical Program