George C. Necula, Peter Lee
CMU

Safe Kernel Extensions Without Run-Time Checking
Presented at OSDI'96, October 1996.

URL: http://raw.cs.berkeley.edu/Papers/pcc_osdi96.ps

This paper received the "Best Paper Award" at OSDI'96. This is the gentler introduction to Proof-Carrying Code and its applications in systems. As a case study, we analyze in this paper the use of PCC for ensuring the safety of network packet filters. We show that PCC can be used even for hand-optimized packet filters written in assembly language. As a result the runtime performance of PCC packet filters is the best attainable on a given architecture. Measurements show that this approach yields filters that are about an order of magnitude faster than interpreted Berkeley Packet Filters and about 30% faster than filters "sandboxed" filters using Software Fault Isolation. The cost of PCC filters lies in proof checking. Measurements show that proof-checking is fast and its one-time cost is usually amortized over a few thousand network packets.

George C. Necula, Peter Lee
CMU

Efficient Representation and Validation of Proofs
Presented at LICS'98.

URL: http://raw.cs.berkeley.edu/Papers/lfi_lics98.ps

This paper presents a logical framework derived from the Edinburgh Logical Framework (LF) that can be used to obtain compact representations of proofs and efficient proof checkers. These are essential ingredients of any application that manipulates proofs as first-class objects, such as a Proof-Carrying Code system, in which proofs are used to allow the easy validation of properties of safety-critical or untrusted code.

Our framework, which we call LFi, inherits from LF the capability to encode various logics in a natural way. In addition, the LFi framework allows proof representations without the high degree of redundancy that is characteristic of LF representations. The missing parts of LFi proof representations can be reconstructed during proof checking by an efficient reconstruction algorithm. We also describe an algorithm that can be used to strip the unnecessary parts of an LF representation of a proof. The experimental data that we gathered in the context of a Proof-Carrying Code system shows that the savings obtained from using LFi instead of LF can make the difference between practically useless proofs of several megabytes and manageable proofs of tens of kilobytes.

Somesh Jha (web), Tom Reps (web)
Computer Sciences Department (web), University of Wisconsin, Madison (web)

Analysis of SPKI/SDSI Certificates Using Model Checking
Published at CSFW'15 (2002)

We will read the journal version. Please email Mihai (mihai at cs dot wisc dot edu) for a copy.

SPKI/SDSI is a framework for expressing naming and authorization issues that arise in a distributed-computing environment. In this paper, we establish a connection between SPKI/SDSI and a formalism known as pushdown systems (PDSs). We show that the SPKI/SDSI-to-PDS connection provides a framework for formalizing a variety of certificate-analysis problems. Moreover, the connection has computational significance: Many analysis problems can be solved efficiently (i.e., in time polynomial in the size of the certificate set) using existing algorithms for model checking pushdown systems.