Most research on Java Bytecode Verification is focussed on the soundness of the bytecode verifier. From the security point of view it is important to know that bytecode which is accepted by the verifier does not violate type conditions at run-time. From the practical point of view it is also important to know that bytecode that is generated by a Java compiler from legal well-typed Java programs is accepted by the verifier afterwards. During an attempt to prove that a Java compiler generates verifiable code, however, we found examples of legal Java programs which are rejected by any Bytecode Verifier. The examples show that Java Bytecode Verification as it has been introduced by Sun is not possible. We propose therefore to restrict the so-called rules of definite assignment for the try-finally statement as well as for the labeled statement such that our example programs are no longer allowed. Then we can prove, using the framework of Abstract State Machines, that each program from the restricted Java language is verifiable by the Java Bytecode Verifier.

The slides of the talk are available here.