Exploit Generation

This document describes the process of generating exploit HTML markups based on a taint flow trace. The exploit will be loaded through initial DOM-clobberable lookup, converting type of controlled value from DOM nodes to string, and leading them to the sink by leveraging operations recorded in the trace.

Unlike typical exploit generation, where the attacker's input is usually a string and only the string constraints need to be tracked from input to sink, our context involves input in the form of DOM nodes (or HTMLCollections). This requires leveraging operations along the trace to secondary load the attacker-controlled string into the program and guide its flow to the sink. Therefore, we perform symbolic execution of DOM nodes on the taint trace to collect constraints that enables conversions from DOM nodes to other DOM nodes or from DOM nodes to strings. Once the attacker-controlled value is converted to a string, we apply existing symbolic execution techniques for strings to fullfill the string-related constraints on the last stage.

Next, we will describe our approach in three steps: 1/ Taint Dependency Graph Construction, 2/ Operation Capability Inference and 3/ Constraints modeling and Solving. First, we construct a Taint Dependency Graph (TDG) based on the collected taint trace, detailing how the attacker-controlled value is used in each operation, along with value snapshots at the time of execution. Given that the complete exploit requires at least one type conversion from DOM to String, we assign objectives to each operation based on its capabilities and the type requirements of subsequent operations. Finally, we traverse the TDG in a top-down manner to collect constraints for each operation's input based on its assigned objective, then solve these constraints to generate a set of satisfying DOM trees as input.

Taint Dependency Graph

Operation Objectives

For the operations that can be recorded in the taint trace, we define the operation objectives are DOCUMENT2DOM, WINDOW2DOM, DOM2DOM, DOM2STRING, STRING2STRING.

Symbolic Modeling of DOM Tree

Here, we formally define a simplified DOM Tree as a ranked alphabet, which is a couple $(F, Arity)$, where $F$ is a finite set and $Arity$ is a mapping from $F$ into $\mathbb{N}$. The arity of a symbol $f \in F$ is $Arity(f)$. Elements of arity $0, 1, ..., p$ are respectively called constants, unary, ..., p-ary symbols.

$$ F = {\text{Strings}^*, \text{Attribute Names}, \text{DOM Node Names}, \text{hasAttribute}, \text{hasType}, \text{hasChild}, \text{hasSibling}, \text{hasSrcDoc}, \text{isRoot}} $$

$$ \text{Arity}(f) = \begin{cases} 0 & \text{if } f \in {\text{Strings}^*, \text{Attribute Names}, \text{DOM Node Names}} \\ 1 & \text{if } f = \text{isRoot} \\ 2 & \text{if } f \in {\text{hasType}, \text{hasChild}, \text{hasSibling}, \text{hasSrcDoc}} \\ 3 & \text{if } f = \text{hasAttribute} \end{cases} $$

In this formalism:

• Strings(^*) represents the set of possible string values within the DOM, such as text node contents or attribute values.
• Attribute Names includes all possible attribute names that can appear in a DOM node (e.g., id, class, href).
• DOM Node Names represents all possible DOM node types (e.g., div, span, a).
• hasAttribute is a ternary operation that checks if a DOM node has a specific attribute with specific value.
• hasType is a binary operation that verifies the type of a DOM node.
• hasChild is a binary operation that checks the parent-child relationship between two DOM nodes.
• hasSibling is a binary operation that checks the sibling relationship between two DOM nodes.
• isRoot is a unary operation that set the symbol as the root node.

Then, we define the constraints for each operation with objectives on the DOM tree $(F, Arity)$. Initially, the input, without any constraints, represents arbitrary valid DOM trees (i.e., any structure or attributes with any value are allowed). However, processing an operation at each step will impose a set of predefined constraints on the input based on the DOM standard and browser behavior, restricting the set of satisfying DOM trees. For example, given the document.x operation with a DOCUMENT2DOM objective, only a limited set of DOM trees can be used, such as a DOM node of type iframe with the name attribute set to x. The following constraints can be applied:

$$ \begin{align*} & \text{ Declare } \text{ Node } R; \\ & (\text{ isRoot }\ R\ ) \land (\text{ hasType }\ R\ \text{ "iframe" }) \land (\text{ hasAttribte }\ R\ \text{ "name" } \text{ "x" }) \end{align*} $$

Even with these constraints, the symbol still represents a variety of trees. For instance, arbitrary valid DOM nodes can be nested, and additional attributes with any values can be present as long as they don't conflict with the imposed constraints.

Objective:DOCUMENT2DOM - Operation:GetField

Considering the operation document.prop, all the following constraints should add the shared constraint: $\text{ Declare } \text{ Node } R,\text{ String } x; (=\ x\ prop)$

• iframe tag with name attribute
  • $(\text{ isRoot }\ R\ ) \land (\text{ hasType }\ R\ \text{ "iframe" }) \land (\text{ hasAttribte }\ R\ \text{ "name" } \text{ x })$
• TS4, Embed, form tag with name attribute
  • $(\text{ isRoot }\ R\ ) \land ((\text{ hasType }\ R\ \text{ TS4 }) \lor (\text{ hasType }\ R\ \text{ "embed" }) \lor (\text{ hasType }\ R\ \text{ "form" }))\land (\text{ hasAttribte }\ R\ \text{ "name" } \text{ x })$
• object tag with id attribute
  • $(\text{ isRoot }\ R\ ) \land (\text{ hasType }\ R\ \text{ "object" }) \land (\text{ hasAttribte }\ R\ \text{ "id" } \text{ x })$

Objective:WINDOW2DOM - Operation:GetField

Refer to the "Named Access Window" section for the Table 2 in the It's clobbering time paper.

Objective:DOM2DOM - Operation:GetField

Refer to the "Form Parent-Child", "Nested Window Proxy", and "HTMLCollection" section for the Table 2 in the It's clobbering time paper.

Considering the operation base.prop, all the following constraints should add the shared constraint: $\text{ Declare } \text{ Node } R, \text{ Node } C, \text{ String } x; (=\ x\ prop)$

• form parent and input child
  • $(\text{ isRoot }\ R\ ) \land (\text{ hasChild }\ R\ \ C\ ) \land (\text{ hasType }\ R\ \text{ "form" }) \land (\text{ hasType }\ C\ \text{ "input" }) \land (\text{ hasAttribte }\ R\ \text{ "id" } \text{ y }) \land (\text{ hasAttribte }\ C\ \text{ "form" } \text{ y }) \land (\text{ hasAttribte }\ C\ \text{ "id" } \text{ x })$

(Novel) Objective:DOM2String - Operation:GetField

Here, we summarize a list of property lookups for each DOM nodes type which can be used to load string value from attributes.

(Novel) Objective:DOM2String - Operation:Binary

Implicit toString method call during binary operation '+'.

(Novel) Objective:DOM2String - Operation:FunctionCall

Here, we document the function call whose base or arguments can be DOM nodes and the return value is based on the DOM nodes in type of String. There are different cases:

1. DOM nodes and JavaScript builtins objects have shared method name and signature (arguments and return value).
2. Different DOM node type have shared method name, for example, getAttribute between iframe and script element. The developer may assume the document.scripts return all the script tags in the document but can be clobbered by the attacker-injected iframe element. Since they are sharing the same getAttribute method call, the method call on script to get attribute might also works for injected the iframe element.
3. Implicit toString call on base or args. For example, [].join(arg0) where arg0's toString function will be implicitly called.

• getAttribute function
  • base.getAttribute(arg0) where base is the attacker-controlled value
  • $(\text{ isRoot }\ R\ ) \land (\text{ hasAttribte }\ R\ \text{ arg0 } \text{ x })$