Higher-Order and Symbolic Computation, 15(1)7-55
Formalization and Analysis of Class Loading in JavaAkihiko Tozawa, IBM Research, Tokyo Research Laboratory, IBM Japan Ltd., Japan
Masami Hagiya, Graduate School of Science, University of Tokyo, Japan
|
Abstract: Since Java security relies on the type-safety of the
JVM, many formal approaches have been taken in order to prove the
soundness of the JVM. This paper presents a new formalization of the
JVM and proves its soundness. It is the first model to employ dynamic
linking and bytecode verification to analyze the loading constraint
scheme of Java2. The key concept required for proving the soundness of
the new model is augmented value typing, which is defined from
ordinary value typing combined with the loading constraint scheme. In
proving the soundness of the model, it is shown that there are some
problems inside the current reference implementation of the JVM with
respect to our model. We also analyze the findClass scheme, newly
introduced in Java2. The same analysis also shows why applets cannot
exploit the type-spoofing vulnerability reported by Saraswat, which
led to the introduction of the loading constraint scheme.
Keywords: Java, class loading, security |
This article can be downloaded [here].
![[picture of journal cover]](../LISP.JPG)