JVM Dataflow abstract
Standard Fixpoint Iteration for Java Bytecode Verification
Abstract
Java bytecode verification forms the basis for Java-based Internet security and needs a rigorous description. One important aspect of bytecode verification is to check if a Java Virtual Machine (JVM) program is statically well-typed. So far several formal specifications have been proposed to define what the static well-typedness means.
This paper takes a step further and presents a chaotic fixpoint iteration, which represents a family of fixpoint computation strategies to compute a least type for each JVM program within a finite number of iteration steps. Since a transfer function in the iteration is not monotone, we choose to follow the example of a non-standard fixpoint theorem, which requires that all transfer functions are increasing, and monotone in case the bigger element is already a fixpoint. The resulting least type is the artificial top element if and only if the JVM program is not statically well-typed. The iteration is standard and close to Sun’s informal specification and most commercial bytecode verifiers.
(This paper supersedes two old papers at this place with the titles “Constraint-Based Specification and Dataflow Analysis for Java(TM) Bytecode Verification” and “Least Types for Memory Locations in (Java) Bytecode”.)