Java bytecode verification via static single assignment form

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Java bytecode verification via static single assignment form

Full text

Pdf (658 KB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 30 , Issue 4 (July 2008) table of contents

Article No. 21

Year of Publication: 2008

ISSN:0164-0925

Authors

Andreas Gal	University of California, Irvine
Christian W. Probst	Technical University of Denmark, Kongens Lyngby
Michael Franz	University of California, Irvine

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 13, Downloads (12 Months): 167, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1377492.1377496 What is a DOI?

ABSTRACT

Java Virtual Machines (JVMs) traditionally perform bytecode verification by way of an iterative dataflow analysis. Bytecode verification is necessary to ensure type safety because temporary variables in the JVM are not statically typed. We present an alternative verification mechanism that transforms JVM bytecode into Static Single Assignment Form (SSA) and thereby propagates definitions directly to uses. Type checking at control flow merge points can then be performed in a single pass.

Our prototype implementation of the new algorithm is faster than the standard JVM bytecode verifier. It has the additional benefit of generating SSA as a side effect, which may be immediately useful for a subsequent dynamic compilation stage.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Wolfram Amme , Niall Dalton , Jeffery von Ronne , Michael Franz, SafeTSA: a type safe and referentially secure mobile-code representation based on static single assignment form, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.137-147, June 2001, Snowbird, Utah, United States
	2	Davey, B. A. and Priestley, H. A. 1990. Introduction to Lattices and Order. Cambridge University Press.
	3	Robert Fitzgerald , Todd B. Knoblock , Erik Ruf , Bjarne Steensgaard , David Tarditi, Marmot: an optimizing compiler for Java, Software—Practice & Experience, v.30 n.3, p.199-232, Mar.1.2000 [doi>10.1002/(SICI)1097-024X(200003)30:3<199::AID-SPE296>3.0.CO;2-2]
	4	Freund, S. N. 1998. The costs and benefits of java bytecode subroutines. In Proceedings of the Formal Underpinnings of Java Workshop at OOPSLA.
	5	Stephen N. Freund , John C. Mitchell, A formal framework for the Java bytecode language and verifier, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.147-166, November 01-05, 1999, Denver, Colorado, United States
	6	Freund, S. N. and Mitchell, J. C. 1999b. Specification and verification of Java bytecode subroutines and exceptions. Tech. rep. CS-TN-99-91, Stanford University.
	7	Stephen N. Freund , John C. Mitchell, A Type System for the Java Bytecode Language and Verifier, Journal of Automated Reasoning, v.30 n.3-4, p.271-321, 2003 [doi>10.1023/A:1025011624925]
	8	Gal, A., Probst, C. W., and Franz, M. 2005. Structural encoding of static single assignment form. In Proceedings of the 4th International Workshop on Compiler Optimization Meets Compiler Verification (COCV'05). Elsevier Science Publishers, Amsterdam, The Netherlands.
	9	League, C., Trifonov, V., and Shao, Z. 2001. Functional Java Bytecode. In Proceedings of the 5th World Conference on Systemics, Cybernetics, and Informatics Workshop on Intermediate Representation Engineering for the Java Virtual Machine.
	10	Xavier Leroy, Java Bytecode Verification: Algorithms and Formalizations, Journal of Automated Reasoning, v.30 n.3-4, p.235-269, 2003 [doi>10.1023/A:1025055424017]
	11	Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
	12	Stärk R. and Schmid, J. 2001. Java bytecode verification is not possible (extended abstract). In Proceedings of Eurocast'01 Formal Methods and Tools for Computer Science, R. Moreno-Díaz and A. Quesada-Arencibia, Eds. 232--234.
	13	Robert F. Stark , E. Borger , Joachim Schmid, Java and the Java Virtual Machine: Definition, Verification, Validation with Cdrom, Springer-Verlag New York, Inc., Secaucus, NJ, 2001
	14	Raymie Stata , Martin Abadi, A type system for Java bytecode subroutines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.1, p.90-137, Jan. 1999 [doi>10.1145/314602.314606]