Java Project

Team:

Bytecode verification and class loading are the components of the Java Virtual Machine (JVM) that enforce type safety. Type safety is the basis of Java security.

We have developed a complete formalization of bytecode verification. Our formalization includes several improvements to Sun’s specification and implementation of the bytecode verifier. See [1, 2, 3] for preliminary, partial formalizations (our final formalization differs from them in some aspects).

We have written this formalization in Specware and we have refined it to a running implementation, which has been successfully tested on several thousands of Java classes. See [4] for a description of a preliminary version of our bytecode verifier (our final version differs from it in some aspects).

We have devised a novel technique to verify bytecode with subroutines. Subroutines constitute the most complex aspect of bytecode verification. Existing bytecode verifiers reject certain programs with subroutines generated by mundane compilers. Our technique is very simple yet powerful, and it accepts arguably all code produced by compilers. See [11, 12].

We have studied the subtleties of checking access to protected members in the JVM. See [13, 14].

We have found some subtle bugs in the bytecode verifier of Java 2 SDK (versions 1.2, 1.3, and 1.4) that lead to type safety violations. See [7, 8, 14].

We have analyzed in detail Sun’s specification of bytecode verification and proposed several improvements. See [9, 10].

We have formalized the class loading mechanisms of the JVM, including multiple class loaders, interaction with bytecode verification, and invocation of user code that realizes customized loading policies. We have proved type safety results of this formalization. See [5 ,6].

Publications:

  1. A Specification of Java Loading and Bytecode Verification
    Allen Goldberg
    October 1998
    5th ACM Conference on Computer and Communications Security (CCS'98), pages 49-58
    {A specification of some salient aspects of bytecode verification and class loading, in a data flow analysis framework. This work is the basis of the preliminary version of our bytecode verifier in Specware described in [4].}
  2. A Formal Specification of Java Virtual Machine Instructions for Objects, Methods and Subroutines
    Zhenyu Qian
    1999
    Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science, pages 271-312
    {A specification of several bytecode instructions, comprehensive of operational semantics and bytecode verification. Concepts from this work have been used in the development of our bytecode verifier in Specware.}
  3. Standard Fixpoint Iteration for Java Bytecode Verification
    Zhenyu Qian
    July 2000
    ACM Transactions on Programming Languages and Systems (TOPLAS), 22(4):638-672
    {A solution to the non-monotonicity problem that arises in typical data flow formulations of bytecode verification, based on [2].}
  4. Towards a Provably-Correct Implementation of the JVM Bytecode Verifier
    Alessandro Coglio, Allen Goldberg, and Zhenyu Qian
    October 1998
    OOPSLA'98 Workshop on the Formal Underpinnings of Java
    {A description of a preliminary version of our bytecode verifier in Specware, based on [1]. The architecture of our current, complete bytecode verifier is slightly different, closer to Sun’s. This paper also appears in DARPA Information Survivability Conference and Exposition (DISCEX'00), volume 2, pages 403-410, IEEE Computer Society Press, January 2000, as well as in 1st NSA Conference on High Confidence Software and Systems, March 2001.}
  5. A Formal Specification of Java Class Loading
    Zhenyu Qian, Allen Goldberg, and Alessandro Coglio
    April 2000, revised July 2000
    Technical Report, Kestrel Institute
    {A complete formalization and type safety proof for an abstraction of the JVM with all the essential features of class loading, plus an improvement over Sun’s design. An overview of the formalization and proof is contained in [6].}
  6. A Formal Specification of Java Class Loading
    Zhenyu Qian, Allen Goldberg, and Alessandro Coglio
    October 2000
    15th ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'00), volume 35, number 10 of ACM SIGPLAN Notices, pages 325-336
    {An overview of the formalization and proof in [5], augmented with additional informal descriptions and examples.}
  7. Type Safety in the JVM: Some Problems in JDK 1.2.2 and Proposed Solutions
    Alessandro Coglio and Allen Goldberg
    June 2000
    2nd ECOOP Workshop on Formal Techniques for Java Programs
    {An overview of the bugs we found in Sun’s bytecode verifier, with a detailed desciption of one of them, along with solutions. A description of all the bugs we found and of solutions to them is contained in [8].}
  8. Type Safety in the JVM: Some Problems in Java 2 SDK 1.2 and Proposed Solutions
    Alessandro Coglio and Allen Goldberg
    November 2001
    Concurrency and Computation: Practice and Experience, 13(13):1153-1171
    {A complete description of all the bugs we found in Sun’s bytecode verifier, along with solutions. An overview, with details about only one of the bugs, is contained in [7]. This paper supersedes the Kestrel Technical ReportType Safety in the JVM: Some Problems in JDK 1.2.2 and Proposed Solutions of April 2000. Source code, compilation instructions, and class files to demonstrate the bugs are available here .}
  9. Improving the Official Specification of Java Bytecode Verification
    Alessandro Coglio
    June 2001
    3rd ECOOP Workshop on Formal Techniques for Java Programs
    {Preliminary version of [10].}
  10. Improving the Official Specification of Java Bytecode Verification
    Alessandro Coglio
    February 2003
    Concurrency and Computation: Practice and Experience, 15(2):155-179
    {A comprehensive analysis of Sun’s specification of bytecode verification and a comprehensive plan for improvement. A preliminary version is [9].}
  11. Simple Verification Technique for Complex Java Bytecode Subroutines
    Alessandro Coglio
    June 2002
    4th ECOOP Workshop on Formal Techniques for Java-like Programs
    {An overview of our novel technique to verify subroutines and its comparison with related work. The full formalization of the technique, including proofs, is contained in [12].}
  12. Simple Verification Technique for Complex Java Bytecode Subroutines
    Alessandro Coglio
    June 2004
    Concurrency and Computation: Practice and Experience, 16(7):647-670
    {A formalization of our novel technique to verify subroutines, including proofs of its properties and comparison with related work. An overview of this material can be found in [11]. This paper supersedes the Kestrel Technical ReportSimple Verification Technique for Complex Java Bytecode Subroutines of December 2001, revised May 2002.}
  13. Checking Access to Protected Members in the Java Virtual Machine
    Alessandro Coglio
    June 2004
    6th ECOOP Workshop on Formal Techniques for Java-like Programs
    {A detailed analysis of the requirements on protected member access in the Java Virtual Machine and how to check them. Examples of incorrect checking in Sun’s Java 2 SDK version 1.4 are in [14].}
  14. Checking Access to Protected Members in the Java Virtual Machine
    Alessandro Coglio
    October 2005
    Journal of Object Technology
    {Detailed analysis of the requirements on protected member access in the Java Virtual Machine and how to check them; examples of incorrect checking in Sun’s Java 2 SDK version 1.4. A shorter version is [13]. This paper supersedes the Kestrel Institute Technical ReportChecking Access to Protected Members in the Java Virtual Machine of February 2004.}