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{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}\} \\ 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:

$ \text{ Declare } \text{ Node } R; \$ $ (\text{ isRoot }\ R\ ) \land (\text{ hasType }\ R\ \text{ iframe" }) \land (\text{ hasAttribte }\ R\ \text{ name" } \text{ ``x" })$

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.