A type system for object initialization in the Java bytecode language

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.

REFERENCES

• AG96: Ken Arnold , James Gosling, The Java programming language (2nd ed.), ACM Press/Addison-Wesley Publishing Co., New York, NY, 1998
• 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.
• DE97: S. Drossopoulou and S. Eisenbach. Java is type safe ---probably. In European Conference On Object Oriented Programming, pages 389-418, 1997.
• DFW96: D. Dean , Felten , Wallach, Java Security: From HotJava to Netscape and Beyond, Proceedings of the 1996 IEEE Symposium on Security and Privacy, p.190, May 06-08, 1996
• Gol98: Allen Goldberg, A specification of Java loading and bytecode verification, Proceedings of the 5th ACM conference on Computer and communications security, p.49-58, November 02-05, 1998, San Francisco, California, United States [doi>10.1145/288090.288104]
• 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.
• Lia97: Sheng Liang. personal communication, November 1997.
• LY96: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• MCGW98: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-97, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268954]
• NvO98: 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]
• PV98: Joachim Posegga , Harald Vogt, Byte Code Verification for Java Smart Card Based on Model Checking, Proceedings of the 5th European Symposium on Research in Computer Security, p.175-190, September 16-18, 1998
• Qia98: Zhenyu Qian, A Formal Specification of Java Virtual Machine Instructions for Objects, Methods and Subrountines, Formal Syntax and Semantics of Java, p.271-312, January 1999
• SA98: 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]
• Sar97: Vijay Saraswat. The Java bytecode verification problem. Available from http://www.research.att.com/'vj, November 1997.
• SMB97: Emin Grin Sirer, Sean McDirmid, and Brian Betshad. Kimera: A java system architecture. Available from http://kimera.cs.washington.edu, November 1997.
• Sym97: Don Syme. Proving Java type soundness. Technical Report 427, University of Cambridge Computer Laboratory Technical Report, 1997.
• TMC+96: D. Tarditi , G. Morrisett , P. Cheng , C. Stone , R. Harper , P. Lee, TIL: a type-directed optimizing compiler for ML, ACM SIGPLAN Notices, v.31 n.5, p.181-192, May 1996

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Java

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Design, Languages, Performance, Theory, Verification