| In the standard Java implementation, a Java language program is compiled to bytecode. This bytecode may be sent across the network to another site, where it is then executed by the 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 for system security. However, there is no existing specification which fully captures how Java bytecodes must be type checked.; In order to analyze verification of such a language and to understand the properties that should be checked to preserve system security, we develop a precise specification of statically-correct Java bytecode, in the form of a type system. We study a subset of the bytecode language including classes, interfaces, constructors, methods, exceptions, and byte-code subroutines. We also describe a prototype implementation of a type checker for our system and discuss some applications of this work. For example, we show how to extend our formal system to check other program properties, such as the correct use of object locks.; This work has helped to clarify the original bytecode verifier specification, uncovered a security flaw in the Sun verifier implementation, and points to ways in which the bytecode language may be simplified and extended. |
