A TYPE SYSTEM FOR OBJECT INITIALIZATION IN THE JAVA(TM) BYTECODE LANGUAGE

In the standard Java implementation, a Java language program is compil ed to Java bytecode. This bytecode may be sent across the network to a nother site, where it is then interpreted by the Java Virtual Machine. Since bytecode may be written by hand, or corrupted during network tr ansmission, the Java Virtual Machine contains a bytecode verifier that performs a number of consistency checks before code is interpreted. A s illustrated by previous attacks on the Java Virtual Machine, these t ests, which include type correctness, are critical for system security . In order to analyse existing bytecode verifiers and to understand th e properties that should be verified, we develop a precise specificati on of statically-correct Java bytecode, in the form of a type system. Our focus in this paper is a subset of the bytecode language dealing w ith object creation and initialization. For this subset, we prove that for every Java bytecode program that satisfies our typing constraints , every object is initialized before it is used. The type system is ea sily combined with a previous system developed by Stata and Abadi for bytecode subroutines. Our analysis of subroutines and object initializ ation reveals a previously unpublished bug in the Sun JDK bytecode ver ifier.