Abstract
The byte-code verifier is advertised as a key component of the security and safety strategy for the Java language, making it possible to use and exchange Java programs without fearing too much damage due to erroneous programs or malignant program providers. As Java is likely to become one of the languages used to embed programs in all kinds of appliances or computer-based applications, it becomes important to verify that the claim of safety is justified.
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
G. Barthe, G. Dufay, L. Jakubiec, S. Melo de Sousa, and B. Serpette. A Formal Executable Semantics of the JavaCard Platform. In D. Sands, editor, Proceedings of ESOP’01, volume 2028 of LNCS, pages 302–319. Springer-Verlag, 2001.
Yves Bertot. A coq formalization of a type checker for object initialization in the java virtual machine. Research Report RR-4047, INRIA, 2000.
Ludovic Casset and Jean-Louis Lanet. How to formally specify the java byte code semantics using the b method. In proceedings of the Workshop on Formal Techniques for Java Programs at ECOOP 99, June 1999.
Christina Cornes and Delphine Terrasse. Automatizing inversion of inductive predicates in coq. In Types for Proofs and Programs, volume 1158 of Lecture Notes in Computer Science. Springer-Verlag, 1995.
Gilles Dowek, Amy Felty, Hugo Herbelin, Gérard Huet, Chet Murthy, Catherine Parent, Christine Paulin-Mohring, and Benjamin Werner. The Coq Proof Assistant User’s Guide. INRIA, May 1993. Version 5.8.
Stephen N. Freund and John C. Mitchell. A Formal Framework for the Java Bytecode Language and Verifier. In ACM Conference on Object-Oriented Programming: Systems, Languages and Applications, November 1999.
Stephen N. Freund and John C. Mitchell. A Type System for Object Initialization in the Java Bytecode Language. ACM Transactions on Programming Languages and Systems, September 2000.
A. Goldberg. A specification of Java loading and bytecode verification. In Proceedings of 5th ACM Conference on Computer and Communication Security, 1998.
Ulrich Hensel, Marieke Huisman, Bart Jacobs, and Hendrik Tews. Reasoning about classes in object-oriented languages: Logical models and tools. In Proceedings of European Symposium on Programming (ESOP’ 98), volume 1381 of LNCS, pages 105–121. Springer-Verlag, March 1998.
Marieke Huisman. Java program verification in Higher-order logic with PVS and Isabelle. PhD thesis, University of Nijmegen, 2001.
G. A. Kildall. A unified approach to global program optimization. In Proceedings of the ACM Symposium on Principles of Programming Languages, pages 194206, 1973.
Tobias Nipkow. Verified bytecode verifiers. unpublished, available at URL http://www.in.tum.de/~nipkow/pubs/bcv2.html , 2000
Tobias Nipkow, David von Oheimb, and Cornelia Pusch. µJava: Embedding a programming language in a theorem prover. In Friedrich L. Bauer and Ralf Steinbrüggen, editors, Foundations of Secure Computation, volume 175 of NATO Science Series F: Computer and Systems Sciences, pages 117–144. IOS Press, 2000.
R. O'Callahn. A simple, comprehensive type system for java bytecode subroutines. In ACM Symposium on Principles of Programming Languages, pages 70–78. ACM Press, 1999.
David von Oheimb and Tobias Nipkow. Machine checking the Java specification: Proving type-safety. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, LNCS. Springer, 1998. To appear.
Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, feb 1995.
Christine Paulin-Mohring and Benjamin Werner. Synthesis of ML programs in the system Coq. Journal of Symbolic Computation, 15:607–640, 1993.
Lawrence C. Paulson and Tobias Nipkow. Isabelle: a generic theorem prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.
Cornelia Pusch. Proving the soundness of a Java bytecode verifier specification in Isabelle/HOL. In W. Rance Cleaveland, editor, Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), volume 1579 of LNCS, pages p. 89–103. Springer-Verlag, 1999.
Z. Qian. A formal specification of Java Virtual machine instructions for objects, methods, and subroutines. In Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science. Springer-Verlag, 1999.
Joseph Rouyer. Développement de l'algorithme d'unification dans le calcul des constructions avec types inductifs, September 1992. (In french), available at URL http://coq.inria.fr/contribs/unification.html
Raymie Stata and Martín Abadi. A type system for Java bytecode subroutines. In Proceedings of the 25th Annual ACM Symposium on Principles of Programming Languages, pages 149–160. ACM Press, January 1998.
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
Bertot, Y. (2001). Formalizing a JVML Verifier for Initialization in a Theorem Prover. In: Berry, G., Comon, H., Finkel, A. (eds) Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44585-4_3
Download citation
DOI: https://doi.org/10.1007/3-540-44585-4_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42345-4
Online ISBN: 978-3-540-44585-2
eBook Packages: Springer Book Archive