Treffer: Constraint-Based Specification and Dataflow Analysis for Java Bytecode Verification

(Java) bytecode verification should prevent various runtime errors in Java Virtual Machine (JVM) programs and play an important part in ensuring Java-based internet security. The official JVM specification is inadequate for security-critical applications. Recent research work has proposed using formal typing systems to specify bytecode verification. However, it is still unknown how to make an implementation, whose correctness and completeness with respect to the formal specification can be proved. This paper proposes an approach to bridging the gap. We first give formal typing rules enforcing formal constraints on types for memory locations in simplified legal JVM programs. Then we present a dataflow analysis algorithm (scheme) as a bytecode verifier, which non-deterministically uses the formal rules to compute the smallest types for memory locations that satisfy the constraints, or to report a failure if the computation fails. By formally proving the correctness, termination and co.