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 executed 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 run. These checks include type correctness and, as illus-trated by previous attacks on the Java Virtual Machine, 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 article 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 unpub-lished bug in the Sun JDK bytecode verifier.

REFERENCES

• 1: Ken Arnold , James Gosling, The Java programming language (2nd ed.), ACM Press/Addison-Wesley Publishing Co., New York, NY, 1998
• 2: COHEN, R. 1997. Defensive Java virtual machine version 0.5 alpha release. Available via http//www, cli. co m/so ftw are/djvm/in de x. html.
• 3: Sophia Drossopoulou , Susan Eisenbach , Sarfraz Khurshid, Is the Java type system sound?, Theory and Practice of Object Systems, v.5 n.1, p.3-24, Jan. 1999 [doi>10.1002/(SICI)1096-9942(199901/03)5:1<3::AID-TAPO2>3.0.CO;2-T]
• 4: Drew Dean , Edward W. Felten , Dan S. Wallach , Dirk Balfanz, Java security: Web browsers and beyond, Internet besieged: countering cyberspace scofflaws, ACM Press/Addison-Wesley Publishing Co., New York, NY, 1997
• 5: 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]
• 6: Masami Hagiya , Akihiko Tozawa, On a New Method for Dataflow Analysis of Java Virtual Machine Subroutines, Proceedings of the 5th International Symposium on Static Analysis, p.17-32, September 14-16, 1998
• 7: JONES, M. 1998. The functions of Java bytecode. In Proceedings of the Workshop on the Formal Underpinnings of the Java Paradigm.
• 8: Pietro Cenciarelli , Alexander Knapp , Bernhard Reus , Martin Wirsing, An Event-Based Structural Operational Semantics of Multi-Threaded Java, Formal Syntax and Semantics of Java, p.157-200, January 1999
• 9: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 10: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 11: 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]
• 12: Robert O'Callahan, A simple, comprehensive type system for Java bytecode subroutines, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.70-78, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292549]
• 13: 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
• 14: 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
• 15: 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]
• 16: SARASWAT, V. 1997. The Java bytecode verification problem. Available via http://www. research, att.com/-vj.
• 17: SIRER, E. G., MCDIRMID, S., AND BERSHAD, B. 1997. Kimera: A Java system architecture. Available via http://kimera.cs.washington.edu.
• 18: SYME, D. 1997. Proving Java type soundness. Tech. Rep. 427, Univ. of Cambridge Computer Laboratory.
• 19: 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
• 20: Phillip M. Yelland, A compositional account of the Java virtual machine, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.57-69, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292548]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Languages, Verification

Keywords:
Java, bytecode languages, object initialization, type checking