Xavier Leroy
email: xavier.leroy@inria.fr

François Rouaix

Security properties of typed applets

This paper formalizes the folklore result that strongly-typed applets are more secure than untyped ones. We formulate and prove several security properties that all well-typed applets possess, and identify sufficient conditions for the applet execution environment to be safe, such as procedural encapsulation, type abstraction, and systematic type-based placement of run-time checks. These results are a first step towards formal techniques for developing and validating safe execution environments for applets.

Introduction

What, exactly, makes strongly-typed applets more secure than untyped ones? Most frameworks proposed so far for safe local execution of foreign code rely on strong typing, either statically checked at the client side [START_REF] Gosling | The Java language environment -a white paper[END_REF][START_REF] Yellin | Low level security in Java[END_REF], statically checked at the server side and cryptographically signed [START_REF] Rouaix | A Web navigator with applets in Caml[END_REF], or dynamically checked by the client [START_REF] Borenstein | Email with a mind of its own: the Safe-Tcl language for enabled mail[END_REF]. However, the main property guaranteed by strong typing is type soundness: "well-typed programs do not go wrong", e.g. do not apply an integer as if it were a function. While violations of type soundness constitute real security threats (casting a well-chosen string to a function or object type allows arbitrary code to be executed), there are many more security concerns, such as integrity of the running site (an applet should not delete or modify arbitrary files) and confidentiality of user's data (an applet should not divulge personal information over the network). The corresponding security violations do not generally invalidate type soundness in the conventional sense.

If we examine the various security problems identified for Java applets [START_REF] Dean | Java security: from HotJava to Netscape and beyond[END_REF], only few of them cause a violation of Java type soundness [START_REF] Hopwood | Java security bug (applets can load native methods)[END_REF]; the others correspond to malicious, but well-typed, uses of improperly protected functions from the applet's execution environment [START_REF] Billon | Security breaches in the JDK 1[END_REF]. Another typical example is the ActiveX applet doing a Trojan attack on the Quicken home-banking software described in [START_REF] Brunnstein | Hostile ActiveX control demonstrated[END_REF]: money gets transferred from the user's bank account to some offshore account, all in a perfectly type-safe way.

On these examples, it is intuitively obvious that security properties must be enforced by the applet's execution environment. It is the environment that eventually decides which computer resources the applet can access. This is the essence of the so-called "sandbox model". Strong typing comes in the picture only to guarantee that this environment is used in accordance with its publicized interface. For instance, typing prevents an applet from jumping in the middle of the code for an environment function, or scanning the whole memory space of the browser, which would allow the applet to abuse or bypass entirely the execution environment.

The purpose of this paper is to give a formal foundation to the intuition above. We formulate and prove several security properties that all well-typed applets possess. Along the way, we identify sufficient conditions for the execution environment to be safe, such as procedural encapsulation, type abstraction, and systematic type-based placement of run-time checks. These results are a first step towards formal techniques for developing and validating safe execution environments for applets.

The remainder of this paper is organized as follows. Section 2 introduces a simple language for applets and their environment, and formalizes the security policy that they must obey. Section 3 proves a security property based on the notion of lexical scoping, then extends it to take procedural abstraction into account. In section 4, we equip our language with a simple type system, which is used in section 5 to prove three type-based security properties, two relying on run-time checks and the other on a combination of run-time checks and type abstraction. After a brief parallel with object-oriented languages in section 6, related work is discussed in section 7, followed by concluding remarks in section 8.

2 The language and its security policy

The language

The language we consider in this paper is a simple lambdacalculus with base types (integers, strings, . . . ), pairs as the only data structure, and references in the style of ML. The syntax of terms, with typical element a, is as follows: References are included in the language from the beginning not only to account for imperative programming (all kinds of assignment on variables and mutable data structures such as arrays can easily be modeled with references), but also to provide easily observable criteria on which we base the security policy.

The security policy

The security policy we apply to applets is based on the notion of sensitive store locations: locations of references that an applet must not modify during its execution, or more generally references that can be modified during the applet execution, but whose successive contents must always satisfy some invariant, i.e. remain within a given set of permitted values.

The first motivation for this policy is to formalize the intuitive idea that an applet must not trash the memory of the computer executing it. In particular, the internal state of the browser, the operating system, and other applications running on the machine must not be adversely affected by the applet.

This security policy can also be stretched to account for input/output behavior, notably accesses to files and simple cases of network connections. A low-level, hardwareoriented view of I/O is to consider hardware devices such as the disk controller and network interface as special locations in the store; I/O is then controlled by restricting what can be written to these locations. For a higher-level view, each file or network connection can be viewed as a reference, which can then be controlled independently of others. Here, the file system, the name service and the routing tables become dictionary-like data structures mapping file names and network addresses to the references representing files and connections.

(By concentrating on writes to sensitive locations, we focus on integrity properties of the system running the applet. It is also possible to control reads from sensitive locations, thus establishing privacy properties. We will not do it in this paper for the sake of simplicity, but the results of section 3 also extend to controlled reads.)

The instrumented semantics

To enforce the security policy, we give a semantics to our language that monitors reference assignments, and reports run-time errors in the case of illegal writes. We use a standard big-step operational semantics in the style of [START_REF] Plotkin | A structural approach to operational semantics[END_REF][START_REF] Tofte | Type inference for polymorphic references[END_REF][START_REF] Milner | The definition of Standard ML (revised)[END_REF]. Source terms are mapped to values, which are terms with the following syntax:

::= [x 1 ← v 1 . . . , x n ← v n ] Stores: s ::= [ 1 ← v 1 . . . , n ← v n ]
The evaluation relation, defined by the inference rules in figure 1, is written ϕ, e, s a → r, meaning that in evaluation environment e, initial store s, and store control ϕ, the source term a evaluates to the result r, which is either err if an illegal write was detected or a pair v/s of a value v for the source term and a modified store s .

The only unusual ingredient in this semantics is the ϕ component, which maps store locations to sets of values: if ϕ( ) is defined, values written to the location must belong to the set ϕ( ), otherwise a run-time error err is generated (and propagated by rules 12-21); if ϕ( ) is undefined, any value can be stored at . (See rules 10 and 11.) For instance, taking ϕ( ) = ∅ prevents any assignment to .

The rules for propagating the err result and aborting execution (rules 12-21) are the same rules as for propagating run-time type errors (wrong) in [START_REF] Tofte | Type inference for polymorphic references[END_REF]; the only difference is that we have no rules to detect run-time type errors, thus making no difference between run-time type violations and non-terminating programs (no derivations exist in both cases): the standard type soundness theorems show that type violations cannot occur at run-time in well-typed source terms.

An unusual aspect of our formalism is that the store control ϕ must be given at the start of the execution. The reason is that, with big-step operational semantics, it does not suffice to perform a regular evaluation e, s a → v/s and observe the differences between s and s to detect illegal writes. For one thing, we would not observe temporary assignments, where a malicious applet writes illegal values to a sensitive location, then restores the original values before terminating. Also, we could not say anything about nonterminating terms: the applet could perform illegal writes, then enter an infinite loop to avoid detection. By providing the store control ϕ in advance, we ensure that the first write error will be detected immediately and reported as the err result. Unfortunately, this provides no way to control stores to locations created during the evaluation (rule 8 chooses these locations outside of Dom(ϕ), meaning that writes to these locations will be free): only preexisting locations can be sensitive. (This can be viewed as an inadequacy of big-step semantics, and a small-step, reduction-based semantics would fare better here. However, there are other features of big-step semantics that are crucial to our study: the clean separation between browser-supplied environment and applet-supplied source term, and the ability to interpret abstract type names by arbitrary sets of values.)

3 Reachability-based security

Simple reachability

The first security property for our calculus formalizes the idea that an applet can only write locations that are reachable in the initial environment in which it executes, or that are created during the applet's execution. For instance, if the references representing files are not reachable from the execution environment given to applets, then no applet can write to a file.

Reachability, here, is to be understood in the garbage collection sense: a location is reachable if there exists a path in the memory graph from the initial environment to the location, following one or several pointers. More formally, we define the set RL(v, s) of locations reachable from a value v in a store s by the following equations:

RL(b, s) = ∅ RL(λx.a[e], s) = RL(e, s) RL((v 1 , v 2 ), s) = RL(v 1 , s) ∪ RL(v 2 , s) RL( , s) = { } ∪ RL(s( ), s)
Normal rules:

RL(e(x), s)

The definition above is not well-founded by induction on v, since in the fourth case the value s( ) is arbitrarily large and may contain again. It should be viewed as a fixpoint equation RL = F (RL), where F is an increasing operator; RL is, then, the smallest fixpoint of that operator. If p is a set of sensitive locations, we define Prot(p) as the store control that maps locations ∈ p to ∅, thus disallowing all writes on , and is undefined on locations / ∈ p. We can now formulate the first security property:

Security property 1 Let p be a set of sensitive locations. If p ∩ RL(e, s) = ∅, then for all applets a, we have Prot(p), e, s a → err.

In other words, if none of the locations in p is reachable from the initial environment e and store s, then no applet a can trigger an error by writing to a location in p: the applet will either terminate normally or loop. The proof of this property is a simple inductive argument on the evaluation derivation, using the following proposition as the induction hypothesis: Proposition 1 If p ∩ RL(e, s) = ∅ and Prot(p), e, s a → r, then r = err. Instead, r = v/s for some v and s . Moreover, p ∩ RL(v, s ) = ∅, and for all values w such that p ∩ RL(w, s) = ∅, we have p ∩ RL(w, s ) = ∅.

It is important to remark that even if property 1 makes no hypothesis about applet a being well-typed, it is crucial that a be well-typed in some type system, in order to guarantee that its evaluation on an actual processor adheres to the rules given in figure 1. In particular, the actual evaluation of a must never use the bit pattern representing an integer as if it were a store location; otherwise, the applet could write to arbitrary locations. We rely on a being welltyped in any sound type system (such as the one presented below in section 4) to ensure that this cannot happen.

Property 1, though simple and already well-known in the field of garbage collection [START_REF] Morrisett | Abstract models of memory management[END_REF], establishes a number of properties without which no security is possible at all. First, our language has safe pointers: locations cannot be forged by casting well-chosen integers. Second, automatic memory management (garbage collection) is feasible and does not weaken security: a location that becomes unreachable remains unreachable; moreover, newly allocated locations are always initialized; therefore, unreachable locations can be reused safely. Third, the language enforces lexical scoping: the execution of the applet depends only on the environment in which it proceeds; the applet does not have access to the full execution environment of the browser -as would be the case in a dynamically-scoped language, such as Emacs Lisp, or a language with special constructs to access the environment of the caller, such as Tcl.

Reachability and procedural abstraction

In defining reachable locations, we have treated closures like tuples (as garbage collectors do): the locations reachable from λx.a[e] are those reachable from e(y) for some y. There is, however, a big difference between closures and tuples. Tuples are passive data structures: any piece of code that has access to the tuple can then obtain pointers to the components of the tuple. Closures are active data structures: only the code part of the closure can access directly the data part of the closure (the values of the free variables); other code pieces can only apply the closure, but not get at the data part directly. In other words, the code part of a closure mediates access to the data part. This property is often referred to as procedural abstraction [START_REF] Reynolds | User-defined types and procedural data structures as complementary approaches to data abstraction[END_REF].

For instance, consider the following function, similar to many Unix system calls, where uid is a reference holding the identity of the caller (applet or browser): λx. if !uid = browser then do something with high privileges else do something with low privileges Assume this function is part of the applet environment, but not the reference uid itself. Then, there is no way that the applet can modify the location of uid, even though that location is reachable from the environment. A less obvious example, where the reference uid is not trivially read-only, is the following function in the style of the Unix setuid system call: λnewid. if !uid = browser then uid := newid else raise an error Assuming uid is not initially browser, an applet cannot change uid by calling this function.

Procedural abstraction can be viewed as the foundation for access control lists and similar programming techniques where resources are systematically encapsulated inside functions that check the identity and credentials of the caller before granting access to the requested resources. For instance, a file opening function contains the whole data structure representing the file system in its closure, but grants access only to files with suitable permissions. Thus, while all files are reachable from the closure of the open function, only those that have suitable permissions can be modified by the caller.

To formalize these ideas, we set out to define the set of locations ML(v, s) that are actually modifiable (not merely reachable) from a value v and a store s, and show that if a location is not in ML(e, s), then any applet evaluated in the environment e does not write to . This result is stronger than property 1 because the location that is not modifiable from e in s can still be reachable (via closures) from e in s.

For passive data structures (locations, tuples), modifiability coincides with reachability: a location is modifiable from v/s if a sequence of fst, snd, and ! operations applied to v in s evaluates to that location. The difficult case is defining modifiable locations for a function closure. The idea is to consider all possible applications of the closure to an argument: a location is considered modifiable from the closure only if one of those applications writes to the location, or causes the location to become modifiable otherwise.

More precisely, let e api be the execution environment given to applets, and let c = λx.a[e] be one of the closures contained in e api . A location is modifiable from c in store s if there exists a value v such that the following conditions hold:

Condition 1. The application of the closure to v causes to be modified, i.e. { → ∅}, e{x ← v}, s a → err.

Example: Let e be the environment [r ← ]. Then, is reachable from (λx. r := x + 1)[e] in any store, since any application of the closure causes to be assigned. Condition 2. Alternatively, the application of c to v does not modify , but returns a result value and a new store from which is modifiable.

Example: With e as in the previous example, is reachable from (λx. (r, 1))[e], since any application of that closure returns a pair with as first component. An applet can thus write to by applying the closure, extracting from the returned result, and assigning directly. Condition 3. Alternatively, the application of c to v modifies a reference accessible to the applet in such a way that becomes modifiable from that reference.

Example:

Consider c = (λp. p := r)[e]
, where e = [r ← ] as usual. Applying c to a location , we obtain a modified store s such that s ( ) = , i.e. is modifiable from in s and can be modified by the applet.

Condition 4. Alternatively, the application of c to v assigns references internal to the browser functions in such a way that becomes modifiable from the environment eapi in the store s at the end of the application.

Example: Consider the following environment eapi:

e api (f ) = (λx. n := !n + 1)[n ← n ] e api (g) = (λx. if !n ≥ 1 then r := 0)[n ← n ; r ← ]
In a store s such that s( n ) = 0, the location is not modifiable from e api (g). However, is modifiable from e api (f ) in s, since one application of that closure returns a store s such that s ( n ) = 1, and in that store s , is modifiable from e api (g): any application of e api (g) with initial store s writes to .

Condition 5. In conditions 1-4 above, it must be the case that the location found to be modifiable from the closure c is not actually modifiable from the argument v passed to the closure. Otherwise, we would not know whether the location really "comes from" the closure c, or is merely modified by the applet-provided argument v.

Example:

Consider the higher-order function c = (λf. f (0))[∅]. If we apply c to (λn. r := n)[r ← ],
we observe a write to location . However, should not be considered as modifiable from c, since it is also modifiable from the argument given to c.

As should now be apparent from the conditions 1-5 above, the notion of modifiability raises serious problems, both practical and technical. On the practical side, the set of modifiable locations ML(v, s) is not computable from v and s (unlike RL(v, s)): in the closure case, we must consider infinitely many possible arguments. Thus, we need general proof to determine ML(v, s).

Moreover, modifiable locations cannot be determined locally. As condition 4 shows, the modifiable locations of a closure depend on the modifiable locations of all functions from the applet environment e api . Thus, if we manage to determine ML(e api , s), then add one single function to the applet environment, we must not only determine the modifiable locations from the new function, but also reconsider all other functions in the environment to see whether their modifiable locations have changed. This is clearly impractical. Hence, the notion of modifiability is not effective and is interesting only from a semantic viewpoint and as a guide to derive decidable security criteria in the sequel.

On the technical side, the conditions 1-5 above do not lead to a well-founded definition of the sets of modifiable locations ML(v, s). The problem is condition 5 (the requirement that the location must not be modifiable from the argument given to the closure): viewing conditions 1-4 as a fixpoint equation for some operator, that operator is not increasing because of the negation in condition 5.

In appendix B, we tackle this problem and show that non-modifiable locations are indeed never modified in the particular case where the applet's environment e api is welltyped and its type E api does not contain any ref types, so that no references are exchanged directly between the applet and its environment. In the remainder of this paper, we abandon the notion of modifiability in its full generality, and develop more effective techniques to restrict writes to reachable locations, relying on type-based instrumentation of the browser code.

The type system

We now equip our language with a simple type system. The type system is based on simply-typed λ-calculus, with the addition of named, user-defined types. Despite its simplicity, this type system does not restrict drastically the expressiveness of our language. In particular, recursive functions can still be defined using references [START_REF] Tofte | Type inference for polymorphic references[END_REF]. The type algebra is:

Named types

The overall approach followed in section 5 is to identify groups of references having the same type, and apply them a given security policy. However, types from the simply-typed λ-calculus are too coarse for this purpose: references of type string ref can hold many different kinds of data, such as messages, filenames, and cryptographic keys; clearly, different security restrictions must be applied to these different kinds of strings.

To this end, we introduce named types t, defined by a mapping TD for type names to type expressions, stating that the type t is interconvertible with its implementation type TD(t). For instance, we could introduce a type filename, defined to be equal to string. An expression e of type string cannot be used implicitly with type filename; an explicit injection into filename, written filename(e), is required. Conversely, accessing the string underlying an expression e of type filename is achieved by string(e ). (See rules 35 and 36.) In this respect, our named types behave very much like the is new type definition in Ada, and unlike type abbreviations in ML. Making the coercions explicit facilitates the definition of the program transformations in section 5, ensuring in particular that each term has a unique type.

The mapping TD of type definitions is essentially global: type definitions local to an expression are not supported. Still, it is possible to type-check some terms against a set of type definitions TD that is a strict subset of TD, thus rendering the named types not defined in TD abstract in that term. We will use this facility in section 5.2 and 5.3 to make named types abstract in the applet.

Run-time validation of values

The other unusual feature of our type system is the family of operators OK t (one for each named type t) used to perform run-time validation of their argument. For each named type t, we assume given a set P V (t) of permitted values for type t. (We actually allow P V (t) to be undefined for some types t, which we take to mean that all values of type t are valid.) The expression OK t (e) checks whether the value of e is in P V (t); if yes, it returns the value unchanged; if no, it aborts the execution of the applet and reports an error. In the evaluation rules, the "yes" case corresponds to rule 23; there is no rule for the "no" case, meaning that no evaluation derivation exists if an OK t test fails. In effect, we do not distinguish between failure of OK t and non-termination. At any rate, we must not return the err result when OK t fails: no write violation occurred.

By varying P V (t), we can control precisely the values of type t that will pass run-time validation. For instance, P V (filename) could consist of all strings referencing files under the applet's temporary directory /tmp/applet.x, a new directory that is created empty at the beginning of the applet's execution. Combined with the techniques described in section 5, this would ensure that only files in this temporary directory can be accessed by the applet. Similarly, the set P V (widget) could consist of all widget descriptors referring to widgets that are children of the applet's top widget, thus preventing the applet from interacting with widgets belonging to the browser. Other examples of run-time validation include checking cryptographic signatures on data structures that the applet must carry around without tampering with.

In practice, validation OKt(e) involves not only the value of its argument e, but also external information such as the identity of the principal, and possibly user replies to dialog boxes. A typical example is the Java SecurityManager class, which determines the identity of the principal by inspection of the call stack. For simplicity, we still write OKt as a function of the value of its argument.

The evaluation rule for OKt assumes of course that mem-

Figure 2: Extra evaluation rules for coercions and run-time checks

E x : E(x) (25) E b : Typeof (b) (26) E{x ← τ } a : τ E λx.a : τ → τ (27) E a 1 : τ → τ E a 2 : τ E a 1 (a 2 ) : τ (28) E a1 : τ1 E a2 : τ2 E (a1, a2) : τ1 × τ2 (29) E a : τ1 × τ2 E fst(a) : τ1 (30) E a : τ1 × τ2 E snd(a) : τ2 (31) E a : τ E ref(a) : τ ref (32) E a : τ ref E !a : τ (33) E a 1 : τ ref E a 2 : τ E (a 1 := a 2 ) : unit (34) E a : τ τ = TD(t) E t(

Type soundness

To relate the typing rules to the dynamic semantics, we define a semantic typing relation S |= v : τ saying whether the value v is semantically a correct value for type τ . The S component is a store typing, associating types to store locations. We simultaneously extend the |= relation to stores and store typings (|= s : S), and to evaluation environments and typing environments (S |= e : E). The definition of |= is shown below, and is completely standard [START_REF] Tofte | Type inference for polymorphic references[END_REF][START_REF] Leroy | Polymorphic typing of an algorithmic language[END_REF]. Using the semantic typing relations defined above, we then have the familiar strong soundness property below for the type system. We say that a store typing S extends S if Dom(S ) ⊇ Dom(S), and for all ∈ Dom(S), we have S ( ) = S( ). Remark that semantic typing is stable under store extension: if S |= v : τ and S extends S, we also have The type-based security properties developed in this section are based on a common idea: assuming all sensitive references have types of the form t ref, we instrument the functions composing the execution environment by inserting OK t run-time checks at certain program points, in order to prevent illegal writes to references of type t ref.

• S |= b : ι if Typeof (b) = ι • S |= v : t if S |= v : TD(t) • S |=
S |= v : τ .
The applets themselves are not instrumented, of course, since their source code is generally unavailable. All we know about the applet is that it is well typed in a given typing environment and set of type definitions. It is the combination of this well-typing with the instrumented environment functions that guarantees security.

Instrumentation of writes and procedural abstraction

The first transformation we consider inserts an OK t check before any write to a reference of type t ref with t ∈ Dom(P V ). This way, we are certain that if a sensitive reference has type t ref, the environment functions will always store in it values that belong to P V (t). Formally, we define the instrumentation scheme IW , operating on terms a τ annotated with their type τ , as follows:

IW ((a t ref := b t ) unit ) = IW (a t ref ) := OKt(IW (b t )) if t ∈ Dom(P V )
On other kinds of terms, IW is a simple morphism, e.g. IW ((λx.a τ ) σ→τ ) = λx.IW (a τ ), etc. It is easy to show that write errors cannot happen inside instrumented terms. Given the permitted values P V and a store typing S, we define P rot(P V, S) as the store control that restricts references of type t ref, t ∈ Dom(P V ) to values in P V (t), and allows arbitrary writes to other references: P rot(P V, S)( ) = P V (t) if S( ) = t and t ∈ Dom(P V ), and P rot(P V, S)( ) is undefined otherwise. Proof: If τ = t for some named type t ∈ Dom(P V ), then by definition of the instrumentation scheme, the right-hand side of the assignment is of the form OK t (b ) for some b , which can only evaluate to an element of P V (t) by rule 23. Hence, the assignment is valid with respect to P rot(P V, S). If τ is not a t type or is outside Dom(P V ), by proposition 2, IW (a) evaluates to a location which does not have a type of the form t ref, t ∈ Dom(P V ), and therefore such that P rot(P V, S)( ) is undefined; hence, no write error occurs either.

2

Proposition 3 only provides half of the security property: it shows that writes in instrumented code are safe, but only the execution environment contains instrumented code; the applet code is not instrumented and could therefore perform illegal writes to sensitive locations, if it could access those locations. In other terms, we must make sure that all sensitive locations are encapsulated inside functions, as in section 3.2. To this end, we will restrict the type E api of the applet's execution environment e api to ensure that sensitive references cannot "leak" into the applet, and be assigned illegal values there. There are several ways by which a sensitive reference of type t ref could leak into an applet:

• The reference is exported directly in the environment, e.g.

E api (x) = t ref or E api (x) = int × (t ref).
• The reference is returned by one of the functions of the environment, e.g. Eapi(f ) = int → t ref.

• The environment contains a higher-order function such as Eapi(h) = (t ref → int) → int. The applet could get access to a sensitive reference if h passes one to its functional argument, which can be provided by the applet.

• However, our proof of property 2, and in particular the crucial containment lemma 7, does not extend to this weaker hypothesis.

Instrumentation of coercions and type abstraction

Instead of putting run-time checks on writes to references of type t ref, we can ensure that all values of type t ∈ Dom(P V ) that flow through the applet's execution environment always belong to P V (t). This way, values stored in a t ref will automatically satisfy P V (t) as well. This is achieved by adding checks to all creations of values of type t ∈ Dom(P V ) in the execution environment, i.e. to coercions of the form t(a), following the instrumentation scheme IC below:

IC(t(a)) = OK t (t(IC(a))) if t ∈ Dom(P V )
Of course, this is not enough: the applet could forge unchecked values of type t, by direct coercion from t's implementation type, and pass them to environment functions. Hence, we also need to make the types t ∈ Dom(P V ) abstract in the applet, by type-checking it with a set of type definitions TD obtained from TD by removing the definitions of the types t ∈ Dom(P V ). Then, for any t ∈ Dom(P V ), the only values of type t that can be manipulated by the applet have been created and checked by the environment.

To capture the run-time behavior of instrumented terms, we introduce a variant of the semantic typing predicate, written P V, S |= v : τ , which is similar to the predicate S |= v : τ introduced in section 4.3, with the difference that a value v belongs to a named type t only if v ∈ P V (t) in addition to v belonging to the definition TD(t) of t: Compared with proposition 2, we now use the more restrictive interpretation of named types P V , and require that all terms occurring in the evaluation derivation have been instrumented with IC. The proof is essentially identical to that of proposition 2.

• P V, S |= b : ι if Typeof (b) = ι • P V, S |= v : t if P V, S |= v : TD(t)
Notice that an applet a well-typed within the restricted set TD of type definitions contains no coercions t(a) for any t ∈ Dom(P V ), hence is equal to IC(a). Thus, proposition 4 applies not only to the terms from the execution environment, but also to the applet itself. In a sense, this proposition can be viewed as a parametricity result, in that it shows soundness for arbitrary interpretations P V of the types left abstract in TD . From this remark, we immediately obtain the following security property: Security property 3 Let e be the execution environment for applets, and s the initial store. Assume that all function closures in e and s have been instrumented with the IC scheme (that is, e and s are obtained by evaluating source terms instrumented with IC). Assume P V |= s : S and P V, S |= e : E. Then, for every applet a well-typed in E and in the restricted set TD of type definitions, we have P rot(P V, S), s, e a → err.

One practice that property 3 formally justifies is systems based on capabilities: by making the type of capabilities abstract to the applets, run-time security checks are necessary only at points where new capabilities are constructed and returned to the applet; capabilities presented by the applet can then be trusted without further checks.

Unlike property 2, property 3 does not require that types t ref do not occur in the typing environment E. Indeed, once t is made abstract, it is perfectly safe to make references of type t ref accessible to the applet: the applet can then write to them, but only write safe values of type t. Hence, sensitive references no longer need to be systematically wrapped inside functions. As Reynolds points out [START_REF] Reynolds | User-defined types and procedural data structures as complementary approaches to data abstraction[END_REF], type abstraction and procedural abstraction are two orthogonal ways to protect data.

Another advantage of the approach described in this section over the instrumentation of writes described in section 5.1 is that it often leads to fewer run-time checks. In particular, checks at coercions can sometimes be proven redundant and therefore can be eliminated. Consider the following function that adds a .old suffix to a file name: λf.OK filename (filename(concat(string(f),".old")))

With the definition of P V (filename) given in section 4.2, it is easy to show that if f belongs to P V (filename), then so does the concatenation of f and .old. Hence, the OK test can be removed.

Of course, not all run-time tests can be removed this way: consider what happens if the suffix was given as argument: λf.λs.OKfilename(filename(concat(string(f),s)))

and the applet passes a suffix s starting with "../".

Instrumenting coercions without type abstraction

In some cases, the types t ∈ Dom(P V ) cannot be made abstract in the applet, e.g. because it would make writing the applet too inconvenient, or entail too much run-time overhead. We can adapt the approach presented in section 5.2 to these cases, by reverting to procedural abstraction and putting checks not only at coercions, but also on all values of types t ∈ Dom(P V ) that come from the applet. (This matches current practice in Unix kernels, where parameters to system calls are always checked for validity on entrance to the system call.) This is achieved by a standard wrapping scheme applied to all functions of the execution environment, inserting OK t coercions at all negative occurrences of types t ∈ Dom(P V ). For instance, if the execution environment needs to export a function f : t → t, it will actually export the function λx.f (OK t (x)), which validates its argument before passing it to the original function.

We formalize these ideas in a slightly different way, in order to build upon the results of section 5.2. Start from an applet environment defined by top-level bindings of the form let f i :

τ i = a i
We assume given a set TD of type definitions against which the ai and the applets are type-checked, and a valuation P V assigning permitted values to named types in TD . We first associate a new named type t to each sensitive type t ∈ Dom(P V ). The type t is defined as synonymous with t, and is intended to represent those values of type t that have passed run-time validation. We define the t types by taking

TD = TD ⊕ [ t → t | t ∈ Dom(P V )]
and restrict the values they can take using the valuation P V defined by P V ( t ) = P V (t) and P V undefined on other types.

Let Σ be the substitution {t ← t | t ∈ Dom(P V )}. We transform the bindings for the applet environment as follows:

let fi : τi = W + (IC(Σ(ai)) : τi)
That is, we rewrite the terms a i to use the type t instead of t for all t ∈ Dom(P V ); then apply the IC instrumentation scheme to it, thus adding an OK t check to each coercion t(a); finally, apply the W + wrapping scheme to the instrumented term, in order to perform both validation and coercion from t to t on entrance, and the reverse coercion from t to t on exit. Wrapping is directed by the expected type for its result, and is contravariant with respect to function types. We thus define both a wrapping scheme W + for positive occurrences of types and another W -for negative occurrences.

W + (a : ι) = W -(a : ι) = a W + (a : t) = t(a) if t ∈ Dom(P V ) W -(a : t) = OK t( t(a)) if t ∈ Dom(P V ) W + (a : t) = W -(a : t) = a if t / ∈ Dom(P V ) W + (a : τ1 × τ2) = (W + (fst(a) : τ1), W + (snd(a) : τ2) W -(a : τ1 × τ2) = (W -(fst(a) : τ1), W -(snd(a) : τ2) W + (a : τ 1 → τ 2 ) = λx.W + (a(W -(x : τ 1 )) : τ 2 ) W -(a : τ 1 → τ 2 ) = λx.W -(a(W + (x : τ 1 )) : τ 2 ) W + (a : τ ref) = W -(a : τ ref) = a if no t ∈ Dom(P V ) occurs in τ
Wrapping is not defined on reference types containing a t ∈ Dom(P V ) because there is no way to validate these references so that they are protected against future modifications.

It is easy to see that the transformed bindings are welltyped: Σ(ai) has type Σ(τi); the IC instrumentation preserves typing; the W + wrapping applied to a term of type Σ(τi) returns a term of type τi, as shown by a simple induction over τi.

Moreover, the right-hand sides of the bindings always perform an OK t check before each coercion to a type t: this is ensured by the IC instrumentation for the coercions initially in Σ(ai), and by definition of the wrapping scheme for the coercions introduced by the wrapping.

Finally, the applets themselves are still type-checked in the original set TD of type definitions, in which the types t are not defined, and thus abstract for the applet.

We are therefore back to the situation studied in section 5.2: the types t are abstract in the applets and all coercions to t are instrumented in the applet environment. Thus, by property 3, we obtain that the values of references with types t ref always remain within P V ( t ) = P V (t) during the execution of any well-typed applet.

Security property 4 Let e be the execution environment for applets and s the initial store. Assume that e and s are obtained by evaluating a set of transformed bindings let f i : τi = W + (IC(Σ(ai)) : τi) as described above. Assume P V |= s : S and P V, S |= e : E. Then, for every applet a well-typed in E and in the initial set TD of type definitions, we have P rot(P V, S), s, e a → err.

Connections with object-oriented languages

Although the language used for this work is functional, the techniques developed here translate reasonably well to object-oriented languages.

Procedural abstraction as presented in section 3.2 corresponds most closely to Smalltalk-style private instance variables: just as variables in a closure environment can only be accessed by the code associated with that closure, private instance variables of a Smalltalk object can only be accessed by the methods of that object. Java does not offer a strictly equivalent mechanism: the private modifier makes instance variables accessible not only to the methods of the object, but also to methods of other objects of the same class. Still, the visibility rules associated with the package mechanism and the private and protected modifiers also ensure some degree of procedural abstraction, since they restrict the set of methods that can access a given instance variable.

Similarly, type abstraction as exploited in section 5.3 corresponds most closely to final classes in Java. A final class containing only private fields and having a private constructor offers the same level of guarantees as our abstract types: the applet cannot create directly an object of that class, nor tamper with the fields of an existing object. In non-final classes, the visibility rules might still ensure some degree of type abstraction, though it is unclear how much is guaranteed. Subtype polymorphism in systems such as F <: [START_REF] Cardelli | An extension of system F with subtyping[END_REF] also provide some amount of type abstraction, but this is not so in Java because the actual type of an object can be tested at run-time (downcasts).

7 Related work

Type systems for security

The work most closely related to ours is the recent formulations of Denning's information flow approach to security [START_REF] Denning | A lattice model of secure information flow[END_REF][START_REF] Denning | Certification of programs for secure information flow[END_REF] as non-standard type systems by Palsberg and Ørbaek [START_REF] Palsberg | Trust in the λ-calculus[END_REF], Volpano and Smith [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], and Heintze and Riecke [START_REF] Heinze | The SLam calculus: programming with secrecy and integrity[END_REF]. The main points of comparison with our work are listed below.

Information flow vs. integrity:

The type systems developed in previous works all focus on flow of information between high-security and low-security parts of a program. In particular, they allow high-security data to be exposed as long as no low-security code uses this data. In the context of applets, we have no control over the low-security code and are therefore forced to ensure that high-security data is never exposed directly. Thus, our work does not concentrate on information flow proper, but mainly on protecting sensitive data via procedural or type abstraction.

Imperative vs. purely functional programs: [START_REF] Palsberg | Trust in the λ-calculus[END_REF] and [START_REF] Heinze | The SLam calculus: programming with secrecy and integrity[END_REF] consider purely functional languages in the style of the λ-calculus. This makes formulating the security properties delicate: [START_REF] Palsberg | Trust in the λ-calculus[END_REF] proves no security property properly speaking, only a subject reduction property that shows the internal consistency of the calculus, but not its relevance to security; [START_REF] Heinze | The SLam calculus: programming with secrecy and integrity[END_REF] does show a non-interference property (that the value of a low-security expression is independent of the values of high-security parameters), but it is not obvious how this result applies to actual applet/browser interactions, especially input/output. Instead, we have followed [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] and formulated our security policy in terms of in-place modifications on a store, which provides a fairly intuitive idea of what constitutes a security violation.

Run-time validation of data: Only [START_REF] Palsberg | Trust in the λ-calculus[END_REF] and our work consider the possibility of checking low-security data at run-time and promoting them to high security. In [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] Heinze | The SLam calculus: programming with secrecy and integrity[END_REF], once some data is labeled "low security", it remains so throughout the program and causes all data it comes in contact with to be marked "low security" as well. We believe that, in a typical applet/browser interaction, this policy leads to rejecting almost all applets as insecure. Run-time validation of untrusted data is essential in practice to allow a reasonable range of applets to run.

Subtyping vs. named types and coercions: All previous works consider type systems with subtyping, which provides a good match for the flow analysis approach they follow [START_REF] Palsberg | A type system equivalent to flow analysis[END_REF]. In contrast, we only use type synonyms with possibly checked coercions between a named type and its implementation type. However, the connections between subtyping and explicit coercions are well known [START_REF] Breazu-Tannen | Inheritance as implicit coercion[END_REF], and we do not think this makes a major difference.

Security of applets

Concerning the security issues raised by applets in general, we are aware of case studies of security flaws [START_REF] Dean | Java security: from HotJava to Netscape and beyond[END_REF], as well as informal descriptions of current and proposed security architectures for applets [START_REF] Erdos | Security reference model for the Java Developer's Kit 1.0.2. Java-Soft[END_REF][START_REF] Yellin | Low level security in Java[END_REF][START_REF] Rouaix | A Web navigator with applets in Caml[END_REF][START_REF] Wallach | Extensible security architectures for Java[END_REF]. Our work seems to be one of the first formal studies of applet security.

On the Java side, considerable effort has been expended in proving the soundness of the Java type system [START_REF] Drossopoulou | Java is type safeprobably[END_REF][START_REF] Nipkow | JavaLight is type-safe -definitely[END_REF] and of the JVM bytecode verifier [START_REF] Qian | A formal specification of a large subset of Java Virtual Machine instructions[END_REF]. Other aspects of Java that are equally important for security, such as formalizing the visibility rules and the encapsulation guarantees they provide, have only recently started to receive attention [START_REF] Jensen | A formalisation of visibility and dynamic loading in Java[END_REF]. We are not aware of any formal description of security policies for Java applets.

Proof-carrying code [START_REF] Necula | Safe kernel extensions without run-time checking[END_REF][START_REF] Necula | Proof-carrying code[END_REF] provides an elegant framework to establish the safety of mobile code, but requires general proof from the applet's developer. Our approach lies at the other end of the complexity spectrum: all we require from the applet is that it is well typed in a simple, standard type system.

Concluding remarks

We have identified three basic techniques for enforcing a fairly realistic security policy for applets: lexical scoping, procedural abstraction, and type abstraction. These programming techniques are of course well known, but we believe that this work is the first to characterize precisely their implications for program security.

The techniques proposed here seem to match relatively well current practice in the area of Web applets. In particular, they account fairly well for Rouaix's implementation of safe libraries in the MMM browser [START_REF] Rouaix | A Web navigator with applets in Caml[END_REF]. Some aspects of MMM are still unaccounted for, such as the necessity of taking copies of mutable objects before validating them. Also, MMM applets have the ability to install functions in various stages of the browser (HTML display machine, document decoding), and this requires validation of these functions at times other than those suggested by our framework.

Our techniques put almost no constraints on the applets, except being well-typed in a simple, completely standard type system. The security effort is concentrated on the execution environment provided by the browser. Typing the applets in a richer type system, such as the type systems for information flow of [START_REF] Palsberg | Trust in the λ-calculus[END_REF][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] Heinze | The SLam calculus: programming with secrecy and integrity[END_REF] or the effect and region system of [START_REF] Talpin | The type and effect discipline[END_REF], could provide more information on the behavior of the applet and enable more flexible security policies in the execution environment. However, it is probably impractical to rely on rich type systems for applets, because these type systems are not likely to be widely accepted by applet developers. Whether these rich type systems can be applied to the execution environment only is an interesting open question.

On the technical side, the proofs of the type-based security properties are variants of usual type soundness proofs. It would be interesting to investigate the security content of other classical semantic results such as representation independence and logical relations. Given the importance of communications between the applet and its environment, it could be worthwhile to reformulate our security results for a calculus of communicating processes [START_REF] Banâtre | A security proof system for networks of communicating processes[END_REF][START_REF] Abadi | Reasoning about cryptographic protocols in the Spi calculus[END_REF].

A Appendix: the containment lemma

In this appendix, we formalize the intuition that if the type of the applet environment does not contain certain ref types, then references of those types cannot be exchanged between the applet and the environment, and remain "contained" in one of them.

We annotate each source-language term a as coming either from the execution environment (aenv) or from the applet (aapp). We let m, n range over the two "worlds" env and app, and write m for the complement of m, i.e. env = app and app = env .

Let T be a set of type expressions satisfying the following closure property: if τ ∈ T , then all types τ that contain τ as a sub-term also belong to T . (In section 5.1, we take T to be the set of all types containing an occurrence of t ref; in appendix B, T is the set of all types containing an occurrence of any ref type). We partition the set of locations into three countable sets:

• Lapp is the set of locations with type τ ref ∈ T that have been allocated by the applet;

• Lenv is the set of locations with type τ ref ∈ T that have been allocated by the environment (i.e. either initially present in the applet environment, or allocated by environment functions);

• L shared is the set of locations whose type τ ref does not belong to T .

To ensure that locations allocated during evaluation are drawn from the correct set, we assume all source terms a τ m annotated with their static type τ and their world m and replace the evaluation rule for reference creation (rule 8) by the following rule:

ϕ, e, s a τ m → v/s / ∈ Dom(s ) ∪ Dom(ϕ) ∈ L env if τ ref ∈ T and m = env ∈ L app if τ ref ∈ T and m = app ∈ L shared if τ ref / ∈ T ϕ, e, s ref(a) τ ref m → /s { ← v} (8')
It is easy to see that the modified rule produces the same evaluation derivations as the initial rule, up to a renaming of fresh locations: if ϕ, e, s a → r with the initial rule, then ϕ, e, s a → r with the modified rule, where r is identical to r up to a renaming of locations not in Dom(s) ∪ Dom(ϕ). We say that a value v in a store s is contained in world m, and we write Cm(v, s), if any source term operating on v in s can directly access only locations that are in Lm or L shared , but not locations in L m . Formally, Cm(v, s) is defined by case analysis on v, as follows:

• Cm(b, s) is always true

• C m (λx.a n [e], s) if C n (e, s) • C m ((v 1 , v 2 ), s) if C m (v 1 , s) and C m (v 2 , s) • C m ( , s) if l /
∈ L m and C m (s( ), s)

• Cm(e, s) if Cm(e(x), s) for all x ∈ Dom(e).

Notice that for closures, it's the world n of the function body an that determines the containment of the closure environment, not the world m in which the closure value is being used. The reason is that the environment values can only be accessed by the function body, not arbitrary terms of world m. This is characteristic of procedural abstraction in the sense of section 3.2.

As usual, the definition of C above is not well-founded by induction on v. We view the equations above as fixpoint equations for an operator, which is increasing, and define C as the greatest fixpoint of that operator. (The smallest fixpoint is always false on value/store pairs that contain a cycle, which is not what we want; it's the greatest fixpoint that gives the expected behavior for C. See [START_REF] Tofte | Type inference for polymorphic references[END_REF] for detailed explanations.)

Here are two important lemmas on the C predicate. First, assigning a value contained in world m to a location which is not in L m preserves the containment of all other values.

C n (w, s) implies C n (w, s 2 ) for all n, w S 2 |= v 1 : σ → τ S 2 |= v 2 : σ |= s 2 : S 2 .
Hence, v1 is a closure λx.a n [e ], and the last evaluation rule used is rule 4.

If n = m (intra-world call), we have C m (e {x ← v 2 }, s 2 ) as a consequence of C m (v 1 , s 2 ) and C m (v 2 , s 2 ), and the two conclusions follows easily from the induction hypothesis applied to the evaluation of a n .

If n = m (cross-world call), then the type σ → τ of the function must occur as a sub-term of the typing environment E api . Hence, σ / ∈ T and τ / ∈ T . Since the type of v 2 is not in T , by proposition 6 it follows that C n (v 2 , s 2 ). Hence, C n (e {x ← v 2 }, s 2 ), and we can apply the induction hypothesis to the evaluation of a n : ϕ, e {x ← v 2 }, s 2 a n → v/s . The resulting value v is contained in world n and has type τ ; applying again proposition 6, we get C m (v, s ), which is the expected result. 2 B Appendix: modifiable locations in the case of systematic procedural encapsulation

In this appendix, we formalize the notion of modifiable locations, as introduced in section 3.2, in the particular case where the applet environment eapi is well-typed and its type Eapi does not contain any ref types. This is not to say that eapi is purely functional: the functions it provide may very well have side-effects and use references internally. Only, all those internal references must be encapsulated inside functions and never handed to the applet directly. This systematic procedural encapsulation does not reduce expressiveness in any significant way, and at any rate is a reasonable thing to do given that our goal is to characterize semantically procedural encapsulation.

ML(b, s) = ∅ ML((v 1 , v 2 ), s) = ML(v 1 , s) ∪ ML(v 2 , s) ML(λx.a[e], s) = { | there exists v 1 , s ML(e(x), s) From the technical side, requiring that no ref types occur in the applet's interface Eapi has an interesting consequence: only source terms from the browser can operate directly on locations allocated by the browser, and only terms from the applet can operate directly on locations allocated by the applet. Thus, all references are contained (in the sense of appendix A, taking T to be the set of all types where the ref constructor occurs) either in the browser or in the applet, but never go from one world to the other.

We then rely on the notion of containment to define the set ML(v, s) of locations modifiable from value v in store s as the smallest fixpoint of the equations shown in figure 4. The case for closures follows conditions 1 and 4 in the informal discussion from section 3.2. For condition 5, we use the condition Capp(v1, s1) instead of the more natural / ∈ ML(v1, s1), so that the equations remain increasing in ML and the existence of the smallest fixpoint is guaranteed. The typing hypothesis (that Eapi contains no ref types) renders condition 3 vacuous, and also dispenses us with defining ML over locations.

The following lemma show that modifiable locations are indeed the only locations modified during the application of a closure. Proof: Assume, by way of contradiction, that r = err. Given the evaluation rules, there must exist ∈ p such that { ← ∅}, e{x ← v}, s a → err. By definition of ML, this means that ∈ ML(λx.a[e], s). This contradicts the hypothesis p ∩ ML(λx.a[e], s) = ∅. Hence, r = err. We therefore have P rot(p), e{x ← v}, s a → v /s for some v and s . Given the evaluation rules, this implies that we can also derive ∅, e{x ← v}, s a → v /s . Hence, by definition of ML, any belonging to ML(v , s ) or ML(e api , s ) also belongs to ML(λx.a[e], s). It follows that p ∩ ML(v , s ) = ∅ and p ∩ ML(e api , s ) = ∅.

2

Using the notion of modifiable locations instead of reachable locations, we finally obtain a security property similar to property 1: the execution of an applet cannot write to locations that are not modifiable from the initial execution environment. The proof is by induction on the evaluation derivation. We rely on propositions 2 and 7 to ensure that the semantic typing and containment hypotheses go through the induction. The two non-obvious cases are assignment and application of a closure of a browser function. We write ϕ = P rot(p).

Assignment: a is a 1 := a 2 . Applying the induction hypothesis twice, we obtain ϕ, e, s a 1 → v 1 /s 1 and ϕ, e, s 1 a 2 → v 2 /s 2 , with C app (v 1 , s 2 ) and C app (v 2 , s 2 ) and S 2 |= v 1 : σ ref and S 2 |= v 2 : σ and p ∩ ML(e api , s 2 ) = ∅. Hence, v 1 is a location , and since v 1 is contained in app, we have ∈ L app . Thus, / ∈ p and the evaluation of the assignment does not result in err. Moreover, by definition of ML, we have ML(e api , s) = ML(e api , s ) if s( ) = s (l) for all ∈ L env . In the present case, the store s at the end of the evaluation is s 2 { ← v 2 }, with / ∈ L env by containment, hence ML(e api , s ) = ML(e api , s 2 ) and thus p ∩ ML(e api , s ) = ∅ as expected.

  Terms: a ::= x identifiers | b constant of base type (integer, . . . ) | λx.a function abstraction | a1(a2) function application | (a1, a2) pair construction | fst(a) | snd(a) pair projections | ref(a) reference creation | !a dereferencing | a1 := a2 reference assignment

  Values: v ::= b values of base types | λx.a[e] function closures | (v1, v2) pairs of values | store locations Results: r ::= v/s normal termination | err write violation detected Environments: e

Figure 1 :

 1 Figure 1: Evaluation rules

  Types: τ ::= ι base type (int, string, etc.) | t named type | τ1 → τ2 function type | τ1 × τ2 product type | τ ref reference type Conversely, we enrich the syntax of terms with two new constructs: explicit coercions to and from named types, and run-time validation of values of named types. Terms: a ::= . . . (as before) | τ (a) coercion to type τ | OK t (a) run-time validation at type t The typing rules for the calculus are shown in figure 3, and the extra evaluation rules for the new constructs in figure 2.

2 •

 2 λx.a[e] : τ1 → τ2 if there exists a typing environment E such that S |= e : E and E λx.a : τ 1 → τ S |= (v1, v2) : τ1 × τ2 if S |= v1 : τ1 and S |= v2 : τ2 • S |= : τ ref if τ = S( ) • S |= e : E if Dom(e) = Dom(E) and for all x ∈ Dom(e), S |= e(x) : E(x) • |= s : S if Dom(s) = Dom(S) and for all ∈ Dom(s), S |= s( ) : S( ).

Proposition 2 ( 2 5

 22 Type soundness) Assume E a : τ and |= s : S and S |= e : E. If ϕ, e, s a → v/s , then there exists a store typing S extending S such that S |= v : τ and |= s : S .Proof: The proof is a simple inductive argument on the evaluation derivation; see[17, prop. 3.6] for details. Type-based security properties

Proposition 3

 3 Assume E (a τ ref := b τ ) : unit and S |= e : E and |= s : S. Write ϕ = P rot(P V, S). If ϕ, e, s IW (a τ ref ) → err and ϕ, e, s IW (b τ ) → err, then ϕ, e, s IW (a τ ref := b τ ) → err.

Figure 4 :

 4 Figure 4: Definition of the set ML(v, s) of locations modifiable from value v in store s

Proposition 8

 8 Let p be a set of locations, with p ⊆ L env . Let λx.a env [e] be a closure of an environment function. Assume p ∩ ML(λx.a[e], s) = ∅ and C app (v, s). If P rot(p), e{x ← v}, s a → r, then r = err. Instead, r = v /s , and moreover p ∩ ML(v , s ) = ∅ and p ∩ ML(e api , s ) = ∅.

Security property 5 Proposition 9

 59 Assume S |= e api : E api and |= s : S. Further assume that E api contains no ref types. If p ⊆ Dom(s) and p ∩ ML(eapi, s) = ∅, then for all applets a, we have Prot(p), eapi, s a → err. The property follows from the inductive proposition below. Assume S |= e api : E api and |= s : S and E api contains no ref types. Further assume p ⊆ L env and p ∩ ML(e api , s) = ∅. Assume E a app : τ and S |= e : E and C app (e, s). If Prot(p), e, s a app → r, then r = err. Instead, r = v /s and we have p ∩ ML(e api , s ) = ∅ Proof:

  Application: a is a1(a2). By induction hypothesis, we have ϕ, e, s a1 → v1/s1 and ϕ, e, s1 a2 → v2/s2, with Capp(v1, s2) and Capp(v2, s2) and S2 |= v1 : σ → τ and S2 |= v2 : σ and p ∩ ML(eapi, s2) = ∅. Hence, v1 is a closure λx.a m [e ]. If m = app (the function comes from the applet), the result follows from the induction hypothesis applied to the evaluation of a . If m = env (the function comes from the applet environment), the closure λx.a m [e ] can only be obtained by looking up a variable bound in eapi, then possibly performing some function applications or fst and snd operations. Thus, we have ML(λx.a m [e ], s2) ⊆ ML(eapi, s2), and the result follows by proposition 8. 2

  Assume S |= e api : E api and |= s : S. Further assume that E api contains no occurrence of t ref for any t, and that all function closures in e and s have been instrumented with the IW scheme (that is, e and s are obtained by evaluating source terms instrumented with IW ). Then, for every applet a well-typed in E, we have P rot(P V, S), s, e a → err. More precisely, we apply appendix A with T being the set of all type expressions where t ref occurs, L app being the set of locations with types in T allocated by the applet, and L env being the set of locations with types in T allocated by environment functions or initially present in e api . The containment lemma (proposition 7) then shows that the location being assigned does not belong to L env . Moreover, by construction of P rot and L The requirement that no t ref occurs in Eapi is clearly too strong: nothing wrong could happen if, for instance, one of the environment functions has type t ref → unit (the t ref argument is provided by the applet). We conjecture that it suffices to require that type t ref does not occur in Eapp at a positive occurrence nor under a ref constructor.

	Security property 2 Proof: We consider all assignments to references that oc-
	cur in the evaluation derivation for a. By proposition 3, as-
	signments performed by environment functions cannot cause
	a write error, since the right-hand side has been instru-
	mented by IW . For assignments performed by the applet,
	we use a containment lemma developed in appendix A to
	show that the reference being assigned cannot belong to
	Dom(P rot(P V, S)).
	The environment contains a function taking as
	argument an applet-provided reference to a t ref,
	e.g. Eapi(f ) = t ref ref → unit. The environment
	function f could then store a sensitive location into
	that t ref ref, from which the applet can recover
	the sensitive location later.
	We rule out all these cases by simply requiring that no type
	t ref occurs (at arbitrary depths) in Eapi. This leads to the
	following security property:

env , we have Dom(P rot(P V, S)) ⊆ L env . Thus, assignments performed by the applet do not cause write violations either. Hence, the applet cannot evaluate to err.

2

  Proposition 5 Assume either ∈ Lm and Cm(v, s), or ∈ L shared and Capp(v, s) and Cenv(v, s). Then, for all values w and worlds n, Cn(w, s) implies Cn(w, s{ ← v}). The proof is a standard argument by coinduction, close to the proof of lemma 4.6 in[START_REF] Tofte | Type inference for polymorphic references[END_REF]. The only nontrival case is w = (the modified location). By hypothesis Cn(w, s), we have / ∈ L Notice that s ( ) = v. If n = m, we have Cn(v, s) by assumption, hence Cn(v, s ) by the coinduction hypothesis, from which it follows that Cn( , s ). If n = m, since / ∈ L n , we have / ∈ Lm and thus it must be the case that ∈ L shared and C app (v, s) and C env (v, s) to comply with the assumptions of the proposition. Thus, we have C n (v, s) and we conclude as in the previous case.2 By structural induction on τ . If τ is a base type or a function type, then v is a base value or a closure, and the containment of v is independent of the world m. If τ is a product type τ 1 ×τ 2 , the closure condition over T guarantees that τ 1 / ∈ T and τ 2 / ∈ T ; the result follows from the induction hypothesis. Finally, if τ is a ref type, we have v = and τ = S( ) ref. Since τ / ∈ T , it follows that belongs to L shared , but neither to L app nor L env . Hence, l / ∈ L m . Moreover, S( ) / ∈ T by the closure condition on T , hence C m (s( ), s) by application of the induction hypothesis. It follows that C m ( , s). 2 If ϕ, e, s a m → v/s , then C m (v, s ), and for all values w and worlds n such that C n (w, s), we have C n (w, s ). The proof is by induction on the evaluation derivation and case analysis on a. Notice that by proposition 2, we have the additional result that there exists a store typing S extending S such that S |= v : τ and |= s : S . This makes the semantic typing hypotheses go through the induction. The interesting cases are assignment and function application; the other cases are straightforward. Hence, v 1 is a location , and since v 1 is contained in m, we have / ∈ L m . Therefore, either ∈ L m or ∈ L shared . But in the latter case, σ / ∈ T by construction of L shared , hence Cm(v2, s2) implies C m (v2, s2) as well by proposition 6. In both cases, the hypotheses of proposition 5 are met. Writing s = s2{ ← v2}, we obtain the expected result: Cn(w, s) implies Cn(w, s ) for all n, w. The other expected result, Cm((), s ), is trivial.

	Proof: Second, values that belongs to a type τ / ∈ T can be exchanged between the app and env worlds without breaking containment. We can now show that containment is preserved at each evaluation step: Proposition 7 (Containment lemma) Let E api be the type of the execution environment for applets. Assume E api (x) / ∈ T for all x ∈ Dom(E api ). Further assume E a Proof: Assignment: a is (a σ ref 1 hypothesis twice, obtaining ϕ, e, s a 1 → v 1 /s 1 C m (v 1 , s 2 ) Cn(w, s) implies Cn(w, s2) for all n, w := a σ 2 ). We apply the induction ϕ, e, s 1 a 2 → v 2 /s 2 C m (v 2 , s 2 ) S2 |= v1 : σ ref S2 |= v2 : σ |= s2 : S2. Application: a is a σ→τ 1 (a σ 2 ). By applying the induction hypothesis twice, we obtain ϕ, e, s a1 → v1/s1 ϕ, e, s1 a2 → v2/s2 Cm(v1, s2) Cm(v2, s2)

n and Cn(s( ), s). Write s = s{ ← v}. Proposition 6 Assume S |= v : τ and |= s : S. If τ / ∈ T , then C m (v, s) implies C m (v, s) for all worlds m. Proof: m : τ and S |= e : E and |= s : S and C m (e, s).

  1 , v 2 , s 2 such that Capp(v1, s1) and s1( ) = s( ) for all ∈ Lenv, and either { ← ∅}, e{x ← v1}, s1 a → err, or ∅, e{x ← v 1 }, s a → v 2 /s 2 and ∈ ML(v 2 , s 2 ) ∪ ML(e api , s 2 )}

	ML(e, s) =
	x∈Dom(e)


Xavier Leroy

The e ectiveness of type-based unboxing

We compare the e ciency of type-based unboxing strategies with that of simpler, untyped unboxing optimizations, building on our practical experience with the Gallium and Objective Caml compilers. We nd the untyped optimizations to perform as well on the best case and signi cantly better in the worst case.

Introduction

In Pascal or C, the actual types of all data are always known at compile-time, allowing the compilers to base data representation decisions on this typing information, thus supporting e cient memory layout of data structures as well as e cient calling conventions for functions. This is no longer true for languages featuring polymorphism and type abstraction, such as ML: there, the static, compile-time type information does not always determine the actual, run-time type of a data (e.g. when the static type contains type variables or abstract type identi ers).

Hence, compilers for these languages often abandon C-style type-based data representations and revert to uniform, Lisp-style data representations, where all data structures t a common format (usually, one word), if necessary by boxing (i.e. heap-allocating and handling through a pointer) data that does not naturally t the common format.

However, the extra boxing involved can be quite expensive in terms of performance, and is a bottleneck in certain applications, especially numerical computation. To address this issue, a number of unboxing strategies for polymorphically-typed languages have been proposed: some rely on static typing information, just like C-style representation algorithms, but extended to cope with polymorphism and abstract types [START_REF] Morrisett | Compiling with types[END_REF]12,[START_REF] Leroy | The Objective Caml system. Software and documentation available on the Web[END_REF][START_REF] Shivers | Control-ow analysis in Scheme[END_REF][START_REF] Shao | A type-based compiler for Standard ML[END_REF]; others rely on program analyses distinct from typing and apply equally well to untyped or dynamically-typed languages [START_REF] Appel | Run-time tags aren't necessary[END_REF][START_REF] Peyton-Jones | Unboxed values as rst-class citizens in a non-strict functional language[END_REF].

Authors' address: projet Cristal, B.P.105, 78153 Le Chesnay, France. E-mail: Xavier.Leroy@inria.fr.

If only core ML polymorphism is considered, a simpler alternative to these unboxing strategies is monomorphisation (duplicating polymorphic functions once for each instantiation type to obtain a monomorphic program). Experimental evidence [START_REF] Goubault | Generalized boxing, congruences and partial inlining[END_REF][START_REF] Ohori | An unboxed operational semantics for ML polymorphism[END_REF] suggests that monomorphisation does not result in major increase in code size, even though it remains delicate to implement e ciently in a separate compilation context. But the real challenge is with the SML module system, especially functors and type abstraction in structures, which results in large quantities of generic code (code that manipulates values whose representation types are statically unknown). Here, monomorphisation does not appear viable, leaving the unboxing strategies mentioned above as the only alternatives.

In this position paper, we build on our practical experience with unboxing strategies in the Gallium and Objective Caml compilers to assess the e ciency of typebased unboxing. We claim that while type-based unboxing strategies can be very e ective on some monomorphic programs (e.g. numerical applications), they also add signi cant overhead to polymorphic programs and some monomorphic programs as well (e.g. symbolic computation). On the other hand, we found that untyped unboxing strategies can also achieve good performances on numerical applications, without penalizing symbolic computations. In other words, the best case for untyped strategies is almost as good as for typebased strategies, but the worst case is signi cantly better.

The remainder of this paper is organized as follows. Section 2 recalls the main type-based unboxing strategies proposed so far. Section 3 analyzes some of the overheads incurred by these strategies. Section 4 presents untyped unboxing optimizations that avoid these overheads. Section 5 discusses experimental results obtained with our Caml compilers, followed by concluding remarks in section 6.

2 Type-directed unboxing Type-directed techniques for avoiding unnecessary boxing fall in three classes:

Coercions: In this approach, coercions between boxed and unboxed data representations are inserted at type specialization points, so that generic code always operates on boxed representations, while monomorphic code can take advantage of unboxed representations [START_REF] Leroy | The Objective Caml system. Software and documentation available on the Web[END_REF][START_REF] Serrano | Control ow analysis: a functional language compilation paradigm[END_REF]. This approach is particularly e ective for supporting e cient, register-based calling conventions (with tuple arguments attened and oat arguments passed in oat registers). Its main weakness is that it does not support deep unboxing inside generic data structures (e.g. lists or arrays with unboxed elements).

Run-time type inspection: Here, run-time representations of static typing information are maintained in the program, as extra arguments to polymorphic functions and extra components of structures de ning abstract types; generic code then inspects those run-time type expressions to determine the locations and sizes of values with statically unknown types [START_REF] Shivers | Control-ow analysis in Scheme[END_REF][START_REF] Leroy | Le syst eme Caml Special Light: modules et compilation e cace en Caml[END_REF]. Earlier proposals in the context of stack-based abstract machines 9, 10] pass only size information as extra parameters, instead of full type expressions. Unlike the coercion-based approach, this approach supports arbitrary unboxing inside data structures, but does not accommodate very well e cient register-based calling conventions for generic functions.

Tag-based unboxing: Tagging is a well-known technique for implementing dynamically-typed languages (Lisp, Smalltalk). It can be used as a special case of run-time type inspection, where type information is attached to data structures instead of being passed separately, and type expressions are mapped to a small set of base types, e ciently encoded at the bit level. Tagging supports only type inspection over types of existing values, and is best performed on large data structures, where the space overhead of storing the tag is negligible.

As an example of tag-based unboxing, we show how arrays are handled in the Gallium 2 and Objective Caml compilers. The run-time system supports two kinds of arrays: arrays of pointers and tagged integers, and arrays of unboxed oats. The two kinds have di erent tag bytes in the array header. Operations on arrays with a known type ( array where is neither a type variable nor an abstract type) generate directly the correct code for accessing arrays of pointers or oats. Array operations with statically unknown type test the array tag at run-time, and if it is a oat array, perform the required boxing and unboxing of oating-point numbers. This scheme supports fast operations over oat arrays with known type, without the expense of extra type parameters, but at the cost of slower operations over generic arrays.

Overheads of type-directed unboxing

The overall goal of unboxing is to make program run faster by reducing the number of heap allocations and pointer dereferences. However, the unboxing techniques presented above also add extra run-time operations. The overheads of unboxing techniques must therefore be weighted carefully against the bene ts. It must be kept in mind that the load operations eliminated by unboxing are relatively inexpensive operations on a modern processor with good memory hierarchy and possibly several load/store units. Heap allocations eliminated by unboxing represent more signi cant savings. Still, even small overheads can result in unboxing techniques being globally less e cient than no unboxing at all. Run-time type inspection: Propagating type information at run-time adds some overhead to polymorphic function calls: there are more arguments to pass, and more importantly some heap allocation is often performed to build the tree-shaped structures representing types at run-time. Even constant type expressions, entirely built at compile-time, entail the overhead of loading constant pointers in registers1 . The second source of overhead is actually testing the run-time type information inside generic code. This can involve complex pattern-matching on the type expressions, resulting in additional loads and conditional branches, as well as a general increase in code size.

Several techniques have been proposed to reduce the overhead of type building or type inspection, but not both. Tolmach 19] uses an indirect representation of type expressions, reminiscent of explicit substitutions, so that only the variable parts of type expressions need to be passed at run-time. This greatly reduces runtime heap allocations of type expressions, but still requires arbitrary pattern-matching for type discrimination. Shao 16] uses hash-consing to reduce most type tests to simple pointer equality tests, but this makes type construction even more expensive.

Little experimental data on the actual cost of runtime type passing and type inspection has been published. The gures in 18] are not conclusive, since they are given for small test programs where all run-time type handling has been eliminated through aggressive inlining. Morrisett 8] reports slow-downs of 10% to 350% between single-module test programs (hence completely monomorphised by the compiler) and the same programs split in several separately-compiled modules (hence still containing run-time type tests). However, the slow-downs reported also include the cost of calling unknown functions instead of using pre-de ned inlined operations. Even if its precise cost has not yet been determined, we believe that run-time type inspection can have a fairly high price on modern processors: it increases code size and introduces lots of conditional branches, which are di cult to schedule well and consume extra entries in the processor's branch prediction tables. Both phenomena favor code stalls, which are very expensive on modern processors.

Tag-based unboxing: Tagging shares some of the costs of run-time type inspection, but not all. Storing tags in newly-allocated blocks often has zero cost, since the tag can often be merged with GC information, which has to be maintained in any case. In Objective Caml, for instance, each heap block has a onebyte tag stored in the one-word header containing the block size and GC marking bits. There is no overhead on function calls, since no extra type parameters are introduced. Run-time tag tests are relatively inexpensive (one load and one integer comparison), never requiring pattern-matching on arbitrary trees. However, some of the drawbacks of run-time type inspection still apply to tag tests: increased code size and extra conditional branches. For instance, in Objective Caml 1.05, a polymorphic array copy function runs 10 times slower than the same function specialized to integer arrays, and 8 times slower than the same function specialized to oat arrays.

GC overhead

The sources of overhead discussed so far apply only to generic code: fully monomorphic code pays no performance penalty. This is not the case for the GC-related overhead, discussed below, which a ects all programs.

Unboxing strategies can add signi cant overhead to the traversal of the memory graph performed by the garbage collector. With a conventional, fully-boxed data representation strategy, walking the memory graph is relatively e cient: typically, one bit needs to be tested in every value to distinguish pointers from integers; then, for each pointer, one word of header must be consulted to determine the size of the block and whether it contains other pointers or just raw data. Most unboxing strategies complicate this traversal of the memory graph:

Getting the roots in the stack With unboxing, stack frames usually contain a mixture of valid pointers (or well-tagged integers) and raw, unboxed integers and oats. A non-conservative garbage collector needs to distinguish the pointers from the raw data. One possibility, used in Gallium and Objective Caml, is to associate frame descriptors, listing the locations of the pointers in the frame, to return addresses. Finding the descriptors associated with the return addresses in the stack frames and interpreting them adds some overhead compared with a fully boxed model where all stack words are valid pointers or tagged integers.

Handling mixtures of pointers and raw data in heap blocks Some unboxing strategies result in heap blocks that contain pointers intermingled with unboxed integers or oats. For instance, in Gallium, a heap block containing a value of type string * float * int list contains two pointers at byte o sets 0 and 12, separated by 8 bytes of raw data for the unboxed oat. In this case, nding all the pointers contained in a block is no longer a yes/no question. The Gallium runtime system stores, in the block header, a pointer to a block descriptor enumerating the machine types (address, integer or oat) of all block elds. The garbage collector then decodes that information to follow the pointers contained in the block. Despite various optimizations for frequent special cases (no pointers, all pointers, etc.), we found that this decoding of block descriptors accounts for a fairly large part of the time spent in garbage collection.

Type-directed garbage collection Some garbage collectors abandon tags and header words altogether, and base their traversal of the memory graph on static type information, using either run-time type parameters for polymorphic code 19] or GC-time type reconstruction 2, 1]. Here, determining where pointers lie inside blocks is even more expensive than in the previous case, since instead of reading pre-digested block descriptors, the garbage collector must interpret full type expressions. In addition, since type information is not attached to data, a Cheney-style breadth-rst traversal of the memory graph is no longer feasible and must be replaced by a depth-rst traversal 2, 19] or allocate extra heap memory for storing types. Tolmach 19] reports execution times ranging from 0.6 to 2.6 relative to a Gallium-style garbage collector on small programs. (Some of the extra cost of garbage collection is compensated by the fact that heap blocks are smaller { no extra header word is required). We believe more important slow-downs would be observed relative to a conventional, fully-tagged garbage collector, especially on larger programs.

In conclusion, the GC overhead of an unboxing strategy can be signi cant, and a ects not only generic code, but fully monomorphic programs as well. This is especially bad for heavy symbolic processing (e.g. theorem proving), which is GC-intensive (it is not unusual to spend more than 30% of total running time in garbage collection), and does not bene t much from unboxing optimizations: most of the computation is performed on tree-shaped datatypes representing expressions, which remain fully boxed with all existing unboxing strategies. Symbolic processing often runs slower with aggressive unboxing optimizations than with a conventional, fullyboxed data representation, since the main code is identical but the garbage collector runs slower. In our opinion, this is not acceptable: symbolic processing, which is ML's bread and butter, should never run slower due to optimizations targeted towards hypothetical numerical or byte-oriented applications.

Recovering the e ciency of a conventional, fullytagged garbage collector can be done in two directions. The rst is to restrict the unboxing strategy so that it never produces heap blocks containing both pointers and unboxed data. For instance, a heap block containing a value of type float * float has the two oats unboxed (and is marked as \raw data" for the garbage collector), but a block containing a float * string holds two pointers, the oat being allocated separately. Both SML/NJ and Objective Caml go even further and atten only records of oating-point numbers, keeping everything else boxed inside heap blocks [START_REF] Serrano | Control ow analysis: a functional language compilation paradigm[END_REF][START_REF] Jones | Partial evaluation for dictionary-free overloading[END_REF].

The second direction is to allow mixed heap blocks, but group all pointers at the beginning of the block. The garbage collector is then instructed to follow the rst N elds as pointers, with N possibly null or smaller than the actual size of the block. This greatly complicates access to block elds: a block of type 1 * 2 , no longer contains a value of type 1 followed by a value of type 2 ; for instance, if 1 = string * int and 2 = string, the rst component of the pair is composed of elds 0 and 2 of the block, while the second component is eld 1. Also, there are practical di culties with storing both a size and a pointer count in a one-word block header.

Untyped unboxing techniques

In addition to the type-directed unboxing techniques recalled in section 2, there also exists several unboxing techniques that use no or very little typing information, yet achieve most of the performance of type-based techniques, usually with a better worst-case behavior.

Local unboxing

Boxing and unboxing operations that cancel each other in the same function body are easily eliminated by a straightforward data ow analysis. For instance, the following Objective Caml code let f a x = let y = a.(0) *. x in y +. 1.0 performs only one oat unboxing (on the x argument) and one oat boxing (on the function result); the intermediate results remain unboxed. Also, the access to the array a performs neither unboxing nor type testing, since a is statically known to be a oat array. Trivial as it may seem, local unboxing is already very e ective on numerical code, provided loops are not represented as tail-recursive functions in the intermediate language, but kept as part of the current function using special loop constructs in the intermediate language.

For instance, the core of our FFT benchmark (see section 5) is composed of one fairly large function with four nested loops; local unboxing succeeds in eliminating all oating-point boxing and unboxing in this function, resulting in assembly code that looks very much like the one produced by a good C compiler.

Like all data ow analyses, local unboxing can be extended to an inter-function analysis operating on whole compilation units, by combining it with a control-ow analysis (to determine the call graph) and an escape analysis (to determine data structures for which all creation and use sites are known). The Bigloo Scheme compiler performs unboxing of oats and oat arrays this way, and achieves respectable performance on numerical code 13].

Known functions and partial inlining

A standard trick for making function calls with multiple arguments e cient in ML is to have two entry points per function: a standard entry point, using the regular calling conventions (take a heap-allocated tuple of arguments for uncurried function, or take one argument and return a closure for a curried function), and a fast entry point, taking all the arguments in registers. A direct call to the fast entry point is generated when the caller \knows" which function is being called (i.e. a control-ow analysis has determined that only one function ows to the call site) and provides exactly the expected number of arguments (no partial application). In all other cases (call to an unknown function, partial application, etc.), a regular call through the function's closure is generated, and the closure points to the standard entry point. The standard entry point can be a code prelude sequence, which dispatches the arguments to registers before falling through the fast entry point, or (to save code space) a shared combinator, which dispatches the arguments before tail-calling the fast entry point, stored in a conventional eld of the closure. For calling known functions taking a tuple of arguments, this scheme is essentially as e cient as unboxed tuples in a coercion-based unboxing scheme 6]. Unboxed tuples work better for calls to unknown functions with known types, but the multiple entry point scheme deals with curried functions equally well, while unboxing schemes are ine ective against currying.

Peyton-Jones and Launchbury 12] and independently Goubault 3] proposed an elegant reformulation of the multiple entry point trick as a partial inlining problem, which allows not only tuples of arguments to be unboxed, but also tuples of results, oating-point arguments and results, and possibly more. It is obvious that inlining a function at point of call and applying a local unboxing optimization gets rid of all unnecessary boxing of the function arguments and results. However, most functions are too large to be inlined. The solution is to decompose functions into three parts: a prelude that unboxes those arguments that need to be unboxed (as determined by the local unboxing analysis); a body that takes unboxed arguments and computes unboxed results; a postlude that boxes the results. Then, the function is partially inlined at call sites where it can be determined that the function is the only one that ows to these call sites: the prelude and postlude are inlined, hopefully canceling the boxing and unboxing operations around the call site; the function body is not inlined, but simply called.

No experimental results have been published for the partial inlining approach to unboxing, but, based on our experience with multiple entry points for curried and uncurried functions in Objective Caml, we expect this scheme to be very e ective for removing boxing and unboxing operations around function calls. The only potential problem is a certain growth in code size when the inlined preludes and postludes do not cancel cleanly with other operations around the call site. Also, inlining a postlude can prevent tail call optimization.

Of course, both multiple entry points and partial inlining apply only to calls to known functions. On our test suite for the Objective Caml compiler, 80% to 100% of all dynamically executed function calls are statically turned into direct calls to known functions. However, Objective Caml uses a very simple-minded control-ow analysis, comparable to the rst iteration of the 0CFA algorithm 17, 14]; we expect that better control-ow analyses would lead to even better gures. Objective Caml's simple-minded control-ow analysis works quite well not only on the core ML language, but across structures and functors as well. We have not yet extended it to the object-oriented features of Objective Caml, however. It is likely that more sophisticated control-ow analyses are needed to recognize invocations of known methods.

Experimental results

We now discuss some experimental results obtained with the Gallium 1, Gallium 2 and Objective Caml compilers. Gallium 1 was the rst implementation of the coercion-based type-directed unboxing presented in 6]. It generated code for the MIPS processor and had a simple, one-generation copying collector. Gallium 2, brie y described in 19], also uses coercion-based unboxing, but adds a better, more portable code generator, a two-generation copying collector, as well as tag-based unboxing of oats in arrays (as described in section 2). The Objective Caml native-code compiler 5, 7] abandons coercion-based unboxing and uses conventional, mostly-tagged data representations in combination with local unboxing of oats (as described in section 4.1), multiple entry points to uncurried and curried functions (section 4.2), and tag-based handling of unboxed oat arrays (section 2). The garbage collector has two generations, using an incremental mark-and-sweep collector on the old generation. The main reason coercion-based unboxing was abandoned in Objective Caml is because of the GC overhead discussed in section 3.2, and also to allow more code sharing with the Objective Caml bytecode compiler.

The rst series of experimental results are shown in gure 1. They compare the Gallium 1 compiler with type-directed unboxing versus a simple variant of the same compiler using conventional, fully boxed or tagged data representations. The intent was to compare unboxed and boxed representation strategies with all other things (code generator, garbage collector, etc) being equal. The compiler using boxed representations did not implement any kind of local unboxing nor optimizations for multiple-argument functions, though. The results are taken from 6].

As gure 1 shows, unboxing is most e ective on programs that perform a lot of oating-point computation, such as integral, achieving speedups of 3 to 4. Integer computations (sieve, sumlist) run at about the The second set of results ( gure 2) pit the Gallium 2 compiler, with coercion-based type-directed unboxing, against the Objective Caml 1.05 native-code compiler, which uses mostly standard (tagged or boxed) data representations combined with a number of tricks for oats, oat arrays, and multiple-argument functions. The comparison is not completely fair, since both compilers use slightly di erent code generators and garbage collectors.

As gure 2 shows, despite its inferior unboxing technology, Objective Caml matches the performances of Gallium 2 on most tests. Objective Caml is even slightly faster than Gallium 2 on some symbolic processing tests (knuth-bendix, bdd), a fact we attribute to the simpler heap traversal in the Objective Caml garbage collector, which, unlike Gallium's, does not have to deal with mixed pointers and raw data in heap blocks. On the other hand, the Objective Caml garbage collector is handicapped by the fact that the major heap is not contiguous (it grows on demand without copying), making it more expensive to determine which pointers point to the heap than in Gallium; this accounts for Gallium's better performance on boyer.

On oating-point tests (fft, nucleic), local unboxing of oats as in Objective Caml is just as e ective as the more general unboxing strategy of Gallium 2. Integer tests (fib, takeushi, sieve, solitaire) show no signi cant di erences, thus con rming that 63-bit tagged arithmetic is essentially as fast as 64-bit native arithmetic.

Tests involving arrays (fft, quicksort, solitaire, bdd) show a large performance advantage for Objective Caml. This is a consequence of much more e cient array bounds checking in Objective Caml. To compensate for this, we also give measurements with array bounds checking turned o (the starred tests in gure 2).

The only test where Objective Caml is noticeably slower is mandelbrot, which operates on references to oats. The Gallium compiler gets rid of the two levels of indirection (the reference, then the oat), while the local unboxing algorithm of Objective Caml 1.05 eliminates only one level. This is to be construed as a bug in Objective Caml 1.05, which we expect to x shortly.

Conclusions

Like all typing analyses, type-directed unboxing is highly systematic: all data having the same type must have the same representation. This leads to unboxing strategies that either unbox very little, as in SML/NJ, or unbox quite a lot but slow down the garbage collector and other parts of the runtime system, as in Gallium. We believe unboxing is best viewed as an optimization, in the classic compiler sense of the term: a transformation that can be applied or not on a case-by-case basis, without compromising correctness. Following this approach, we have found that a modest amount of typedirected unboxing (tag-based handling of unboxed oat arrays and records of unboxed oats) combined with mostly-standard, untyped optimizations (local unbox- ing, special calling protocols for known functions) performs just as well as, and even slightly better than aggressive coercion-based type-directed unboxing. We conclude that unboxing is not the \killer app" for type-based compilation: good unboxing can be achieved without propagating type information through the whole compilation chain2 . This is not to say that it's a bad idea to propagate types throughout an ML compiler; just that there must be other motivations to do so besides unboxing optimizations.

Figure 2 :

 2 Figure 2: Performance comparison between Gallium 2 and Objective Caml 1.05

  Times are given in seconds, averaged on three runs. The tests were conducted on an Alpha 21064-based Decstation 3000/400 running Digital Unix.

	Test bdd bdd * boyer fft fft * fib genlex knuth-bendix mandelbrot nucleic quad quad succ quicksort quicksort * sieve solitaire solitaire * takeushi	Gallium 2 Obj. Caml What is tested 19.0 12.3 term processing, hash tables 17.8 11.0 same as bdd, without array bounds checking 0.52 0.62 term processing, function calls 3.49 2.00 oating-point arithmetic, oat arrays 2.02 1.58 same as fft, without array bounds checking 0.33 0.34 integer arithmetic, function calls (1 argument) 0.69 0.76 lexing, parsing, symbolic processing 3.00 2.47 term processing, function calls, functionals 2.52 7.31 oating-point arithmetic, loops 0.88 0.89 oating-point arithmetic, tree searching 0.53 0.12 Church numerals, functionals, polymorphism 1.44 0.65 integer arrays, loops 0.54 0.43 same as quicksort, without array bounds checking 1.03 1.01 integer arithmetic, list processing, functionals 1.51 0.56 arrays, loops 0.41 0.38 same as solitaire, without array bounds checking 0.41 0.39 integer arithmetic, function calls (3 arguments)

With position-independent code, as is now standard on the Alpha and PowerPC, loading a constant pointer is not as cheap as it seems, since it is turned into a load and requires the global pointer to be properly set up.

The Objective Caml compiler exploits type information in the rst compilation pass only { the one that goes from ML abstract syntax to the lambda intermediate code. All type-directed transformations are performed there. This greatly simpli es further compilation passes, which do not have to keep typing information up to date.