A formal specification of Java class loading

ABSTRACT

The Java Virtual Machine (JVM) has a novel and powerful mechanism to support lazy, dynamic class loading according to user-definable policies. Class loading directly impacts type safety, on which the security of Java applications is based. Conceptual bugs in the loading mechanism were found in earlier versions of the JVM that lead to type violations. A deeper understanding of the class loading mechanism, through such means as formal analysis, will improve our confidence that no additional bugs are present.The work presented in this paper provides a formal specification of (the relevant aspects of) class loading in the JVM and proves its type safety. Our approach to proving type safety is different from the usual ones since classes are dynamically loaded and full type information may not be statically available. In addition, we propose an improvement in the interaction between class loading and bytecode verification, which is cleaner and enables lazier loading.

REFERENCES

• 1: E. Borger and W. Schulte. Modular design for the Java virtual machine architecture. ftp://ftp.di.unipi.it/pub/Papers/boerger/ jvmarch.ps, 1999.
• 2: G. Bracha. A critique of 'Security and dynamic loading in Java: A formalisation'. http://java.sun.com/people/gbracha /critique-jmt.html, 1999.
• 3: Luca Cardelli, Program fragments, linking, and modularization, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.266-277, January 15-17, 1997, Paris, France [doi>10.1145/263699.263735]
• 4: A. Coglio and A. Goldberg. Type safety in the JVM: Some problems in JDK 1.2.2 and proposed solutions. In Proc. ECOOP Workshop on Formal Techniques for Java Programs, 2000. Long version available at http://www.kestrel.edu/java.
• 5: A. Coglio, A. Goldberg, and Z. Qian. Towards a provably-correct implementation of the JVM bytecode verifier. In Proc. OOPSLA'98 Workshop Formal Underpinnings of Java, 1998.
• 6: Drew Dean, The security of static typing with dynamic linking, Proceedings of the 4th ACM conference on Computer and communications security, p.18-27, April 01-04, 1997, Zurich, Switzerland [doi>10.1145/266420.266428]
• 7: S. Drossopoulou. Towards an abstract model of Java dynamic linking and verification. Department of Computing, Imperial College, London, UK.
• 8: Philip W. L. Fong , Robert D. Cameron, Proof linking: an architecture for modular verification of dynamically-linked mobile code, Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, p.222-230, November 01-05, 1998, Lake Buena Vista, Florida, United States
• 9: Formal Methods Program - SRI Computer Science Laboratory. The PVS specification and verification system. http://pvs.csl.sri.com/, 1999.
• 10: Neal Glew , Greg Morrisett, Type-safe linking and modular assembly language, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.250-261, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292563]
• 11: 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]
• 12: Li Gong, Inside Java 2 platform security architecture, API design, and implementation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 13: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 14: T. Jensen , D. Le Métayer , T. Thorn, Security and Dynamic Class Loading in Java: A Formalization, Proceedings of the 1998 International Conference on Computer Languages, p.4, May 14-16, 1998
• 15: Sheng Liang , Gilad Bracha, Dynamic class loading in the Java virtual machine, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.36-44, October 18-22, 1998, Vancouver, British Columbia, Canada
• 16: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 17: Zhenyu Qian, Standard fixpoint iteration for Java bytecode verification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.4, p.638-672, July 2000 [doi>10.1145/363911.363915]
• 18: 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
• 19: Z. Qian, A. Goldberg, and A. Coglio. A formal specification of JavaTM class loading. Long version. http://www.kestrel.edu/java, 2000.
• 20: V. Saraswat. Java is not type-safe. Technical report, AT&T Research, 1997. http://www.research.att.com/~vj/bug.html.
• 21: A. Tozawa and M. Hagiya. Careful analysis of type spoofing. In JIT'99 Java-Informations-Tage 1999, Clemens H. Cap, Hrsg., Informatik aktuell, pages 290-296. Springer Verlag, 1999.
• 22: A. Tozawa and M. Hagiya. New formalization of the JVM. http://nicosia.is.s.u-tokyo.ac.jp/members /miles/papers/cl-99.ps, 1999.

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.4 Processors
          Subjects: Compilers

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

General Terms:
Design, Languages, Performance, Theory