Treffer: Least Types for Memory Locations in Java Bytecode

(Java) bytecode verification should ensure type-safety for Java Virtual Machine (JVM) programs (bytecode) and form a basis for Java-based internet security. Recent research work has proposed using formal typing rules to enforce constraints on types for memory locations in bytecode and thus formally specify (part of) bytecode verification. In this paper, we take one step forward and show that typing rules can be non-deterministically and repeatedly used in an arbitrary order to compute the least types for memory locations satisfying the constraints, if there are any, or to report a failure, if there are none. The result implies that theoretically a bytecode verifier can have any strategy visiting program points in bytecode without affecting the acceptance of bytecode, i.e. without causing denial of services provided by bytecode. It also suggests ways to implement bytecode verification directly using formal specification. 1 Introduction Java programs are usually compiled into Java b.