Xavier Leroy

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 typebased 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: Web browsers and beyond[END_REF], some of them do cause a violation of Java type soundness [START_REF] Hopwood | Java security bug (applets can load native methods)[END_REF]; 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.1 beta2 security API. Dyade[END_REF]. Another typical example is the ActiveX applet described in [START_REF] Brunnstein | Hostile ActiveX control demonstrated[END_REF] that does a Trojan attack on the Quicken home-banking software: money gets transferred from the user's bank account to some offshore account, all in a perfectly type-safe way.

Appeared in Secure Internet Programming -Security issues for Mobile and Distributed Objects, edited by J. Vitek and C. Jensen, pages 147-184, Springer-Verlag LNCS 1603, 1999. François Rouaix's current affiliation is Liquid Market Inc, 5757 West Century Bld, Los Angeles, CA 90045, USA.

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, section 7 outlines the security architecture for applets in the MMM Web browser and discusses the relevance of our results to this practical example. Related work is discussed in section 8, followed by concluding remarks in section 9.

2 The language and its security policy

The language

The language we consider in this paper is a simple lambda-calculus 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, hardware-oriented 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 higherlevel 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, host 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 simple 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. More advanced privacy properties, as provided for instance by information flow models, are well beyond our approach, however.

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: ϕ, e, s a ϕ, e, s a

1 → v 1 /s 1 ϕ, e, s 1 a 2 → v 2 /s 2 ϕ, e, s (a 1 , a 2 ) → (v 1 , v 2 )/s 2 (
1 → /s 1 ϕ, e, s 1 a 2 → v 2 /s 2 / ∈ Dom(ϕ) or v 2 ∈ ϕ( ) ϕ, e, s (a 1 := a 2 ) → ()/s 2 { ← v 2 } (10) ϕ, e, s a 1 → /s 1 ϕ, e, s 1 a 2 → v 2 /s 2 ∈ Dom(ϕ) and v 2 / ∈ ϕ( ) ϕ, e, s (a1 := a2) → err (11)
Error propagation rules:

ϕ, e, s a

::= [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 Fig. 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; 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 non-terminating 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, several semantic features that play an important role in our study are easier to express in a big-step semantics than in a reduction semantics: 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 to locations that are reachable from 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) RL(e, s) = x∈Dom(e)

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 lemma as the induction hypothesis: Lemma 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 Property 1 holds in practice only if the evaluation of a on an actual processor adheres to the rules given in Fig. 1. For instance, the rules do not allow the evaluation of b := a where b is an integer constant, but an untyped or weakly-typed implementation might execute b := a without crashing nor reporting an error in the case where b is a valid memory address; this would allow the applet to write to arbitrary locations. We rely on a being evaluated by a type-safe implementation to ensure that this cannot happen: either the evaluator must perform run-time type-checking, or a must be well-typed in some sound static type system (such as the one presented below in section 4). 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 dynamicallyscoped 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 ∈ Dom(e). 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 fragments can only apply the closure, but not access 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, which systematically encapsulate resources 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 e api in the store s at the end of the application.

Example: Consider the following environment e api :

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 appletprovided 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: in the closure case, we must consider infinitely many possible arguments. Thus, a full mathematical proof is needed 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 well-typed 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:

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 Fig. 3, and the extra evaluation rules for the new constructs in Fig. 2.

ϕ, e, s a → r ϕ, e, s τ (a) → r [START_REF] Jensen | Security and dynamic class loading in Java: A formalisation[END_REF] ϕ, e, s a → v/s t ∈ Dom(P V ) implies v ∈ P V (t)

ϕ, e, s OKt(a) → v/s [START_REF] Leroy | Polymorphic typing of an algorithmic language[END_REF] ϕ, e, s a → err ϕ, e, s OK t (a) → err

Fig. 2. Extra evaluation rules for coercions and run-time checks

Named types

The overall approach followed in section 5 is to identify groups of references having the same type, and apply a given security policy to all of them. 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.

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 a 1 : τ 1 E a 2 : τ 2 E (a 1 , a 2 ) : τ 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(a) : t (35) E a : t τ = TD(t) E τ (a) : τ (36) E a : t E OK t (a) : t (37)

Fig. 3. Typing rules

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 has occurred yet.

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 GUI 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 the applet code itself or on sensitive data presented by the applet.

In practice, validation OK t (e) involves not only the value of its argument e, but also external information such as the identity of the principal, extra capability arguments passed to the validation functions, 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 [START_REF] Wallach | Understanding stack inspection[END_REF]. For simplicity, we still write OK t as a function of the value of its argument.

The evaluation rule for OK t assumes of course that membership in P V (t) is decidable. This raises obvious difficulties if t stands for a function type, at least if the domain type is infinite. Difficulties for defining P V (t) also arise if t is a reference type: checking the current contents of the references offers no guarantees with respect to future modifications; checking the locations of the references against a fixed set of locations is very restrictive. For those reasons, we restrict ourselves to types t that are defined as algebraic datatypes: type expressions obtained by combining base types with datatype constructors such as list or tuples, but not with ref nor the function arrow.

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 a semantically 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 another store typing 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 S |= v : τ . Proof. The proof is a simple inductive argument on the evaluation derivation; see [START_REF] Leroy | Polymorphic typing of an algorithmic language[END_REF]Prop. 3.6] for details.

-S |= b : ι if Typeof (b) = ι -S |= v : t if S |= v : TD(t) -S |= λx.a[e] : τ 1 → τ 2 if there exists a typing environment E such that S |= e : E and E λx.a : τ 1 → τ 2 -S |= (v 1 , v 2 ) : τ 1 × τ 2 if S |= v 1 : τ 1 and S |= v 2 : τ 2 -S |= : τ ref if τ = S( ) -S |= e : E if

Type-based security properties

The type-based security properties we develop 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. 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.

To illustrate the three instrumentation schemes proposed below, we use pictures in the style of Fig. 4 showing the flow of values between the applet and its execution environment. We focus on values of a named type t whose implementation type is τ = TD(t). The goal of our instrumentation schemes is to make sure that only checked values of type t (solid arrows in the pictures) can reach an assignment on a t ref performed by the execution environment.

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). See Fig. 5 for a graphical illustration. Formally, we define the instrumentation scheme IW , operating on terms a τ annotated with their type τ , as follows: On other kinds of terms, IW is a simple morphism, e.g. IW ((λx.a τ ) σ→τ ) = λx. IW (a τ ), etc.

IW ((a t ref := b t ) unit ) = IW (a t ref ) := OK t (IW (b t )) if t ∈ Dom(P V ) applet environment t(
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 Lemma 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.

Lemma 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. . We conjecture that it suffices to require that no type t ref occurs in E app at a positive occurrence or under a ref constructor. However, our proof of Property 2, and in particular the crucial containment lemma, does not extend to this weaker hypothesis.

E api (f ) = int → t

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. This is depicted in Fig. 6.

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 : τ from 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:

-P V, S |= b : ι if Typeof (b) = ι -P V, S |= v : t if P V, S |= v : TD(t) and t ∈ Dom(P V ) implies v ∈ P V (t) -P V, S |= λx.a[e] : τ 1 → τ 2 if
there exists a typing environment E such that P V, S |= e : E and E λx.a : We then have the following characterization of the the behavior of terms instrumented with IC: Compared with Lemma 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 Lemma 2.

τ 1 → τ 2 -P V, S |= (v 1 , v 2 ) : τ 1 × τ 2 if P V, S |= v 1 : τ 1 and P V, S |= v 2 : τ 2 -P V, S |= : τ ref if τ = S( ) -P V,
Lemma 4.
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, Lemma 4 applies not only to the terms from the execution environment, but also to the applet itself. In a sense, this lemma 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.

Property 3 can be viewed as a formal justification for capability-based systems: 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 is given as argument: λf.λs.OK filename (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.) Figure 7 depicts this approach.

The checking of values coming from the applet 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 a i 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 f i : τ i = W + (IC(Σ(a i )) : τ 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 well-typed: Σ(a i ) 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 Σ(a i ), 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(Σ(a i )) : τ 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 no default constructors offers the same level of guarantees as our abstract types: the applet cannot tamper with the fields of an existing object, nor create an object with arbitrary initial values for the fields. 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 Application: safety in the MMM browser MMM [START_REF] Rouaix | A Web navigator with applets in Caml[END_REF] is a Web browser with applets developed by the second author. MMM ensures safe execution of applets using various techniques similar in spirit to those formulated earlier in this paper. (Essentially identical techniques are now used in the SwitchWare project at U. Penn [START_REF] Alexander | The SwitchWare active network architecture[END_REF][START_REF] Alexander | Security in active networks[END_REF], an active network infrastructure that allows safe downloading of applets on network routers.) Indeed, the formalization presented in this paper grew out of a desire to make more systematic and prove correct the security techniques used in MMM. This section presents the main techniques used in the MMM safe execution environment for applets, and relates them with the formal results we have obtained in this paper.

Type-safe dynamic linking

The MMM browser is written in Objective Caml [START_REF] Leroy | The Objective Caml system. Software and documentation available on the Web[END_REF] and compiled to bytecode by the Caml bytecode compiler. The bytecode is then executed by the Caml virtual machine. Applets are also compiled to Caml bytecode, then loaded in memory and linked with the browser by the Caml dynamic linker (the Dynlink library).

The dynamic linker can be configured to restrict the set of external modules and C primitives that the object file can reference. MMM uses this feature to enforce lexical scoping for applets: only the modules of MMM that comprise the applet execution environment can be referenced by the applet object code; modules internal to MMM are not made accessible to the applet.

The Caml bytecode was designed before applets were fashionable, and is therefore ill-suited to JVM-style bytecode verification. In particular, a number of low-level optimizations are performed in this bytecode (such as erasing type annotations and conflating several high-level types into the same machine-level representations) that makes type reconstruction on bytecode if not impossible, but at least very difficult.

Instead of bytecode verification, the Objective Caml dynamic linker relies on type annotations on the relocation information contained in object files to guarantee type correctness. Bytecode object files contain a list of names of external modules referenced in the file, along with the type interfaces of those modules. The object file thus records which interfaces for those external modules were used for type-checking the source code of the file. The dynamic linker, then, checks that those interfaces are identical to those of the implementations of those modules provided by the MMM browser. This ensures that the applet and the browser have been type-checked against the same type specifications for the applet-browser interface, and can therefore safely be linked together.

To keep them small, object files actually do not contain the whole Caml type interfaces for their imported modules, but only MD5 checksums of those interfaces. The dynamic linker then compares interfaces by comparing their checksums. Since MD5 is a hash function of cryptographic quality, the probability that two different interfaces have the same checksum is extremely low, and thus we can safely assume that if the checksums are equal, then so are the interfaces. However, this approach forces the two interfaces (the one expected by the object file and the one provided by the MMMimplementation) to be exactly identical, while, if we kept whole interfaces, we could use a more lenient comparison such as Caml's interface matching. The latter would allow more flexibility in evolving the applet-browser API.

Of course, comparing import interfaces at link-time guarantees type safety only if the object code contained in the object file is indeed type-correct with respect to the interfaces contained in the object file. Thus, we need to make sure that this object file has been produced by a correct Caml compiler (a compiler that performs sound static type-checking and records correctly all external modules referenced) and has not been modified afterwards (e.g. by hand-modifying some of the interfaces in the object file). This can be enforced in two ways in the context of Web applets.

The first way is to transmit applets over the network as Caml source code, which is type-checked and compiled locally (by calling the Objective Caml bytecode compiler), then dynamically linked inside the browser. Unless the local host is compromised, no tampering with the object files nor the Caml type-checker itself can happen. Unlike applet systems based on source-level interpretation, we still benefit from the efficiency of the Caml bytecode interpreter.

Transmission of applets in source form is often criticized on several grounds: the source code is larger than compiled bytecode; local compilation takes too much time; applet writers do not want to publicize their source. Our experience with Caml is that bytecode object files are about the same size as the source code (unless heavily commented); the bytecode compiler is very fast and the compilation times are small compared with Internet latencies; finally, bytecode is easy to decompile and does not offer significant protection against reverse engineering.

Another way to ensure the correctness of type annotations in bytecode object files is to rely on a cryptographic signature on the object file, which is checked locally by the MMM browser against a list of trusted signers before linking the object file in memory. Unlike Microsoft-style applet signing, this signature is not necessarily made by the author of the applet, and carries no guarantees on what the applet actually does; instead, the signature is made by the person or site who performs the compilation and type-checking of the applet, and certifies only that the applet passed type-checking by an unmodified Caml compiler and that its object file has not been tampered since.

We initially envisioned having some centralized type-checking authority: one or several reputable sites (such as INRIA) that accept source code from applet developers, type-check and compile them locally, sign the object file and return it to the applet developer. The object file can then be made available on the Web. Seeing the authority's signature, browsers can trust the type information contained in the object file and use it to validate the applet against the environment they provide. In retrospect, this approach relies too much on a centralized authority to scale up to the world-wide Web. However, it is perfectly suited to the distribution of compiled applets across a restricted network such as a corporate Intranet.

The execution environment for applets

The execution environment made available to applets is composed of a number of modules that provide a safe subset of the Caml standard library, as well as access to the CamlTk graphical user interface and to selected parts of the MMM browser internals. In particular, an MMM applet can not only interact graphically with the user and trigger navigation functions, like Java applets, but also extend the MMM browser itself by installing new navigation functions, menu items, viewers for new types of embedded documents, display functions for new HTML tags, and decoding functions for new "content-encoding" types.

The applet environment is derived from the OCaml standard library modules and the MMM implementation modules by two major techniques: hiding of unsafe functions via module thinning, and wrapping of unsafe functions with capability checks.

Module thinning: The ML module system offers the ability to take a restricted view of an existing module via a signature constraint:

module RestrM = (M : RestrSig)
Only those components of M that are mentioned in the signature RestrSig are visible in RestrM, and they have the types specified in RestrSig, which may be less precise (more abstract) than their original types in M. This module thinning mechanism thus supports both hiding components (functions, variables, types, exceptions, sub-modules) of a module and making some type components abstract. No code duplication occurs during thinning: the functions in RestrM share their code with the corresponding functions in M.

Large parts of the applet environment are obtained by thinning existing OCaml library modules. In the OCaml standard library, we hide by thinning all file input-output functions, as well as related system interface functions (such as reading environment variables and executing shell commands), and of course all type-unsafe operations (such as array accesses without bound checks and functions that operate on the low-level representation of data structures). For good measure, we also make abstract a few data types such as lexer buffers to hide their internal structure.

In the CamlTk GUI toolkit, we hide all functions that return widgets that may belong to the browser or to other applets. Such functions include finding the parent of a widget, finding a widget by its name, finding which widget owns the focus or the selection, etc. This is less restrictive than checking that widgets manipulated by the applet are children of its top-level widget: the applet can still open new windows and populate them with widgets unrelated with its initial toplevel widget. Other functions that might affect browser widgets (such as binding events on all widgets of a given class or tag) are also removed.

Capabilities: MMM uses capabilities to control potentially harmful functionalities, such as file and network input/output, as well as extending the browser. Individual capabilities include:

-Reading files whose names match a given regular expression.

-Writing files whose names match a given regular expression.

-Accessing the contents of Web documents (e.g. the pages being displayed).

-Installing extension functions in the browser.

Applets are given an initial set of capabilities at load time, which is empty for applets loaded through the network, but allows document access and browser extension for applets loaded from the local disk. Capabilities are of course represented by an abstract data type, to prevent an applet from forging extra capabilities.

All input/output operations as well as registration of browser extensions check the capabilities presented by the applet. If the applet does not possess the capability to perform the requested operation, the browser prompts the user via a pop-up window. The user can then refuse the operation (aborting the execution of the applet), grant permission for this particular operation, or grant permission for further operations of the same kind as well. In the latter case, the browser extends in place the capabilities of the applet. To minimize the number of times the user is prompted, an applet can also request in advance the capabilities it needs later.

Hiding capability arguments: A well-known problem with capability-based security for applets is that all sensitive functions require an extra capability argument [START_REF] Wallach | Extensible security architectures for Java[END_REF]. This clutters the source code for the applet and makes it difficult to convert a piece of stand-alone code into an applet: capability arguments must be added at many different places in the source code.

In functional languages, partial application can be used to pass the capability argument only once per sensitive function. The remainder of the applet can then use the functions open_in and open_out thus obtained by partial application as if they were the normal file opening functions.

MMM makes this approach more convenient by using ML functors to perform the partial applications. Functors are parameterized modules, presented as functions from modules to modules. They provide a convenient mechanism for parameterization en masse: rather than partially applying n functions to m parameters, a structure containing the m parameters is passed once to a functor that return a structure containing the n functions already partially applied to the parameters. In the case of MMM, we thus have a number of functors that take the applet's capability as argument and return structures defining capabilityenabled variants of the standard I/O and browser interface functions, with the same interface as for standalone programs. For instance, to perform file I/O, an MMM applet does the following: module MyCapa = struct let capabilities = Capabilities.get() end module IO = Safeio(MyCapa) open IO . . . code using open_in and other I/O operations as usual. . .

Assessment

The MMM security architecture relies heavily on the three basic ingredients that we considered in our formalization:

-Lexical scoping ensures that applets cannot access all the modules composing the browser and the Caml standard library, but only those "safe" modules made available to the applet during linking. -Type abstraction prevents the applet from forging or tampering with its capability list. It also ensures that the applet cannot forge file descriptors or GUI widgets, but has to go through the safe libraries to create them. -Procedural abstraction is used systematically to wrap sensitive functions (such as opening files or network connections, as well as installing a browser extension) with capability checks.

In particular, capability checks inside environment functions are placed essentially as suggested by the wrapping scheme W + of section 5.3. In the MMM implementation, those capability checks were placed by hand and the same type was used for checked and unchecked data, instead of exploiting two different types as in section 5.3. One of the motivations for our formalization was to systematize the placement of those capability checks, based on typing information. Some aspects of the MMM security architecture are not accounted for by our formalism. The first one is the necessity of taking copies of mutable objects before validating them. A prime example is character strings, which, in Caml, can be modified in place like character arrays. An applet could pass a string containing a valid file name to the file opening function, then modify the string in place between the time it is validated and the time the file is actually opened. This concurrent modification can be achieved via multiple threads or via GUI callback functions.

To avoid this attack, the execution environment must first take private copies of all strings provided by the applet, then validate and utilize the private copies of those strings. Symmetrically, the execution environment must not return strings shared with its internal data structures to the applet, but copies of those strings. Inserting those string copy operations is tedious and error-prone. From the standpoint of applet security, it would be much better to have immutable strings in the language. The guarantees offered by immutable strings could possibly be achieved just by removing all string modification primitives from the applet execution environment, but we have not investigated this approach yet.

Another issue not addressed by our framework is validation of functional values, such as document decoders and HTML tag handling functions installed by the applet. The main reason our framework does not handle function validation is that membership of a functional value in a set P V (t) is in general undecidable. In the particular case of MMM, this problem does not arise: depending on the capabilities given to the applet, either all functions presented by the applet are rejected, or they are all accepted. For more complex situations, we could also move the validation inside the applet-provided function, by wrapping this function with checks on its inputs or outputs.

Resources that can be explicitly deallocated and reassigned later raise interesting problems. A prime example is Unix file descriptors, which are small integers. The type of file descriptors is abstract, and an applet cannot forge a file descriptor itself. However, it could open a file descriptor on a permitted file, close it immediately, keep the abstract value representing the descriptor, and wait until the browser opens a file or network connection and receives the same file descriptor in return. Then, the applet can do input/output directly on the file descriptor, thus accessing unauthorized files or network connections. This "reuse" attack is of course possible only with explicitly-deallocated resources: with implicit deallocation, the resources cannot be deallocated and reallocated as long as the applet keeps a handle on the resource. MMM addresses this problem by wrapping Unix file descriptors in an opaque data structure containing a "valid" bit that is set to false when the file descriptor is closed, and checked before every input/output operations.

The last MMM security feature not addressed by our framework is confidentiality. Our framework focuses on ensuring the integrity of the browser and of the host machine. The MMM applet environment contains security restrictions to ensure integrity (such as controlled write access to files), but also restrictions intended to protect the confidentiality of user data (such as controlled read accesses to files and restricted access to the network). Some restrictions address both integrity and confidentiality problems: for instance, a malicious document decoder could both distort the document as displayed by the browser (an integrity threat) and leak confidential information contained in the document to a third party (a confidentiality threat).

However, the confidentiality policy enforced by the MMM applet environment is simple and does not go beyond traditional access control. While the formal framework presented in this paper focuses on integrity via access control on writes, we believe that parts of this framework (procedural encapsulation and type abstraction) can be extended to deal with access control on reads, thus ensuring simple confidentiality properties adequate for MMM. More advanced confidentiality policies (such as allowing an applet to read local files or open network connections, but not both) are definitely beyond the scope of our framework, however.

8 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] Heintze | The SLam calculus: programming with secrecy and integrity[END_REF]. (Abadi et al. [START_REF] Abadi | A core calculus of dependency[END_REF] reformulate some of those type systems in terms of a more basic calculus of dependency.) 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 secrecy properties, following the information flow approach. In particular, they allow high-security data to be exposed as long as no low-security code uses this data. Our work focuses on more basic integrity properties via access control. We view those integrity guarantees as a prerequisite to establishing meaningful confidentiality properties.

Imperative vs. purely functional programs: [START_REF] Palsberg | Trust in the λ-calculus[END_REF] and [START_REF] Heintze | 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] Heintze | 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 simple and intuitive notion of 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] Heintze | 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: Web browsers 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[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][START_REF] Gong | Java security architecture (JDK1.2)[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 safe -probably[END_REF][START_REF] Syme | Proving JavaS type soundness[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][START_REF] Stata | A type system for Java bytecode subroutines[END_REF][START_REF] Freund | A type system for object initialization in the Java bytecode language[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 | Security and dynamic class loading in Java: A formalisation[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.

Our techniques put almost no constraints on the applets, except being welltyped 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] Heintze | 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 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, while still using a standard type system for the applets, 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][START_REF] Abadi | Secrecy by typing in security protocols[END_REF]. proceedings of the 25th ACM symposium on Principles of Programming Languages.

ϕ, 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 C m (v, s), if any source term operating on v in s can directly access only locations that are in L m or L shared , but not locations in L m . Formally, C m (v, s) is defined by case analysis on v, as follows:

-C m (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) -C m (e, s) if C m (e(x), s) for all x ∈ Dom(e).
Notice that for closures, it's the world n of the function body a n 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. Proof. The proof is by induction on the evaluation derivation and case analysis on a. Notice that by Lemma 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.

Assignment: a is (a σ ref 1 := a σ
2 ). We apply the induction hypothesis twice, obtaining

ϕ, e, s a 1 → v 1 /s 1 ϕ, e, s 1 a 2 → v 2 /s 2 C m (v 1 , s 2 ) C m (v 2 , s 2 ) C n (w, s) implies C n (w, s 2 ) for all n, w S 2 |= v 1 : σ ref S 2 |= v 2 : σ |= s 2 : S 2 .
Hence 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 Lemma 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 Lemma 6, we get C m (v, s ), which is the expected result.

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 e api is welltyped and its type E api does not contain any ref types. This is not to say that e api 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. From the technical side, requiring that no ref types occur in the applet's interface E api 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 following equations: ML(e(x), s)

ML(b, s) = ∅ ML((v 1 , v 2 ), s) = ML(v 1 , s) ∪ ML(v 2 ,
The case for closures follows conditions 1 and 4 in the informal discussion from section 3.2. For condition 5, we use the condition C app (v 1 , s 1 ) instead of the more natural / ∈ ML(v 1 , s 1 ), so that the equations remain increasing in ML and the existence of the smallest fixpoint is guaranteed. The typing hypothesis (that E api 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 ) = ∅.

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. Proof. The proof is by induction on the evaluation derivation. We rely on Lemmas 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).

Security property 5 Assume

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.

Application: a is a 1 (a 2 ). By induction hypothesis, we have ϕ, 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

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

  , s x → e(x)/s (1) ϕ, e, s b → b/s (2) ϕ, e, s λx.a → λx.a[e]/s (3) ϕ, e, s a1 → λx.a [e ]/s1 ϕ, e, s1 a2 → v2/s2 ϕ, e {x ← v2}, s2 a → r ϕ, e, s a1(a2) → r (4)

  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( ).

Lemma 2 (

 2 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 .

Fig. 5 .Fig. 6 .Fig. 7 .

 567 Fig. 5. Instrumentation of writes and procedural abstraction

Lemma 3 .

 3 Assume E (a τ ref := b τ ) : unit and S |= e : E and |= s : S. Define ϕ = 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.

  S |= e : E if Dom(e) = Dom(E) and for all x ∈ Dom(e), P V, S |= e(x) : E(x) -P V |= s : S if Dom(s) = Dom(S) and for all ∈ Dom(s), P V, S |= s( ) : S( ).

  Assume defined the functions open in cap : capability → string → in channel and open out cap : capability → string → out channel as capability-checking variants of the normal file opening functions open in : string → in channel and open out : string → out channel. Then, an applet can begin with the following definitions: let mycapa = Capabilities.get() let open_in = open_in_capa mycapa let open_out = open_out_capa mycapa . . . code using open_in and open_out as usual. . .

Lemma 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 ) = ∅.

  S |= e api : E api and |= s : S. Further assume that E api contains no ref types. If p ⊆ Dom(s) and p ∩ ML(e api , s) = ∅, then for all applets a, we have Prot(p), e api , s a → err. The property follows from the inductive lemma below. Lemma 9. 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 ) = ∅

  ) and C app (v 2 , s 2 ) and S 2 |= v 1 : σ → τ and S 2 |= v 2 : σ and p ∩ ML(e api , s 2 ) = ∅. Hence, v 1 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 e api , then possibly performing some function applications or fst and snd operations. Thus, we have ML(λx.a m [e ], s 2 ) ⊆ ML(e api , s 2 ), and the result follows by Lemma 8.

  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 any depth) in E api . This leads to the following security property: Security property 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.Proof. We consider all assignments to references that occur in the evaluation derivation for a. By Lemma 3, assignments performed by environment functions cannot cause a write error, since the right-hand side has been instrumented 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)). More precisely, we apply the results of 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 (Lemma 7) then shows that the location being assigned does not belong to L env . Moreover, by construction of P rot and L 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. The requirement that no t ref occurs in E api 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)

ref. -The environment contains a higher-order function such as E api (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. -The environment contains a function taking as argument an applet-provided reference to a t ref, e.g. E api (f ) = t ref ref → unit.

  Lemma 5. Assume either ∈ L m and C m (v, s), or ∈ L shared and C app (v, s) and C env (v, s). Then, for all values w and worlds n, C n (w, s) implies C n (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 non-trival case is w = (the modified location). By hypothesis C n (w, s), we have / ∈ L n and C n (s( ), s). Write s = s{ ← v}. Notice that s ( ) = v. If n = m, we have C n (v, s) by assumption, hence C n (v, s ) by the coinduction hypothesis, from which it follows that C n ( , s ). If n = m, since / ∈ L n , we have / ∈ L m 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 lemma. Thus, we have C n (v, s) and we conclude as in the previous case. Second, values that belong to a type τ / ∈ T can be exchanged between the app and env worlds without breaking containment. Lemma 6. Assume S |= v : τ and |= s : S. If τ / ∈ T , then C m (v, s) implies C m (v, s) for all worlds m. Proof. 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). can now show that containment is preserved at each evaluation step: Lemma 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 m : τ and S |= e : E and |= s : S and C m (e, s). 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

	ProofWe

n (w, s ).

  , 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 C m (v 2 , s 2 ) implies C m (v 2 , s 2 ) as well by Lemma 6. In both cases, the hypotheses of Lemma 5 are met. Writing s = s 2 { ← v 2 }, we obtain the expected result: C n (w, s) implies C n (w, s ) for all n, w. The other expected result, C m ((), s ), is trivial.Application: a is a σ→τ 1 (a σ 2 ). By applying the induction hypothesis twice, we obtainϕ, e, s a 1 → v 1 /s 1 ϕ, e, s 1 a 2 → v 2 /s 2 C m (v 1 , s 2 ) C m (v 2 , s 2 ) 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, v 1 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 .

  s) ML(λx.a[e], s) = { | there exists v 1 , s 1 , v 2 , s 2 such that C app (v 1 , s 1 ) and s 1 ( ) = s( ) for all ∈ L env , and either { ← ∅}, e{x ← v 1 }, s 1 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)

Acknowledgements

This work has been partially supported by GIE Dyade under the "Verified Internet Protocols" project. A preliminary version of this paper appeared in the

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 (a env ) or from the applet (a app ). 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:

-L app is the set of locations with type τ ref ∈ T that have been allocated by the applet; -L env 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: