Abstract
We introduce a generic framework for proof carrying code, developed and mechanically verified in Isabelle/HOL. The framework defines and proves sound a verification condition generator with minimal assumptions on the underlying programming language, safety policy, and safety logic. We demonstrate its usability for prototyping proof carrying code systems by instantiating it to a simple assembly language with procedures and a safety policy for arithmetic overflow.
supported in part by NSF grant CCR-0208618.
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
Appel, A. W. (2001). Foundational proof-carrying code. In 16th Annual IEEE Symposium on Logic in Computer Science (LICS’ 01), pages 247–258.
Appel, A. W. and Felty, A. P. (2000). A semantic model of types and machine instructions for proof-carrying code. In 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’ 00), pages 243–253.
Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.W. (2003) A Resource-aware Program Logic for a JVM-like Language In Trends in Functional Programming, editor: S. Gilmore, Edinburgh
Berghofer, S. and Nipkow, T. (2000). Proof terms for simply typed higher order logic. In Theorem Proving in Higher Order Logics, Springer LNCS vol. 1869, editors: J. Harrison, M. Aagaard
Berghofer (2003). Program Extraction in simply-typed Higher Order Logic. In Types for Proofs and Programs, International Workshop, (TYPES 2002), Springer LNCS, editors: H. Geuvers, F. Wiedijk
Colby, C., Lee, P., Necula, G. C., Blau, F., Plesko, M., and Cline, K. (2000). A certifying compiler for Java. In Proc. ACM SIGPLAN conf. Programming Language Design and Implementation, pages 95–107.
Hamid, N., Shao, Z., Trifonov, V., Monnier, S., and Ni, Z. (2002). A syntactic approach to foundational proof-carrying code. In Proc. 17th IEEE Symp. Logic in Computer Science, pages 89–100.
Klein, G. (2003). Verified Java Bytecode Verification. PhD thesis, Institut fur Informatik, Technische Universität München.
League, C., Shao, Z., and Trifonov, V. (2002). Precision in practice: A type-preserving Java compiler. Technical Report YALEU/DCS/TR-1223, Department of Computer Science, Yale University.
Morrisett, G., Walker, D., Crary, K., and Glew, N. (1998). From system F to typed assembly language. In Proc. 25th ACM Symp. Principles of Programming Languages, pages 85–97. ACM Press.
Necula, G. C. (1997). Proof-carrying code. In Proc. 24th ACM Symp. Principles of Programming Languages, pages 106–119. ACM Press.
Necula, G. C. (1998). Compiling with Proofs. PhD thesis, Carnegie Mellon University.
Necula, G. C. and Lee, P. (2000). Proof generation in the touchstone theorem prover. In McAllester, D., editor, Automated Deduction — CADE-17, volume 1831 of Lect. Notes in Comp. Sci., pages 25–44. Springer-Verlag.
Necula, G. C. and Schneck, R. R. (2002). A gradual approach to a more trustworthy, yet scalable, proof-carrying code. In Voronkov, A., editor, Proc.CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, volume 2392 of Lect. Notes in Comp. Sci., pages 47–62. Springer-Verlag.
Necula, G. C. and Schneck, R. R. (2003). A sound framework for untrustred verification-condition generators. In Proc. IEEE Symposium on Logic in Computer Science. (LICS03), pages 248–260.
Nipkow, T., Paulson, L. C., and Wenzel, M. (2002). Isabelle/HOL-A Proof Assistant for Higher-Order Logic, volume 2283 of Lect. Notes in Comp. Sci. Springer.
Klein, G. and Nipkow, T. (2004) A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler Technical Report, National ICT Australia, Sydney
Wildmoser, M. and Nipkow, T. (2004) Certifying machine code safety: shallow versus deep embedding. TPHOLs 2004
VeryPCC website in Munich (2004), http://isabelle.in.tum.de/verypcc/.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer Science + Business Media, Inc.
About this paper
Cite this paper
Wildmoser, M., Nipkow, T., Klein, G., Nanz, S. (2004). Prototyping Proof Carrying Code. In: Levy, JJ., Mayr, E.W., Mitchell, J.C. (eds) Exploring New Frontiers of Theoretical Informatics. IFIP International Federation for Information Processing, vol 155. Springer, Boston, MA. https://doi.org/10.1007/1-4020-8141-3_27
Download citation
DOI: https://doi.org/10.1007/1-4020-8141-3_27
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4020-8140-8
Online ISBN: 978-1-4020-8141-5
eBook Packages: Springer Book Archive