[Prev][Next][Index][Thread]
work on Java bytecode verification
The following paper on Java bytecode verification is available from URL:
http://www.research.digital.com/SRC/personal/Martin_Abadi/Papers/jvm-short-preprint.ps
A Type System for Java Bytecode Subroutines
Raymie Stata and Martin Abadi
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 and a rational
reconstruction of a delicate part of Sun's bytecode verifier.
(This paper will be presented at POPL98.)
Some related results are described below; a paper on these results is
in preparation.
A Type System for Object Initialization
in the Java Bytecode Language
Stephen Freund and John Mitchell
The Java language enables the creation of portable programs which
can be transmitted over a network and run safely on any computer.
To support this paradigm, Java compilers typically translate a
Java program into an intermediate language which can be interpreted
by any Java Virtual Machine. This intermediate language is a typed,
machine-independent bytecode language, and it is the foundation
for many of Java's features, including portability across platforms,
dynamic type resolution, and run-time type safety. Despite the
bytecode language's important role in the success of Java, there
is no precise definition of its type system. We have developed
a sound type system for a small set of ten bytecode instructions
which are sufficient to study the type rules associated with object
creation and initialization. Our type system is based on a system
previously developed by Stata and Abadi to describe Java bytecode
subroutines.
We begin by developing a model of the Java Virtual Machine's bytecode
interpreter using the standard framework of structured operational
semantics. We then formulate syntax-directed type rules for the
bytecodes in our language. We show our type system is sound by
proving that any well-typed program will not produce a run-time
type error.
In addition, we integrate the earlier work of Stata and Abadi to
develop a sound type system encompassing both bytecode subroutines
and object initialization. We have used the soundness proof for
this system to understand the relationship between uninitialized
objects and subroutines. This analysis has led to the discovery
of a previously unpublished bug in Sun's implementation of the
bytecode verifier that allows a program to use an object before
it has been initialized.
This work is part of an effort to specify a type system for the
whole bytecode language. Once this system has been developed, we
can formally specify type safety for a compiled Java program and
precisely describe the security guarantees which can be made by
the verifier. In addition, this study may lead to more expressive,
but simpler, typed intermediate languages in the future.
Thanks to Martin Abadi and Raymie Stata (DEC SRC) for their assistance
on this project.
Martin Abadi, Stephen Freund, John Mitchell, and Raymie Stata