Abstract
Using the theorem prover Isabelle/HOL we have formalized and proved correct an executable bytecode verifier in the style of Kildall’s algorithm for a significant subset of the Java Virtual Machine. First an abstract framework for proving correctness of data flow based type inference algorithms for assembly languages is formalized. It is shown that under certain conditions Kildall’s algorithm yields a correct bytecode verifier. Then the framework is instantiated with a model of the JVM.
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
Y. Bertot. A Coq formalization of a type checker for object initialization in the Java Virtula Machine. Technical Report RR-4047, INRIA, Nov. 2000.
L. Casset and J. L. Lanet. A formal specification of the Java bytecode semantics using the B method. In ECOOP’99 Workshop Formal Techniques for Java Programs, 1999.
A. Coglio, A. Goldberg, and Z. Qian. Toward a provably-correct implementation of the JVM bytecode verifier. In Proc. DARPA Information Survivability Conference and Exposition (DISCEX’00), Vol. 2, pages 403–410. IEEE Computer Society Press, 2000.
S. N. Freund and J. C. Mitchell. A type system for object initialization in the Java bytecode language. In ACM Conf. Object-Oriented Programming: Systems, Languages and Applications, 1998.
S. N. Freund and J. C. Mitchell. A formal framework for the java bytecode language and verifier. In ACM Conf. Object-Oriented Programming: Systems, Languages and Applications, 1999.
A. Goldberg. A specification of Java loading and bytecode verification. In Proc. 5th ACM Conf. Computer and Communications Security, 1998.
M. Hagiya and A. Tozawa. On a new method for dataflow analysis of Java virtual machine subroutines. In G. Levi, editor, Static Analysis (SAS’98), volume 1503 of Lect. Notes in Comp. Sci., pages 17–32. Springer-Verlag, 1998.
G. A. Kildall. A unified approach to global program optimization. In Proc. ACM Symp. Principles of Programming Languages, pages 194–206, 1973.
T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996.
S. S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann, 1997.
T. Nipkow and D. v. Oheimb. Javalight is type-safe — definitely. In Proc. 25th ACM Symp. Principles of Programming Languages, pages 161–170, 1998.
T. Nipkow, D. v. Oheimb, and C. Pusch. μJava: Embedding a programming language in a theorem prover. In F. Bauer and R. Steinbruggen, editors, Foundations of Secure Computation, pages 117–144. IOS Press, 2000.
C. Pusch. Proving the soundness of a Java bytecode verifier specification in Isabelle/HOL. In W. Cleaveland, editor, Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), volume 1579 of Lect. Notes in Comp. Sci., pages 89–103. Springer-Verlag, 1999.
Z. Qian. A formal specification of Java Virtual Machine instructions for objects, methods and subroutines. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lect. Notes in Comp. Sci., pages 271–311. Springer-Verlag, 1999.
Z. Qian. Standard fixpoint iteration for Java bytecode verification. ACM Trans. Programming Languages and Systems, ?:?-?, 200? Accepted for publication.
R. Stata and M. Abadi. A type system for Java bytecode subroutines. In Proc. 25th ACM Symp. Principles of Programming Languages, pages 149–161. ACM Press,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
Nipkow, T. (2001). Verified Bytecode Verifiers. In: Honsell, F., Miculan, M. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2001. Lecture Notes in Computer Science, vol 2030. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45315-6_23
Download citation
DOI: https://doi.org/10.1007/3-540-45315-6_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41864-1
Online ISBN: 978-3-540-45315-4
eBook Packages: Springer Book Archive