A formal framework for the Java bytecode language and verifier

ABSTRACT

This paper presents a sound type system for a large subset of the Java bytecode language including classes, interfaces, constructors, methods, exceptions, and bytecode subroutines. This work serves as the foundation for developing a formal specification of the bytecode language and the Java Virtual Machine's bytecode verifier. We also describe a prototype implementation of a type checker for our system and discuss some of the other applications of this work. For example, we show how to extend our work to examine other program properties, such as the correct use of object locks.

REFERENCES

• Ber98: Peter Bertelsen. Dynamic semantics of Java bytecode. In Workshop on Principles of Abstract Machines, September 1998.
• BS98: Egon Börger , Wolfram Schulte, A Programmer Friendly Modular Definition of the Semantics of Java, Formal Syntax and Semantics of Java, p.353-404, January 1999
• CGQ98: Alessandro Coglio, Allen Goldberg, and Zhenyu Qian. Toward a provably-correct implementation of the JVM bytecode verifier. In Workshop on the Formal Underpinnings of the Java Paradigm, October 1998.
• Coh97: Rich Cohen. Defensive Java Virtual Machine Version 0.5 Mpha Release. Available from http://www.cli.com/software/djvm/index.html, November 1997.
• Coo89: W.R. Cook. A proposal for making Eiffel typesafe. In European Conf. on Object-Oriented Programming, pages 57-72, 1989.
• CvE98: Grzegorz Czajkowski , Thorsten von Eicken, JRes: a resource accounting interface for Java, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.21-35, October 18-22, 1998, Vancouver, British Columbia, Canada
• DE97: S. Drossopoulou and S. Eisenbach. Java is type safe probably. In European Conference On Object Oriented Programming, pages 389-418, 1997.
• DFWB97: 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
• FA99: Cormac Flanagan , Martín Abadi, Types for Safe Locking, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.91-108, March 22-28, 1999
• FM98: 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
• FM99: Stephen Freund and John Mitchell. Specification and verification of Java bytecode subroutines and exceptions, August 1999. To appear as a Stanford University Technical Note. Currently available from http ://cs. stanford, edu/'freunds.
• Ghe99: Sanjay Ghemawat.srcjava.Available from http://www.research.digital.com/SRC/java, August 1999.
• 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]
• Jav99: Java-Powered Ring.Available from http://www.ibutton.com, March 1999.
• Jon98: Mark Jones. The functions of Java bytecode. In Workshop on the Formal Underpinnings of the Java Paradigm, October 1998.
• 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]
• Nec97: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 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]
• O’C99: 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]
• Pus99: Cornelia Pusch, Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.89-103, March 22-28, 1999
• 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(tin) Virtual Machine Instructions. In 3. Alves-Foss, editor, Formal Syntax and Semantics of Java. Springer Verlag LNCS 1523, 1998.
• Qia99: Zhenyu Qian. Least types for memory locations in (Java) bytecode. In Sixth Workshop on Foundations of Object-Oriented Languages, January 1999.
• Ros98: Eva Rose. Towards secure bytecode verification on a Java card. Master's thesis, University of Copenhagen, 1998.
• RR98: Eva Rose and Kristoffer Hogsbro Rose. Toward a provably-correct implementation of the JVM bytecode verifier. In Workshop on the Formal Underpinnings of the Java Paradigm, October 1998.
• SA99: 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]
• SMB97: Emin Grin Sirer, Scan McDirmid, and Brian Bershad. Kimera: A Java system architecture. Available from http://kimera.cs.washington.edu, November 1997.
• Sym97: Don Syme. Proving Java type soundness. Technieat 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
• WF98: Dam S. Wallach and Edward W. Felten. Understanding Java stack inspection. In Proceedings of IEEE Symposium on Security and Privacy, May 1998.
• XP99: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]
• Yel99: 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
      D.3.2 Language Classifications

          Nouns: Java

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Frameworks

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

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