be a heap location (if the property points to another object),
a function declaration, a security type, or a primitive value.
Security types keep track of taints; a sink object’s security
type acquires a taint associated with a source object, if there
is an explicit flow from the source object to the sink object.
A security type is modeled as a pair (taint value, source
string); the taint value could either be Low or High and the
taint source is a string identifying the source object of the
taint. The primitive string values are preserved and propagated through string operations, whenever they evaluate to
constant strings. All other primitive values are abstracted.
computed using the Vex analysis. Every object and function
while the properties of the object are represented using edges
in the graph. In the figure, the global object loc_Global
has five properties ObjectProt,FunctionProt,
Array, ArrayProt, and array_instance pointing to
the nodes loc_ObjProt,loc_FunProt,loc_ 1,loc_
ArrayProt, and loc_ 4 respectively. Every node in the
heap is associated with a taint value, High or Low—High representing the untrusted objects and Low representing the
trusted objects. High taints and low taints are represented
by red and blue nodes, respectively, in the figures (all nodes
in Figure 2 are Low). Figure 3 shows the initial abstract
heap representation of the
object and the
window.document object; notice that one
of the nodes loc_document has a high taint.
the analysis: Vex analysis is based on a set of rules that transform abstract heaps according to each statement in the program, and it works by essentially over-approximating the
effect of the statements on the abstract heap. These rules
closely follow the small-step operational semantics proposed
by Maffeis et al.,
13 which covers the ECMA-262 standard for
summary is given in Section 4. 2. Variables and functions
that are not initialized in the current program execution or
through summaries, are initialized to point to placeholder
dummy objects with High taints. The default taint of an object
created in the extension is set to Low unless the analysis
explicitly sets the value to High or a variable is uninitialized.
FunctionProt loc_ 1
The loops in the program are unrolled a bounded number of
times and function calls are inlined for a bounded unrolling
of recursive calls, and every path of the resulting program is
explored. Thus Vex may overlook certain flows, as discussed
in Section 4. 3. The static analysis does not evaluate the conditions in conditional statements of the program because
of the abstraction. Whenever it reaches a conditional statement, both branches are traversed, in a depth-first manner,
to ensure that the entire program is covered. The analysis is
flow-sensitive and, due to inlining, also context-sensitive.
property, which is used to specify inheritance chains.
Additionally, every function (that can be used as a constructor in new) has a prototype property. This prototype
property is used to instantiate the @Proto property when
a new object is created using the function constructor. An
object inherits all the properties of its @Proto and of all the
objects in the prototype’s @Proto chain.
Figure 2 illustrates how Vex handles prototype-based
as the node loc_ 1 in the figure. Since the Array object is
a constructor, which can be used to create new instances of
the array, it has a prototype field pointing to the object,
ArrayProt, represented in the graph by the node loc_
ArrayProt. A new Array instance, array_instance
object, is created in the program using the statement: array_
instance = new Array (). In Figure 2, loc_ 4 represents the array_instance object. The @Proto field of this
object points to the object loc_ArrayProt. Therefore, the
push method is accessible to the array_instance object
and can be called using the array_instance.push.
function and object summaries: Natively supported functions and objects are replaced with stubs that summarize
figure 3. window.content.document object.