Java is typically compiled into an intermediate language, JVML, that is interpreted by the Java Virtual Machine. Because mobile JVML code is not always trusted, a bytecode verifier enforces static constraints that prevent various dynamic errors. Given the importance of the bytecode verifier for security, its current descriptions are inadequate. We consider the use of typing rules to describe the bytecode verifier because they are more precise than prose, clearer than code, and easier to reason about than either. We explore the viability of this approach by developing a sound type system for a subset of JVML. Although this subset is small, it includes two of the main sources of complexity for the bytecode verifier: subroutines and object initialization.
(This talk describes joint work with Raymie Stata, and significant extensions of this work due to Stephen Freund and John Mitchell. Part of this material has just been presented at POPL 98.)