A type system for object initialization in the Java bytecode language

In the standard Java implementation, a Java language program is compiled to Java bytecode. This bytecode may be sent across the network to another sit e, where it is then executed by the Java Virtual Machine. Since bytecode ma y be written by hand, or corrupted during network transmission, the Java Vi rtual Machine contains a bytecode verifier that performs a number of consis tency checks before code is run. These checks include type correctness and, as illustrated by previous attacks on the Java Virtual Machine, are critic al for system security. In order to analyze existing bytecode verifiers and to understand the properties that should be verified, we develop a precise specification of statically correct Java bytecode, in the form of a type s ystem. Our focus in this article is a subset of the bytecode language deali ng with object creation and initialization. For this subset, we prove, that , for every Java bytecode program that satisfies our typing constraints, ev ery object is initialized before it is used. The type system is easily comb ined with a previous system developed by Stata and Abadi for bytecode subro utines. Our analysis of subroutines and object initialization reveals a pre viously unpublished bug in the Sun JDK bytecode verifier.