Paper on type-safety bugs in JDK1.2.2

The following paper is available under http://www.kestrel.edu/java.

 Alessandro Coglio

 Kestrel Institute
 3260 Hillview Avenue, Palo Alto, CA 94304

Type Safety in the JVM: Some Problems in JDK 1.2.2 and Proposed

In the course of our efforts to formalize various components of the JVM,
we have uncovered subtle bugs in Sun JDK 1.2.2 that lead to type safety
violations. These bugs are in the bytecode verifier and relate to the
naming of reference types. We found that in certain circumstances these
names can be spoofed by suitable use of delegating class loaders. Since
the JVM specification is informal English prose, we cannot crisply
characterize these bugs as errors in the specification or just in one or
more implementations. However, some of these bugs are consistent with a
reasonable interpretation of the specification. We have verified that
the bugs exist in Sun JDK 1.2.2 (on both Solaris and Windows NT). Some
are fixed in Sun JDK 1.3 Beta by restricting access to system packages.
Overall, these flaws raise the issue of a more precise specification of
the bytecode verifier and the loading mechanisms, and increased
assurance of type safety properties. We propose fixes of all the bugs,
and discuss a more general approach to insuring type safety that has
additional advantages, including lazier class loading.