Results We have developed a complete formalization of bytecode verification and proved type safety properties on it. Our formalization includes several improvements to Sun's specification and implementation of the bytecode verifier. A paper containing this formalization will appear shortly. We have written this formalization in Specware and we have refined it to a running implementation, which has been successfully tested on more than 4,000 Java classes. We have devised novel techniques to verify bytecode with subroutines.
Subroutines constitute the most complex aspect of bytecode verification.
Our techniques are much simpler to understand and implement, and accept more type-safe bytecode than Sun's and other approaches. We have also studied in detail the approach implemented by Sun, and found formal evidence that it does guarantee type safety. A paper on these topics will appear shortly. We have found some subtle bugs in the bytecode verifier of Java 2 SDK vers. 1.2 that lead to type safety violations.