Seminar, 10th July 1997

[ Changed 8th July 1997 ]

Speaker:

Martín Abadi, DEC Systems Research Center

Date:

Thursday 10th July at 15:00

Place:

Room TP4, Computer Laboratory

Title:

SECURITY AND TYPES IN THE JAVA VIRTUAL MACHINE

Java is typically compiled into an intermediate language, which we call JVML. The Java Virtual Machine interprets JVML code. 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 to 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. This subset, despite its small size, is interesting because it includes JVML subroutines, a source of substantial difficulty for the bytecode verifier. (Joint work with Raymie Stata.)

NOTE: the time is nonstandard for a security seminar.