Typechecking JVML

In Java 6 (Mustang) we will be releasing a new version of the byte code verifier. For those of you living in blessed ignorance, the verifier is in essence a typechecker for machine language of the JVM, which I will refer to as JVML below.  

So why are we doing this? To make verification faster, simpler and more adaptable. The existing verifier performs type inference (more precisely,  type reconstruction). In JVML, types are declared for fields, formal parameters of methods and method return types - but not for local variables or the operand stack.  Hence, the verifier must infer the types of local variables and the operand stack based on how they are used. This is slow, memory intensive and very complicated.

The new scheme is rooted in research done by Eva Rose for her master's thesis a few years back.

The new verifier requires additional type declarations for local variables and the operand stack in JVML. As a consequence of this and other detailed changes, it doesn't need to infer them, and is about twice as fast, uses a fraction of the memory and is vastly simpler than the old verifier.

So increased speed and reduced space are obviously good. Simplicity is also obviously good, but looking at the software industry, it's clear that it worships complexity. An appreciation of simplicity for its own sake is sorely lacking. Most people need very concrete examples before they are willing to invest any effort for the sake of simplicity.

Here is one example of why this simplification might be useful. Let's imagine that at some point in time, it might be plausible (in terms of compatibility) to reify generics. Among many other issues, this entails verification of generics. It will be relatively straightforward to extend the new verifier to typecheck generics. Anyone who would seek to get the old verifier to do this is probably in need of clinical assistance.

In Mustang, javac will generate the necessary type information in the class files it produces. It won't generate code using jsr and ret either (nor will other tools Sun releases). Other vendors may need more time to catch up, which is why we will fall back to the old verifier for a while.

The spec for all this is being worked out as part of JSR202 where you can get a draft spec. You can also get more detail on practicalities in  Wei Tao's article on the typechecking verifier. Obviously, the verifier is critical to the security and integrity ofthe Java platform. Because of this, we'd like to get the community involved in banging on both the spec and the implementation. If there are any holes, we want to find them before the release.

To that end, Sun is asking for knowledgable people to have a go at cracking the new verification scheme. If you find a hole in the spec, you'll get recognized at the JavaOne 2006 conference. Honorable mention for finding holes in the implementation. Details should be available soon at the  Crack the Verifier Initiative   web page.
Comments:

Post a Comment:
  • HTML Syntax: NOT allowed
About

gbracha

Search

Categories
Archives
« April 2014
SunMonTueWedThuFriSat
  
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
   
       
Today
Feeds