A Type System for Java Bytecode Subroutines

13 years 8 months ago

Download www.eecs.umich.edu

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 veriﬁer enforces static constraints that prevent various dynamic errors. Given the importance of the bytecode veriﬁer for security, its current descriptions are inadequate. This paper proposes using typing rules to describe the bytecode veriﬁer 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-ﬁnally statement. Subroutines are a major source of complexity for the bytecode veriﬁer because they are not obviously last-in/ﬁrst-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 veriﬁcation an...

Raymie Stata, Martín Abadi

Real-time Traffic