Michael Jones, PhD

1. Main problem:
When a user downloads a java program, the JVM performs a static analysis of the byte code to ensure that the byte code meets certain requirements required to securely execute the byte code on the host JVM. This is usually done by a polynomial dataflow analysis algorithm. The paper explores potentially exponential model checking algorithms for doing the same thing. The problem with the dataflow algorithm is that it marks certain kinds of valid programs as invalid (such as classes that use "subroutines in different contexts"). Using a model checker to do the bytecode verification results in a precise characterization of valid and invalid programs but requries more time and space. This is useful in settings where precise correctness is important, but time and space resources are not. In some settings, such a JVMs for smart cards, the bytecode verification is done off-line and signed. This is an application in which model checking for bytecode verification makes sense.

2. Approach to solving the problem.
For each Java bytecode instruction, define an abstract operation that modifies the JVM state visible to the type system. The type system keeps track of the program counter, the stack and the registers. Each instruction is translated into its effect on the current type. Thus instruction execution is simply traversal through a set of types. This solves problems with multiple inheritance (for each type, take its maximal supertype and call that the current type. That's hard if a type has several different super types) and multiple return values. The verification works by checking that certain type safety conditions, like the stack doesn't overflow, hold at every program point. In SPIN, this is done by checking "always type-safe". Here's some sample promela code they've generated:

proctype transitions( ) {
do
:: pc==0 -> atomic { opst[opst_ptr]=loc[1]; opst_ptr=opst_ptr+1; pc=1 };
:: pc==2 -> atomic { opst[opst_ptr]=13; opst_ptr=opst_ptr+1; pc=3 };
:: pc==3 -> atomic { break };

3. What is the authors claim about their approach?
Claim #1 Model checking for byte code verification is slower but more accurate than static analysis. Claim #2 Explicit state ennumeation is more efficient for this problem than symbolic methods.

4. How do the authors support their claim?
By verifying the byte code for all the methods in the java.lang package.