Accession Number : ADA322252

Title :   Safe Kernel Extensions Without Run-Time Checking,

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Personal Author(s) : Necula, George C. ; Lee, Peter

PDF Url : ADA322252

Report Date : 1996

Pagination or Media Count : 16

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 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 difficulty of PCC 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 PCC binaries for them using a special prototype assembler. The PCC binaries can be executed with no run-time over-head, 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.

Descriptors :   *OPERATING SYSTEMS(COMPUTERS), *COMPUTER PROGRAM VERIFICATION, SOFTWARE ENGINEERING, SYSTEMS ANALYSIS, SYSTEM SAFETY, FIELDS(COMPUTER PROGRAMS), COMPUTER PROGRAM RELIABILITY, EXECUTIVE ROUTINES, BINARY PROCESSORS, PACKET SWITCHING, ASSEMBLY LANGUAGES.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE