Java programs are commonly transmitted across a network in the compiled bytecode representation and are then executed by a Java Virtual Machine. Since bytecode may be written by hand, or corrupted during network transmission, the Java Virtual Machine contains a bytecode verifier that performs a number of consistency checks before code is run. These checks include type correctness, and, as illustrated by previous attacks on the Java Virtual Machine, they are critical to maintain system security.
In order to study the process of verification for a language like Java bytecodes, we have developed a precise specification of a statically-correct bytecode language. This specification takes the form of a type system, and the language features examined include classes, interfaces, constructors, methods, exceptions, and bytecode subroutines.
This talk describes the methodology used to develop the formal system and its benefits. In addition, we describe a prototype implementation of a type checker for our system and discuss some applications of this work. For example, we may augment the type system to check for other program properties, such as the correct use of object locks. This work has also helped to clarify the original bytecode verifier specification, uncovered a security flaw in the Sun verifier implementation, and points to ways in which the Java bytecode language may be simplified and extended.