As Chapter 2 describes, one of the essential pieces of the Java security model is the Verifier, which is responsible for checking the integrity of a class file and its byte code. Each VM, including the VM in your browser, has its own version of the Verifier. Thus the Verifier acts as a kind of independent verification mechanism to double-check the integrity of mobile Java that arrives from unknown parts.
The University of Washington's Kimera Project, led by Professor Brian Bershad, implemented a clean-room Verifier as part of a larger mobile code architecture experiment. The main idea behind the Kimera Project is to centralize Verification of byte code instead of having a Verifier running on each client. Their aims in creating a Verifier were to make it small, simple, and able to work independently. The discussion here is distilled from extensive Kimera Web documentation, which can be found at kimera.cs.washington.edu.
After creating their Verifier, the Kimera Project team wanted to test it to make sure it performed in a secure and robust manner. The question was, how to do this? The answer to that question led to an empirical demonstration that the Kimera Verifier was safer than many commercial Verifiers then in widespread use.
Most commercial Verifiers perform security checks in a series of stages that are distributed throughout the VM architecture. In particular, Chapter 2 describes how verification is traditionally broken into static and runtime processes. By contrast, the Kimera Verifier packages a complete verification system as one single component. An added bonus to the Kimera Verifier is the inclusion of a number of safety axioms distilled by the Kimera Project from the Java VM specification. This has the advantage of allowing the Kimera Verifier to be checked for correctness in a more thorough manner than the code for commercial Verifiers.
The Kimera Verifier aligns closely with class file verification as described in the VM specification. That means the process of verification is logically divided into four stages (see Chapter 2 for more on these stages):
According to this paradigm, whenever results from a number of distinct Verifiers disagree, further investigation into the cause of the disagreement is warranted. The obvious problem with this approach is that if all Verifiers perform equally incorrectly on a test case, nothing suspicious will be observed, and all Verifiers will be incorrectly thought to have done the right thing. Regardless of that serious flaw, the Kimera test suite was able to identify a large number of errors in commercial Verifiers, which led to correction of the Kimera Verifier throughout its testing.
The Kimera testing paradigm has much in common with N-version programming, in which N distinct versions of a piece of software are run simultaneously and a vote determines the final result. (For more on N-version programming see [Voas and McGraw, 1998].) We believe Kimera's testing methodology is a glimpse at the future of testing. Given the vast computational resources of today, there is no reason not to automate testing to a much greater extent than was feasible just a few years ago. Traditional metrics, such as test coverage, can be used to gauge the efficacy of such automated testing.
In April of 1997, the Kimera Project announced the discovery of 24 flaws in Sun's Verifier implementations and 17 flaws in Microsoft's Internet Explorer. Because Netscape's Verifier is very closely based on the one in Sun's JDK, it is safe to assume that most of the 24 flaws in Sun's Verifier exist in Netscape's as well (in fact, testing confirmed this). As we detail next, the flaws can be divided into several categories: security holes, weaknesses, and ambiguities.
The most serious flaw was a type-safety error that allowed a number to be converted into a pointer to any object in the VM. An attack applet based on this flaw could gain access to privileged information or otherwise force an illegal operation. As we describe in Chapter 2, type-confusion errors of the sort that this bug could lead to can be used to circumvent Java's security mechanisms entirely. This flaw allowed applets to assign a long or a double into an object reference, which can in turn be used to forge pointers inside the VM. Both JDK 1.0.2 and Netscape's Navigator Gold 3.01 included this bug.
Five other type-safety problems were also discovered in Sun's Verifier. One of these errors prompted Sun's security patch. This flaw, which existed in JDK 1.1.1 and JDK 1.0.2, involved the fact that a method can declare its maximum number of locals to be N, but take M arguments in its signature, where M can be greater than N. A description of the type-safety problems can be found at kimera.cs.washington.edu/flaws/sunflaws0423.html.
Besides the type-safety flaws, 11 access-flag flaws were identified. One example of such a flaw found in JDK 1.1.1 and JDK 1.0.2 is a flaw in which access flags for some methods are unrestricted. A properly constructed attack might be able to affect type safety and lead to a type-confusion attack. Once again, more information is available on the Kimera Web site. Finally, seven flaws can be classified as instruction or class file validity problems. The most serious of these flaws, found in JDK 1.0.2, was a problem whereby the class namespace management system could become confused by malformed classnames.
The most serious flaw was the same flaw discovered in the JDK implementation: the ability to assign a long or a double into an object reference. This flaw prompted the security patch. A list briefly explaining of all the flaws can be found at kimera.cs.washington.edu/flaws/msflaws0423.html.
One of the most interesting things about the Verifier bugs discovered by the Kimera group was the way in which the news broke in the press. Somehow, Sun was able to stage a preemptive PR strike before the Kimera announcement was even made. Their version of the story, which was later changed to more closely align with reality, was covered in the Wall Street Journal. In particular, the Sun announcement focused on only one of the many bugs.
The importance of type safety to the Java security model was also reemphasized by the Kimera Project findings. Sun claimed that many problems in the type system might lead to a denial-of-service attack through a crash, but did not acknowledge that it is often trivial to turn these crashes into more insidious type-confusion attacks. The next Java security hole, also discovered by the Kimera Project, served to bring that point home.
Copyright ©1999 Gary McGraw and Edward Felten.