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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Mark Plesko, and Kenneth Cline. A certifying compiler for Java. ACM SIGPLAN Notices, 35(5):95–107, May 2000.
N. DeBruijn. Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation. Indag. Mat., 34:381–392, 1972.
Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143–184, January 1993.
Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From system F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):527–568, May 1999.
George C. Necula. Proof-carrying code. In The 24th Annual ACM Symposium on Principles of Programming Languages, pages 106–119. ACM, January 1997.
George C. Necula. Compiling with Proofs. PhD thesis, Carnegie Mellon University, September 1998. Also available as CMU-CS-98-154.
George C. Necula and Peter Lee. Safe kernel extensions without runtime checking. In Second Symposium on Operating Systems Design and Implementations, pages 229–243. Usenix, October 1996.
George C. Necula and Peter Lee. Efficient representation and validation of proofs. In Thirteenth Annual Symposium on Logic in Computer Science, pages 93–104, Indianapolis, June 1998. IEEE Computer Society Press.
George C. Necula and Shree P. Rahul. Oracle-based checking of untrusted programs. In The 28th Annual ACM Symposium on Principles of Programming Languages. ACM, January 2001. To appear.
R. Ramesh, I. V. Ramakrishnan, and David Scott Warren. Automatadriven indexing of Prolog clauses. Journal of Logic Programming, 23(2):151–202, May 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Necula, G.C. (2001). A Scalable Architecture for Proof-Carrying Code. In: Kuchen, H., Ueda, K. (eds) Functional and Logic Programming. FLOPS 2001. Lecture Notes in Computer Science, vol 2024. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44716-4_2
Download citation
DOI: https://doi.org/10.1007/3-540-44716-4_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41739-2
Online ISBN: 978-3-540-44716-0
eBook Packages: Springer Book Archive