A Formal Specification of Java Class Loading
The Java Virtual Machine (JVM) has a novel and powerful
mechanism to support lazy, dynamic class loading according to
user-definable policies. Class loading
directly impacts type safety,
on which the security of Java applications is based.
Conceptual
bugs in the loading mechanism were found in earlier versions of the
JVM that lead to type violations. A deeper understanding of the
class loading mechanism, through such means as formal analysis, will
improve our confidence that no additional bugs are present.
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.
Our approach to proving type safety is different from the usual ones
since classes are dynamically loaded and full type
information may not be statically available.
In addition, we propose an improvement
in the interaction between class loading and bytecode verification,
which is cleaner and enables lazier loading.
Both
the paper
and the long version are available.
For a hard copy send a message to Zhenyu Qian.