Formalization and Analysis of Class Loading in Java.
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.
Introduction
Unlike its predecessor, C++, Java supports platform-independent bytecodes
which are compiled from source programs written in Java, sent over the network
as mobile codes, and executed by the Java Virtual Machine running within a
local application such as a Web browser.
The JVM links bytecodes sent over the network in a type-safe manner, whose
meaning is as follows.
It is guaranteed that linking bytecodes, with their type information consistent
with themselves, does not destroy the consistency of the JVM state,
which has its own type information.
The following requirement should also be satised.
If the current JVM state is consistent with its own type information, then
at its next execution step, it is still consistent.
Java is in this way a type-safe language, if these two requirements are satised.
Note that if the above consistency is broken, then the JVM incorrectly interprets
the contents pointed to by its inner pointer references. The type safety of the
JVM guarantees the memory safety of the JVM, and thus it plays the primary
role in the Java Security. In order to show the type safety property of the JVM,
Akihiko Tozawa and Masami Hagiya are at the Graduate School of Science, University
of Tokyo, Japan. Any suggestions or comments to this article are appreciated. Please send
email: fmiles, hagiyag@is.s.u-tokyo.ac.jp
a number of studies have been made so far. They are brie
y summaried in the
next subsection. This paper gives another formalization of the JVM and proves
its soundness.
Bytecodes running inside the JVM are structures into classes, each of which
is separatedly loaded and linked by the JVM. Objects called class loaders have
the responsibility of loading and linking a class. By supporting a variety of
class loaders, the JVM achieves the
exibility of class loading. However, this
exibility has been causing problems with respect to the above mentioned type-safety
of Java.
The rst contribution of our work is that of developing the new model of
the JVM. It is described in Section 2 of this paper in detail. Our model has
several improvements over those dened in the previous studies. First of all, it
includes class loaders. Java class loaders are instances of a user-dened class,
whose primary function is a map from class names to class objects. They are,
however, closely related to how the JVM internally builds its class environments.
In other words, the class environments of the JVM are not statically given, but
they are lazily built by dynamic evaluations of class loaders. Our model gives
dynamic environments which represent internal heaps of the JVM. It seems to
be the best approach to model the lazy linking semantics of the JVM by its
class loaders. Since we do not consider any static language from which these
environments can be constructed, our model is a practical one that faithfully
re
ects JVM implementations.
In 1998, Sun Microsystems released the version 1.2 of Java Development
Kit (JDK1.2), which is based on the newly proposed design principle called
Java2. This comes with the rewritten specication of the JVM, The Java Virtual
Machine Specication (2nd Edition) [9]. The most important feature introduced
to the new specication is the loading constraint scheme, which is originally
introduced by Liang and Bracha [8]. The scheme is the x of Saraswat's problem
[13] related to the unique design of Java class loaders. Our formalization also
includes this scheme. The second contribution of our work is that we have
found three problems inside the current o-cial implementation of the JVM
with respect to this scheme. These problems are not trivial ones because they
require a careful analysis of the scheme, which is done through our work on the
formalization. They are described in Section 3.
The third contribution of our work is that of proving the soundness of our
model, given in Section 2. The key notion required for the soundness proof is
the augmented value typing, which is dened from the ordinary value typing
combined with the loading constraint scheme. This new typing is shown to be
consistent with the subtype relation under the existence of the loading constraint
scheme. Note that this consistency is crucial for the soundness of the model, and
the problems we found inside the current o-cial implementation of the JVM
are due to its violation against the consistency.
Another new feature of Java2 is the findClass implementation of the class
loading. Technically speaking, both the loading constraint scheme and the
findClass scheme give constraints to the dynamic class loading of Java. Such
constraints restrict what will happen in the future, so that they further complicate
the lazy linking semantics of Java. For example, the problem we found
in the loading constraint scheme is sensitive to the timing of introducing con-
straints. This fact re
ects the subtleties of the semantics of such constraints.
The analysis of the findClass scheme in Section 4 is the fourth contribution.
By the analysis, we can also answer the old question why applets cannot cause
Saraswat's problem [13].
1.1 Related Work
Since the Java security deeply relies on the JVM and its type-safety, giving
formal models to the JVM is recently one of the major research issues in network
security.
Stata and Abadi [15] gave the JVM model including its bytecode verication.
They try to grasp the JVM as a type system, and its bytecode verication as
typing rules, whereby the correctness of the JVM is proved in the form of a
soundness theorem. Our work lays its concept for modeling the bytecode verier
on Stata and Abadi's work. In other words, we extended their model to cope
with class loaders.
Freund and Mitchell worked on a specic problem related to object initialization
[4]. Their work is also based on Stata and Abadi's.
Qian rst succeeded in modeling a large part of the JVM [12]. Formalizations
covering a wider range of the JVM (but without proofs) were given by Goldberg
[5] and Jensen, et al. [6]. In particular, Jensen, et al. dealt with Saraswat's
bug by modeling both class loading and operational semantics. Saraswat [13]
himself gave formal explanations to his problem. Dean also gave a formal model
of class loading [2]. However, it cannot explain the type spoong problems.
The lazy semantics of class loaders has not yet been fully modeled as far as
we know. We think that it has something to do with the study of modularity
as in the work by Cardelli [1].
Machine verications are also being applied to prove the type soundness of
Java [10][11].
1.2 Organization
The rest of the paper is structured as follows. Section 2 gives a basic formal
model of the JVM and also a soundness proof of the model. Section 3 mainly
explains problems with an implementation of the JVM. In Section 4, we give
further discussions related to the findClass scheme. We formally answer the
old question why applets cannot cause Saraswat's problem [13] in Section 4. We
also have discovered a new method to implement the loading constraint scheme
e-ciently.
Model and its Soundness
The formal model of the JVM presented in this paper has the following new
features compared to those in previous studies.
Modeling lazy class loading of the JVM.
Dening loading constraints.
Modifying the value typing statement.
Giving a rigorous denition of an environment, which is enough to model
all the above features.
In particular, lazy class loading of the JVM was rst modeled in this study.
Note also that for the last feature, it is necessary to dene the well-formedness
type
type  option := None
Some of
type Env := f
!(StringString listT Class )
cl
(iface : String list)
class
I : Instruction list
lvars : TValue list
list
type VerifyRecord := f
lvars : String list
stack : String list
invokevirtual of String  String  String
areturn
::::

Figure

1: Type denitions
of an environment, which in turn is dened in terms of the well-formedness of
its various components.
In this section, we rst explain several basic denitions. Section 2.4 gives
the denition of the loading constraint scheme. Our main soundness theorem is
described in Section 2.5.
2.1 Environments
2.1.1 Denition of Environments
An environment, which represents an internal heap of the JVM, is the most
basic data structure in our formalization. Of course, every component of such
a heap cannot be modeled. Instead we give a well-dened set of components to
which some mathematical examinations are possible. It is represented by type
Env.
See the denition of types in Figure 1. An environment, i.e., an element of
Env, is a record consisting of four subsets, T Class , T Loader , TValue and T Method , of
the set, Loc, of locations, and ve maps, C, W , R. The meaning
of each subset should be clear from its index. As we will note at the end of
this section, type Env can be considered as a dependent type, since each map
and R) has an arrow type, which is constructed by using the
subsets (T Class , T Loader , TValue and T Method ) as types. Members M, C and V map
locations to appropriate denitions, i.e., they return denitions stored in E from
their references. Member W represents class loading, while R represents method
resolution. These two maps are explained later. We use the notation, E:m, to
extract member m from environment E.

Figure

2: Abbreviations inside judgments
For any type ,  option denotes the type composed of constructor None
and values of  wrapped with constructor Some. For example, the value of
E:W(l)(n) is either None or of the form Some c. For any type ,  list denotes
the type of nite lists of . For list, the i-th element of x is denotes by
x[i], and its length by len(x).
Note that in Classdef(T ),
T denotes the tuple consisting of T Class , T Loader , TValue and T Method . We dene
T Class and Classdef(T ) separately, so that there are two kinds of identity between
classes. The same situation happens for values and methods. We usually
identify an object by its reference.
A state, i.e., an element of State(T ), is either  exeption , which denotes an
error state, or a record consisting of four elements, pc, method, lvars and stack.
Elements of VerifyRecord give types to the local variables and the stack of a
state. They are used in the bytecode verication. The type of instructions,
Instruction, is not dened completely. For the sake of this study, we only assume
the invokevirtual instruction and the areturn instruction.
Type theories use a -type for representing such types as Env. Tuple T is
considered as an element of the index set, Index, dened as follows.
We use a reference, i.e., an element of Loc, to access a component of an en-
vironment. Of course, there are dierent ways to dene and identify these
components. In some studies a class is identied by a tuple of a class name and
a class loader, because there should not be two classes with the same name and
loader inside a single JVM.
Our model gives a low level abstraction which re
ects practical JVM im-
plementations. In any such implementation, the class identity property is only
one of the various properties implicitly satised by the internal structure of the
heap. In practice, there is no two classes with the same name and loader only
when class loaders are synchronized. If two threads start loading the same class
by the same loader at the same time, the property would easily be violated.
Here we are not going into how to implement the JVM which always satises
such properties. Instead we have extracted a set of properties, which are
essential for the soundness of the model, called the well-formedness of the en-
vironment, and given an assumption that any modication or update of the
environment must preserve this well-formedness. The well-formedness of the
environment, denoted by wf (E), is composed of the following properties.
The property related to the classes inside an environment.
The property related to the methods inside an environment.
The property that states that all methods are statically veriable, i.e.,
have gone through the bytecode verication.
The Bridge Safety property related to the loading constraint scheme.
The above properties are denoted by wf class(E), wf method (E), veried(E)
and bridge safe(E), and are described in Sections 2.2.4, 2.3.5, 2.5.1 and 2.4.3,
respectively.
2.2 Objects, Classes and Loaders
This section gives basic denitions of objects, classes and class loaders. Each
class of Java is actually an object instance of java.lang.Class and each class
loader is of java.lang.ClassLoader, but unlike other objects, they play essential
roles in the JVM architecture, which refers to them automatically and
implicitly. Therefore, it is appropriate to dene objects, classes and class loaders
separately.
2.2.1 Classes
Let us rst explain the denition of classes in Figure 1. A class denition,
i.e., an element of Classdef(T ), is a tuple consisting of a class name, a direct
super class name and a class loader. As we have noted, if we assume c is a
class reference, then the components of c's denition are simply written inside a
judgement as c:name, c:super and c:cl, respectively. The two other components
of c, the method dispatch table, c:mt, and the implemented interfaces of the
class, c:iface, will be discussed later.
2.2.2 Class Loaders
Each Java object instantiating java.lang.ClassLoader has a private member
declared as a hashtable which maps names of classes to class objects themselves.
We model this mapping with E:W as follows.
Denition 2.1 (Subtyping)
Denition 2.2 (Widening)
cl
Denition 2.3 (Normal Value Typing)
Denition 2.4 (Well-Formedness)

Figure

3: Predicates related to classes
The class name resolution n l (= E:W(l)(n)) results in Some c if name n is
associated with a certain class c by class loader l, and None if not.
We also say that n is resolved into c by l.
In the above sense, each class loader has its own name space. Therefore, a
class loader is also called a context. Each class c has its dening class loader
c:cl, whereby every class name resolution related to c is done. In this sense, c:cl
is the context of c. Throughout this paper, we use the word context and class
loader as synonyms.
As

Figure

shows, each value
uniquely refers to a class, and thus to a class loader. We say that value v is
created in context v:class:cl or method m is executed in context m:cc:cl.
2.2.3 Subtyping
Subtyping between classes is dened in Figure 3. In our model, predicate sub
represents the relation.
For class c, if its parent class name, c:super, is resolved into c 0 in context
c:cl, then c is a direct subtype of c 0 . The (indirect) subtyping is dened
as the re
exive and transitive closure of the direct subtyping.
2.2.4 Well-Formedness of Classes
An actual class loader of the JVM resolve classes in one of the following two
ways.
When a class loader, l, denes class c whose name is n, it sets c:cl to l,
and resolves n into c.
When a class loader, l, delegates class loading to another class loader, it
resolves n into c whose c:cl is not equal to l.
Actual class loaders therefore satisfy the following statement, the well-formedness
of classes dened in Figure 1, since each class should be once dened by the
above rst process which sets n l to that class.
For each c in E:T class , c:name is resolved into c itself in context c:cl.
Note that this statement immediately implies the class identity property described
in Section 2.1.3.
2.2.5 Object Values and States
If a JVM state,  : State(E:T ), is not an error state,  exception , it has the following
components.
:method denotes the method that the JVM is now processing.
:pc, the program counter, points to a certain instruction of :method:I.
Both :lvars and :stack are represented by a list of values which stores
contents of the local variables and the local stack, respectively.
While both the state and the environment represent internal data structures of
the JVM, their transitions, !  and , respectively, are distinct and independent

In our model, all values found inside :lvars or :stack are objects. An object
value, v, is a record with just one member, v:class, which represents a type (class)
of that value 1 . In practice, a Java object value may also have a reference to an
array of values, i.e., its eld values. There is no di-culty to extend our model to
represent elds, since it already has a value heap. We can just add v:eld, which
represents a list of value references. Our model omits elds of Java, because the
get=puteld instructions are in large part similar to invokevirtual and also easier
to handle.
2.2.6 Predicates with Respect to Subtyping and Value Typing
We introduce two predicates with respect to subtyping, one of which represents
the widening conversion, and the other represents the typing judgment of values.
Their formalizations are given in Figure 3.
The widening conversion denes a quasi-order 2 between class names. The
order between two names is dened only if both of them are resolved in cl ,
except for the case that two names are equal. The ordering itself follows
the subclass relation between the classes into which names are resolved.
The normal value typing is a typing judgment which denotes that the type
of value v is a subtype of n in context cl . It is also dened only if n is
already resolved in cl .
Note that both predicates depend on a context, cl .
2.3 Methods
This section simply describes the specication of invokevirtual [9], while the practical
method invocation of the JVM involves further di-culties and problems.
Such remaining problems will be explained in Section 3.
2.3.1 Instructions
As dened in Figure 1, our JVM model includes only two instructions, invokevirtual
and areturn. Instruction invokevirtual is the most fundamental but the most non-
1 Java has a null value which represents an uninitialized object value. We do not model this
for simplicity.
2 According to our denition, both sub and  cl
satisfy transitivity but not anti-symmetry.
Of course, they should do so in practice.
trivial instruction of the JVM. It is used with three arguments as follows.
The above judgement means that the current JVM state, , is now about to
process invokevirtual, which calls a certain instance method. String name is the
name of the method, and string list desc is the descriptor representing the type
signature of the method, where
are argument types (i.e., class names) of the method, and desc[0] is its return
value type. String classname is the name of the symbolically referenced class [9].
Instruction areturn is one of the return instructions of the JVM, which returns
to the caller, holding one object value as a return value.
2.3.2 Method Invocation
Execution of invokevirtual consists of the following three processes.
The method resolution looks up a method according to the three arguments
of invokevirtual. The method found by this process is called the
symbolically referenced method and denoted by SRmethod.
The method selection looks up a method accessible from the class of the
object on top of the local stack.
The method invocation calls the method found by the method selection
process.
Assume that invokevirtual is inside a method whose class is c and whose
context is l(= c:cl). The method resolution process is modeled as follows.
We just look up the method, SRmethod, which is already registered to the en-
vironment, E:R (cf. Section 2.1), by the given name and descriptor, name
and desc. SRclass, the symbolically referenced class, is the result of resolving
classname by l. Remember that (name; desc; SRclass) l abbreviates E:R(l)(name; desc; SRclass).
Its further denition is given at the end of this section and also in Section 3.
Practically, the JVM remembers whether a symbolic reference is already re-solved
or not, so that it never resolves the same reference twice 3 . Our model
re
ects this behavior.
The method selection process will be dened in Section 3. In this section,
we just assume that the process results in a unique value, denoted by method.
When we write a judgement having E and  in its left hand side, we assume
that SRmethod and method inside the right hand side denote the symbolically
referenced method and the selected method, respectively.
'    SRmethod    method
Although the dention of the value, method , is left blank until we discuss
the implementation later, we can examine the soundness of the JVM, i.e., the
3 This is implemented by the internal class representation which attaches a
ag to each
resolvable constant pool entry, which remembers whether the entry is resolved or not. It also
remembers the result of resolution.
correctness of the new loading constraint scheme (cf. Section 2.4), provided that
we assume Lemmas 1, 1' and 1", described in Sections 2.3.4 and 2.3.5.
The value, SRmethod , is identical to the value of the same variable, appearing
in the predicate, invv OK (E; ), dened below.
Denition 2.5 (invokevirtual OK)
where Some
The predicate means that the JVM is now about to execute invokevirtual, and
the method resolution has normally succeeded, i.e., it has not raised exceptions.
Unlike what is specied about the method resolution, once invv OK (E; ) holds,
i.e., the method resolution succeeds, our JVM model ensures that the method
selection and method invocation will also succeed. This is because method is
always dened in such a case.
Formally, name, desc, classname, SRclass, SRmethod and objectref in the
denition of invv OK (E; ) should be existentially quantied. However, in a
situation where we assume invv OK (E; ), we refer to them in a judgement as
if they leak out from the denition of invv OK (E; ), i.e., those variables are
assumed to satisfy invv OK (E; ).
2.3.3 Operational Semantics
Denition 2.6 describes the state transition semantics of invokevirtual, which is
dened in accordance with the specication of the three processes of invokevir-
tual. (Note that @ denotes list concatenation.)
It rst tries to resolve its method. If it cannot be resolved,
If the method can be resolved, it generates a new state,  in , whose method
is the selected one. Its local variables should store the proper value of
values of arguments, each of which is originally
stored in :stack.
There must be a transition of the form
where  out should point at instruction areturn, the return instruction of
the JVM. This means that the invoked method can be safely executed.
At last,  out :stack has a return value on its top, which will be pushed onto
denotes the transitive closure of the one-step transition, !.
Transitions for other instructions are not given in this paper (See [15] or [7]).
exception .
Denition 2.6 (Operational Semantics of invokevirtual)
exeception
in :lvars = [objectref ]@arg ;
in
in
out :method:I[ out
[retval
[retval]@rest ;
State <
references to
method :cc

Figure

4: Subtyping relations related to invokevirtual
2.3.4 Invocation Correctness
With respect to SRmethod and method , the following lemma should be con-
sidered, while the lemma itself will be examined in Section 3. In the following
several sections, the lemma will be assumed to hold.
(Correctness of invokevirtual)
Let E be an environment, and  be a JVM state.
method overrides SRmethod
In other words, Lemma 1 (Correctness of invokevirtual) guarantees that if
the JVM is about to execute invokevirtual, then
if the JVM is in a safe state, a method whose dening class is a superclass
of the class of objectref should be invoked.
Furthermore, if the JVM is in a safe state, then a method that overrides
the symbolically referenced method should be invoked.
The second premise of the lemma, the subtyping relation between objectref :class
and SRclass , is a property that should be invariantly satised by a safe execution
of the JVM (cf. Section 2.4.1). The rst consequence of the lemma, the
subtyping relation between objectref :class and method :cc, is derived from the
method selection algorithm described in Section 3.1.1. See Figure 4.
The method overriding relation, overrides, has not yet been dened for certain
reasons. One reason is that although the term, override, is often used in the
specication of the JVM, its accurate meaning is not dened, so that its interpretation
depends on implementations. In this paper, we will dene predicate
overrides in Section 3.1.1 in conjunction with predicate select.
The predicate, overrides, should satisfy the following conditions.
LEMMA 1'
The implementation of Sun's JDK1.2 is inconsistent with Lemma 1' and exposes
a new
aw, as we will explain in Section 3. The relation, , between
environments is dened in Section 2.5.3.
2.3.5 Well-Formedness of Methods
The following well-formedness property of methods is required mainly for the
discussions in Section 4.
selects SRmethod
Predicate selects models the method selection process and its denition can be
found in Denition 3.1 in Section 3.1.1.
class RT { .
RR new RR();
. }

Figure

5: Saraswat's bug code
With predicate selects, the equivalence of descriptors should also hold.
LEMMA 1"
2.4 Bridge Safety
Bridge safety of the JVM is a notion originally introduced by Saraswat in his
report on type-spoong in JDK1.1 [13]. He insisted that applet loaders never
suers from his bug because they never break this property. Sheng and Bracha
have devised a x of Saraswat's bug, implemented in JDK1.2 [8][9], which forces
the JVM to check the bridge safety at runtime.
2.4.1 Type-Spoong in JDK1.1
See the source code in Figure 5, which revealed the bug of type-spoong in
JDK1.1. The code itself has nothing suspicious, but if there exist two contexts
l 1 and l 2 (the code itself runs under l 1 ) and delegation of class loading
RR
is dened, the invocation of r.speakup() would result in a serious violation of
the type system of the JVM.
Expression r.speakUp() is complied into the following instruction of the
JVM.
The above ()V is dierent from our notation of method descriptors. It represents
a method which takes no argument and returns nothing.
With respect to this invokevirtual, its objectref , the value on top of the
local stack, is equal to the value of r, which comes from context l 2 via the
invocation of rr.getR().
l 2
The symbolically referenced class, SRclass, is the class into which the
current context l 1 resolves R (the third string of invokevirtual).
l 1
The code causes a problem when R
l 1 is dierent from R
l 2 . For any invokevirtual
to be correctly executed, the subtyping relation
Denition 2.7 (Loading Constraints)
(method overriding)
(method resolution)
cl m:desc[i]  m:cc:cl
(re
exivity)
cl n
cl
cl n
cl
cl 00
cl n
cl 00
cl n
cl 0
cl 0 n
cl
is absolutely necessary (of course, objectref :class = SRclass su-ces). Recall
that this subtyping relation is the second premise of Lemma 1. In other words,
method in Section 2.3 is completely unrelated to SRmethod .
More accurately, the bug results in the incompatibility of the dispatch tables
of two classes, by applying a method index obtained from SRclass onto
a completely unrelated method table of objectref :class. JDK1.1 would thus
either invoke method with argument values of incompatible types or just core-
dump. The method dispatch table, which is excluded from Sun's specication
and therefore from our model, is an implementation technique of the method
selection algorithm (cf. Section 3.1.3).
2.4.2 Loading Constraints
Go back to the example of Section 2.4.1. Suppose that the JVM has already
noticed at the invocation of rr.getR() that the method brought a value of type
R from context l 2 to l 1 . In this case we can check beforehand if this
ow of the
value is acceptable or not. We may simply try to check it as follows.
l 2
But this attempt should fail, since before the method resolution of speakUp(),
R
l 1 cannot be evaluated, i.e., under the environment, E ' R
we must consider an alternative, i.e., the loading constraint scheme. In this case,
the new scheme introduces the following loading constraint.
R
If the JVM remembers the above constraint, R
l 1 is not allowed to be resolved
into a dierent class from R
l 2 in the method resolution process.
How the JVM can notice the possibility of a value
ow is not easy to un-
derstand. It is related to Lemma 3 (Existence of Constraints) described later in
this section. Here, we only give rules to introduce the loading constraints.
For any method m, which overrides m 0 , the following constraint is introduced
with respect to each class name n appearing in their descriptor.
For any method resolution at  which nds SRmethod , the following constraint
is introduced (for each class name n appearing in the descriptor of
SRmethod ).
SRmethod :cl
Relation n
is dened to be transitive, re
exive and symmetric, so that it is an
equivalence relation. It should also be the minimal relation among all satisfying
the above conditions. Denition 2.7 formally describes the predicate by
inductive denition.
As shown later in Section 2.5, the relation is -invariant, i.e., relation
between the environments subsumes n
. This enables the JVM to incrementally
construct the relation, n
, as it resolves a method reference of invokevirtual, or
it links a class whose method overrides another method. This is the reason
why the loading constraint scheme is light-weight, and why it has been actually
adopted among many other solutions. The history of Saraswat's problem and
its solutions are described in [8][13].
2.4.3 Bridge Safety Predicate
Denition 2.8 denes predicate bridge safe(E) as follows.
For environment E, any class loader in E has made no resolutions of
classes which contradict with loading constraints existing inside E.
This predicate forbids any environment modication, i.e., class loading and
method linking, which violates constraints. It is the same as what JDK1.2 is
doing.
2.4.4 Augmented Value Typing
The augmented value typing,
cl n, is dened as follows.
There is another context cl 0 , in which v has type n in the normal sense,
cl 0 n, and there also exists the following constraint.
cl n
cl 0
The intent of the denition may not obvious. Roughly, it means that value v
itself has been created, i.e., instantiated from n, in context cl 0 , and it has been
transfered to the current context, cl.
This predicate was called dynamic conformity in our previous paper [16]. As
we noted in the introduction, it is crucial for proving the type soundness of the
loading constraint scheme, and its denition is one of the contributions of this
study.
With respect to this predicate, the following lemma is important.
cl -invariance of Augmented Typing)
Denition 2.8 (Bridge Safety)
bridge safe(E) def
cl
cl n
cl cl cl 0
cl 0
Denition 2.9 (Augmented Value Typing)
cl
cl n
cl cl 0 n
list
cl (ns : String list)
cl ns[i]
Let E be an environment, n and n 0 be class names, and cl be any class loader,
bridge cl n 0
cl
cl
Proof
The following fact is proved by examining Def.2.3 Def.2.9 and Def.2.8.
bridge
cl n =)
(n cl 6= None =) cl n)
Assume the rst line of the lemma. From Def.2.2 Def.2.3 and Def.2.1,
we have
cl n =) v :: cl
By applying E ' cl n
cl to Def.2.9, the lemma is proved.
The lemma states that the augmented typing is invariantly satised against the
widening conversion described in Section 2.2.6. This is an important statement
which relates runtime typing to static typing, i.e., the bytecode verication.
The proof of the lemma requires that the denition of the widening conversion,
cl n 0 , force additional loadings of n cl and n 0cl in case of n 6= n 0 .
We have found two inconsistencies between our denition of  cl and the
bytecode verication of JDK1.2. By exploiting each of these, we can still entirely
escape additional checks newly imposed. See Section 3 or [16] for detail.
Note that it is relatively easy to show that the augmented typing is also
-invariant, which will be used later in the soundness proof.
2.4.5 Constraint Existence
Lemma 3 (Existence of Constraints) states that if the JVM is in a safe state
and about to execute invokevirtual, there already exist loading constraints for
each class name appearing in the descriptor of invokevirtual between the current
context and the context of the invoked method.
We now assume Lemma 1 (Correctness of invokevirtual). Note that E '
cl
desc[]
cl 0 abbreviates cl
desc[i]
cl 0 .
Denition 2.10 (Verication Rules)
(rule of
(rule of invokevirtual)6 6 6 6 6 6 4
(i):stack[0]  m:cl cname
(rule of areturn)4
LEMMA 3 (Existence of Constraints)
Let E be an environment, and  be a JVM state.
method:desc[]  method :cl
Assume the rst line of the lemma. From Def.2.7(method overriding
and symmetry) and Lemma 1, we have
' SRmethod :cl method:desc[]  method :cl:
From Def.2.7(method rosolution) and Def.2.5, we have
Applying Lemma 1' and Def.2.7(transitivity) yields the lemma.
2.5 Soundness
This section follows the framework of the soundness proof by Stata and Abadi [15].
One dierence is in the introduction of environments. Another is in the treatment
of invokevirtual, the instruction that does not exist in their model.
2.5.1 Bytecode Verication
One uniqueness underlying the language design of Java is found in its bytecode
verication. The idea is to guarantee the runtime well-typedness by the static
verication, which allows minimum type checks at runtime.
See Denition 2.10. Type VerifyRecord represents an imaginary store for the
static class name information about local variables and local stacks. A map, ,
stores an element of VerifyRecord for each instruction of :method. The bytecode
verication is a problem of nding such  that is consistent with the veried
method, m.
Denition 2.11 (k-transition)
exeception
out
kn
Denition 2.12 (well-typedness)
veries :method
:cl (:pc):lvars
:cl (:pc):stack
It should be veried that contents of  satisfy all  m:cl relations imposed
by the verication rules.
In our model, the consistency of  is represented by predicate veries. Predicate
veried(E) states that each method in E has already been veried.
The well-typedness predicate, E ' wt(), means that state  is safe inside
environment E.
Both :lvars and :stack should have their values typed by the class names
recorded in  which veries :method.
State  exception representing an error state is always well-typed.
Note that :lvars ::
:cl (:pc):lvars abbreviates 8i
:cl
(:pc):lvars[i].
The interesting work by Yelland [17] implements the bytecode verier based
on the type inference of Haskell.
2.5.2 Soundness Theorem
Here is our main theorem.
THEOREM (Soundness)
be environments, and  and  0 be states.
This theorem states that any execution step of the JVM preserves the well-typedness
While the intuitive meaning of the invariant
is not so trivial, it is su-cient to guarantee the correctness of invokevirtual. If
then we have
which is the second premise of Lemma 1. Any instruction that is not modeled
in this paper also preserves this invariant, whereby the correct behavior of the
instruction should be guaranteed.
The theorem can be divided into two lemmas in the following sections.
Denition 2.13 (Sub-Environment relation)
String list E:T Class :
2.5.3 Soundness of Environment Updates
Denition 2.13 describes how environments can be updated as the JVM dynamically
links objects, classes, etc. It denes the sub-environment relation,
between two environments.
Following is the rst lemma needed to prove the main soundness theorem.
This lemma states that any modication of environments preserves the well-
typedness, and its proof is as follows. Remember that we are assuming Lemmas
1, 1' and 1".
We rst assume
guarantees that any components of E are compatible with
those of E 0 . Therefore, from Def.2.13 and Def.2.1, we have
We also have, from Def.2.13 and Def.2.3,
cl cl n:
We say that relations sub  and :: cl are -invariant. Furthermore,
Lemma 1' and Def.2.13 guarantee the following facts, respectively.
They imply that relation n
is also -invariant, because it is minimal
among those that satisfy Denition 2.7. Therefore, the augmented
cl , is also -invariant, because it is dened in Def.2.9 as
follows.
cl cl n
cl 0
From Def.2.12, the lemma is proved.
2.5.4 Soundness of State Transitions
Following is the second lemma for the soundness theorem.
This lemma states that every state transition under a xed environment, E,
preserves well-typedness.
Before examining the lemma, we redene state transitions as described in
which adds depth k to each transition. Obviously, we have
Note that 0
denotes a state transition to  exception or a transition by an instruction
other than invokevirtual, which we do not dene in this paper.
The proof of the lemma is as follows:
We rst note that the following fact holds.
cl cl n
cl 0
cl 0
It expresses the n
-invariance of the augmented typing and can be
easily proved by examining Def.2.9 and Def.2.7(transitivity). By the
transitivity of !  , the following fact is a su-cient condition of the
lemma.
This is proved by induction on k. The base case of the induction is
as follows.
Its proof is omitted here. See [15] or [7] for detail.
The remaining subgoal is to show the case of k+1 from the induction
hypothesis.
Assume the rst line of [iii]. From the only state transition rule that
denes
where  in and  out are dened as in Def.2.6. From the induction
hypothesis, we have
holds here, there exists  that satises the following
condition.
:cl ([:pc]):stack
Applying Def.2.10(rule of invokevirtual) and Lemma 2, we obtain
where x[0; ::; n 1] denotes a sublist, [x[0]; ::; x[n 1]], and n is the
length of desc. Assuming invv OK (E; ), we have
Lemma 1 can be used here. It implies
method:cl method :cc:name
together with wf class(E). On the other hand, Lemmas 1, 1' and 1"
imply
together with wf method(E). We can then use Lemma 3 and [i] to
obtain
method:cl method :desc[1; ::; n 1]:
Therefore, Lemma 2 and Def.2.10(rule of imply
method:cl  0 (0):lvars
for some  0 that satises  0 veries method(=  in :method) and
Finally, Def.2.6 implies
in :lvars = :stack[0; ::; n
and therefore
From the induction hypothesis, [iv], we have
of areturn) and Lemma 2 lead to
method:cl method :desc[0]:
Similarly as above, we can use Lemma 3 and [i] to obtain
Finally, Def.2.10(rule of invokevirtual), Lemma 2, Def.2.6 and Def.2.12
imply
Denition 3.1 (Predicate selects)
3 Analysis of Implementations
Another main topic of this paper is the analysis of Sun's JVM implementation.
The latter half of this section describes several
aws that we have found in
JDK1.2 with respect to Saraswat's bug and the loading constraint scheme. Before
describing the
aws, let us examine Lemma 1 (Correctness of invokevirtual).
3.1 (Correctness of invokevirtual)
3.1.1 Method Selection
In Section 2.3, we dened the method invocation processes only partially. In this
section, Denition 3.1 formalizes the recursive procedure employed in method
resolution and selection. We dene it as predicate selects.
A pair of a key and a class, (key ; c), selects method m whose key is equal
to key , if m is found by a lookup over the subtype tree from c to its
superclasses.
In the denition, key denotes the pair, (name; desc), and the key of m, m:key,
denotes a pair (m:name; m:desc). If ( ; desc; c) selects m, then we have the following

The latter condition is what Lemma 1" requires. The predicate is also -
invariant from its denition.
In the denition of selects, the selection process terminates once a method,
m, is found inside c, no matter whether another method, m 0 , can be found
inside some superclass of c or not. However, in such a case, i.e., if m makes m 0
invisible from c, we say that
For any class c and method m such that (m:key; c) selects m, if a direct
superclass of c selects a dierent method, m 0 , with its key the same as
m:key, we dene
Predicate overrides is then dened as the re
exive and transitive closure of predicate
overrides - .
If we faithfully follow Sun's specication, SRmethod and method are simply
dened as follows.
The method resolution process will nd SRmethod which satises the following

selects SRmethod
The method selection process will nd method which satises the following.
selects method
As we see below, the above two denitions derive Lemma 1 (Correctness of
invokevirtual) by simply applying the premise of the lemma, objectref :class sub  SRclass,
to the dention of overrides.
By the denitions and Lemma 1",
method :desc
holds no matter whether a method overriding exists or not. This is because the
specication explicitly uses desc to select a method. However, the implementation
diers from the speciciation in that it employs the method dispatch table
of a class to select a method.
As long as the above descriptor equivalence holds, the JVM never falls into
an error state or coredumps, even though state  may be badly-typed. This is
the reason why it is di-cult for the specication to explain the type-spoong
problem. Figure 6 describes the problem graphically.
3.1.2 Proof of Lemma 1
In this paper, we only show Lemma 1 with respect to the above specication,
though it must be and can be proved for existing implementations.
We rst show the existence of method , since in our model the method
selection process should always succeed. Assume invv OK (E; ),
which implies E;  ' (SRmethod :key; SRclass) selects SRmethod . Also
assume
from which Denition 3.1 implies the existence of method that sat-
ises
As we already noted, relation select holds between objectref :class
and method :cc, so we obtain the rst consequence of the lemma.
The second consequence is the following.
method overrides SRmethod
This can be proved by induction on sub  , because overrides is the reexive
and transitive closure of overrides - . If objectref :class sub SRclass
holds, then either method = SRmethod or method overrides - SRmethod .
3.1.3 Method Dispatch Table
A method dispatch table is a list of methods which satises the following conditions

A method is selected by a class, c, i the method is inside the method
dispatch table of the class, c:mt.
An overriding method has the same index as the overridden one, i.e.,
for any class c and any superclass c 0 of c, and any index i less than the
length of c 0 :mt.
The JVM can incrementally build such a table structure for each class that
satises the above conditions, by referring to the table of its direct superclass,
which has already been built. Here, suppose that we already have a method
dispatch table for each class. Since SRclass:mt is a collection of methods selected
by SRclass , the method resolution process of JDK1.2 searches inside SRclass :mt.
In the method resolution, threfore, this dierence between the specication and
the implementation by method dispatch tables cannot be seen from outside.
On the other hand, as to the method selection process, the implementation
remarkably diers from the specication. It is an O(1)-time procedure rather
than a recursive procedure represented by predicate selects. A method selection
process is as follows.
There is index i which satises
because SRclass selects SRmethod .
The selected method, method , is
The above selection process is also sound, as it also satises Lemma 1 (Correct-
ness of invokevirtual). For the proof of the lemma, the sub  relation,
should necessarily be used.
In the implementation, the equivalence of the descriptors, desc = method :desc,
and even the existence of method , depend on this sub  relation. Without such
a relation, index i of SRclass :mt has no meaning inside method :mt. By exploiting
the inconsistency between desc and method :desc, one can falsify an integer
value as an object value, and vice vasa. If method does not exist, the JVM
coredumps [13].
3.2 Bytecode Verier and Loading Constraints
3.2.1 Problem with Respect to the Widening Conversion
Now we go back to Saraswat's bug code (Figure 5) in Section 2.4. Suppose that
a modication described below is applied to the original bug code.
original code modied code6 4
new R'()
R is not load by L 1
R
L1 inside method resolution
loaded
JDK1:2 . :r ::
L1 R R L 2 not loaded VIOLATION
VIOLATION JDK1:1 #
spec: . &
Executing r.speakUp()
Some
In any case where
method
even if method is unexpected,
execution continues.
It is posible that
method :desc 6= desc,
or in a worse case, method may not
exist. Type confusion or coredump.

Figure

Type spoong chart
class RR {
public R getR() {
return new R'(); // originally ``new R()''
Assume that L 2 loads class RR, and L 1 loads class RT, which invokes rr.getR()
and also r.speakUp(). It is also assumed that L 1 resolves R dierently from L 2 .
The method invocation, r = rr.getR(), which calls a method inside class RR,
returns a value not of type R but of type R'. Inside context L 2 , R' is a subtype
of R.
Recall that to check this widening conversion, R L2 should have already been
resolved. Therefore, the constraint,
R
will be checked at the invocation of r.speakUp(), when R
L1 is resolved.
Assume, conversely, that R L2 has not been resolved yet. Even though class
R L1 has been resolved, and though the above constraint indeed exists, the constraint
will never be checked. Figure 6 describes what happens in such a case.
In fact, JDK1.2 sometimes does not resolve R L2 , although its resolution is a
role of the bytecode verier.
3.2.2 Two Inconsistencies
We have found two inconsistencies in the bytecode verier of JDK1.2 against
our model, each of which still enables the type spoong. These inconsistencies
are as follows.
Some widening conversion, n  cl n 0 , is not correctly checked and n 0 is not
resolved.
System classes are not veried at runtime.
These bugs are brie
y explained in [16] with example codes.
Let us emphasize the signicance of our work. The problem is concerned
with the augmented typing, which is an alternative of the naturally dened
typing. Since the bytecode verication seemed unrelated with Saraswat's bug,
the designer of JDK1.2 did not modify the bytecode verication of JDK1.1.
However, the JVM requires Lemma 2 ( cl -invariance) as well, which relates
the well-typedness invariant to the bytecode verication based on the widening
conversion. It is our model that makes all of these points clear and visible.
3.3 Interfaces and Loading Constraints
In addition to the above problem with its bytecode verier, one more
aw inside
the JDK1.2 implementation was found during the analysis of the invokeinterface
instruction, which has been excluded from our model so far.
3.3.1 The invokeinterface Instruction
In order to discuss the problem of invokeinterface, we extend our model to be
able to deal with the interfaces of Java. The only thing to do is to allow a class
to have multiple parent classes. Throughout this section, a class, c, has its list
of the names of implemented interfaces, c:iface.
We redene the subtyping relation, c sub c 0 , i.e., c is a direct subtype of
We introduce a new predicate, is class(c), which is true i c is a pure class,
i.e., c is not an interface.
Though any class has no more than a single direct supertype in the previous
sections, this fact was not used throughout our soundness proof, which
thus requires no further changes. The invokeinterface instruction, which similarly
resolves and selects a method, will have exactly the same semantics as
invokevirtual. The only modication must be considered with predicate selects.
If pure class c itself does not declare a method with the required key, the
predicate should select a method not inside implementing interfaces of c, but
inside some pure superclass of c. Therefore, we should redene the second rule
of Denition 3.1 as follows.
class(c) =) is class(c
3.3.2 Problem with Respect to Constraint Existence
A question may be raised about the code in Figure 7. Is D.getR overriding
I.getR, or not? If we accept our denition of overrides, the answer is yes,
even though there is no subtyping relation between the declaring classes of two
methods. Since class D selects D.getR for the key representing R getR() and
one of its direct supertype, I, also selects I.getR, we conclude that D.getR
overrides I.getR from the denition of override,
In fact, the following code invokes a method inside class D safely.
interface I {
R getR();
class D {
R getR() { . }
class C extends D implements I {}

Figure

7: Problem of invokeinterface
I
Since JDK1.2 fails to recognize such complex method overriding relations,
the code in Figure 7 is what brings another problem of the loading constraint
scheme. The overriding relation between D.getR and I.getR is not recognized,
so that there may be no constraint between the loaders that dene D and I with
respect to the name of the return type, R.
4 The findClass Scheme
4.1 Formalization of the findClass Scheme
There is also one more new feature in Java2, i.e., the implementation of class
loadings by findClass. Java2 recommends to implement class loaders by
findClass rather than the old loadClass method, though loadClass is also
accepted for backward compatibility.
The findClass scheme denes a tree structure among class loaders. The
delegation of class loadings should follow this tree structure.
In the old version of Java, Applet loaders are implemented in a similar manner
as the findClass scheme. It is also known that applets never cause the
Saraswat's problem (though it has never been proved completely). This leads
to the following question. Can the findClass scheme replace the loading constraint
scheme?
Our last theorem, Theorem (Trusted Environments), which will be proved
in Section 4.2, gives a negative answer.
Even if we follow this findClass scheme, class loadings may violate constraints
unless no delegations are allowed other than those to system loaders

As the above theorem states, and also as Saraswat has correctly mentioned,
applet loaders are safe since they only delegate to system loaders. However, as
[8] describes in its rst half, class loaders are recently increasing their variety
of applications. Consider an applet loader which delegates to another applet
loader. Although such loaders seem to be safe at a glance, the theorem correctly
states that they possibly violate constraints.
4.1.1 Parent Loaders
The following denitions incorporate the findClass scheme into our model.
Denition 4.1 (Parent Loader)
true
l vP :Parentdef l
l vP l 0
The direct parent loader of each loader. If
l does not have a parent loader, we assume P l. The inductively dened
predicate, l vP l 0 , denotes that l is one of the (indirect) parents of l 0 .
Denition 4.2 (Correct Delegation to Parent Loaders)
The denition formalizes the following delegation strategy of Java2. If a loader,
l, has its direct parent loader, l 0 , any class loading by l is rst delegated to l 0 .
The class is loaded by l itself only if l 0 cannot resolve the class name. Otherwise,
l will return the same class as l 0 returns.
In the above denition,
=) expresses that there is no loading delegation that does not follow the
parent loader relation.
(= expresses that two loaders in the parent loader relation correctly delegate
class loadings according to the above strategy.
The second condition implies that if c:cl vP l, then l has already resolved
c:name. Therefore, if wf parent(E; P ) holds, each loader in E is considered to
have resolved all the classes it can do so. In other words, E represents such
an environment that all possible class loadings have been completed. Ordinary
environments are thus considered as sub-environments of such environments.
We therefore use dient font, such as E , for those environments.
Note that wf parent(E ; P ) implies wf class(E).
4.1.2 Parent Environment
We dene a relation between envirnoments that represents an extension of environments
through delegations to parent loaders.
Denition 4.3 (Parent Environment)
The second line of the denition of E that a method loaded by a
loader in E should already exist in E . The third line states that delegations are
allowed only to a direct parent loader in E .
4.2 Trusted Environments
Theorem (Trusted Environments) states that even if we follow the ndClass
scheme, the JVM never violates constraints only if all parent loaders are system
loaders.
We st dene system environments.
Denition 4.4 (System Environment)
The above predicate denes a condition that system environments should satisfy.
That is, when all system classes are loaded, any class name appearing in any
method descriptor should have been resolved.
THEOREM (Trusted Environments)
The following proposition is satised if and only if i  1,
called a trusted environment if it satises the consequence of the theorem.
The theorem states that E 1 is a trusted environment and E 2 is not. For example,
applet loaders are inside a certain E 1 and applets never violate constraints.
Prior to the proof of the theorem, we introduce an additional relation. The
l 0 , means there is a one-step constraint between l and l 0 .
We allow (method resolution), (method overriding), and (symmetry) in Deni-
tion 2.7. If we ignore the symmetry, there are two cases in which E ' l n
l 0
holds. Assume wf method(E) in Section 2.3.5 for now.
There is a method resolution
where l Remember that l should be the context which
resolves classname.
This implies that if wf parent(E; P ), then SRclass:cl vP l. Note that
also holds from wf method (E) and Def.3.1.
Generally, if the one-step subtyping relation, holds, then for
any P such that wf parent(E; P ), we have
from Def.2.1 and Def.4.2. Consequently, the subtyping relation, sub  , also
implies vP . Therefore, if wf parent(E; P ), then
holds.
Otherwise, we have the overrides relation,
In this case, according to Section 3, there
are a class, c, which selects m, and a superclass of c, which selects m 0 .
The fact implies the following one.
Therefore,
From Def.4.1, if a loader has two dierent (indirect or direct) parent load-
ers, then one is a (direct) parent of the other, so we have
In both cases, we have the following result with respect to n
l 0 =) l vP l 0 _ l 0 vP l ::[i]
Furthermore, we can easily show the following in both cases.
Note that l <P l 0 abbreviates l vP l From these results, Theorem
(Trusted Environment) can be proved as follows:
(proof)
Assume that there are given E
Assume that l and l 0
l 0 and also l <P l 0 . Def.4.3
implies that l should be a system loader. Therefore [ii] implies:
Note that a method dened by some system loader should be a
system method (cf. Def.4.3). From Def.4.4, we have
Our next goal is to prove the following fact.
This is proved by induction on the derivation of the loading con-
straint, l n
l 0 . Suppose that the following one-step constraint is
appended to above l n
l 0 to generate l n
l 00 by the transitivity.
l 00
We assume by the induction hypothesis and show
l 0 vP l 00 _ l 00
The left case of the disjunction, l 0 vP l 00 , is easy since vP is transi-
tive. Therefore, assume l 00 <P l 0 . In this case, [iii] says that there
exists c 0 in E 1 :T Class which satises
Together with Def.4.2, this leads to
the induction hypothesis implies
implies
Some c;
so l 00 is derived from E 1 ' c 0 :cl vP l 00 .
Lemma [iv] naturally leads to
bridge
It is easy to show that bridge safe(E) holds if
We can make a counter example which violates con-
straints. For example, E 1 is as follows.
loader 0.
{ Loader 0 denes class C.
Class C has method M with signature [X].
does not satisfy system(E 1 ), we assume that class X is never
resolved by loader 0, i.e.,
where m is the method M resolved by loader 0 (= m:cl). Additionally,
loader 1.
{ Loader 1 denes class D.
Class D calls method M of class C with signature [X].
{ Loader 1 denes class X.
{ Loader 1 delegates to loader 0 for other classes.
loader 2.
{ Loader 2 denes class D.
Class D extends C.
Class D has method M with signature [X].
{ Loader 2 denes class X.
{ Loader 2 delegates to loader 0 for other classes.
We can assume that
where c is the class, C, dened by loader Obviously, M in loader 2
overrides m. Therefore, from the denition of  - , we have
2:
However, X in loader 1 and X in 1 are dierent. Therefore, bridge
does not hold.
5 Conclusion
We have presented a new model of the JVM, which explains various unique features
of the JVM, and also species several conditions on its implementations.
In particular, the model includes the loading constraint scheme and the ndclass
scheme, both of which are new features of JDK1.2, Through the formalization,
we could analyze the extremely subtle relationship between the loading constraint
scheme and the bytecode verication. We believe that such an analysis
is possible only through a rigorous formalization and soundness proofs.
However, our model excludes many features of the JVM: its primitive types,
eld members, array types, member modiers, threads, most of its instructions,
etc. We have several ideas to incorporate them into our model. For example,
our model can easily express the object and class nalization of the JVM. The
soundness theorem in Section 2.5 states that when an environment is updated
into a larger environment, the well-typedness invariant is preserved. There-
fore, if we can introduce a reduced environment which also preserves the same
invariant, then the soundness of the nalization is guaranteed.
As for the ndclass scheme, we showed that it should work with the loading
constraint scheme. However, we have also obtained a method which allows
some loading constraints to be omitted under the cooperation with the ndclass
scheme. This result is not included in this paper, as we do not think that it is
the best solution, and we expect that both schemes should be improved in the
future.



--R

Linking and Moduralization
Formal Aspects of Mobile Code Security
Web Browers and Beyond.
A Type System for Object Initialization in the Java Bytecode Language
A speci
Security and Dynamic Class Loading in Java: A Formalisation
On a New Method for Data ow Analysis of Java Virtual Machine Subroutines
Dynamic Class Loading in the Java Virtual Ma- chine
The Java Virtual Machine Speci
Java light is type-safe - de nitely
Proving the Soundness of a Java Bytecode Veri
A Formal Speci
Java is not type-safe
Nicht veri
A Type System for Java Bytecode Subroutines
Careful Analysis of Type Spoo
A compositional account of the Java virtual machine
--TR

--CTR
Modeling multiple class loaders by a calculus for dynamic linking, Proceedings of the 2004 ACM symposium on Applied computing, March 14-17, 2004, Nicosia, Cyprus
class loading;security