A type system for Java bytecode subroutines

ABSTRACT

Java is typically compiled into an intermediate language, JVML, that is interpreted by the Java Virtual Machine. Because mobile JVML code is not always trusted, a bytecode verifier enforces static constraints that prevent various dynamic errors. Given the importance of the bytecode verifier for security, its current descriptions are inadequate. This article proposes using typing rules to describe the bytecode verifier because they are more precise than prose, clearer than code, and easier to reason about than either. JVML has a subroutine construct which is used for the compilation of Java's try-finally statement. Subroutines are a major source of complexity for the bytecode verifier because they are not obviously last-in/first-out and because they require a kind of polymorphism. Focusing on subroutines, we isolate an interesting, small subset of JVML. We give typing rules for this subset and prove their correctness. Our type system constitutes a sound basis for bytecode verification and a rational reconstruction of a delicate part of Sun's bytecode verifier.

REFERENCES

• 1: COHEN, R. M. 1997. Defensive Java Virtual Machine version 0.5 alpha release. Web pages at http ://www. cli. com/.
• 2: DROSSOPOULOU, S. AND EISENBACH, S. 1997. Java is type safe--probably. In Proceedings of ECOOP '97. Springer-Verlag, 389-418.
• 3: Stephen N. Freund , John C. Mitchell, A type system for object initialization in the Java bytecode language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.310-327, October 18-22, 1998, Vancouver, British Columbia, Canada
• 4: 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]
• 5: 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
• 6: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 7: MORRISETT, G. 1995. Compiling with types. Ph.D. thesis, Carnegie Mellon University.
• 8: MORRISETT, G., TARDITI, D., CHENG, P., STONE, C., HARPER, R., AND LEE, P. 1996. The TIL/ML compiler: Performance and safety through types. In Workshop on Compiler Support for Systems Software.
• 9: 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]
• 10: 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
• 11: SARASWAT, V. 1997. The Java bytecode verification problem. Web page at http://www.research art. com/~vj/bcv, html.
• 12: SIRER, E. G., MCDIRMID, S., AND BERSHAD, B. 1997. Kimera: A Java system security architecture. Web pages at http ://kimera. cs. washington, edu/.
• 13: SYME, D. 1997. Proving Java type soundness. Tech. Rep. 427, University of Cambridge Computer Laboratory. June.
• 14: TIC 1997. ACM SIGPLAN Workshop on Types in Compilation (TIC97).
• 15: YELLIN, F. 1997. Private communication.

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
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Invasive software (e.g., viruses, worms, Trojan horses)

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

General Terms:
Languages, Security, Theory, Verification

Keywords:
Java, bytecode verification