Stephen N. Freund
John C. Mitchell
ABSTRACT
In the standard Java implementation, a Java language program is compiled to Java bytecode. This bytecode may be sent across the network to another site, where it is then interpreted by the Java Virtual Machine. Since bytecode may be written by hand, or corrupted during network transmission, the Java Virtual Machine contains a bytecode verifier that performs a number of consistency checks before code is interpreted. As illustrated by previous attacks on the Java Virtual Machine, these tests, which include type correctness, are critical for system security. In order to analyze existing bytecode verifiers and to understand the properties that should be verified, we develop a precise specification of statically-correct Java bytecode, in the form of a type system. Our focus in this paper is a subset of the bytecode language dealing with object creation and initialization. For this subset, we prove that for every Java bytecode program that satisfies our typing constraints, every object is initialized before it is used. The type system is easily combined with a previous system developed by Stata and Abadi for bytecode subroutines. Our analysis of subroutines and object initialization reveals a previously unpublished bug in the Sun JDK bytecode verifier.
- AG96.Ken Arnold and James Gosling. The Java Programming Language. Addison-Wesley, 1996.]] Google Scholar
Digital Library
- Coh97.Rich Cohen. Defensive Java Virtual Machine Version 0.5 alpha Release. Available from ht tp: / / www. c I i. corn/software / djvm/index, ht m 1, November 1997.]]Google Scholar
- DE97.S. Drossopoulou and S. Eisenbach. Java is type safe ---probably. In European Conference On Object Oriented Programming, pages 389-418, 1997.]]Google ScholarCross Ref
- DFW96.Drew Dean, Edward W. Felten, and Dan S. Wallach. Java security: from Hot Java to netscape and beyond. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy, pages 190-200, 1996.]] Google ScholarDigital Library
- Gol98.Allen Goldberg. A specification of java loading and bytecode verification. In Proceedings of the Fifth A CM Conference on Computer and Communications Security, 1998. Available from http: //www. kest rel.edu/~ goldberg.]] Google ScholarDigital Library
- HT98.Masami Hagiya and Akihiko Tozawa. On a new method for dataflow analysis of Java Virtual M achi ne subroutines. Available from http://nicosia.is.s.utokyo.ac.j p/members/hagiya.html. A preliminary version appeared in SIG-Notes, PRO-17-3, Information Processing Society of Japan, 1998.]]Google Scholar
- Lia97.Sheng Liang. personal communication, November 1997.]]Google Scholar
- LY96.Tim Lindholm and Frank Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996.]] Google ScholarDigital Library
- MCGW98.Greg Morrisett, Karl Crary, Neal Glew, and David Walker. From system F to typed assembly language. In Proc. PSth A CM Symposium on Principles of Pro- 9rammin9 Languages, January 1998.]] Google ScholarDigital Library
- NvO98.qbbias Nipkow and David yon Oheimb. Javatight is Type-Safe- Definitely. In Proc. 25th A CM Symposium on Principles of Programming Languages, January 1998.]] Google ScholarDigital Library
- PV98.Joachim Posegga and Harald Vogt. Byte code verification for java smart cards based on model checking. In 5th European Symposium on Research in Computer Security (ESORICS), Louvain-la-Neuve, Belgium, 1998. Springer LNCS.]] Google ScholarDigital Library
- Qia98.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. Springer-Verlag, 1998.]] Google ScholarDigital Library
- SA98.Raymie Stata and Martfn Abadi. A type system for Java bytecode subroutines. In Proc. 25th A CM Symposium on Principles o/ Programming Languages, January 1998.]] Google ScholarDigital Library
- Sar97.Vijay Saraswat. The Java bytecode verification problem. Available from http://www.research.att.com/'vj, November 1997.]]Google Scholar
- SMB97.Emin Grin Sirer, Sean McDirmid, and Brian Betshad. Kimera: A java system architecture. Available from http://kimera.cs.washington.edu, November 1997.]]Google Scholar
- Sym97.Don Syme. Proving Java type soundness. Technical Report 427, University of Cambridge Computer Laboratory Technical Report, 1997.]]Google Scholar
- TMC+96.D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A type-directed optimizing compiler for ML. A CM SIGPLAN Notices, 31(5):181-192, May 1996.]] Google ScholarDigital Library
Index Terms
- A type system for object initialization in the Java bytecode language
Recommendations
A type system for object initialization in the Java bytecode language
In the standard Java implementation, a Java language program is compiled to Java bytecode. This bytecode may be sent across the network to another site, where it is then executed by the Java Virtual Machine. Since bytecode may be written by hand, or ...
A type system for object initialization in the Java bytecode language
In the standard Java implementation, a Java language program is compiled to Java bytecode. This bytecode may be sent across the network to another site, where it is then interpreted by the Java Virtual Machine. Since bytecode may be written by hand, or ...
Comments