Abstract
Compiled Java programs may be downloaded from the World Wide Web and be executed on any host platform that implements the Java Virtual Machine (JVM). However, in general it is impossible to check the origin of the code and trust in its correctness. Therefore standard implementations of the JVM contain a bytecode verifier that statically checks several security constraints before execution of the code. We have formalized large parts of the JVM, covering the central parts of object orientation, within the theorem prover Isabelle/HOL. We have then formalized a specification for a Java bytecode verifier and formally proved its soundness. While a similar proof done with paper and pencil turned out to be incomplete, using a theorem prover like Isabelle/HOL guarantees a maximum amount of reliability.
Research supported by DFG project Bali.
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
Peter Berstelsen. Semantics of Java Byte Code.. http://www.dina.kvl.dk/~pmb/, August 1997.
Richard M. Cohen. The defensive Java Virtual Machine Specification. Technical report, Computational Logic Inc., 1997. Draft version.
Stephen N. Freund and John C. Mitchell. A Type System for Object Initialization in the Java Bytecode Language. In ACM Conf. on Object-Oriented Programming: Systems, Languages and Applications, 1998.
James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. Addison-Wesley, 1996.
A. Goldberg. A Specification of Java Loading and Bytecode Verification. Technical report, Kestrel Institute, Palo Alto, CA, 1997.
Pieter Hartel, Michael Butler, and Moshe Levy. The Operational Semantics of a Java Secure Processor. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lect. Notes in Comp. Sci. Springer-Verlag, 1998.
The Isabelle library. http://www.in.tum.de/~isabelle/library/.
Tim Lindholm and Frank Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996.
Tobias Nipkow, David von Oheimb, and Cornelia Pusch. Project Bali. http://www.in.tum.de/~isabelle/bali/.
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, volume 1523 of Lect. Notes in Comp. Sci. Springer-Verlag, 1998.
Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lect. Notes in Comp. Sci. Springer-Verlag, 1994.
Cornelia Pusch. Formalizing the Java Virtual Machine in Isabelle. Technical Report TUM-I9816, Institut für Informatik, Technische Universität München, 1998. Available at http://www.in.tum.de/~pusch/.
Zhenyu Qian. A formal specification of Java Virtual Machine instructions. Technical report, 1997. Dept. of Comp. Sci., University of Bremen.
Zhenyu Qian. A Formal Specification of Java Virtual Machine instructions for Objects, Methods and Subroutines. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lect. Notes in Comp. Sci. Springer-Verlag, 1998.
Raymie Stata and Martín Abadi. A type system for Java bytecode subroutines. In Proc. 25th ACM Symp. Principles of Programming Languages. ACM Press, 1998. To appear.
Types forum. http://www.cs.indiana.edu/hyplan/pierce/types/.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pusch, C. (1999). Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL. In: Cleaveland, W.R. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1999. Lecture Notes in Computer Science, vol 1579. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49059-0_7
Download citation
DOI: https://doi.org/10.1007/3-540-49059-0_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65703-3
Online ISBN: 978-3-540-49059-3
eBook Packages: Springer Book Archive