A type system for Java bytecode subroutines

Java is typically compiled into an intermediate language, JVML, that is int erpreted by the Java Virtual Machine. Because mobile JVML code is not alway s trusted, a bytecode verifier enforces static constraints that prevent Var ious dynamic errors. Given the importance of the bytecode verifier for secu rity, its current descriptions are inadequate. This article proposes using typing rules to describe the bytecode verifier because they are more precis e than prose, clearer than code, and easier to reason about than either. JV ML has a subroutine construct which is used for the compilation of Java's t ry-finally statement. Subroutines are a major source of complexity for the bytecode verifier because they are not obviously last-in/first-out and beca use they require a kind of polymorphism. Focusing on subroutines, we isolat e an interesting, small subset of JVML. We give typing rules for this subse t and prove their correctness. Our type system constitutes a sound basis fo r bytecode verification and a rational reconstruction of a delicate part of Sun's bytecode verifier.