Abstract
In earlier work, Necula and Lee developed proof-carrying code (PCC) [3,5],which is a mechanism for ensuring the safe behavior of programs. In PCC, a program contains both the code and an encoding of an easy-to-check proof. The validity of the proof, which can be automatically determined by a simple proof-checking program, implies that the code, when executed, will behave safely according to a user-supplied formal definition of safe behavior. Later, Necula and Lee demonstrated the concept of a certifying compiler [6,7].Certifying compilers promise to make PCC more practical by compiling high-level source programs into optimized PCC binaries completely automatically, as opposed to depending on semi-automatic theorem-proving techniques. Taken together, PCC and certifying compilers provide a possible solution to the code safety problem, even in applications involving mobile code [4].
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery 40(1), 143–184 (1993)
Leroy, X.: The ZINC experiment, an economical implementation of the ML language. Technical Report 117, INRIA (1990)
Necula, G., Lee, P.: Safe kernel extensions without run-time checking. In: Second Symposium on Operating Systems Design and Implementation, Seattle, October 1996, pp. 229–243 (1996)
Necula, G., Lee, P.: Safe, untrusted agents using proof-carrying code. In: Vigna, G. (ed.) Mobile Agents and Security. LNCS, vol. 1419, p. 61. Springer, Heidelberg (1998)
Necula, G.C.: Proof-carrying code. In: Jones, N.D. (ed.) Conference Record of the 24th Symposium on Principles of Programming Languages (POPL 1997), Paris, France, pp. 106–119. ACM Press, New York (1997)
Necula, G.C.: Compiling with Proofs. PhD thesis, Carnegie Mellon University (October 1998); Available as Technical Report CMU-CS-98-154
Necula, G.C., Lee, P.: The design and implementation of a certifying compiler. In: Cooper, K.D. (ed.) Proceedings of the Conference on Programming Language Design and Implementation (PLDI 1998), Montreal, Canada, pp. 333–344. ACM Press, New York (1998)
Necula, G.C., Rahul, S.P.: Oracle-based checking of untrusted soft-ware. Submitted to Programming Language Design and Implementation. In: PLDI 2000 (November 1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Colby, C., Lee, P., Necula, G.C. (2000). A Proof-Carrying Code Architecture for Java. In: Emerson, E.A., Sistla, A.P. (eds) Computer Aided Verification. CAV 2000. Lecture Notes in Computer Science, vol 1855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722167_44
Download citation
DOI: https://doi.org/10.1007/10722167_44
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67770-3
Online ISBN: 978-3-540-45047-4
eBook Packages: Springer Book Archive