[Prev][Next][Index][Thread]
Paper on Java class loading
The following paper is available under http://www.kestrel.edu/java.
Regards,
Alessandro Coglio
Kestrel Institute
3260 Hillview Avenue, Palo Alto, CA 94304
--------------------------------------
TITLE:
A Formal Specification of Java Class Loading
ABSTRACT:
The Java Virtual Machine (JVM) has a novel and powerful mechanism to
support lazy, dynamic class loading according to user-definable
policies. Class loading is essential to type safety, on which security
of Java applications is based. Because of the inherent complexity of
this mechanism, conceptual bugs were found in earlier versions of the
JVM that lead to type violations. Although these bugs have been fixed,
it is still hard to assess that the fixes do guarantee type safety.
The work presented in this paper provides a formal specification of (the
relevant aspects of) class loading in the JVM and proves its type
safety. In addition, the work proposes an improvement of Sun's design of
the interaction between class loading and bytecode verification; the new
design is cleaner and allows lazier loading. Another contribution is the
clarification that type soundness (which is a stronger property than
type safety) does not hold in our model and in the JVM.
--------------------------------------