A Type System for Java Bytecode Subroutines

8 years 9 months ago
A Type System for Java Bytecode Subroutines
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. This paper proposes using typing rules to describe the bytecode verifier because they are more precise than prose, clearer than code, and easier to reason about than either. JVML has a subroutine construct used for the compilation of Java’s try-finally statement. Subroutines are a major source of complexity for the bytecode verifier because they are not obviously last-in/first-out and because they require a kind of polymorphism. Focusing on subroutines, we isolate an interesting, small subset of JVML. We give typing rules for this subset and prove their correctness. Our type system constitutes a sound basis for bytecode verification an...
Raymie Stata, Martín Abadi
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where POPL
Authors Raymie Stata, Martín Abadi
Comments (0)