A Specification of Java Loading and Bytecode Verification

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 JavaTM Virtual

• Type: Conference
• Year: 1998
• Where: CCS
• Authors: Allen Goldberg
• Keywords: CCS 1998, JVM Verifier, Security Privacy, Specification, Verifier