Xavier Leroy
email: xavier.leroy@inria.fr

Java bytecode verification: algorithms and formalizations

Bytecode verification is a crucial security component for Java applets, on the Web and on embedded devices such as smart cards. This paper reviews the various bytecode verification algorithms that have been proposed, recasts them in a common framework of dataflow analysis, and surveys the use of proof assistants to specify bytecode verification and prove its correctness.

Introduction

Web applets have popularized the idea of downloading and executing untrusted compiled code on the personal computer running the Web browser, without user's approval or intervention. Obviously, this raises major security issues: without appropriate security measures, a malicious applet could mount a variety of attacks against the local computer, such as destroying data (e.g. reformatting the disk), modifying sensitive data (e.g. registering a bank transfer via a home-banking software [START_REF] Brunnstein | Hostile ActiveX control demonstrated[END_REF]), divulging personal information over the network, or modifying other programs (Trojan attacks).

Beyond Web services, the applet model is now being transferred to high-security embedded devices such as smart cards: the Java Card architecture [START_REF] Chen | Java Card Technology for Smart Cards: Architecture and Programmer's Guide. The Java Series[END_REF] allows for post-issuance downloading of applets on smart cards. Smart cards are used as security tokens in sensitive application areas such as payment, mobile telephony, and authentication. This makes the security issues with applets even more acute.

The solution put forward by the Java programming environment is to execute the applets in a so-called "sandbox", which is an insulation layer preventing direct access to the hardware resources and implementing a suitable access control policy [START_REF] Gong | Inside Java 2 platform security: architecture, API design, and implementation[END_REF][START_REF] Vigna | Mobile Agents and Security[END_REF][START_REF] Mcgraw | Securing Java[END_REF]. The security of the sandbox model relies on the following three components:

1. Applets are not compiled down to machine executable code, but rather to bytecode for a virtual machine. The virtual machine manipulates higher-level, more secure abstractions of data than the hardware processor, such as object references instead of memory addresses.

2. Applets are not given direct access to hardware resources such as the serial port, but only to a carefully designed set of API classes and methods that perform suitable access control before performing interactions with the outside world on behalf of the applet.

3. Upon downloading, the bytecode of the applet is subject to a static analysis called bytecode verification, whose purpose is to make sure that the code of the applet is well typed and does not attempt to bypass protections 1 and 2 above by performing ill-typed operations at run-time, such as forging object references from integers, illegal casting of an object reference from one class to another, calling directly private methods of the API, jumping in the middle of an API method, or jumping to data as if it were code [START_REF] Gosling | Java intermediate bytecodes[END_REF][START_REF] Yellin | Low level security in Java[END_REF][START_REF] Lindholm | The Java Virtual Machine Specification[END_REF].

Thus, bytecode verification is a crucial security component in the Java "sandbox" model: any bug in the verifier causing an ill-typed applet to be accepted can potentially enable a security attack. At the same time, bytecode verification is a complex process involving elaborate program analyses. Consequently, considerable research efforts have been expended to specify the goals of bytecode verification, formalize bytecode verification algorithms, and prove their correctness.

The purpose of the present paper is to survey this work on bytecode verification. We explain what bytecode verification is, describe the various algorithms that have been proposed, outline the main problems they are faced with, and give references to machine-assisted proofs of correctness.

The remainder of this paper is organized as follows. Section 2 gives a quick overview of the Java virtual machine and of bytecode verification. Section 3 presents the basic bytecode verification algorithm based on dataflow analysis. Sections 4 and 5 concentrate on two delicate verification issues: checking object initialization and dealing with JVM subroutines. Section 6 presents polyvariant verification algorithms that address the subroutine issue. Some issues specific to low-resources embedded systems are discussed in section 7, followed by conclusions and perspectives in section 8.

Overview of the JVM and of bytecode verification

The Java Virtual Machine (JVM) [START_REF] Lindholm | The Java Virtual Machine Specification[END_REF] is a conventional stack-based abstract machine. Most instructions pop their arguments off the stack, and push back their results on the stack. In addition, a set of registers (also called local variables) is provided; they can be accessed via "load" and "store" instructions that push the value of a given register on the stack or store the top of the stack in the given register, respectively. While the architecture does not mandate it, most Java compilers use registers to store the values of source-level local variables and method parameters, and the stack to hold temporary results during evaluation of expressions. Both the stack and the registers are part of the activation record for a method. Thus, they are preserved across method calls. The entry point for a method specifies the number of registers and stack slots used by the method, thus allowing an activation record of the right size to be allocated on method entry.

Control is handled by a variety of intra-method branch instructions: unconditional branch ("goto"), conditional branches ("branch if top of stack is 0"), multi-way branches (corresponding to the switch Java construct). Exception handlers can be specified as a table of (pc 1 , pc 2 , C, h) quadruples, meaning that if an exception of class C or a subclass of C is raised by any instruction between locations pc 1 and pc 2 , control is transferred to the instruction at h (the exception handler).

About 200 instructions are supported, including arithmetic operations, comparisons, object creation, field accesses and method invocations. The example in Figure 1 should give the general flavor of JVM bytecode.

An important feature of the JVM is that most instructions are typed. For instance, the iadd instruction (integer addition) requires that the stack initially contains at least two elements, and that these two elements are of type int; it then pushes back a result of type int. Similarly, a Source Java code:

static int factorial(int n) {
int res; for (res = 1; n > 0; n--) res = res * n; return res; } Corresponding JVM bytecode: method static int factorial(int), 2 registers, 2 stack slots 0: iconst_1 // push the integer constant 1 1: istore_1 // store it in register 1 (the res variable) 2: iload_0 // push register 0 (the n parameter) 3: ifle 14 // if negative or null, go to PC 14 6: iload_1 // push register 1 (res) 7: iload_0 // push register 0 (n) 8: imul // multiply the two integers at top of stack 9: istore_1 // pop result and store it in register 1 10: iinc 0, -1 // decrement register 0 (n) by 1 11: goto 2 // go to PC 2 14: iload_1 // load register 1 (res) 15: ireturn // return its value to caller Figure 1: An example of JVM bytecode getfield C.f.τ instruction (access the instance field f of type τ declared in class C) requires that the top of the stack contains a reference to an instance of class C or one of its sub-classes (and not, for instance, an integer -this would correspond to an attempt to forge an object reference by an unsafe cast); it then pops it and pushes back a value of type τ (the value of the field f ). More generally, proper operation of the JVM is not guaranteed unless the code meets at least the following conditions:

• Type correctness: the arguments of an instruction are always of the types expected by the instruction.

• No stack overflow or underflow: an instruction never pops an argument off an empty stack, nor pushes a result on a full stack (whose size is equal to the maximal stack size declared for the method).

• Code containment: the program counter must always point within the code for the method, to the beginning of a valid instruction encoding (no falling off the end of the method code; no branches into the middle of an instruction encoding).

• Register initialization: a load from a register must always follow at least one store in this register; in other terms, registers that do not correspond to method parameters are not initialized on method entrance, and it is an error to load from an uninitialized register.

• Object initialization: when an instance of a class C is created, one of the initialization methods for class C (corresponding to the constructors for this class) must be invoked before the class instance can be used.

One way to guarantee these conditions is to check them dynamically, while executing the bytecode. This is called the "defensive JVM approach" in the literature [START_REF] Cohen | The defensive Java virtual machine specification[END_REF]. However, checking these conditions at run-time is expensive and slows down execution significantly. The purpose of bytecode verification is to check these conditions once and for all, by static analysis of the bytecode at loading-time. Bytecode that passes verification can then be executed faster, omitting the dynamic checks for the conditions above.

It must be emphasized that bytecode verification by itself does not guarantee secure execution of the code: many crucial properties of the code still need to be checked dynamically, for instance via array bounds checks and null pointer checks in the virtual machine, and access control checks in the API. The purpose of bytecode verification is to shift the verifications listed above from run-time to loading-time.

Basic verification by dataflow analysis

The first JVM bytecode verification algorithm is due to Gosling and Yellin at Sun [START_REF] Gosling | Java intermediate bytecodes[END_REF][START_REF] Yellin | Low level security in Java[END_REF][START_REF] Lindholm | The Java Virtual Machine Specification[END_REF]. Almost all existing bytecode verifiers implement this algorithm. It can be summarized as a dataflow analysis applied to a type-level abstract interpretation of the virtual machine. Some advanced aspects of the algorithm that go beyond standard dataflow analysis are described in sections 4 and 5. In this section, we describe the basic ingredients of this algorithm: the type-level abstract interpreter and the dataflow framework.

iconst n : (S, R) → (int.S, R) if |S| < M stack ineg : (int.S, R) → (int.S, R) iadd : (int.int.S, R) → (int.S, R) iload n : (S, R) → (int.S, R) if 0 ≤ n < M reg and R(n) = int and |S| < M stack istore n : (int.S, R) → (S, R{n ← int}) if 0 ≤ n < M reg aconst null : (S, R) → (null.S, R) if |S| < M stack aload n : (S, R) → (R(n).S, R) if 0 ≤ n < M reg and R(n) <: Object and |S| < M stack astore n : (τ.S, R) → (S, R{n ← τ }) if 0 ≤ n < M reg and τ <: Object getfield C.f.τ : (τ .S, R) → (τ.S, R) if τ <: C putfield C.f.τ : (τ 1 .τ 2 .S, R) → (S, R) if τ 1 <: τ and τ 2 <: C invokestatic C.m.σ : (τ n . . . τ 1 .S, R) → (τ.S, R) if σ = τ (τ 1 , . . . , τ n ), τ i <: τ i for i = 1 . . . n, and |τ.S| ≤ M stack invokevirtual C.m.σ : (τ n . . . τ 1 .τ .S, R) → (τ.S, R) if σ = τ (τ 1 , . . . , τ n ), τ <: C, τ i <: τ i for i = 1 . . . n, |τ.S| ≤ M stack

The type-level abstract interpreter

At the heart of all bytecode verification algorithms described in this paper is an abstract interpreter for the JVM instruction set that executes JVM instructions like a defensive JVM (including type tests, stack underflow and overflow tests, etc), but operates over types instead of values. That is, the abstract interpreter manipulates a stack of types (a sequence of types) and a register type (a tuple of types associating a type to each register number). It simulates the execution of instructions at the level of types. For instance, for the iadd instruction (integer addition), it checks that the stack of types contains at least two elements, and that the top two elements are the type int. It then pops the top two elements and pushes back the type int corresponding to the result of the addition.

Figure 2 defines more formally the abstract interpreter on a number of representative JVM instructions. The abstract interpreter is presented as a transition relation i : (S, R) → (S , R ), where i is the instruction, S and R the stack type and register type before executing the instruction, and S and R the stack type and register type after executing the instruction. Errors such as type mismatches on the arguments, stack underflow, or stack overflow, are denoted by the absence of a transition. For instance, there is no transition on iadd from an empty stack.

Notice that method invocations (such as the invokestatic and invokevirtual instructions in Figure 2) are not treated by branching to the code of the invoked method, like the concrete JVM does, but simply assume that the effect of the method invocation on the stack is as described by the method signature given in the "invoke" instruction. All bytecode verification algorithms described in this paper proceed method per method, assuming that all other methods are well-typed when verifying the code of a method. A simple coinductive argument shows that if this is the case, the program as a whole (the collection of all methods) is well typed. The types manipulated by the abstract interpreter are similar to the source-level types of the Java language. They include primitive types (int, long, float, double), array types, and object reference types represented by the fully qualified names of the corresponding classes. The boolean, byte, short and char types of Java are identified with int. Three extra types are introduced: null to represent the type of the null reference, ⊥ to represent the absence of any value (at unreachable instructions), and to represent the contents of uninitialized registers, that is, any value. ("Load" instructions explicitly check that the accessed register does not have type , thus detecting accesses to uninitialized registers.)

Object int float C D E Object[] C[] D[] E[] int[] float[] Object[][] C[][] D[][] E[][] null
These types are equipped with a subtyping relation, written <:, which is essentially identical to the subtyping relation of the Java language (the "assignment compatibility" predicate). Figure 3 illustrates the subtyping relation. Precise definitions of <: can be found in [START_REF] Rose | Vérification de code d'octet de la machine virtuelle Java: formalisation et implantation[END_REF][START_REF] Nipkow | Verified bytecode verifiers[END_REF][START_REF] Klein | Verified bytecode verifiers[END_REF][START_REF] Klein | Verified Java bytecode verification[END_REF], but are omitted here. For the purposes of this article, all we require from the subtyping relation is the following property: Property 1 (Well-founded semi-lattice.) The set of types ordered by the <: relation is a semilattice: any pair of types has a least upper bound. Moreover, the <: ordering is well founded: there does not exist infinite strictly increasing sequences of types.

The <: relation between types is extended pointwise to register types and stack types. Two stack types are in the <: relation only if they have the same size. It is easy to see that the <: relation on register types and on stack types is well founded.

The type-level abstract interpreter must satisfy several formal properties. First and foremost is correctness with respect to the dynamic semantics of the defensive JVM: if the abstract interpreter can do a transition i : (S, R) → (S , R ), then for all concrete states (s, r) matching (S, R), the defensive JVM, started in state (s, r), will not stop on a run-time type violation: it will either loop or transition to a state (s , r ) that matches (S , R ). This correctness property was formalized and proved by several authors, including Pusch [START_REF] Pusch | Proving the soundness of a Java bytecode verifier specification in Isabelle/HOL[END_REF] (using the Isabelle/HOL prover), Coglio et al [START_REF] Coglio | Towards a provably-correct implementation of the JVM bytecode verifier[END_REF] (using SpecWare), Goldberg [START_REF] Goldberg | A specification of Java loading and bytecode verification[END_REF] and Qian [START_REF] Qian | A formal specification of Java virtual machine instructions for objects, methods and subroutines[END_REF] (using standard mathematics).

i : (S, R) → (S 1 , R 1 ) and i : (S, R) → (S 2 , R 2 ), then S 1 = S 2 and R 1 = R 2 .
Property 3 (Monotonicity.) If i : (S, R) → (S , R ), then for all stack types S 1 <: S and register types R 1 <: R, there exists a stack type S 1 and a register type R 1 such that i : (S 1 , R 1 ) → (S 1 , R 1 ), and moreover S 1 <: S and R 1 <: R.

The dataflow analysis

Verifying a method whose body is a straight-line piece of code (no branches) is easy: we simply iterate the transition function of the abstract interpreter over the instructions, taking the stack type and register type "after" the preceding instruction as the stack type and register type "before" the next instruction. The initial stack and register types reflect the state of the JVM on method entrance: the stack type is empty; the types of the registers 0 . . . n -1 corresponding to the n method parameters are set to the types of the corresponding parameters in the method signature; the other registers n . . . M reg -1 corresponding to uninitialized local variables are given the type . If the abstract interpreter gets "stuck", i.e. cannot make a transition from one of the intermediate states, then verification fails and the code is rejected. Otherwise, verification succeeds, and since the abstract interpreter is a correct approximation of a defensive JVM, we are certain that a defensive JVM will not get stuck either executing the code. Thus, the code is correct and can be executed safely by a regular, non-defensive JVM.

Branches and exception handlers introduce forks and joins in the control flow of the method. Thus, an instruction can have several predecessors, with different stack and register types "after" these predecessor instructions. Sun's bytecode verifier deals with this situation in the manner customary for data flow analysis: the state (stack type and register type) "before" an instruction is taken to be the least upper bound of the states "after" all predecessors of this instruction. For instance, assume classes D and E extend C, and we analyze a conditional construct that stores a value of type D in register 0 in one arm, and a value of type E in the other arm. (See Figure 4.) When the two arms meet, register 0 is assumed to have type C, which is the least upper bound (the smallest common supertype) of D and E.

More precisely, write instr (p) for the instruction at program point p, in(p) for the state "before" the instruction at p, and out(p) for the state "after" the instruction at p. The verification algorithm sets up the following forward dataflow equations:

instr (p) : in(p) → out(p) in(p) = lub{out(q) |
q predecessor of p} for every valid program point p, plus in(0) = (ε, (P 0 , . . . , P n-1 , , . . . , ))

for the entry point (the P k are the types of the method parameters). These equations are then solved by standard fixpoint iteration using Kildall's worklist algorithm [35, section 8.4]: a program point p is taken from the worklist and its state "after" out(p) is determined from its state "before" in(p) using the abstract interpreter; then, we replace in(q) by lub(in(q), out(p)) for each successor q of p, and enter those successors q for which in(q) changed in the worklist. The fixpoint is reached when the worklist is empty, in which case verification succeeds. Verification fails if a state with no transition is encountered, or one of the least upper bounds is undefined.

As a trivial optimization of the algorithm above, the dataflow equations can be set up at the level of extended basic blocks rather than individual instructions. In other terms, it suffices to keep in working memory the states in(p) where p is the beginning of an extended basic block (i.e. a branch target); the other states can be recomputed on the fly as needed.

The least upper bound of two states is taken pointwise, both on the stack types and the register types. It is undefined if the stack types have different heights, which causes verification to fail. This situation corresponds to a program point where the run-time stack can have different heights depending on the path by which the point is reached; such code cannot be proved correct in the framework described in this section, and must be rejected. (See section 6.2 for an alternate verification algorithm that can handle this situation.)

The least upper bound of two types for a register (or stack slot) can be , causing this register to have type in the merged state. This corresponds to the situation where a register holds values of incompatible types in two arms of a conditional (e.g. int in one arm and an object reference in the other), and therefore is treated as uninitialized (no further loads from this register) after the merge point.

Several formalizations and proofs (on paper or on machine) of the bytecode verification algorithm described above have been published. Nipkow and Klein's development in Isabell/HOL [START_REF] Nipkow | Verified bytecode verifiers[END_REF][START_REF] Klein | Verified bytecode verifiers[END_REF][START_REF] Klein | Verified Java bytecode verification[END_REF] is the closest to the dataflow presentation that we gave above. Other formalizations and correctness proofs of the dataflow approach include those of Qian [START_REF] Qian | A formal specification of Java virtual machine instructions for objects, methods and subroutines[END_REF], Coglio et al [START_REF] Coglio | Towards a provably-correct implementation of the JVM bytecode verifier[END_REF], and Stärk et al [START_REF] Stärk | Java and the Virtual Machine[END_REF]. Bytecode verification can also be specified and proved sound using type systems [START_REF] Stata | A type system for Java bytecode subroutines[END_REF][START_REF] Freund | A formal framework for the java bytecode language and verifier[END_REF][START_REF] Freund | A type system for the Java bytecode language and verifier[END_REF]; in this framework, the forward dataflow analysis algorithm that we described can be viewed as a type inference algorithm for these type systems. Hartel and Moreau [START_REF] Hartel | Formalizing the safety of Java, the Java virtual machine and Java Card[END_REF] survey other approaches.

Interfaces and least upper bounds

The dataflow framework presented above requires that the type algebra, ordered by the subtyping relation, constitutes a semi-lattice. That is, every pair of types possesses a smallest common supertype (least upper bound).

Unfortunately, this property does not hold if we take the verifier type algebra to be the Java source-level type algebra (extended with and null) and the subtyping relation to be the Java source-level assignment compatibility relation. The problem is that interfaces are types, just like classes, and a class can implement several interfaces. Consider the following classes:

interface I { ... } interface J { ... } class C1 implements I, J { ... } class C2 implements I, J { ... }
The subtyping relation induced by these declarations is:

Object I J C1 C2
This is obviously not a semi-lattice, since the two types C1 and C2 have two common super-types I and J that are not comparable (neither is subtype of the other).

There are several ways to address this issue. One approach is to manipulate sets of types during verification instead of single types as we described earlier. These sets of types are to be interpreted as conjunctive types, i.e. the set {I, J}, like the conjunctive type I ∧ J, represents values that have both types I and J, and therefore is a suitable least upper bound for the types {C1} and {C2} in the example above. This is the approach followed in [START_REF] Goldberg | A specification of Java loading and bytecode verification[END_REF][START_REF] Qian | A formal specification of Java virtual machine instructions for objects, methods and subroutines[END_REF][START_REF] Pusch | Proving the soundness of a Java bytecode verifier specification in Isabelle/HOL[END_REF][START_REF] Stärk | Java and the Virtual Machine[END_REF].

Another approach is to complete the class and interface hierarchy of the program into a lattice before performing verification [START_REF] Knoblock | Type elaboration and subtype completion for Java bytecode[END_REF]. This is an instance of a general mathematical construction known as the Dedekind-MacNeille completion of a poset. In the example above, the completion would add a point IandJ to the lattice of types, which is a subtype of both I and J, and a supertype of C1 and C2. We then obtain the following semi-lattice:

Object I J IandJ C1 C2
The additional type IandJ plays the same role as the type set {I, J} in the first approach described above. The difference is that the completion of the class/interface hierarchy is performed once and for all, and verification manipulates only simple types rather than sets of types. This keeps verification simple and fast.

The simplest solution to the interface problem is to be found in Sun's implementation of the JDK bytecode verifier. (This approach is documented nowhere, but can easily be inferred by experimentation.) Namely, bytecode verification ignores interfaces, treating all interface types as the class type Object. Thus, the type algebra used by the verifier contains only proper classes and no interfaces, and subtyping between proper classes is simply the inheritance relation between them. Since Java has single inheritance (a class can implement several interfaces, but inherit from one class only), the subtyping relation is tree-shaped and trivially forms a semi-lattice: the least upper bound of two classes is simply their closest common ancestor in the inheritance tree.

The downside of Sun's approach, compared with the set-based or completion-based approach, is that the verifier cannot guarantee statically that an object reference implements a given interface. In particular, the invokeinterface I.m instruction, which invokes method m of interface I on an object, is not guaranteed to receive at run-time an object that actually implements I: the only guarantee provided by Sun's verifier is that it receives an argument of type Object, that is, any object reference. The invokeinterface I.m instruction must therefore check dynamically that the object actually implements I, and raise an exception if it does not.

Verifying object initialization

Object creation in the Java virtual machine is a two-step process: first, the instruction new C creates a new object, instance of the class C, with all instance fields filled with default values (0 for numerical fields and null for reference fields); second, one of the initialization methods for class C (methods named C.<init> resulting from the compilation of the constructors of class C) must be invoked on the newly created object. Initialization methods, just like their source-level counterpart (constructors), are typically used to initialize instance fields to non-default values, although they can also perform nearly arbitrary computations.

The JVM specification requires that this two-step object initialization protocol be respected. That is, the object instance created by the new instruction is considered uninitialized, and none of the regular object operations (i.e. store the object in a data structure, return it as method result, access one of its fields, invoke one of its methods) is allowed on this uninitialized object. Only when one of the initialization methods for its class is invoked on the new object and returns normally is the new object considered fully initialized and usable like any other object. (Additional restrictions that we will not discuss here are imposed on initialization methods themselves; see [START_REF] Lindholm | The Java Virtual Machine Specification[END_REF][START_REF] Freund | A type system for object initialization in the Java bytecode language[END_REF][START_REF] Freund | A type system for the Java bytecode language and verifier[END_REF].)

Unlike the register initialization property, this object initialization property is not crucial to ensure type safety at run-time: since the new instruction initializes the instance fields of the new object with correct values for their types, type safety is not broken if the resulting default-initialized object is used right away without having called an initializer method. However, the object initialization property is important to ensure that some invariants between instance fields that is established by the constructor of a class actually hold for all objects of this class.

Static verification of object initialization is made more complex by the fact that initialization methods operate by side-effect: instead of taking an uninitialized object and returning an initialized object, they simply take an uninitialized object, update its fields, and return nothing. Hence, the code generated by Java compilers for the source-level statement x = new C(arg) is generally of the following form: That is, two references to the uninitialized instance of C are held on the stack. The topmost reference is "consumed" by the invocation of C.<init>. When this initializer returns, the second reference is now at the top of the stack and now references a properly initialized object, which is then stored in the register allocated to x. The tricky point is that the initializer method is applied to one object reference on the stack, but it is another object reference contained in the stack (which happens to reference the same object) whose status goes from "uninitialized" to "fully initialized" in the process. As demonstrated above, static verification of object initialization requires a form of alias analysis (more precisely a must-alias analysis) to determine which object references in the current state are guaranteed to refer to the same uninitialized object that is passed as argument to an initializer method. While any must-alias analysis can be used, Sun's verifier uses a fairly simple analysis, whereas an uninitialized object is identified by the position (program counter value) of the new instruction that created it. More precisely, the type algebra is enriched by the types C p denoting an uninitialized instance of class C created by a new instruction at PC p. An invocation of an initializer method C.<init> checks that the first argument of the method is of type C p for some p, then pops the arguments off the stack type as usual, and finally finds all other occurrences of the type C p in the abstract interpreter state (stack type and register types) and replaces them by C.

The following example shows how this works for a nested initialization corresponding to the Java expression new C(new C(null)):

0: new C // stack type after: C 0 3: dup // C 0 , C 0 4: new C // C 0 , C 0 , C 4 7: dup // C 0 , C 0 , C 4 , C 4 8: aconst_null // C 0 , C 0 , C 4 , C 4 , null 9: invokespecial C.<init> // C 0 , C 0 , C 12: invokespecial C.<init> // C 15: ...
In particular, the first invokespecial initializes only the instance created at PC 4, but not the one created at PC 0.

This approach is correct only if at any given time, the machine state contains at most one uninitialized object created at a given PC. Thus, the verifier must prevent situations where several distinct objects created by the same instruction new C at p can be "in flight": these would be given the same type C p , and initializing one would cause the verifier to assume incorrectly that the others are also initialized. This could potentially happen if a new instruction is executed repeatedly as part of a loop; another example involving subroutines is given in [START_REF] Freund | A type system for object initialization in the Java bytecode language[END_REF].

To avoid this problem, Sun's verifier requires that no uninitialized object type appear in the machine state when a backward branch is taken. Freund and Mitchell [START_REF] Freund | A type system for object initialization in the Java bytecode language[END_REF] formalize a simpler, equally effective restriction: they propose that when verifying a new C instruction at location p, there must be no occurrence of the type C p in the stack type and register type at p. Bertot [START_REF] Bertot | Formalizing a JVML verifier for initialization in a theorem prover[END_REF] proves the correctness of this approach using the Coq theorem prover, and extracts a verification algorithm from the proof. (Bertot's algorithm is not a standard dataflow analysis, since it features an additional pass of constraint solving.) Both Sun's restriction and Freund and Mitchell's restriction are not monotone, in the sense that raising the type of a register or stack location from C p to can transform an abstract state from which no transitions are possible into an abstract state from which a transition is possible. In other terms, property 3 does not hold, and this causes difficulties with dataflow analysis. To address this issue, a modified formulation of Freund and Mitchell's restriction is introduced in [START_REF] Stärk | Java and the Virtual Machine[END_REF] and used in [START_REF] Klein | Verified bytecode verifiers[END_REF][START_REF] Klein | Verified Java bytecode verification[END_REF][START_REF] Freund | A type system for the Java bytecode language and verifier[END_REF]: a new C instruction at location p does not fail if there are occurrences of the type C p in the stack and register types before p; instead, it sets these entries to in the resulting state.

This suffices to enforce non-aliasing (the unitialized objects whose types were set to cannot be initialized nor used later on), while respecting the monotonicity property. Subroutines, as described in section 5, complicate the verification of object initialization. As discovered by Freund and Mitchell [START_REF] Freund | A type system for object initialization in the Java bytecode language[END_REF], a new instruction inside a subroutine can result in distinct uninitialized objects having the same static type C p , thus fooling Sun's verifier into believing that all of them become initialized after invoking an initialization method on one of them. The solution is to prohibit or set to all registers and stack locations that have type C p across a subroutine call.

Coglio [START_REF] Coglio | Improving the official specification of Java bytecode verification[END_REF] observes that Sun's restriction on backward branches as well as Freund and Mitchell's restriction on new are unnecessary for a bytecode verifier based on monovariant dataflow analysis. More precisely, [9, section 5.8.2] shows that, in the absence of subroutines, a register or stack location cannot have the type C p just before a program point p containing a new C instruction. Thus, the only program points where uninitialized object types in stack types or register types must be prohibited (or turned into ) are subroutine calls.

Subroutines

Subroutines in the JVM are code fragments that can be called from several points inside the code of a method. To this end, the JVM provides two instructions: jsr branches to a given label in the method code and pushes a return address to the following instruction; ret recovers a return address (from a register) and branches to the corresponding instruction. Subroutines are used to compile certain exception handling constructs, and can also be used as a general code-sharing device. The difference between a subroutine call and a method invocation is that the body of the subroutine executes in the same activation record as its caller, and therefore can access and modify the registers of the caller.

The verification problem with subroutines

Subroutines complicate significantly bytecode verification by dataflow analysis. First, it is not obvious to determine the successors of a ret instruction, since the return address is a first-class value. As a first approximation, we can say that a ret instruction can branch to any instruction that follows a jsr in the method code. (This approximation is too coarse in practice; we will describe better approximations later.) Second, the subroutine entry point acts as a merge point in the control-flow graph, causing the register types at the points of call to this subroutine to be merged. This can lead to excessive loss of precision in the register types inferred, as the example in Figure 5 shows.

The two jsr 100 at 0 and 52 have 100 as successor. At 0, register 0 has type ; at 52, it has type int. Thus, at 100, register 0 has type (the least upper bound of and int). The subroutine body (between 101 and 110) does not modify register 0, hence its type at 110 is still . The ret 1 at 110 has 3 and 55 as successors (the two instructions following the two jsr 100). Thus, at 55, register 0 has type and cannot be used as an integer by instructions 55 and 56. This code is therefore rejected.

This behavior is counter-intuitive. Calling a subroutine that does not use a given register does not modify the run-time value of this register, so one could expect that it does not modify the // register 0 uninitialized here 0: jsr 100 // call subroutine at 100 3: ... The subroutine-based compilation scheme for the try. . . finally construct produces code very much like the above, with a register being uninitialized at one call site of the subroutine and holding a value preserved by the subroutine at another call site. Hence it is crucial that similar code passes bytecode verification. In the remainder of this section and in section 6, we will present refinements of the dataflow-based verification algorithm that achieve this goal.

Sun's solution

We first describe the approach implemented in Sun's JDK verifier. It is described informally in [33, section 4.9.6], and formalized (with various degrees of completeness and faithfulness to Sun's implementation) in [START_REF] Stata | A type system for Java bytecode subroutines[END_REF][START_REF] Qian | A formal specification of Java virtual machine instructions for objects, methods and subroutines[END_REF][START_REF] Stärk | Java and the Virtual Machine[END_REF][START_REF] Freund | A type system for the Java bytecode language and verifier[END_REF][START_REF] Stärk | Completeness of a bytecode verifier and a certifying Java-to-JVM compiler[END_REF]. This approach implements the intuition that a call to a subroutine should not change the types of registers that are not used in the subroutine body.

First, we need to make precise what a "subroutine body" is: since JVM bytecode is unstructured, subroutines are not syntactically delimited in the code; subroutine entry points are easily detected (as targets of jsr instructions), but it is not immediately apparent which instructions can be reached from a subroutine entry point. Thus, a dataflow analysis is performed, either before or in parallel with the main type analysis. The outcome of this analysis is a consistent labeling of every instruction by the entry point(s) for the subroutine(s) it logically belongs to. From this labeling, we can then determine, for each subroutine entry point , the return instruction Ret( ) for the subroutine, and the set of registers Used ( ) that are read or written by instructions belonging to that subroutine.

The dataflow equation for subroutine calls is then as follows. Let i be an instruction jsr , and j be the instruction immediately following i. Let (S jsr , R jsr ) = out(i) be the state "after" the jsr, and (S ret , R ret ) = out(Ret( )) be the state "after" the ret that terminates the subroutine. Then:

in(j) = S ret , {r → R ret (r) if r ∈ Used ( ) R jsr (r) if r / ∈ Used ( ) }
In other terms, the state "before" the instruction j following the jsr is identical to the state "after" the ret, except for the types of the registers that are not used by the subroutine, which are taken from the state "after" the jsr.

In the example above, we have Ret(100) = 110 and register 0 is not in Used (100). Hence the type of register 0 before instruction 55 (the instruction following the jsr) is equal to the type after instruction 52 (the jsr itself), that is int, instead of (the type of register 0 after the ret 1 at 110).

While effective in practice, Sun's approach to subroutine verification raises a challenging issue: determining the subroutine structure is difficult. Not only are subroutines not syntactically delimited, but return addresses are stored in general-purpose registers rather than on a subroutinespecific stack, which makes tracking return addresses and matching ret/jsr pairs more difficult. To facilitate the determination of the subroutine structure, the JVM specification states a number of restrictions on correct JVM code, such as "two different subroutines cannot 'merge' their execution to a single ret instruction" [33, section 4.9.6]. These restrictions seem rather ad-hoc and specific to the particular subroutine labeling algorithm that Sun's verifier uses. Moreover, the description of subroutine labeling given in the JVM specification is very informal and incomplete.

Several rational reconstructions and formalizations of this part of Sun's verifier have been published. The presentations closest to Sun's implementation are due to Qian [START_REF] Qian | A formal specification of Java virtual machine instructions for objects, methods and subroutines[END_REF] and Stärk et al [START_REF] Stärk | Java and the Virtual Machine[END_REF]. A characteristic feature of Sun's implementation, correctly captured by these presentations, is that the subroutine structure and the Used ( ) sets are not determined prior to setting up and solving the dataflow equations, as we suggested above; instead, the types and the Used ( ) sets are inferred simultaneously during the dataflow analysis. This simultaneous computation of types and Used ( ) sets complicates the analysis: as shown by Qian [START_REF] Qian | Standard fixpoint iteration for Java bytecode verification[END_REF], the transfer function of the dataflow analysis is no longer monotonous, and special iteration strategies are required to reach the fixpoint.

Other approaches to the verification of subroutines

Many alternatives to Sun's verification of subroutine have been proposed in the literature, often in the context of small subsets of the JVM, leading to algorithms that are simpler and more elegant, but do not scale to the whole JVM.

The first formal work on subroutine verification is due to Abadi and Stata [START_REF] Stata | A type system for Java bytecode subroutines[END_REF]: it relies on a separate analysis, performed before type verification proper, that labels bytecode instructions with the names of the subroutines they belong to, thus reconstructing the subroutine structure. The Used ( ) sets can then be computed for each subroutine , and injected in the dataflow equations as described in section 5.2.

Later work by Hagiya and Tozawa [START_REF] Hagiya | On a new method for dataflow analysis of Java virtual machine subroutines[END_REF] also relies on prior determination of the subroutine structure, but expresses the flow of types through subroutines in a different way, using special types last(n) to refer to the type of register n in the caller of the subroutine. The last(n) types behave very much like type variables in a type system featuring parametric polymorphism. In other terms, the subroutine is given a type that is polymorphic over the types of the local variables that it does not use.

While these works shed considerable light on the issue of subroutines, they are carried in the context of a small subset of the JVM that excludes exceptions and object initialization in particular. The delicate interactions between subroutines and object initialization were discussed in section 4. As for exceptions, exception handling complicates significantly the determination of the subroutine structure. Examination of bytecode produced by a Java compiler shows two possible situations: either an exception handler covers a range of instructions entirely contained in a subroutine, in which case the code of the exception handler should be considered as part of the same subroutine (e.g. it can branch back to the ret instruction that terminates the subroutine); or, an exception handler covers both instructions belonging to a subroutine and non-subroutine instructions, in which case the code of the handler should be considered as outside the subroutine. The problem is that in the second case, we have a branch (via the exception handler) from a subroutine instruction to a non-subroutine instruction, and this branch is not a ret instruction; this situation is not allowed in Abadi and Stata's subroutine labeling system.

Thus, it is desirable to develop subroutine verification strategies that do not rely on prior determination of the subroutine structure, but instead "discover" this structure during verification. The polyvariant verification algorithms that we discuss next in section 6 satisfy this requirement. O'Callahan [START_REF] Robert | A simple, comprehensive type system for Java bytecode subroutines[END_REF] proposes a different approach, based on continuation types: the type assigned to a return address contains the complete stack and register type expected at the program point following the jsr instruction. However, O'Callahan gives only type checking rules, but no effective type inference algorithm.

Polyvariant bytecode verification

In this paper so far, we have presented bytecode verification as a monovariant flow analysis: at each program point, only one abstract state (register type and stack type) is considered. Polyvariant flow analyses, also called context-sensitive analyses [37, section 3.6] lift this restriction: several states are allowed per program point. As we show in this section, polyvariant bytecode verification provides an alternate solution to the subroutine problem of section 5: polyvariant analysis allows instructions inside subroutine bodies to be analyzed several times, e.g. once per call site for the subroutine, without merging the corresponding states like the monovariant analysis of section 3.2 does.

Polyvariant verification based on contours

The first polyvariant bytecode verification analysis that we describe is based on contours, and is used in the Java Card off-card verifier [START_REF]Off-card bytecode verifier for Java Card. Distributed as part of Sun's Java Card Development Kit[END_REF]. In contour-based polyvariant flow analysis, the distinct states maintained at each program point are indexed by contours that usually approximate the control-flow path that led to each state.

In the case of bytecode verification, contours are subroutine call stacks: lists of return addresses for the sequence of jsr instructions that led to the corresponding state. In the absence of subroutines, all the bytecode for a method is analyzed in the empty contour. Thus, only one state is associated to each instruction and the analysis degenerates into the monovariant dataflow analysis of section 3.2. However, when a jsr instruction is encountered in the current contour c, it is treated as a branch to the instruction at in the augmented contour .c. Similarly, a ret r instruction is treated as a branch that restricts the current context c by popping one or several return addresses from c (as determined by the type of the register r).

In the example of Figure 5, the two jsr 100 instructions are analyzed in the empty context ε. This causes two "in" states to be associated with the instruction at 100; one has contour 3.ε, assigns type to register 0, and contains retaddr(3) at the top of the stack1 ; the other state has contour 55.ε, assigns type int to register 0, and contains retaddr(55) at the top of the stack. Then, the instructions at 101. . . 110 are analyzed twice, in the two contours 3.ε and 55.ε. In the contour 3.ε, the ret 1 at 110 is treated as a branch to 3, where register 0 still has type . In the contour 55.ε, the ret 1 is treated as a branch to 55 with register 0 still having type int. By analyzing the subroutine body in a polyvariant way, under two different contours, we avoided merging the types and int of register 0 at the subroutine entry point, and thus obtained the desired type propagation behavior for register 0: before and after the jsr 100 at 3, but int before and after the jsr 100 at 52.

More formally, the polyvariant dataflow equation for a jsr instruction at i followed by an instruction at j is in( , j.c) = (retaddr(j).S, T ) where (S, T ) = out(i, c)

For a ret r instruction at i, the equation is

in(j, c ) = out(i, c)
where the type of register r in the state out(i, c) is retaddr(j) and the context c is obtained from c by popping return addresses until j is found, that is, c = c .j.c . Finally, for instructions i other than jsr and ret, the equation is simply

i : in(i, c) → out(i, c)
that is, the instruction triggers no change of contour. Another way to view polyvariant verification is that it is exactly equivalent to performing monovariant verification on an expanded version of the bytecode where every subroutine call has been replaced by a distinct copy of the subroutine body. Instead of actually taking N copies of the subroutine body, we analyze them N times in N different contours. Of course, duplicating subroutine bodies before the monovariant verification is not practical, because it requires prior knowledge of the subroutine structure (to determine which instructions are part of which subroutine body), and as shown in section 5.3, the subroutine structure is hard to determine exactly. The beauty of the polyvariant analysis is that it determines the subroutine structure along the way, via the computations on contours performed during the dataflow analysis. Moreover, this determination takes advantage of typing information such as the retaddr(ra) types to determine with certainty the point to which a ret instruction branches in case of an early return from nested subroutines.

Another advantage of polyvariant verification is that it handles code that is reachable both from subroutine bodies and from the main program, such as the exception handlers mentioned in section 5.3: rather than deciding whether such exception handlers are part of a subroutine or not, the polyvariant analysis simply analyzes them several times, once in the empty contour and once or several times in subroutine contours.

One downside of polyvariant verification is that it is more computationally expensive than Sun's approach. In particular, if subroutines are nested to depth N , and each subroutine is called k times, the instructions from the innermost subroutine are analyzed k N times instead of only once in Sun's algorithm. However, typical Java code has low nesting of subroutines: most methods have N ≤ 1, very few have N = 2, and N > 2 is unheard of. Hence, the extra cost of polyvariant verification is entirely acceptable in practice. A more serious drawback of this approach is that contour-based polyvariant verification can fail to accept valid JVM code because the subroutine structure that it infers through the construction of contours can be infinite. Consider the Java method shown in Figure 6, along with the corresponding JVM code. The subroutine at 15 does not terminate by a ret instruction, but by a goto 0 that branches back to the non-subroutine part of the method code. (This branch corresponds to the continue statement in the source code.)

Polyvariant verification starts by analyzing instructions at 0, 3 and 6 in the empty contour ε. The jsr 15 at 3 causes instructions at 15 and 16 to be analyzed in the contour 15.ε. The goto 0 at 16 does not affect the contour (unlike a ret instruction), thus causing instructions at 0, 3 and 6 to be re-analyzed in the contour 15.ε. Iterating this process, we end up analyzing instructions 0, 3 and 6 in an infinite number of contexts: ε, 15.ε, 15.15.ε, . . . Thus, verification does not terminate.

Alternatively, termination can be ensured by requiring that contours never contain twice the same subroutine label: a jsr in a contour containing is rejected, in accordance with the JVM specification that states that subroutines cannot be recursive. (This is what the Java Card verifier [START_REF]Off-card bytecode verifier for Java Card. Distributed as part of Sun's Java Card Development Kit[END_REF] does.) But in this case we end up rejecting a valid piece of JVM bytecode, generated by compilation of a valid (albeit artificial) Java program. As demonstrated by this example, using data-independent contours to direct polyvariant verification can cause too many -or even infinitely many -different states to be kept for a given program point, even if these states are exactly identical. (In the example, the states at point 0 in contours 15.ε, 15.15.ε, etc, are all identical.) We now describe an alternate approach to polyvariant verification, not using contours, that avoids these issues.

Model checking of abstract interpretations

It is folk lore that dataflow analyses can be viewed as model checking of abstract interpretations [START_REF] Schmidt | Data flow analysis is model checking of abstract interpretations[END_REF]. Since a large part of bytecode verification is obviously an abstract interpretation (of a defensive JVM at the type level), it is natural to look at the remaining parts from a model-checking perspective.

Posegga and Vogt [START_REF] Posegga | Java bytecode verification using model checking[END_REF] were the first to do so. They outline an algorithm that takes the bytecode for a method and generates a temporal logic formula that holds if and only if the bytecode is safe. They then use an off-the-shelf model checker to determine the validity of the formula. While this application uses only a small part of the power and generality of temporal logic and of the model checker, the approach sounds interesting for establishing finer properties of the bytecode that go beyond the basic safety properties of bytecode verification (see section 8). The article by Basin et al. in this volume [START_REF] Basin | Bytecode verification by model checking[END_REF] explores the model-checking approach to bytecode verification in great details.

Brisset [START_REF] Brisset | Vers un vérifieur de bytecode Java certifié[END_REF] and independently Coglio [START_REF] Coglio | Simple verification technique for complex Java bytecode subroutines[END_REF] extract the essence of the "model checking" approach: the idea of exploring all reachable states of the abstract interpreter. They consider the transition relation obtained by combining the transition relation of the type-level abstract interpreter (Figure 2) with the "successor" relation between instructions. This relation is of the form (p, S, R) → (p , S , R ), meaning that the abstract interpreter, started at PC p with stack type S and register type R, can abstractly execute the instruction at p and arrive at PC p with stack type S and register type R . Additional transitions (p, S, R) → err are introduce to reflect states (p, S, R) in which the abstract interpreter is "stuck" (cannot make a transition because some check failed).

(p, S, R) → (p , S , R ) if instr (p) : (S, R) → (S , R ) and p is a successor of p (p, S, R) → err if instr (p) : (S, R) →
The BC (Brisset-Coglio) verification algorithm simply explores all states reachable by repeated applications of the extended transition relation starting with the initial state σ 0 = (0, ε, (P 0 , . . . , P n-1 , , . . . , )) corresponding to the method entry. In other terms, writing C(Σ) = Σ ∪ {σ | ∃σ ∈ Σ. σ → σ } for the one-step closure of a set of states Σ, the BC algorithm computes by fixpoint iteration the smallest set Σ c containing σ 0 and closed under C. If err ∈ Σ c , the error state is reachable and the bytecode is rejected. Otherwise, the bytecode passes verification. In the latter case (err is not reachable), the correctness of the abstract interpretation (as proved in [START_REF] Pusch | Proving the soundness of a Java bytecode verifier specification in Isabelle/HOL[END_REF]) guarantees that the concrete, defensive JVM interpreter will never fail a safety check during the execution of the method code, hence the bytecode is safe.

This algorithm always terminates because the number of distinct states is finite (albeit large), since there is a finite number of distinct types used in the program, and the height of the stack is bounded, and the number of registers is fixed.

The problem with subroutines described in section 5.1 completely disappears in this approach. It suffices to use the following transitions for the jsr and ret instructions:

(p, S, R) → ( , retaddr(p + 3).S, R) if instr (p) = jsr (p, S, R) → (q, S, R) if instr (p) = ret r and R(r) = retaddr(q) (p, S, R) → err if instr (p) = ret r and R(r) = retaddr(q)
The fact that the BC algorithm never merges the types inferred along two execution paths leading to the same instruction guarantees that subroutine bodies are analyzed as many times as necessary to propagate type information correctly across subroutine calls. However, we will never consider twice the same stack and register types at a given point, thus guaranteeing termination and avoiding the problem with contour-based polyvariance. For instance, the example of Figure 6 that cannot be accepted by contour-based polyvariant verification is now correctly accepted: instructions at 0, 3 and 6 are verified exactly twice, once under the assumption r 0 : , the other under the assumption r 0 : retaddr [START_REF] Bertot | Formalizing a JVML verifier for initialization in a theorem prover[END_REF].

Another interest of this approach is that it allows us to reconsider some of the design decisions explained in sections 3.2, 3.3 and 4. In particular, the BC algorithm never computes least upper

r 0 : D or r 0 : E r 0 : D r 0 : E r 1 : D r 1 : E r 2 : D r 2 : E . . .

. , E)

Figure 7: Control-flow joins in the model-checking approach bounds of types, but simply checks subtyping relations between types. Thus, it can be applied to any well-founded subtyping relation, not just relations that form a semi-lattice. Indeed, it can keep track of interface types and verify invokeinterface instructions accurately, without having to deal with sets of types or lattice completion. Similarly, it is possible to verify code where the stack size is not the same on all paths leading to an instruction.

Brisset [START_REF] Brisset | Vers un vérifieur de bytecode Java certifié[END_REF] formalized and proved the correctness of this approach in the Coq proof assistant, and extracted the ML code of a bytecode verifier from the proof. Klein and Wildmoser [START_REF] Klein | Verified bytecode subroutines[END_REF] also prove the correctness of this approach using Isabelle/HOL. Their proof builds on a generic dataflow analysis framework, and thus seems reusable for the variants of the BC algorithm discussed in section 6.3. Coglio [START_REF] Coglio | Simple verification technique for complex Java bytecode subroutines[END_REF] argues that the BC verification algorithm is the most precise of all "reasonable" verification algorithms, in the sense that it accepts all bytecode that does not crash a defensive virtual machine that would follow all execution paths across conditional jumps, regardless of the value of the condition. Thus, the only correct bytecode that could be rejected by the BC algorithm is bytecode whose correctness depends on additional knowledge on the values (and not just the types) of booleans, integers and object references manipulated by the code.

Widening in the model checking approach

The BC verification algorithm based on model checking, described in section 6.2, can be impractical: it runs in time exponential in the number of conditional or N -way branches in the method. Consider the control-flow joint depicted in Figure 7, left part. While the dataflow-based algorithms verify the instructions following the join point only once under the assumption r : C where C = lub(D, E), the BC algorithm verifies them twice, once under the assumption r : D, once under the assumption r : E. Consider now the control-flow graph shown in the right part of Figure 7. It comprises N such conditional constructs in sequence, each assigning a different type to registers r 1 . . . r N . This causes the instructions following the last conditional to be verified 2 N times under 2 N different register types.

One way to improve the efficiency of the BC algorithm is to reduce the number of states that need be explored via judicious application of widening steps: some transitions (pc, S, R) → (pc , S , R ) can be replaced by (pc, S, R) → (pc , S , R ) where R <: R and S <: S . If the error state err is still not reachable, the bytecode remains safe. A widening step such as the above reduces the total number of states to be explored if we judiciously choose R and S , e.g. if the widened state (pc , S , R ) is already reachable.

More formally, define a subtyping relation between states by σ <: err for all states σ, and (p, S, R) <: (p , S , R ) if p = p , S <: S and R <: R . A widening scheme W is a function from sets of states to sets of states, such that for all state σ ∈ Σ, there exists a state σ ∈ W (Σ) such that σ <: σ . Note that this property implies that if err ∈ Σ, then err ∈ W (Σ).

Bytecode verification by "widened model checking", then, computes by fixpoint iteration of W • C the smallest state set Σ w containing the initial state σ 0 and such that W (C(Σ w )) = Σ w . The bytecode passes verification if and only if err / ∈ Σ w . It is easy to show that all bytecode accepted by a widened model checking algorithm is also accepted by the BC model checking algorithm, and is therefore type-safe at runtime. The proof is given in appendix A.

As proposed in [START_REF] Henrio | A framework for bytecode verifiers: Application to intra-procedural continuations[END_REF], we can construct interesting examples of widening functions from an equivalence relation ≈ determining which states should be merged in a single state, and a merging function M from sets of equivalent states to states such that σ <: M (Σ) for all σ ∈ Σ. The widening function W is then defined by

W (Σ) = {M (Σ 1 ), . . . , M (Σ n )}
where Σ 1 , . . . , Σ n is a partition of Σ in equivalence classes for the ≈ relation. The W function thus defined is a widening function, since for every σ ∈ Σ, writing Σ i for the equivalence class of σ in Σ, we have σ <:

M (Σ i ) ∈ W (Σ).
The monovariant dataflow analysis of section 3.2 is a trivial instance of widened model checking where the widening function W merges all stack and register types associated with the same program point by taking their least upper bound. More precisely, the widening function is constructed as described above from the following equivalence relations and merging functions. The equivalence relation ≈ is defined by err ≈ err and (p 1 , S 1 , R 1 ) ≈ (p 2 , S 2 , R 2 ) if and only if p 1 = p 2 . The merging function is defined by

M ({err}) = err M ({(p, S 1 , R 1 ), . . . , (p, S n , R n )}) = (p, lub(S 1 , . . . , S n ), lub(R 1 , . . . , R n )) if |S 1 | = . . . = |S n | M ({(p, S 1 , R 1 ), . . . , (p, S n , R n )}) = err, otherwise
A more interesting widening function is described by Henrio and Serpette [START_REF] Henrio | A framework for bytecode verifiers: Application to intra-procedural continuations[END_REF]. Similar ideas were implemented by Frey [START_REF] Frey | On-terminal verifier for JEFF files[END_REF] and by Coglio [START_REF] Coglio | Simple verification technique for complex Java bytecode subroutines[END_REF]. They propose to merge stack and register types at a given program point if and only if these types agree on return addresses, that is, contain the same retaddr(p) types in the same registers or stack slots, but may differ on non-retaddr types.

More precisely, we say that two types agree on return addresses if they are equal, or none of them is a retaddr type. Two register types agree on return addresses if the types they assign to every register agree. Two stack types agree on return addresses if they have the same size, and the types they contain agree pointwise. Then, define the equivalence relation ≈ by err ≈ err and (p 1 , S 1 , R 1 ) ≈ (p 2 , S 2 , R 2 ) if and only if p 1 = p 2 and S 1 , S 2 agree on return addresses, and R 1 , R 2 agree on return addresses. The merging function is defined by

M ({err}) = err M ({(p, S 1 , R 1 ), . . . , (p, S n , R n )} = (p, lub(S 1 , . . . , S n ), lub(R 1 , . . . , R n ))
(By construction of ≈, M is never presented with stack types of different heights.) The CFHS (Coglio-Frey-Henrio-Serpette) verification algorithm, then, corresponds to widened model checking using the widening function induced by the ≈ relation and M merging function.

In bytecode that contains no subroutines, stack and register types never contain return address types, thus always agree on return addresses; in this case, the CFHS algorithm essentially reduces to standard, efficient monovariant dataflow analysis2 . In the presence of subroutines, however, sufficient polyvariance is ensured because return address types prevent type merging inside subroutines. In the example of Figure 5, analysis of the two jsr at 0 and 52 causes two states with pc = 100 to be explored: one has retaddr(3) at the top of the stack type, and as the type of register 0; the other has retaddr(55) at the top of the stack type, and int as the type of register 0. These two states disagree on return addresses (namely, on the top element of the stack type), thus are not merged. This causes the astore_1 at 100 to be analyzed twice, resulting in two states at 101 that are not mergeable either because one has retaddr(3) for register 1 and the other has retaddr(55) for register 1. Thus, the instructions in the subroutine body (from 100 to 110) are given two independent sets of stack and register types, as needed to verify the two subroutine calls with sufficient precision.

In appendix B, we prove that the CFHS algorithm accepts exactly the same bytecode as the BC algorithm. In other terms, it turns out that the additional merging of type information performed in the CFHS algorithm does not degrade the precision of the analysis. This is a consequence of the following "continuity" property of the type-level abstract interpreter with respect to least upper bounds.

Property 4 (Continuity.) Assume that the stack types S 1 and S 2 agree on return addresses, and the register types R 1 and R 2 agree on return addresses. Further assume that i : (S 1 , R 1 ) → (S 1 , R 1 ) and i : (S 2 , R 2 ) → (S 2 , R 2 ). Then, i : (lub(S 1 , S 2 ), lub(R 1 , R 2 )) → (lub(S 1 , S 2 ), lub(R 1 , R 2 )).

7 Bytecode verification on small computers Java virtual machines run not only in personal computers and workstations, but also in a variety of embedded computers, such as personal digital assistants, mobile phones, and smart cards. Extending the Java model of safe post-issuance code downloading to these devices requires that bytecode verification be performed on the embedded system itself. However, bytecode verification is an expensive process that can exceed the resources (processing power and working memory space) of small embedded systems. For instance, a typical Java card (Java-enabled smart card) has 1 or 2 kilo-bytes of working memory, 16 to 32 kilo-bytes of rewritable persistent memory 3 , and an 8-bit microprocessor that is approximately 1000 times slower than a personal computer.

On such small computing devices, a conventional bytecode verification algorithm (such as Sun's or any of the polyvariant verifiers described in this paper) cannot run in working memory: the amount of RAM available is too small to store the stack and register types inferred during bytecode verification. One avenue is to use persistent rewritable memory instead of RAM to hold the data structures of the verifier. It was long believed that this solution was impractical, because these data structures change rapidly during bytecode verification, resulting in excessive writing times and "wear" on the persistent memory. Recent work by Deville and Grimaud [START_REF] Deville | Building an "impossible" verifier on a Java Card[END_REF] develops speciallydesigned encodings of types and memory representations of the verification data that alleviate this issue, and suggests that this approach is indeed feasible.

Another avenue for fitting a bytecode verifier into a small computing device is to design new verification algorithms that can run in tiny amounts of working memory. We now discuss two such algorithms.

Lightweight bytecode verification using certificates

Inspired by Necula and Lee's proof-carrying code [START_REF] Necula | Proof-carrying code[END_REF], Rose and Rose [START_REF] Rose | Lightweight bytecode verification[END_REF] propose to split bytecode verification into two phases: the code producer computes the stack and register types at branch targets and transmit these so-called certificates along with the bytecode; the embedded system, then, simply checks that the code is well-typed with respect to the types given in the certificates, rather than inferring these types itself. In other terms, the embedded system no longer solves iteratively the dataflow equations characterizing correct bytecode, but simply checks (in a single, linear pass over the bytecode) that the types provided in the code certificates are indeed a solution of these equations.

The benefits of this approach are twofold. First, checking a solution is faster than inferring one, since we avoid the cost of the fixpoint iteration. This speeds up verification to some extent 4 . Second, certificates are only read, but never modified during verification. Hence, they can be stored in persistent rewritable memory without risking to "wear" this memory space by repeated rewriting of the data during verification.

A practical limitation of this approach is that certificates are relatively large: about 50% of the size of the code they annotate [START_REF] Leroy | Bytecode verification for Java smart card[END_REF]. Even if certificates are stored in persistent memory, they can still exceed the available memory space.

Later work by Rose [START_REF] Rose | Vérification de code d'octet de la machine virtuelle Java: formalisation et implantation[END_REF] addresses the issue of the certificate size by noticing that type information for certain branch targets can be omitted from the certificate, as long as this type information is correctly computed by the verification algorithm during its linear scan of the bytecode. This hybrid verification strategy thus reduces the size of the certificate, at the cost of increased working memory requirements to store the inferred type information for branch targets not described in the certificate.

Lightweight bytecode verification is used in the KVM, one of Sun's embedded variants of the JVM [START_REF]Java 2 platform micro edition technology for creating mobile devices[END_REF]. It was formalized and proved sound and complete by Klein and Nipkow [START_REF] Klein | Verified lightweight bytecode verification[END_REF][START_REF] Klein | Verified Java bytecode verification[END_REF], using the Isabelle/HOL prover. These presentations differ in their treatment of subroutines. Rose's presentation [START_REF] Rose | Lightweight bytecode verification[END_REF][START_REF] Rose | Vérification de code d'octet de la machine virtuelle Java: formalisation et implantation[END_REF] deals only with monovariant verification and does not handle subroutines. The KVM implementation follows this approach, and relies on subroutine expansion before verification, as part of the certificate generation phase. Klein and Nipkow's formalization, however, is applicable not only to monovariant verification, but to any verification algorithm that can be expressed using dataflow equations, including the polyvariant algorithms of section 6.

On-card verification with off-card code transformation

The Java Card bytecode verifier described in [START_REF] Leroy | Bytecode verification for Java smart card[END_REF] attacks the memory problem from another angle. Like the standard bytecode verifiers, it solves dataflow equations using fixpoint iteration. To reduce memory requirements, however, it has only one global register type that is shared between all control points in the method. In other terms, the solution it infers is such that a given register has the same type throughout the method. For similar reasons, it also requires that the expression stack be empty at each branch instruction and at each branch target instruction.

With these extra restrictions, bytecode verification can be done in space O(M stack + M reg ), instead of O(N branch × (M stack + M reg )) for Sun's algorithm, where N branch is the number of branch targets. In practice, the memory requirements are small enough that all data structures fit comfortably in RAM on a smart card.

One drawback of this approach is that register initialization can no longer be checked statically, and must be replaced by run-time initialization of registers to a safe value (typically, the value of null) on method entry. Another drawback is that the extra restrictions imposed by the on-card verifier cause perfectly legal bytecode (that passes Sun's verifier) to be rejected.

To address the latter issue, this verifier relies on an off-card transformation, performed on the bytecode of the applet, that transforms any legal bytecode (that passes Sun's verifier) into equivalent bytecode that passes the on-card verifier. The off-card transformations include stack normalizations around branches and register reallocation by graph coloring, and are described in [START_REF] Leroy | Bytecode verification for Java smart card[END_REF].

These transformations can increase the size of the code, as well as the number of registers used by a method. However, experience shows that these increases are minimal: on typical Java Card code, the increase in code size is less than 2%, and the increase in registers is negligible [START_REF] Leroy | Bytecode verification for Java smart card[END_REF].

This off-card code transformation phase plays a role similar to that of adding certificates in Rose and Rose's approach: both are off-card processing that adds enough information to the applet to facilitate its on-card verification. However, the off-card code transformer embeds directly its information inside the code, via code transformations, instead of storing it into separate certificates. Moreover, the size of the extra information is much smaller (2% vs. 50%).

Conclusions and perspectives

Java bytecode verification is now a well-researched technique. The considerable body of formal work reviewed in this paper led not only to a precise understanding of what bytecode verification is and what it guarantees, but also to a number of new verification algorithms (besides Sun's original implementation) that cover a large part of the precision/cost spectrum.

A largely open question is whether bytecode verification can go beyond basic type safety and initialization properties, and statically establish more advanced properties of applets, such as resource usage (bounding the amount of memory allocated) and reactiveness (bounding the running time of an applet between two interactions with the outside world). Controlling resource usage is especially important for Java Card applets: since Java Card does not guarantee the presence of a garbage collector, applets are supposed to allocate all the objects they need at installation time, then run in constant space.

Other properties of interest include access control and information flow. Currently, the Java security manager performs all access control checks dynamically, using stack inspection [START_REF] Gong | Inside Java 2 platform security: architecture, API design, and implementation[END_REF]. Various static analyses and program transformations have been proposed to perform some of these checks statically [START_REF] Jensen | Verification of control flow based security properties[END_REF][START_REF] Walker | A type system for expressive security policies[END_REF][START_REF] Pottier | A systematic approach to static access control[END_REF]. In the Java Card world, inter-applet communications via shared objects raises delicate security issues; [START_REF] Chugunov | Model checking multi-applet Java Card applications[END_REF] applies model-checking technology to this problem. As for information flow (an applet does not "leak" confidential information that it can access), this property is essentially impossible to check dynamically; several type systems have been proposed to enforce it statically [START_REF] Volpano | A sound type system for secure flow analysis[END_REF][START_REF] Volpano | A type-based approach to program security[END_REF][START_REF] Heintze | The SLam calculus: programming with secrecy and integrity[END_REF][START_REF] Abadi | A core calculus of dependency[END_REF][START_REF] Pottier | Information flow inference for ML[END_REF].

Finally, the security of the sandbox model relies not only on bytecode verification, but also on the proper implementation of the API given to the applet. The majority of known applet-based attacks exploit bugs in the API in a type-safe way, rather than breaking type safety through bugs in the verifier. Verification of the API is a promising area of application for formal methods [START_REF] Leroy | Security properties of typed applets[END_REF][START_REF] Huisman | A case study in class library verification: Java's Vector class[END_REF]. instruction at p is not a ret instruction, its successors are independent of the stack and register types "before" the instruction; thus, σ 2 → σ 2 . If the instruction at p is ret r, we have R 1 (r) = retaddr(p ). Since σ 2 → err, it must be the case that R 2 (r) is a retaddr type. Moreover, R 1 <: R 2 . This entails R 2 (r) = R 1 (r) = retaddr(p ). Hence, p is the successor of the instruction at p in state (S 2 , R 2 ). The expected result σ 2 → σ 2 follows. 2

In the following, we write Σ Σ to mean that for all σ ∈ Σ, there exists σ ∈ Σ such that σ <: σ . Choose σ in C(Σ). By definition of C, one of the following two cases holds:

• σ ∈ Σ. Since Σ Σ , there exists σ ∈ Σ such that σ <: σ . Since Σ ⊆ C(Σ ), it follows that σ is a subtype of an element of C(Σ ).

• ρ → σ for some ρ ∈ Σ. Let ρ be an element of Σ such that ρ <: ρ . By hypothesis err / ∈ C(Σ ), we have ρ = err and ρ → err. Applying lemma 1, we obtain σ such that ρ → σ and σ <: σ . Moreover, σ ∈ C(Σ ) since σ is obtained by taking one transition from an element of Σ . Since the result above holds for all σ ∈ C(Σ), the expected result follows.

2

B Relative completeness of the CFHS algorithm

In this appendix, we prove that the CFHS verification algorithm (defined in section 6.3 as an instance of widened model checking) is complete with respect to the BC model-checking algorithm: all programs accepted by the latter algorithm are also accepted by the former. Combined with theorem 1, this result shows that the CFHS algorithm accepts exactly the same programs as the BC algorithm. We recall the definitions that describe the CFHS algorithm: the equivalence relation ≈ is defined by err ≈ err and (p 1 , S 1 , R 1 ) ≈ (p 2 , S 2 , R 2 ) iff p 1 = p 2 and S 1 , S 2 agree on return addresses and R 1 , R 2 agree on return addresses. The merging function M is defined by M ({err}) = err and M ({(p, S 1 , R 1 ), . . . , (p, S n , R n )}) = (p, lub(S 1 , . . . , S n ), lub(R 1 , . . . , R n )). Finally, the widening function W is defined by W (Σ) = {M (Σ 1 ), . . . , M (Σ n )} where Σ 1 , . . . , Σ n is a partition of Σ into equivalence classes for ≈.

The following key lemma shows that the type-level abstract machine performs parallel transitions from a set of equivalent states and from the single state obtained by merging the equivalent states. In particular, if err is not reachable from the equivalent states, it is not reachable from the merged state either. We write T (Σ) for the states reachable by one transition from a state in Σ, that is, T (Σ) = {σ | ∃σ ∈ Σ. σ → σ }.

Lemma 3 Let Σ be a non-empty set of equivalent states such that err / ∈ Σ and err / ∈ T (Σ). We then have W (T (Σ)) = T (W (Σ)).

Proof: Write Σ = {(p, S 1 , R 1 ), . . . , (p, S n , R n )} where the S i agree on return addresses, and the R i also agree on return addresses. Since err / ∈ T (Σ), for every i, there exists S i and R i such that instr (p) : (S i , R i ) → (S i , R i ). According to the continuity property 4, we thus have instr (p) : (lub(S 1 . . . S n ), lub(R 1 . . . R n )) → (lub(S 1 . . . S n ), lub(R 1 . . . R n )). Moreover, by the determinacy property 2, there are no other transitions from these initial states.

Consider the successors of the instruction at p. If instr(p) is not a ret instruction, these successors p 1 , . . . , p k depend only on instr(p) and are independent of the stack and register types. If instr(p) is a ret r instruction, the successor for the instruction is determined by the retaddr type found in R(r), where R is the register type before the instruction. However, the register types "before" considered in this proof, namely R 1 , . . . , R n and lub(R 1 , . . . , R n ), all agree on return addresses. This means that they all assign the same retaddr type to register r. Thus, the successor for the ret r instruction at p is the same in all these register types, just as in the case of a non-ret instruction at p.

It follows from this discussion of successors that the set T (Σ) of states reachable by one transition from Σ is exactly the cartesian product of the set of possible successors p 1 , . . . , p k with the set of stack and register types "after" (S 1 , R 1 ), . . . , (S n , R n ), and similarly for T (W (Σ)): T (Σ) = {(p i , S j , R j ) | i ∈ {1, . . . , k}, j ∈ {1, . . . , n}} T (W (Σ)) = {(p i , lub(S 1 . . . S n ), lub(R 1 . . . R n )) | i ∈ {1, . . . , k}} Finally, notice that the stack and register types "after" S 1 , . . . , S n and R 1 , . . . , R n agree on return addresses: if instr (p) is not a jsr instruction, any retaddr type in the state after comes from a matching retaddr type in the state before; if instr (p) is a jsr instruction, the state after contains an additional retaddr(p + 3) type at the top of the stack, but this type is the same in all stack types after. Thus, W (T (Σ)) = {(p i , lub(S 1 . . . S n ), lub(R 1 . . . R n )) | i ∈ {1, . . . , k}}.

It follows that W (T (Σ)) = T (W (Σ)) as expected.

2

We now prove a number of algebraic properties of the M and W functions.

Figure 2 :

 2 Figure 2: Selected rules for the type-level abstract interpreter. M stack is the maximal stack size and M reg the maximal number of registers.

Figure 3 :

 3 Figure 3: Some type expressions used by the verifier, with their subtyping relation. C, D, E are user-defined classes, with D and E extending C. Not all types are shown.

r 0 :Figure 4 :

 04 Figure 4: Handling joins in the control flow

Figure 5 :

 5 Figure 5: An example of subroutine

Figure 6 :

 6 Figure 6: The problem with contour-based polyvariant verification (left: Java source code; right: corresponding JVM bytecode)

r n : D r n : E 2 n

 2 register types (D, . . . , D) to (E, . .

Lemma 2

 2 Let Σ and Σ be two sets of states such that Σ Σ and err / ∈ C(Σ ). Then, C(Σ) W (C(Σ )). Proof: The relation is transitive, and by hypothesis on the widening function W , we have Σ W (Σ) for all Σ. It therefore suffices to show that C(Σ) C(Σ ).

Theorem 1

 1 Let Σ c be the smallest set closed under C containing σ 0 , and Σ w be the smallest set closed under W •C containing σ 0 . Then, err / ∈ Σ w implies err / ∈ Σ c . In other terms, if the bytecode passes a widened model checking algorithm, it also passes the BC model-checking algorithm. Proof: Write Σ c = n∈N Σ n c and Σ w = n∈N Σ n w , where Σ 0 c = Σ 0 w = {σ 0 } and Σ n+1 c = C(Σ n c ) and Σ n+1 c = W (C(Σ n c )). We now show by induction on n that Σ n c Σ n w . The base case n = 0 is trivial. The inductive case follows from lemma 2, noticing that err / ∈ Σ w implies err / ∈ C(Σ n w ) for all n. It follows that Σ c Σ w . Assume, by way of contradiction, that err ∈ Σ c . Thus, there exists σ ∈ Σ w such that err <: σ. By definition of the <: relation between states, this implies σ = err and contradicts the hypothesis err / ∈ Σ w . Hence err / ∈ Σ c as claimed. 2

Lemma 4 2 Lemma 7 2 Theorem 2

 42722 Let Σ be a non-empty set of equivalent states. Then, M (Σ) is equivalent to every σ ∈ Σ.for j = 1, . . . , k. By lemma 5,M (B j ) = M (∪{A j ∩ Σ i | i ∈ {1 . . . n}, A j ∩ Σ i = ∅}) = M (A j ) It follows that W (W (Σ 1 ) ∪ . . . ∪ W (Σ n )) = {M (B 1 ), . . . , M (B k )} = {M (A 1 ), . . . , M (A k )} = W (Σ 1 ∪ . . . ∪ Σ n )This is the expected result. Let Σ be a set of states such that err / ∈ C(Σ). Then, W (C(Σ)) = W (C(W (Σ))).Proof: Let Σ 1 , . . . , Σ n be a partition of Σ into equivalence classes. By definition of C, we haveC(Σ) = Σ 1 ∪ . . . ∪ Σ n ∪ T (Σ 1 ) ∪ . . . ∪ T (Σ n ).Applying lemma 6, we obtainW (C(Σ)) = W (W (Σ 1 ) ∪ . . . ∪ W (Σ n ) ∪ W (T (Σ 1 )) ∪ . . . ∪ W (T (Σ n ))).It follows from the hypothesis err / ∈ C(Σ) that err / ∈ Σ i and err / ∈ T (Σ i ) for all i = 1, . . . , n. By lemma 3, we thus haveW (T (Σ i )) = T (W (Σ i )). It follows that W (C(Σ)) = W (W (Σ 1 ) ∪ . . . ∪ W (Σ n ) ∪ T (W (Σ 1 )) ∪ . . . ∪ T (W (Σ n ))) = W (C(W (Σ 1 ) ∪ . . . W (Σ n ))) Since Σ 1 , . . . , Σ n is a partition of Σ into equivalence classes, we have W (Σ i ) = {M (Σ i )} and W (Σ) = {M (Σ 1 ), . . . , M (Σ n )} = W (Σ 1 ) ∪ . . . ∪ W (Σ n ).The expected result follows. Let Σ c be the smallest set closed under C containing σ 0 , and Σ w be the smallest set closed under W • C containing σ 0 . Then, err / ∈ Σ c implies err / ∈ Σ w . In other terms, if the bytecode passes the BC algorithm, it also passes the CFHS algorithm.Proof: Write Σ c = n∈N Σ n c and Σ w = n∈N Σ n w , where Σ 0 c = Σ 0 w = {σ 0 } and Σ n+1 c = C(Σ n c ) and Σ n+1 c = W (C(Σ n c )). Assume that err / ∈ Σ c . This implies err / ∈ Σ n c for any n. We now show by induction on n that Σ n w = W (Σ n c ). The base case n = 0 is trivial, since W is the identity function on singleton sets. For the inductive case, assumeΣ n w = W (Σ n c ). Then, Σ n+1 w = W (C(Σ n w )) = W (C(W (Σ n c ))). Note that err / ∈ C(Σ n c ) = Σ n+1 c . Applying lemma 7, it follows that Σ n+1 w = W (C(Σ n c )) = W (Σ n+1 c ),as desired. By construction of the widening function W , for any set of states Σ we have err ∈ W (Σ) if and only if err ∈ Σ. Thus, for any n, we have err / ∈ Σ n w since Σ n w = W (Σ n c ) and err / ∈ Σ n c . It follows that err / ∈ Σ w . 2

The type retaddr(i) represents a return address to the instruction at i. It is subtype of and itself only.

One minor difference with monovariant dataflow analysis is that the latter fails if the stack height differs on several paths that reach a given program point, while the CFHS algorithm does not fail immediately in this case, but analyzes the join point and its successors in a polyvariant manner, once per different stack height. At any rate, subroutine-free bytecode that passes monovariant verification also passes the CFHS algorithm, with only one state being considered for each program point.

Rewritable persistent memory (EEPROM or Flash) is distinct from working memory (RAM) in that writes to the former take 1000-10000 times longer than writes to the latter. Moreover, rewritable persistent memory allows a limited number of writes to the same memory location.

The speedup is not as important as one might expect, since experiments show that the fixpoint is usually reached after examining every instruction at most twice[START_REF] Leroy | Bytecode verification for Java smart card[END_REF].

Acknowledgements

We thank Alessandro Coglio, Ludovic Henrio, and the anonymous referees for their helpful comments and suggestions for improvements.

A Correctness of widened model checking

In this appendix, we formally prove that all bytecode accepted by a widened model checking algorithm (section 6.3) is also accepted by the BC model checking algorithm (section 6.2, and is therefore type-safe at runtime. In the following, W stands for an arbitrary widening function.

Lemma 1 Let σ 1 , σ 2 , σ 1 be three states such that σ 1 <: σ 2 and σ 1 → σ 1 . Further assume that σ 2 = err and σ 2 → err. Then, there exists σ 2 such that σ 2 → σ 2 and σ 1 <: σ 2 .

Proof: We first show that σ 1 = err. Assume, by way of contradiction, that σ 1 → err. This means that σ 1 = (pc, S 1 , R 1 ) and the type-level abstract interpreter cannot make a transition from (S 1 , R 1 ) on instruction instr (pc). By hypotheses σ 1 <: σ 2 and σ 2 = err, we have σ 2 = (pc, S 2 , R 2 ) with S 1 <: S 2 and R 1 <: R 2 . The monotonicity property of the abstract interpreter guarantees that it cannot make a transition from (S 2 , R 2 ) on instr (pc). Thus, σ 2 → err, which is a contradiction.

Therefore, σ 1 = err, and by definition of the → and <: relations, this implies σ 1 = err and σ 2 = err. We can therefore write

and the following properties hold:

By hypothesis σ 2 → err, the abstract interpreter can make a transition on instr (p) from state (S 2 , R 2 ). Let (S 2 , R 2 ) be the result of this transition. The monotonicity and determinacy properties of the type-level abstract interpreter guarantee that S 1 <: S 2 and R 1 <: R 2 . Define σ 2 = (p , S 2 , R 2 ). We thus have σ 1 <: σ 2 .

To conclude the proof, it remains to show that σ 2 → σ 2 . Since instr (p) : (S 2 , R 2 ) → (S 2 , R 2 ), it suffices to show that p is a valid successor of the instruction at p in state (S 2 , R 2 ). By hypothesis σ 1 → σ 1 , we know that p is a valid successor of the instruction at p in state (S 1 , R 1 ). If the Proof: We first show that if two types τ 1 and τ 2 agree on return addresses, then lub(τ 1 , τ 2 ) agrees on return addresses with both τ 1 and τ 2 . Indeed, either τ 1 = τ 2 , in which case lub(τ 1 , τ 2 ) = τ 1 = τ 2 and the result is obvious; or neither τ 1 nor τ 2 are retaddr types, in which case lub(τ 1 , τ 2 ) is not a retaddr type either, thus agrees with τ 1 and with τ 2 .

The previous result extends trivially to the least upper bound of one or several stack types, or one or several register types.

Let Σ be a non-empty set of equivalent states. Either Σ = {err}, or Σ = {(p, S 1 , R 1 ), . . . , (p, S n , R n )}.

In the former case, M (Σ) = err and the expected result obviously holds. In the latter case, M (Σ) = (p, lub(S 1 , . . . , S n ), lub(R 1 , . . . , R n )). For every i, lub(S 1 , . . . , S n ) and S i agree on return addresses, and lub(R 1 , . . . , R n ) and R i agree on return addresses. Thus, M (Σ) ≈ σ for any σ ∈ Σ.

2

Lemma 5 Let Σ 1 , . . . , Σ n be non-empty sets of states such that all states in

Proof: There are two cases to consider. In the first case, the Σ i are all {err}. In this case, the expected equality trivially holds. In the second case, err does not belong to any Σ i . Write

We thus have

By hypothesis, all elements of Σ i are equivalent to all elements of Σ j . By lemma 4, M (Σ i ) is equivalent to all elements of Σ i , and M (Σ j ) is equivalent to all elements of Σ j . By transitivity, it follows that M (Σ i ) ≈ M (Σ j ). This holds for all i, j. We thus have M ({M (Σ 1 ), . . . , M (Σ n )}) = (p, lub i (lub j (S i,j )), lub i (lub j (R i,j ))).

The expected result follows from the associativity and commutativity of the lub operation. 2

for all sets of states Σ 1 , . . . , Σ n .

Proof: Let A 1 , . . . , A k be a partition of Σ 1 ∪ . . . ∪ Σ n into equivalence classes. Thus, for every i,

Consider two elements of this set, M (A j ∩ Σ i ) and M (A j ∩ Σ i ). By lemma 4, the former is equivalent to every element of A j ∩ Σ i , and the latter to every element of A j ∩ Σ i . Moreover, the A 1 , . . . , A k are disjoint equivalence classes. Hence, M (A j ∩ Σ i ) ≈ M (A j ∩ Σ i ) if and only if j = j . Therefore, the equivalence classes of W (Σ 1 ) ∪ . . . ∪ W (Σ n ) for the ≈ relation are the sets