Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
A Scalable Architecture for Proof-Carrying Code
| |
|
A Scalable Architecture for Proof-Carrying Code
George C. Necula6 
| (6) |
Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, CA 94720, USA |
Abstract
Proof-Carrying Code (PCC) is a general mechanism for verifying that a code fragment can be executed safely on a host system.
The key technical detail that makes PCC simple yet very powerful is that the code fragment is required to be accompanied by
a detailed and precise explanation of how it satisfies the safety policy. This leaves the code receiver with the simple task
of verifying that the explanation is correct and that it matches the code in question.
Previous implementations of PCC used safety explanations in the form of explicit formal proofs of code safety, thus gaining
leverage from a substantial amount of previous research in the area of proof representation and checking, but at the expense
of poor scalability due to large proof sizes. In this paper we describe a series of changes that are necessary to achieve
a truly scalable architecture for PCC. These include a new proof representation form along with a better integration of the
various components of a PCC checker. We also present experimental results that show this architecture to be effective for
checking the type safety of even very large programs expressed as machine code.
Acknowledgments We would like to thank Shree Rahul for the help with the collection of the experimental data presented in this paper and to
Peter Lee, Mark Plesko, Chris Colby, John Gregorski, Guy Bialostocki and Andrew McCreight from Cedilla Systems Corporation
who have implemented the certifying compiler for Java used in these experiments.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|