Page:SoK Exploring Current and Future Research Directions on XS-Leaks through an Extended Formal Model.pdf/4

with when a resource is requested, parsed or rendered. Examples of such components include the HTTP cache, the network connection pool (at the level of the browser), the different DOM properties of the attacker’s page and that of the rendered resource, or various aspects of the operating system on the client side such as CPU caches. We also consider components located on the server, which may depend on the infrastructure and environment of the targeted server, but will typically include the network layer at the OS-level and the various aspects related to the execution of the web application’s implementation. Based on the layer at which the components are located, we can group them together in seven component groups, five of which are located on the client side: attacker tab, victim frame, victim tab, browser, and client OS. The remaining two component groups are located on the server-side: environment (e.g. OS or serverless computing environment) and web server.

Each component consists of a 3-tuple, where the first element, $c$, represents the specific characteristics of the component. The latter two elements of the tuple, ${\sigma }_{{s}_{0}}$ and ${\sigma }_{{s}_{1}}$ , represent the state that the component is in, one for each state of $S$, i.e. the two different states that the application can be in based on the user’s authentication. Initially, these two states are equal, but they may differ after the state-dependent resources have been included. For example, the state of the HTTP cache is initially empty, but after rendering the resource in state $s_{0}$, a resource will be added to the cache, whereas this would not happen in application state $s_{1}$ , thus resulting in different component states. We formally denote the set of components as follows: $C=\{C_{0},C_{1},\ldots ,C_{n}\}$, where each individual component is defined as follows: $\{c,{\sigma }_{{s}_{0}},{\sigma }_{{s}_{1}}\}\in C_{i}$. We reference the state of the $i^{th}$ component, Ci , for the first application state, $s_{0}$, as $C_{i}\cdot {\sigma }_{{s}_{0}}$.

Next, we introduce the state-transfer and state-retrieval functions. The state-transfer function, $st$, will execute a specific inclusion technique i on the targeted state-dependent resource, and thus might bring the components in a different state. As such, the aim of this function is to transfer the web application state into the component state. We formalize this function as follows: $st:(sdr,C,i)\rightarrow C_{'}$, where $C_{'}$ represents the same set of components but after inclusion of the $sdr$. This inclusion may cause the initial state of a component to be altered, i.e. when $C_{i}\cdot {\sigma }_{{s}_{0}}\neq C_{i}^{'}\cdot {\sigma }_{{s}_{0}}$ or $C_{i}\cdot {\sigma }_{{s}_{1}}\neq C_{i}^{'}\cdot {\sigma }_{{s}_{1}}$ . For each component that was involved in the state-transfer, the state may have changed differently depending on the web application state (and thus depending which version of the resource was included). We can describe the differential component state in our model as $\Sigma =C_{i}^{'}\cdot {\sigma }_{{s}_{0}}\oplus C_{i}^{'}\cdot {\sigma }_{{s}_{1}}$ (where $\oplus$ is the XOR operator). This differential component state reflects the difference in the final state of the component depending on whether the resource in application state $s_{0}$ or in $s_{1}$ was included. For simplicity, throughout the remainder of the text, we will refer to this differential component state as $C_{i}^{'}\cdot \Sigma$.

The state-retrieval function, $sr$, aims to subsequently extract the differentiating state-changes that were introduced by the statetransfer function. More precisely, given the set of components in their initial state and possibly-altered state, $C$ and $C_{'}$ , this function will return the set of state-changes that could be detected with the leak technique $t$. Formally, we represent this function as follows: $sr:(t,C_{n},C_{n}^{'})\rightarrow L$, where $L$ represents the set of detectable (using leak technique $t$) state-differences (between $C_{i}^{'}\cdot {\sigma }_{{s}_{0}}$ and $C_{i}^{'}\cdot {\sigma }_{{s}_{1}}$). In our running example, the state-difference is that in one application state the resource will be cached, but not in the other application state. We can detect this state-difference by using a timing attack based on the response time. The set of detectable state-differences, $L$, consists of two parts, where the first one, $\Delta$, represents valuative differences, e.g. a difference in the number of frames. The latter part, $\Theta$, represents differences in the time domain, where the resulting value of the leak technique is exactly the same in both states, but where the timing differs. Another example of this case, is where the processing time of a certain request takes longer depending on the state of the user. While the resulting response may be exactly the same, the time it takes for the response to be received by the victim’s browser will differ. We formalize the set of differences in both domains as follows: $L=\{\Delta ,\Theta \}=\{(\delta _{0},{\Delta }_{1},\cdots ,{\Delta }_{n}),({\Theta }_{0},{\Theta }_{1},\cdots ,{\Theta }_{m})\}$.

In the case of our running example, we now get the following:

• We first transfer the application state to one of the components by embedding the resource as an iframe: $st(sdr,C,i)$.
• In application state s₀ , the state of one component, the HTTP cache, will be altered, while this does not occur in the case of $s_{1}:C_{i}\cdot {\sigma }_{{s}_{0}}\neq C_{i}^{'}\cdot {\sigma }_{{s}_{0}}\land C_{i}\cdot {\sigma }_{{s}_{1}}=C_{i}^{'}\cdot {\sigma }_{{s}_{1}}$ . As a result, the differential component state is non-empty: $C_{i}^{'}\cdot \Sigma \neq \emptyset$.
• Using a timing attack as leak technique, we can now retrieve the state from the component: $sr(t,Ci,C_{i}^{'})$.
• This results in a single detectable state-difference in the time domain: $L=\{\{\},\{{\Theta }_{0}\}\}$, where ${\Theta }_{0}$ represents the timing difference when requesting a cached vs. non-cached resource.

A simplified visual representation of our model can be found in Figure 1, showing the seven component groups that each have their own state. Furthermore, when a state-dependent resource is included (black arrow), it can trigger state-changes in all the components that it passes through (as indicated by the red circles). Extracting the detectable state-differences is then performed by launching a leak technique in the state-retrieval function (indicated by the purple dotted line).

3.4 Conditions for XS-Leaks

Using the extended formal model, we can now express the conditions that need to be met for an XS-Leak issue to exist. A first prerequisite is that the state of a component needs to be changed as the result of an inclusion method, i, in at least one of the two application states, s₀ and s₁ , expressed formally: $(\exists C_{i},i)(C_{i}\cdot {\sigma }_{{s}_{0}}\neq C_{i}^{'}\cdot {\sigma }_{{s}_{0}}\land C_{i}\cdot {\sigma }_{{s}_{1}}\neq C_{i}^{'}\cdot {\sigma }_{{s}_{1}})$, where $C_{i}^{'}=st(sdr,C_{i},i)$. Furthermore,