A specification of Java loading and bytecode verification

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A specification of Java loading and bytecode verification

Full text

Pdf (1.15 MB)

Source

Conference on Computer and Communications Security archive
Proceedings of the 5th ACM conference on Computer and communications security table of contents

San Francisco, California, United States

Pages: 49 - 58

Year of Publication: 1998

ISBN:1-58113-007-4

Author

Allen Goldberg

Kestrel Institute, 3260 Hillview Av., Palo Alto, CA

Sponsor

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 0, Downloads (12 Months): 27, Citation Count: 19

Additional Information:

references cited by 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/288090.288104 What is a DOI?

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	J. Cai , R. Paige, Program derivation by fixed point computation, Science of Computer Programming, v.11 n.3, p.197-261, April 1989 [doi>10.1016/0167-6423(88)90033-0]
	2	Drew Dean, The security of static typing with dynamic linking, Proceedings of the 4th ACM conference on Computer and communications security, p.18-27, April 01-04, 1997, Zurich, Switzerland [doi>10.1145/266420.266428]
	3	Cohen, R. "The Defensive Virtual Machine Specification 0.5," available at http:lAwvw.cli.comlsoftwareldjvmlindex.html.
	4	Stephen N. Freund , John C. Mitchell, A Type System for Object Initialization in the Java Bytecode Language, Stanford University, Stanford, CA, 1998
	5	Goldberg, A., A Specification of Java Loading and Bytecode Verification, extended version, available at http:IAvww.kestrel.edtffHTML/people/goldberg/Byteco de.html.
	6	Hagiya, M. and A. Tozawa, "On a New Method for Dataflow Analysis of Java Virtual Machine Subroutines," available at ftp :\knicosia.is. s.utokyo.ae.jplpublstafflhaiyalpro981jvm-pro.dvi.
	7	Java Language Specification, clarifications, available at http:lljava.sun.comldocslbooksljlslclarify.html.
	8	T. Jensen , D. Le Métayer , T. Thorn, Security and Dynamic Class Loading in Java: A Formalization, Proceedings of the 1998 International Conference on Computer Languages, p.4, May 14-16, 1998
	9	Gary A. Kildall, A unified approach to global program optimization, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.194-206, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512945]
	10	The Kimera project, http://kimera.cs.washington.edu/
	11	Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
	12	Steven S. Muchnick, Advanced compiler design and implementation, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1998
	13	Tobias Nipkow , David von Oheimb, Java_light is type-safe—definitely, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.161-170, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268960]
	14	Qian, Zhenyu "A Formal Specification of JavaTM Virtual Machine Instructions," (Draft), http:/lwww.informatik.uni-bremen.de/~qian/absfsjvm.html, Nov. 1997.
	15	Raymie Stata , Martín Abadi, A type system for Java bytecode subroutines, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.149-160, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268959]
	16	Saraswat, V. "Java is not type safe," http ://www.research. att.com/--vj/bug.html
	17	Yellamraju V. Srinivas , Richard Jüllig, Specware: Formal Support for Composing Software, Mathematics of Program Construction, p.399-422, July 17-21, 1995
	18	Aaron Melvin Tenenbaum, Type determination for very high level languages., 1974
	19	Dennis M. Volpano , Geoffrey Smith, A Type-Based Approach to Program Security, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.607-621, April 14-18, 1997

CITED BY 19

	Zhenyu Qian , Allen Goldberg , Alessandro Coglio, A formal specification of Java class loading, ACM SIGPLAN Notices, v.35 n.10, p.325-336, Oct. 2000
	Nael B. Abu-Ghazaleh , Dhananjay S. Phatak, Verification caching: towards efficient and secure mobile code execution environments, Proceedings of the 2002 ACM symposium on Applied computing, March 11-14, 2002, Madrid, Spain
	Stephen N. Freund , John C. Mitchell, A formal framework for the Java bytecode language and verifier, ACM SIGPLAN Notices, v.34 n.10, p.147-166, Oct. 1999
	Stephen N. Freund , John C. Mitchell, The type system for object initialization in the Java bytecode language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.6, p.1196-1250, Nov. 1999
	Gerwin Klein , Tobias Nipkow, Verified bytecode verifiers, Theoretical Computer Science, v.298 n.3, p.583-626, 11 April 2003
	Stephen N. Freund , John C. Mitchell, A type system for object initialization in the Java bytecode language, ACM SIGPLAN Notices, v.33 n.10, p.310-327, Oct. 1998
	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
	Xavier Leroy, Java Bytecode Verification: Algorithms and Formalizations, Journal of Automated Reasoning, v.30 n.3-4, p.235-269, 2003
	G. Klein , M. Wildmoser, Verified Bytecode Subroutines, Journal of Automated Reasoning, v.30 n.3-4, p.363-398, 2003
	Philip W. L. Fong, Pluggable verification modules: an extensible protection mechanism for the JVM, ACM SIGPLAN Notices, v.39 n.10, October 2004
	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
	Marcel Winandy , Armin B. Cremers , Hanno Langweg , Adrian Spalka, Protecting Java component integrity against Trojan Horse programs, Integrity and internal control in information systems V, Kluwer Academic Publishers, Norwell, MA, 2003
	C. Bernardeschi , N. De Francesco , G. Lettieri , L. Martini , P. Masci, Decomposing bytecode verification by abstract interpretation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.31 n.1, p.1-63, December 2008
	Pieter H. Hartel , Luc Moreau, Formalizing the safety of Java, the Java virtual machine, and Java card, ACM Computing Surveys (CSUR), v.33 n.4, p.517-558, December 2001
	Zhenyu Qian, Standard fixpoint iteration for Java bytecode verification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.4, p.638-672, July 2000
	Gerwin Klein , Tobias Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.4, p.619-695, July 2006
	Christian Skalka, Type safe dynamic linking for JVM access control, Proceedings of the 9th ACM SIGPLAN international symposium on Principles and practice of declarative programming, July 14-16, 2007, Wroclaw, Poland
	Greg Morrisett , Karl Crary , Neal Glew , David Walker, Stack-based typed assembly language, Journal of Functional Programming, v.12 n.1, p.43-88, January 2002
	Thomas B. Preußer , Martin Zabel , Rainer G. Spallek, Enabling constant-time interface method dispatch in embedded Java processors, Proceedings of the 5th international workshop on Java technologies for real-time and embedded systems, September 26-28, 2007, Vienna, Austria