Information-flow security for JavaScript and its APIs

3.1.1. Dynamic code evaluation: Eval

The runtime possibility to parse and execute a string in a JavaScript program, provided by the eval instruction, poses a critical challenge for static program analysis, since the string may not be available to a static analysis.

Our approach: Dynamic analysis does not share this limitation, by virtue of the fact that dynamic analysis executes at runtime.

3.1.2. Aliasing and flow sensitivity

The type system of JavaScript is flow sensitive: the types of, e.g., variables and properties are allowed to vary during the execution. In addition, objects in JavaScript are heap allocated and represented by primitive references – their heap location. Hence, objects in JavaScript may be aliased. An alias occurs when two syntactically different program locations (e.g., two variables x and y) refer to the same object (contain the same primitive reference).

Flow sensitivity in the presence of aliases poses a significant challenge for static analysis, since changing the labels of one of the locations requires that the security labels of all aliased locations are changed as well, which requires the static analysis to keep track of the aliasing.

Our approach: Dynamic approaches do not share this limitation, since they are able to store the security label in the referred object instead of associating it with the syntactic program location. Consider the following program:

First, a new object is allocated, and the primitive reference to the object is stored into x. Thereafter, the property f of the newly allocated object is set to 0, and y is made an alias of x. Finally, the property f is overwritten by a secret via y. This kind of programs are rejected by static analysis like Jif [53]. In the dynamic setting, we simply update the security label of the value of the property f of the allocated object.

3.1.3. Dynamic objects: Structure and existence

JavaScript objects are dynamic in the sense that properties can be added to or removed at runtime. This implies that not only the values of property can be used to encode information, but also their presence or absence. Consider the following example:

After execution of the conditional the answer to the question whether q is in the domain of o gives away the value of h. It is important to note that both the presence and the absence of q gives away information – copying the value of h into l via the presence/absence of q can easily be done by executing, e.g., l = (o.q != undefined); (projecting non-existing properties returns undefined).

Our approach: We solve this by associating an existence security label with every property and a structure security label with every object. The demand is that changing the structure of the object by adding or removing properties under secret control is possible only if the structure security label of the object is secret. Once the structure of an object is secret, knowing the absence of properties in the object is also secret.

3.1.4. Exceptions

Exceptions offer further intricacies, since they allow for non-local control transfer. Any instructions following an instruction that may throw an exception based on a secret must be seen as being under secret control, since, similar to the conditional, the instruction may or may not be run based on whether the exception is thrown or not. Consider the following example:

Whether h is 0 or not controls whether the second update is run or not and, hence, l encodes information about h.

Our approach: We introduce a security label for exceptions, the exception security label. The exception security label is an upper bound on the label of the security context in which exceptions are allowed. If the exception security label is public, exceptions under secret control are prohibited. The exception security label and the pc together form the security context that governs side effects. That is, if the exception security label is secret, the security context is secret, and side effects are constrained.

3.1.5. Higher-order functions

Being first class values, functions carry a security type that must be taken into consideration when calling the function. Consider the following example, where a secret function f is created by choosing between two functions under secret control.

Depending on the secret h, a function that writes 1 or a function that writes 0 to l is chosen. Calling the selected function copies the value of h into l.

Our approach: The body of the function must be run in a security context that is at least as secret as the security label of the function. This discipline is inspired by static handling of higher-order functions [55].

3.1.6. Variables and scoping

JavaScript is known for its non-standard scoping rules. Variable hoisting in combination with non-syntactic scoping, the with and eval constructions, and the fact that assigning to undeclared variables causes the variable to be defined globally, cause complex and sometimes unexpected behavior. To appreciate this, consider, e.g, conditional shadowing using eval.

In order to understand this example, we must know more about functions and scoping in JavaScript. First, the variable environments form a chain. Variable lookup starts in the topmost environment and continues down the chain until the variable has been found or the end of the chain has been reached.

Second, both if and eval are unscoped, i.e., the variable declared by the eval is declared in the topmost variable environment of the function call. The use of eval is to prevent variable hoisting until the execution of the conditional branch. Otherwise, l would be hoisted out of the conditional and always be declared regardless of the value of h.

Execution of f is split into two cases. If h is true, the variable is defined locally in the function, and the update of l is captured by the local l. If h is false, l is created in the global variable environment.

A similar situation can be created using with that takes an object and injects it into the variable chain allowing the properties of the injected object to shadow variables declared higher up in the chain. Consider the following example:

When the update l = 0; is executed, the variable lookup will first look in the topmost environment record, i.e., the injected o object. If the object defines a property with the name l, the variable lookup terminates returning a reference to the object. Otherwise, the lookup continues in the remaining variable environment chain. In the above example, in case h is true the update is captured by o. If h is false, l is created in the global variable environment.

The result is that both the value of l in the global variable environment and potentially its existence encode information about h. The latter implies that, similar to objects, we must track the structure of variable environments. In addition, the presence or absence of the l in the local variable environment (or elsewhere in the chain) effects where the update takes place.

Our approach: We show that the intricate variable behavior of JavaScript can be handled by a faithful modeling of the execution context in terms of basic objects and object operations.

3.1.7. Prototype hierarchy

In a similar way, the prototype chain, forming the basis for prototype based inheritance, can cause intricate behavior. In JavaScript, functions are used to create new objects. The body of the function acts as a constructor for the newly created object, and the contents of the prototype property is copied into the prototype chain of the object. The prototype chain is then traversed when looking up a property in the object. This is done in a similar manner to the variable chain. Consider the following example:

Executing x[’l’] would return 0 even though x does not define the property l itself. Instead, it is the property l of the prototype that is returned. Consider the following addition to the above example:

We create a new function g and let the prototype field of g be x, i.e., the object created by f, and we let x be an object created by g. Executing x[’l’] would result in 0 even though neither x nor the immediate prototype of x defines l. The prototype of the prototype of x does, however, and its property l is found and its value, 0, is returned. In this way, x inherits the properties of all prototypes in the prototype chain. Now, consider the following addition to the example:

Since the prototype chain is traversed for each property lookup, modifications of the prototypes in the prototype chain may cause effects on the property lookup. In case h is true, the property l is added to the immediate prototype of x. This shadows the previous property l, and executing x[’l’] now returns 1 instead of 0.

Our approach: We show that the intricacies of prototype inheritance can be handled by a faithful modeling in terms of basic objects and object operations.

3.2.1. Return labels

The core language makes the simplifying assumption that there is a unique return statement at the end of each function. When this assumption is not met in actual code, there are similar challenges to the ones created by exceptions. Consider the following program:

The program copies the secret boolean h into l by returning from the function under secret control. If h is true, the assignment l = false is not executed, and l remains true. If h is false the assignment is performed, and l becomes false. Thus, the return statement has the effect of extending the secret context to the end of the function.

Our solution: we introduce a return label that governs return statements. This label is similar to the exception label in that it defines an upper bound on the control contexts in which return can be executed. The return label is also part of the security context. Hence, a secret return label causes the security context to be secret which constrains side effects.

3.2.2. Labeled statements

JavaScript contains labeled statements and allows jumping to them using break and continue. As with conditional statements, such transfer of control may result in implicit flows. Consider the following example:

If h is true, the continue statement causes do-while to proceed to evaluating the guarding expression, which, in this case, causes the termination of the loop. This prevents the execution of the assignment l = false, and l remains true. If h is false, the assignment is performed, resulting in l becoming false.

Our solution: we associate each statement label with a security label. This label is similar to the exception label and return label in that it defines an upper bound on the control contexts in which jumping to the associated statement is allowed. The security label of labeled statement is also a part of the control context for the labeled statement itself, which constrains side effects.

3.2.3. Accessor properties

In addition to standard value properties, JavaScript supports accessor properties. Accessor properties allow overriding property reads and writes with user functions. When reading, the return value of the getter function of the property is returned, and, similarly, writing to a property invokes the setter function associated with the property. Section 7 shows how getters and setters can be used in complicated interplay with libraries, opening the door for non-obvious information flows.

Our solution: handling accessor properties is akin to handling first-class functions. Instead of storing the actual value in the property, the accessor functions are stored.

3.2.4. Implicit coercions

Many expressions, statements, and API functions of JavaScript convert their arguments to primitive types. JavaScript objects may override this conversion process with user functions. Consider the following example:

The addition operation tries to convert its arguments to primitive values. For an object, the conversion first invokes its valueOf method, if present. If this returns a primitive value, it is used. If not, the toString method is invoked instead. In the example, valueOf is chosen so that toString is invoked only when h is true, which must therefore be reflected in the control context of toString.

Our solution: the information flow introduced by implicit coercions originate from interpreter-internal information flow, i.e., when the interpreter itself inspects labeled values and choses whether or not to invoke the coercion function. Interpreter-internal flows are not limited to the implementation of implicit coercions. They are handled uniformly by generalizing the notion of the pc, see Section 6.

Let H (secret) and L (public) be security labels, ranged over by σ. The security labels are used to label the values with security information. For clarity in the semantic rules, let pc and ϵ range over security labels denoting the program counter label and the exception security label, respectively.

Values are defined in Fig. 2. Primitive values, ranged over by v, are primitive references, strings, numbers, booleans, and the undefined value. Similarly to security labels, r ranges over primitive references in general, while le , ve , and τ range over primitive references denoting lexical environments, variable environments, and the this binding, defined below.

In the semantics, all primitive values occur together with a security label representing the security classification of the value. Let v σ be security labeled primitive values written v ˙ when the actual security label is unimportant. Let v ˙ σ 2 = v σ 1 σ 2 = v σ 1 ⊔ σ 2 .

Let the property names be strings ranged over by s. References, ( r ˙ , s ˙ ) , are pairs of security labeled primitive references and strings, denoting the property named s in the object referred to by r. We let v ˙ range over both security-labeled values and references. Note that the references are not themselves labeled.

In addition to the primitive values, the notion of primitive object, ranged over by o, forms the foundation of the semantics. Let p range over property values. A primitive object is a collection of properties, where each property is an association between a property name and a property value. Each property is decorated with an existence security label and objects carry a structure security label. When seen as maps, the domain of an object consists of a set of strings instead of a set of security labeled strings. This reflects that existence security labels carry information about the existence of the property and not of the property name. The properties are either internal or external indicated by the IsExternal predicate on property names, which is false for strings of the form _ s _ and true otherwise. Internal properties are used in the implementation of the semantics but are not exposed to the programmer – see the semantics of for-in (Iter-2 and Iter-3) in Fig. 7. The values of external properties are security-labeled primitive values, while internal properties may hold algorithms represented by general functions, F , statements, c, and lists of formal parameters, x ‾ .

Heaps, ranged over by ϕ, are mappings from primitive references to primitive objects. Pairs of heaps and exception security labels form the execution environments, ranged over by E. Let E [ r ] = ϕ [ r ] for E = ( ϕ , ϵ ) . In addition, execution takes place with respect to an execution context C , built up by the this binding, τ, a primitive reference, le , to the topmost lexical environment, and a primitive reference, ve , to the topmost variable environment. The lexical environment and the variable environment are built up as chains of environment records, see Section 4.2.3. In each function call, the lexical environment and the variable environment point to the same environment record, see FunctionCall in Section 4.2.7. The difference between the two is that the lexical environment is used to introduce local scope for binding of temporary variables, see rule Try-2 in Section 4.2.10, while the variable environment always points to the initial record. Somewhat contrary to what is indicated by the names, the lexical environment is used for variable lookup, see rule VAR in Section 4.2.9, while the variable environment is used for variable hoisting in eval, see rule Eval in Section 4.2.10. This has the effect that variables introduced by eval are hoisted to the toplevel in each function call.

4.2.2. Semantics of ECMA objects

The ECMA objects provide the foundation of the objects of the JavaScript execution environment. They are built on top of the primitive objects and provide a number of internal algorithm properties that provide a common interface for interacting with the object. In particular, the ECMA objects provide support for prototype inheritance exemplified in Section 3.1.7. The prototype hierarchy is built when a function is used to construct a new object, see FunctionConstruct in Section 4.2.7. In the process, the contents of the prototype property of the function object is copied to the internal _ Prototype _ property of the constructed object. This hierarchy is then traversed by the internal ECMA object algorithm GetProperty when looking for a given property.

Most of the standard is described in terms of this interface. Few algorithms manipulate primitive objects directly. This common core provides an ideal location for handling information-flow security. By showing that the core is secure, we can easily establish (by using compositionality of our security notion) that more complex functionality formulated in terms of the core is secure as well.

We define ECMA objects to be primitive objects extended with a relevant selection of the core functionality. In particular, an ECMA object O is defined by O = { _ GetOwnProperty _ ↦ GetOwnProperty , _ GetProperty _ ↦ GetProperty , _ HasProperty _ ↦ HasProperty , _ Delete _ ↦ Delete , _ Get _ ↦ Get , _ Put _ ↦ Put } The definitions of GetOwnProperty , GetProperty , HasProperty , Delete , Get , and Put are found in Fig. 3. Let d range over property descriptors or undefined, d : : = { value ↦ v } ∣ undefined , and let d σ be defined structurally as { value ↦ v σ } or undefined σ . Property descriptors are used in GetOwnProperty to distinguish between a defined property with value undefined and an undefined property.

OPEN IN VIEWER

Fig. 3.

ECMA objects.

In the case of update (PUT-1 and PUT-2), the structure of the object is not changed, and, hence, there is no demand on the structure security label of the object. With respect to the original value of the property, it is demanded that it is at least as secret as the write context. The label of the new value is raised to the write context. This entails that updating a property might lower the security label. Similarly, in case the existence security label is more secret than the write context (PUT-1), it can be lowered to the write context. In the case the existence security label is not more secret than the context, execution is allowed to continue without modifying the existence label (PUT-2). The intuition is that the existence of the field is not changed. It was there before the execution of the Put, and it remains after.

ECMA object allocation. Let NewEcma allocate a new ECMA object and return the primitive reference to the newly allocated object.

In this rule and in the following, let o [ σ ] denote an update of the structure security label. Further, we use the standard dot notation for method application, defined as follows. For pure functions, r σ . X ( a ‾ ) E = ( E [ r ] [ X ] ( r σ · a ‾ ) E ) σ , where a ‾ (the arguments) denotes a list of security labeled values,  v ˙ . Similarly, for functions with side-effects, pc ⊢ r σ . X ( a ‾ ) E = pc ⊔ σ ⊢ E [ r ] [ X ] ( r σ · a ‾ ) E .

The variable environment is a chain of environment records, chained together by chaining objects, C ( r 1 , r ˙ 2 ) = { _ EnvironmentRecord _ ↦ r 1 , _ OuterEnvironment _ ↦ r ˙ 2 } , where EnvironmentRecord points to the environment record, and OuterEnvironment points to the next chaining object in the chain. The environment records store the variable bindings and come in two forms: object environment records and declarative environment records differing in whether a separate object, the binding object, is used to store the variable bindings or if the bindings are stored in the environment record itself. Object environment records are used to inject objects into the variable environment chain: the global object, see Section 4.2.5, and objects originating from with statements.

We simplify object environment records and declarative environment records to support the same subset of operations: HasBinding, GetBindingValue, SetMutableBinding, DeleteBinding, and ImplicitThisValue. Of these operations, ImplicitThisValue deserves commenting. It is used in the semantics of function call, rule Call in Section 4.2.9, to compute the this value. For object environment records, ImplicitThisValue returns the binding object, which ensures that methods defined on the binding object gets the binding object as the this value.

Object environment records. Let OE be a family of object environment records indexed over the binding object, r ˙ . OE ( r ˙ ) = O [ _ BindingRecord _ ↦ r ˙ , _ HasBinding _ ↦ HasBinding , _ GetBindingValue _ ↦ GetBindingValue , _ SetMutableBinding _ ↦ SetMutableBinding , _ DeleteBinding _ ↦ DeleteBinding , _ ImplicitThisValue _ ↦ ImplicitThisValue ]

The algorithms for object environment records are all defined by deferring the operations to the operations of the binding object.

Thus, for object environment records, variables are stored as properties on the binding object.

The NewObjectEnvironment algorithm allocates a new declarative environment and links it onto the given environment record chain.

Declarative environment records. Let DE denote the declarative environment record, defined as follows. DE = O [ _ HasBinding _ ↦ HasProperty , _ GetBindingValue _ ↦ Get , _ SetMutableBinding _ ↦ Put , _ DeleteBinding _ ↦ Delete , _ ImplicitThisValue _ ↦ ImplicitThisValue ] HasProperty, Get, Put, and Delete are the ECMA object operations, defined in Fig. 3, and ImplicitThisValue ( r 1 σ , s ˙ ) ϕ = undefined σ .

OPEN IN VIEWER

Fig. 4.

Variable lookup.

As before, the NewDeclarativeEnvironment algorithm allocates a new declarative environment and links it onto the given environment record chain.

Variable lookup is performed by GetIdentifierReference defined in Fig. 4. GetIdentifierReference takes a primitive reference to the topmost variable environment and a variable name and traverses the chain of environment records (GIR-3) until the variable is found (GIR-2) or the chain ends (GIR-1). The returned result is a reference that, as mentioned in Section 4.2.1, consists of a pair formed by a security labeled primitive reference and a string. Variable lookup returns a reference ( r ˙ , x L ) , where x is the name of the variable, which is always public, and r is a primitive reference to the environment record containing the variable, or undefined , if the variable is not found. During the traversal, the security label of the access path is computed by accumulating the security labels of the traversed references in the label of the returned reference.

4.2.5. Initial environment and built-in objects

In addition to expressions and statements, the standard execution environment contains a number of built-in objects reachable from the global object, G , defined below. As in JavaScript, the global object ends the variable environment chain via an object environment record. This means that any properties defined on the global object are available to the program as identifiers, see Section 4.2.3. In addition, the global object acts as the store for global variables, see PutValue in Section 4.2.8.

In the following, public existence security labels and value security labels of internal properties are frequently omitted in the case the property cannot be updated. We define a minimal initial heap containing the global object, the object constructor, Object , see Section 4.2.6, the object environment record for the global object, and the corresponding chaining object, the global variable environment. ϕ init = { r G ↦ G , r O ↦ Object , r E ↦ OE ( r G L ) , r V ↦ C ( r E , 0 L ) }

The initial context C init = ( r G L , r V L , r V L ) uses the global object as the initial this value and sets the initial lexical environment, as well as the initial variable environment to the global variable environment. The initial environment E init = ( ϕ init , L ) together with the initial context form the initial execution environment.

Global object. In JavaScript, the global object defines a number of properties that enriches the execution environment with constants, functions, and constructors. For brevity, we include only the object constructor, Object , as a constructor property of the global object, refraining from including the other constructors and prototypes. G = O [ _ Prototype _ ↦ null , Object ↦ r O ]

4.2.6. Object objects

The object constructor Object = O [ _ Prototype _ ↦ null , prototype ↦ null , _ Construct _ ↦ ObjectConstruct ] is a function object that provides functionality for object creation, via the internal _ Construct _ property. Function objects are defined in Section 4.2.7. The ObjectConstruct algorithm allocates a new object, initializes the _ Prototype _ property to null , and returns the new primitive reference.

4.2.7. Function objects

Function objects are objects containing two internal properties, _ Call _ , used by function call and _ Construct _ , used in object construction. There are both internal function objects, e.g., the object constructor, Object , defined in Section 4.2.6, and user defined function objects originating from function expressions, see Section 4.2.9.

User defined function objects. The function objects created when evaluating function expressions are closures storing the context (lexical environment) the function it was created in, the formal parameters of the function, and the code of the function, used by associated _ Call _ , and _ Construct _ . Let F denote the family of function objects defined in the following way, where x ‾ is the list of formal parameters, c is the code of the body of the function, and r ˙ is the lexical environment the function was created in. F ( x ‾ , c , r ˙ ) = O [ _ Scope _ ↦ r ˙ , _ FormalParameters _ ↦ x ‾ , _ Code _ ↦ c , _ Call _ ↦ FunctionCall , _ Construct _ ↦ FunctionConstruct ]

Call. Calling a user defined function first allocates a new declarative environment, see Section 4.2.3, in which the arguments are bound by a process called declaration binding, defined below. Thereafter the body of the function is executed in the updated context, see the semantics of statements in Section 4.2.10. Note that the creation of the declarative environment, the declaration binding, and the body are run in a security context raised to the security label, σ, of the primitive reference, r F , of the function, as is the returned value, see Section 3.1.5.

where this ( undefined σ ) = r G σ and this ( r ˙ ) = r ˙ , otherwise.

Declaration binding. Declaration binding first binds the arguments of the function call and then performs variable hoisting.

The parameters are bound by ignoring any surplus parameters, and setting missing parameters to undefined .

Variable hoisting is performed by HoistVariables , defined in Fig. 5. Hoisting is performed by traversing the body of the function and defining all encountered variables, initializing them to undefined .

OPEN IN VIEWER

Fig. 5.

Variable hoisting.

Construct. Object construction via user defined functions uses the function as an initializer on a newly allocated ECMA object. Before passing the object, the _ Prototype _ property is set to the value of the prototype property of the constructor function, after which the object is initialized by calling the constructor function using the primitive reference to the object as the this argument. In JavaScript, the constructor has the option of returning a reference to an object that will be used as the instance in place of the allocated object. For simplicity, instead of having one rule for the case when the constructor function returns an object and one for when it does not, we assume that all constructor functions return an object reference. This assumption amounts to adding return this; at the end of all constructor functions not returning an object reference.

In the following, let NewFun allocate and set up a new function object from the given list of formal parameters, function body and scope.

There are two auxiliary reference functions used to interact with the target of the reference. First, GetValue fetches the value associated with a reference. Non-reference values are returned untouched. Subject to the limitations discussed in Section 3.1.4, an exception is raised, if the reference is undefined. Note that not only the pc but also the security level of the primitive reference is included in the check against the exception security level.

PutValue takes a reference and a value and updates the location denoted by the reference with the value. In case the reference is undefined, the update is done on the global object. This is what causes writes to undefined variables to result in a global variable being defined. Subject to the limitations discussed in Section 3.1.4, an exception is raised, if the first argument is not a reference. As for GetValue, the security level of the primitive reference is included in the check against the exception security level.

OPEN IN VIEWER

Fig. 6.

Semantics of expressions.

Let u ˙ denote exception lifted values, i.e., u ˙ : : = v ˙ ∣ exc v ˙ . The semantics of expressions is of the form pc , C ⊢ ⟨ e , E 1 ⟩ → ⟨ u ˙ , E 2 ⟩ , read as e executes to ⟨ u ˙ , E 2 ⟩ when run in E 1 , the program counter security label pc , and the context C .

The semantic rules for expressions are found in Fig. 6, where most exception propagation rules have been omitted for clarity. Adding the exception propagation rules is a mechanical process where exception propagation rules should be added for each exception source. As an illustration, consider the rules for expression sequences. The two productive rules (ESeq-1 and ESeq-5) provide the core semantics for the evaluation of expression sequences and the other three rules (ESeq-2, ESeq-3, and ESeq-4) provide exception propagation, corresponding to the following cases, respectively: (1) the first expression, e, results in an exception, (2) the call to GetValue results in an exception, and (3) one of the expressions in the tail of the sequence, e ‾ , results in an exception, respectively. All of these cases terminate the evaluation by propagating the exception.

The expression rules are formulated in terms of the primitives of the previous sections. The string s, numbers, n, booleans, b, and undefined literals evaluate to their semantic counterpart. They are labeled L, whereas the label literals are labeled with themselves (Lit). This allows the label literals to be used as label constants in the upgrade instructions, see Section 4.2.11.

The null literal evaluates to the null primitive reference 0 (Null), and the this literal evaluates to the current this primitive reference τ ˙ (This).

Expression sequences (ESeq-1 and ESeq-5) are used by function call, object construction, projection, assignment, and binary operators. They are evaluated in order, resulting in a sequence of values.

Identifier dereference (Var) uses GetIdentifierReference . All rules that contain evaluation of subexpressions use GetValue to convert the results to values apart from assignment (Asn) that uses PutValue to update the location denoted by the reference.

Delete uses Delete (EDel-1) or DeleteBinding (EDel-3) depending on if the target is an object or an environment record (indicated by IsPropertyReference ). Attempting to delete an undefined variable does not have any effect (EDel-2).

Function creation (Func) uses NewDeclarativeEnvironment to allocate the local variable environment, NewFun to create the new function object and SetMutableBinding to initialize the new environment by binding the function name to the newly created function object in order to allow for recursive calls. Function call (Call) uses Call . Object creation (New) uses Construct .

Note the this ( v ˙ ) E 3 of the function call, which computes the this binding of the invocation, from the reference v ˙ = ( r , s ) σ . It is computed as follows: (1) if the base of the reference, r, is undefined, or if it is a property reference then the base of the reference is returned, otherwise, (2) the base is an environment record, and the result of calling _ ImplicitThisValue _ is returned.

Finally, notice how typeof (Type-3) returns undefined for undefined variables, whereas using an undefined variable in, e.g., a binary operator would cause an exception when trying to apply GetValue on the reference. Thus, typeof can be used to detect whether variables are defined or not.

From an information-flow perspective, only the rules for typeof and binary operators contain primitive information flow (corresponding to the standard treatment of unary and binary operators). The information flow of the rest of the rules is in terms of primitive constructions.

OPEN IN VIEWER

Fig. 7.

Semantics of statements.

Let R : : = E ∣ ⟨ u ˙ , E ⟩ , where E indicates normal termination without return value, and ⟨ u ˙ , E ⟩ indicates either exceptional termination or termination with a return value, depending on whether u ˙ is exc v ˙ or v ˙ . The semantics of statements is of the form pc , C ⊢ ⟨ c , E ⟩ → R , read as c executes to R when run in E, program counter security label pc , and context C .

Figure 7 displays the semantic rules of statements, where the rules for exception propagation have been omitted for clarity. Sequence (Seq-1), iteration in the form of while (While), and conditional choice (If-1 and If-2) are all standard. The conditional choice raises the security context of the chosen branch to the security label of the controlling expression, and while is formulated in terms of conditional choice. The for-in statement (For-In) iterates over the external properties of an object. For each external property name in the object, the given variable is updated with the name using the existence security label of the property as the security label, and the body of the for-in is run. The iteration of for-in is provided by the three rules (Iter-1, Iter-2, and Iter-3) of the form pc , C ⊢ ⟨ ( s ‾ , v ˙ , c ) , E 1 ⟩ → E 2 , that for each s ˙ in s ‾ binds the variable referenced by v ˙ to s ˙ before running c. Note that c is run in the context of the label of the corresponding string (Iter-2), and that internal properties are skipped (Iter-3). The former might seem counterintuitive. In the light of the operation of an ordinary for loop, one might expect an accumulated security content. However, this is not necessary. The reason for this is that there is no way for executions of the body corresponding to properties with secret existence labels (the secret executions) to communicate anything public to later executions corresponding to properties with public existence labels (the public executions), since the secret executions are under secret control. From the perspective of the public executions, it is not possible to detect if or how they are interleaved with secret executions without raising their own security context. Consider the following program, where the property q with public existence may or may not be preceded by the property p with secret existence. The program tries to communicate this fact by accumulating into ihow many times the body of the for-in is executed and storing into l if property q was first or not.

First, the structure of o must be upgraded to allow for the addition of property p under secret control. Consider the two possible execution of the above program. If h is false, property p will not be added to o, and the first execution of the body (corresponding to the property q) will update l to false. If, on the other hand, h is true, property p will be added to o. Since the existence security label of p is secret, the first execution (corresponding to the property p) will be under secret control, and the execution will be stopped when trying to update i on line 6, which is public. In the above terms, the secret execution was prevented to communicate a public value.

Now, consider what happens if we modify the example so that i is secret. If h is false, property p will not be added to o, but now, when the first execution (corresponding to the property q) tries to update l the execution will fail with a security error. The reason for this is, by making i secret we have made the inner conditional on line 5 secret, which prevents any public updates. If, on the other hand, h is true, property p will be added to o and l will remain false. In the above terms, any differences detected by later public executions must be secret and will cause the public execution to enter a secret context.

Exception throwing (Throw) is constrained by the demand that the security context pc is below the exception security label ϵ, i.e., no low exceptions are allowed in secret context.

The execution of try-catch is divided into normal (Try-1) and exceptional (Try-2) execution of the body. In the first case, the result of the execution is returned in the outer exception context, i.e., the exception security label of the try-catch. This allows for containing exception security label upgrades to the try-catch. In the second case, if an exception is thrown in the body of the try-catch, control is passed to the exception handler. The body of the handler is run in a new lexical environment, in which the formal parameter of the handler is bound to the exception value. This means that variables declared in the body of the handler are not local to the handler, but escape to the outer variable environment, similar to variables declared in the bodies of eval and with described below. With respect to information flow, the body of the handler is run in a security context which is the least upper bound of the initial security context and the exception security label at the program point where the exception was thrown. This guarantees that the body of the handler is unable to leak information about the existence of secret exceptions. Further, the body of the handler is run in the outer exception security label, since any (uncaught) exceptions in the handler escape the try-catch.

The return statement (Ret) takes an expression and makes the corresponding value the return value of the function. Note the simplifying assumption that all functions have a unique exit point in terms of a return statement. This is manifested in that the function call expression (Call) demands that a value is returned, while the statement sequence (Seq-1 together with the rules for exception propagation) does not propagate return. In order to support unconstrained use of return a return security label can be introduced, serving a similar purpose as the exception security label. Since the labels are closely related, we have opted to let the exception security label be representative in the formal development. Naturally, in the full implementation this restriction and other restrictions of the formal development have been lifted.

The eval statement (Eval) evaluates its argument, parses the result to a program, which is run after hoisting the variables into variable environment. Hence, variables introduced by eval are defined in the context of the closest enclosing function, or into the global object. The program is run in a security context that is raised to the security label of the parsed string.

Finally, the with statement (With) injects an object into the lexical environment chain. Properties of the injected object shadows existing variables for both reading and writing.

OPEN IN VIEWER

Fig. 8.

Upgrade semantics.

Figure 8 defines one upgrade expression and four upgrade statements. All of the upgrade instructions are dynamic, in the sense that the target label is taken from the reduction of the second argument. This allows upgrading of potential write targets to match the control structure of the program without enforcing specific labels. For example, in the following snippet, l is upgraded to the label of h:

The upgrade expression (Upg) upgrades the result of the first parameter to the label of the second. Upgrading to specific labels is made possible by the introduction of label literals that carry their own label, see Section 4.2.9.

The upgrade exception label statement (UpgExc) upgrades the exception label to the label of the parameter, provided the upgrade can be allowed by the security context. The upgrade structure label statement (UpgS) upgrades the structure of the object referred to by the first parameter to the label of the second, provided that the write context of the object allows the upgrade. Similarly, the upgrade structure label of environment records statement (UpgV) upgrades the structure of the environment record of the given variable x to the label of the second parameter, provided that the write context of the environment record allows the upgrade. Finally, the upgrade existence label statement (UpgE) upgrades the existence label of the property referred to by the first parameter to the security label of the second parameter, provided that the write context of the property allows it. In all upgrade statements, the write context is taken into the account when creating the resulting label.

In designing an information-flow model for a library, its precision must be balanced with its complexity and usability. Increased precision allows more permissive enforcement but typically adds to the complexity of using the library. For example, the user may need to supply security annotations, or otherwise be aware of the model itself. This results in a system that is harder to use and understand. On the other hand, being too imprecise risks having the enforcement reject too many secure programs, thus losing permissiveness. This also places a burden on the programmer, as she will have to work around the false positives.

A library model contains two parts: (1) a information-flow model of any internal state of the library, and (2) information-flow models for all functions of the library. Based on the discussion above, we distinguish between function models, depending on the extent the standard functionality can be deferred to the corresponding functionality in the underlying library. In particular, we categorize information-flow models for library functions into two different types: shallow models and deep models. Shallow models describe the operations on labels and label state in terms of the boundary values and types of the parameters to the library function, whereas deep models may compute internal, intermediate values such as private attributes of objects or local variables inside library code. The model may perform or replicate a part of the computation done by the library, in order to obtain a more precise model.

The remainder of this section discusses key insights gained from modeling the built-in JavaScript API, as well as browser APIs, and gives examples where deep models are necessary to yield useful precision.

7.2. JavaScript standard API

In addition to the core language, JSFlow implements the API mandated by the standard. The information-flow models of the standard API range from simple shallow models to more advanced deep models. Below, String and Array illustrate shallow and deep models, respectively.

String object. The String object acts as a wrapper around a primitive string providing a number of useful operations, including accessing a character by index. We model the internal label state of String objects with a single label matching the security model of its primitive string.

Several of the methods of String objects are shallow models: after converting the parameters, they are passed to the corresponding native method. For instance, consider toLowerCase that converts a string to lowercase. While we could iterate through the entire string converting character by character, we may as well call the corresponding function.

This function model is an example of a shallow model. It first performs all necessary conversions, calls the underlying toLowerCase and returns the result labeled. Note that the model cannot defer the conversion to the underlying model, since the conversion may trigger potentially side-effectful callbacks that must be invoked in the right security context.

As another example of an essentially shallow model, consider the slice method. The slice methods takes two indices and returns the slice of the string between them. We highlight the implementation of slice by means of examples.

First, consider the following program, which passes an object to slice whose valueOf method will return a secret.

This example tries to exploit the conversion to numbers that slice performs on its arguments, which invokes valueOf when they are objects. In order to model this flow properly, the security label of the value returned by valueOf must be taken into account in the result of slice. In the example above, slice would return a secret value.

In addition, it is important that the security context of the calls made by slice include the labels of the indices. Otherwise, side effects in valueOf may leak. In the following example, assume that ix is secret, and that it is chosen to be either an object or a number depending on h.

In the implementation of slice below, lines 7 to 19 perform the mandated conversions. Note how the conversion of end on line 17 is performed in the context of end.label, since the value of end controls whether the conversion is performed or not. Omitting this opens up the coercion for exploits. Once all conversions have been completed, the actual functionality is deferred to the underlying library on line 21, and the result is returned appropriately labeled.

Let us return to side effects in the conversion of the indexes performed on line 11 and conditionally on line 17. Here, the security context of the call to valueOf when converting ix must reflect the label of ix. We ensure this in the internal functions ToString and ToNumber (called by ToInteger), used by slice. For example, the actual security context increase occurs in ToNumber on line 6, where the argument label is pushed onto the pc stack:

This ensures that valueOf in the example above will be called in the right security context.

Array. Array objects are list-like objects that map numerical indices to values. Arrays have a special link between the length property and the mapped values: writing an element past the length of the array will increase the length property accordingly, and decreasing the length property will remove elements from the end of the array. We model the internal state of the array as an ordinary object, while catering for the connection between the length property and the indices. Arrays are mutable and equipped with methods for performing different operations on the elements of the array in different orders. This allows for complicated interplays with accessor properties, which calls for the use of deep models. Consider, for instance, the following example:

The every method of arrays invokes a function on each element, until either the list is exhausted or it returns a value convertible to false. Since all values are convertible to one of true or false, knowing that an element with index greater than 0 is read reveals that the function returned a true-convertible value for all lower indices. By populating an array with a secret followed by a getter, the true value of the secret could be observed. In the example, the first element contains the secret boolean h and the second element is a getter that sets l to true. Since the getter is only invoked in case h is true, this effectively copies h to l. For this reason, a shallow model cannot be used. Each successive call of the iterator function must be called in the accumulated context of the previous results, which is not possible, if we simply delegate the computation to the primitive every method. Instead, we must use a deep model, illustrated below with an excerpt of the inner loop of every.

Notice how line 12 converts the result of the function to a boolean, how line 13 uses the label of the result to accumulatively increase the top of the pc stack, and how line 14 accumulates the label used for the returned value at line 18. Since ToBoolean may have side effects, the accumulation is important. It cannot be implemented if the functionality is deferred to the corresponding underlying function.

7.3. Browser APIs

The execution environment provided by browsers is an extension of the built-in JavaScript environment. To a certain extent, what is provided is browser specific, while some parts are standardized by the World Wide Web Consortium (W3C). Although many of the extensions are fairly straightforward to model from an information-flow perspective, offering similar challenges as the standard library, a notable exception is the implementation of the Document Object Model (DOM) API [38]. The DOM is a standard describing how to represent and interact with HTML documents as objects. The DOM is a central data structure to all web applications. A large part of a web application typically deals with shuttling data to and from the DOM and responding to events generated by the DOM, as the user interacts with it. Tracking information flows to and from the DOM is thus vital to having information-flow tracking that is useful for real web applications.

Sources and sinks in the DOM. Being an object model of the HTML document that makes up the graphical interface of the web application, the DOM naturally contains many sources of potential sensitive information. In particular, essentially all forms of user provided input will be represented in the HTML document. To exemplify, consider the user name and password fields used to log into the web application, or a form used to collect payment information for a purchase. What parts of the HTML document that should be considered sensitive is application dependent. JSFlow offers the possibility to label individual DOM elements, which allows for fine-grained application specific policies.

In addition to information sources, DOM elements may act as information sinks. A natural example of such sinks are forms that submit the entered information to a given URL. While forms are examples of explicit sinks, there are also implicit sinks. Any element that fetches remote resources can be used as an implicit sink by encoding the information in the URL of the resource. The most prominent example of use of implicit sinks are to encode information in the URL of image elements and use it to fetch a zero pixel large image. Among other, this technique is used by many analytics services in order to circumvent the same-origin policy.

However, sources and sinks are not exclusive to the DOM API, but can be found in other browser APIs as well. For instance, an API that gives access to information about the specifics of the execution environment, such as the Navigator object, can be used for fingerprinting and vulnerability scanning. Under certain circumstances such APIs may be considered sensitive sources. Similarly, APIs like XMLHttpRequest and Web Sockets provide general explicit sinks.

Non-local models: Live collections. In addition to acting as a data structure, the DOM also provides a rich set of behaviors. In particular, several features of the DOM force information-flow models to be non-local, i.e., operations on a certain element in the tree may require updates to the model of other elements in the tree. A prime example of such a feature is live collections.

The DOM standard [38] specifies a number of methods for querying the DOM for a collection of certain elements. Collections are represented as objects that behave much like arrays, with one big exception: as the DOM is modified, collections are updated to reflect the current state of the DOM.

For example, getElementsByName returns a live collection of elements with a particular name attribute. If a script changes the name attribute of an element in the page, the corresponding live collections automatically reflect the change. To appreciate this, consider the following example based on a web page containing a div element with id and name ‘A’.

When the following code is executed in the context of this page, it encodes the value of h in the length of the live collection returned by getElementsByName.

This is achieved by conditionally changing the name of the div from ‘A’ to ‘B’. Initially, the collection stored in c has length 1, since there is one element in the document named ‘A’. After the name change, however, the collection contains no elements. Importantly, this is done without any direct interaction with the collection itself; only the div element is referenced and modified.

The security model of live collections must interact with the model for the DOM, making it non-local. We keep in each DOM node a map from queries generating live collections, such as getElementsByName(’A’), to the label representing how that node’s subtree affects that query.

Going back to the above example, the document (the root node of the DOM tree) maintains a map from names to labels. If this map associates ‘A’ with public, the interpreter will stop execution on the attempted name change, since it would be observable on existing public live collections. On the other hand, if this map associates ‘A’ with secret, the name change is allowed. In this case, however, any live collection affected is already considered secret.

Live collections are just one example of non-local behavior in the DOM. For another example, several DOM elements expose properties that are actually computed from state stored elsewhere in the DOM. For instance, a form element exposes values of nested input properties as properties on the form element itself. Also, some element attributes, which are DOM nodes of their own, are exposed as properties on the containing element. The security model of DOM nodes must properly model these cases and label the result appropriately. If we blindly accessed the properties in the underlying API, we could return secret values stripped of their security label.

Beyond handwritten models. At the moment, the library models are handwritten based on the description of the API functions. There are two main challenges related to handwritten library models.

First, without some form of automation the undertaking of producing a library model for a large API is very labor intensive. Already supporting the full standard API of JavaScript is a relatively large effort. Around 30% of the JSFlow code base1

Second, handmade library models are based on analysis and assumptions on the functionality of the library. For shallow and non-local models in particular this may be an issue. Any mismatches between the model and the functionality may open up possibilities for attacks. To avoid this, a more formal connection between the model and the library would be beneficial.

With respect to the first challenge, we envision automatic generation of library models from higher level descriptions. Such descriptions could range from pure functions on the involved security labels, supporting only the most basic shallow models, to functions that take values and side effects into account and even a fully fledged programming language. The design of the model language is a trade-off between expressiveness and benefit. For instance, to support fully deep models, the latter may be necessary, but then the gain over fully handwritten models may be relatively small.

With respect to the second challenge, for cases where the source code or some other functional description of the library is available, we envision using static analysis, e.g., abstract interpretation, to automatically generate library models that are guaranteed to capture the information flows of the library. When possible, this approach would also address the first challenge. We see both approaches as interesting but challenging future directions.