A specification of Java loading and bytecode verification

Abstract

This paper gives a mathematical specification the Java Virtual Machine (JVM) bytecode verifier. The specification is an axiomatic description of the verifier that makes precise subtle aspects of the JVM semantics and the verifier. We focus on the use of data flow analysis to verify type-correctness and the use of typing contexts to insure global type consistency in the context of an arbitrary strategy for dynamic class loading. The specification types interfaces with sufficient accuracy to eliminate run-time type checks. Our approach is to specify a generic dataflow architecture and formalize the JVM verifier as an instance of this architecture. The emphasis in this paper is on readability of the specification and mathematical clarity. The specification given is consistent with the descriptions in the Lindholm's and Yellin's The Java™ Virtual Machine Specification. It less committed to certain implementation choices than Sun's version 1.1 implementation. In particular, the specification does not commit an implementation to any loading strategy, and detects all type errors as early as possible.