Standard fixpoint iteration for Java bytecode verification

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 nonstandard 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