Abstract
Session cookies constitute one of the main attack targets against client authentication on the Web. To counter these attacks, modern web browsers implement native cookie protection mechanisms based on the
Introduction
Providing online access to modern web applications requires tracking a user’s identity across multiple requests. That, in turn, leads naturally to introduce the concept of web session to gather different HTTP(S) requests under the same identity, and implement a stateful, authenticated communication paradigm on top of a stateless protocol like HTTP(S). State information in web sessions is typically encoded by means of cookies: a cookie is a small piece of data generated by the server, sent to the user’s browser and stored therein; the browser will then automatically attach the cookie to all HTTP(S) requests sent to the server which registered it [4]. If the cookie contains a unique session identifier, the server will be able to effectively identify the client and bind together different requests sent by it, thus implementing a stateful communication session.
Cookie-based sessions are exposed to serious security threats, as the inadvertent disclosure of a session cookie provides an attacker with full capabilities of impersonating the client identified by that cookie. Indeed, cookie theft constitutes one of the most prominent web security attacks and several approaches have been proposed in the past to prevent and/or mitigate it [15,27,28,30,33]. Interestingly, this problem is so serious that modern web browsers implement native protection mechanisms based on the
While there is a general understanding that these flags constitute an effective defense, no formal result has so far been proved about the security guarantees they convey. The risk inherent to this gap between intuitive understanding and formal guarantees should not be underestimated, as experience has shown that any such gap between a prescribed protection mechanism and the security properties it is intended to enforce may hide dangerous security vulnerabilities. Without looking too far, it is well known that the intuitive same-origin policy enforced on many web resources can be circumvented by code injection attacks [21].
Contributions. With the present paper we provide the first formal result assessing the robustness of the
The security guarantees provided by our mechanized proof only apply to sessions that draw on appropriately flagged cookies. Clearly, however, poorly engineered websites that do not comply with the recommended flagging still expose their users to serious risks of session hijacking. Our analysis of the Alexa-ranked top 1000 popular websites gives clear evidence that such risks are far from remote, as the
Given that overflagging cookies may hinder client usability,
Structure of the paper. Section 2 provides background material on cookie-based sessions. Section 3 describes our formal model and our main theoretical result. Section 4 focuses on the practical aspects of session cookie security and presents the details of
Comparison with previous publication. This work revises and significantly extends a published conference paper [11]. We present a list of the most important changes:
We revised the formal model in Section 3 to provide a more accurate account of the attacker’s capabilities in terms of a new label pre-order; We reimplemented the original We detail in Section 5 a formal proof of soundness for We report in Section 6 on a larger-scale experiment with the revised version of
We also added a number of additional details which were omitted from the original conference paper due to space constraints.
Session cookie theft: Attacks and defenses
The attack surface against the confidentiality of session cookies is surprisingly large: this justifies the deployment in standard web browsers of native cookie protection mechanisms [4].
Web attacks
Web browsers implement a simple protection mechanism for the cookies they store, based on the so-called same-origin policy, whereby cookies registered by a given domain are made accessible only to scripts retrieved from that same domain [4]. Unfortunately, as it is well known, the same-origin policy can be circumvented by a widespread form of code injection attacks known as cross-site scripting (XSS). XSS is a dangerous vulnerability, which ranked third in the latest list of the top 10 security threats against web applications compiled by OWASP [31]. In these attacks, a script crafted by the attacker is injected in a page originating from a trusted web site and thus acquires the privileges of that site [21]. As a result, the injected script is granted access to the DOM of the page, and in particular to the JavaScript object
To make the explanation more concrete, consider the following example [30]. Assume that a website
weak.com
hosts a web page
The PHP function
The problem can be rectified by escaping the HTML tags from the variable
Network attacks
A network attacker may be able to fully inspect and corrupt all the unencrypted traffic exchanged between the browser and the server. Though adopting HTTPS to encrypt network traffic does provide an effective countermeasure against eavesdropping and active tampering, protecting session cookies against improper disclosure is tricky. For instance, many websites are still only partially deployed over HTTPS [14] and require special attention. In fact, cookies registered by a given domain are by default attached to all the requests sent to that domain: consequently, unless appropriate protection is put in place, loading a page over HTTPS may still leak session cookies in clear, whenever the page retrieves additional contents (e.g., images or scripts) over an HTTP connection to the same domain.
Notice that even websites which are completely deployed over HTTPS may be vulnerable to session cookie theft, whenever an attacker is able to inject (non-existing) HTTP links to these websites in unrelated web pages: indeed, the browser may still end-up accessing these broken links and send unanswered HTTP requests leaking the session cookies in clear [23].
Browser protection mechanisms
Modern web browsers provide two main mechanisms to secure session cookies, based on the
The
Notice that the
Formal browser models
Web browsers can be formalized in terms of constrained labelled transition systems known as reactive systems [9]. Intuitively, a reactive system is an event-driven state machine which waits for an input, produces a sequence of outputs in response, and repeats the process indefinitely.
(Reactive system [9]).
A reactive system is a tuple if if if if
Clauses (1) and (3) ensure that consumer states are always ready to process any input and transit to a producer state; clauses (2) and (4) assert that producer states can always emit one or more outputs in response to an input event.
Defining a notion of information security for reactive systems requires one to identify how input events affect the output events generated in response. Let (possibly infinite) streams of events be coinductively defined as the largest set generated by the following productions: For an input stream I, a reactive system in a given state Q computes an output stream O iff the judgement (Trace [9]).
Reactive noninterference
Given the previous definition, it is possible to introduce an effective notion of information security based on the well-known theory of noninterference. Let
(Reactive noninterference [9]).
A reactive system is noninterferent iff for all labels l and all its traces
The notation
(Visible similarity [7]).
Let
Notice that the definition is parametric with respect to a visibility and a similarity relations for individual stream elements, defining respectively what is visible and what is indistinguishable from the attacker’s perspective. Different instantiations of these relations entail different security guarantees, as we discuss in Section 3.3.
Formalizing web session security
We provide an outline of our mechanized formal proof of reactive noninterference for properly flagged session cookies under the currently available browser protection mechanisms. To ease readability, we keep the presentation informal whenever possible: full details can be found in the online Coq scripts. The scripts have been machine-checked using Coq 8.3pl5 on Windows 8.
Threat model
As it is customary for reactive noninterference [9], we characterize attackers in terms of a pre-order on security labels, which we define as follows.
(Security labels and order).
Let
We can easily prove that

The label pre-order for
It is very natural to characterize the attacker power in terms of a security label in the pre-order above. Specifically, level
We also underline that, since the definition of reactive noninterference (Definition 3) quantifies over all the possible input streams fed to the browser model, our framework implicitly provides any attacker with the ability to inject malicious contents on all the websites, irrespective of the adopted communication protocol. This is important to represent XSS attacks, since they are enabled by server-side vulnerabilities in the input sanitization process and thus orthogonal to the protocol choice. The same universal quantification uniformly captures different capabilities which may be used by the attacker to corrupt the input stream, e.g., the ability to suppress HTTP(S) traffic normally available to active network attackers.
The two security properties we target may informally be described as follows:
the value of an the value of an
The interesting point is that in both cases we target strong confidentiality guarantees, to ensure that the confidentiality of a session cookie is protected against both explicit and implicit flows of information, as prescribed by reactive noninterference. Specifically, we will show that a browser reacting to two input streams that are indistinguishable up to the values of the
Before delving into the technical details, we first provide an intuition about how existing attacks are captured by reactive noninterference and we highlight the threats posed by implicit information flows. Consider a web attacker running the HTTP website
attacker.com
, i.e., an attacker at
http://attacker.com
from our label pre-order, and take the following script snippet, where we assume a function
Now notice that, if the cookie
Notice also that, if the browser implemented dynamic taint tracking of
The entire reasoning can be generalized to the
Formalization
As anticipated, our security analysis is based on an extension of Featherweight Firefox, a core model of a web browser developed in the Coq proof assistant [7]. Our goal here is instantiating the definition of reactive noninterference (Definition 3) by providing visibility and similarity relations for the browser input/output events, which formalize our security policy and the threat model. To improve readability, the presentation is based on a (simplified) representation in standard mathematical notation of selected snippets of the Coq implementation.
Extended Featherweight Firefox
Featherweight Firefox [7] provides a fairly rich subset (∼15K lines of Coq code) of the main functionalities of a standard web browser, including multiple browser windows, cookies, HTTP requests and responses, basic HTML elements, a simple Document Object Model, and some of the essential features of JavaScript (including AJAX). FF is a reactive system: input events can either originate from the user or from the network, and output events can similarly be sent to the user or to the network. In particular, the model defines how the browser reacts to each possible input by emitting (a sequence of) outputs in response to it. For instance, when FF is in a consumer state, it may accept an HTTP response to a previous HTTP request, thus evolving into a producer state where the scripts included in the response are executed.
We extend FF with a number of new features, to include: (i) support for HTTPS communication; (ii) a more accurate management of the browser cookie jar to model the
The implementation of EFF arises as expected, though it required several changes to the existing framework to get a working Coq program: we refer to Appendix A for our implementation of the cookie flags in Coq. Here, we just remark that HTTPS communication is modelled symbolically, by extending the syntax of input and output events to make it possible to discriminate between plain and encrypted exchanges (see below). The syntactic elements we introduce to present the visibility and similarity relations of interest for the present paper are borrowed from the original Featherweight Firefox model, up to the changes detailed above.
Visibility and similarity
Let URLs be defined by the productions:
Output events. Output events are defined by the following productions:
(Visibility for outputs).
We define visibility for output events by means of the following inference rules:
The definition is consistent with the previous characterization of the attacker on the label pre-order. In particular, notice that the presence of both encrypted and unencrypted network traffic is visible to any attacker l such that
(Similarity for outputs).
We define similarity for output events by means of the following inference rules:
In words, we are assuming that the attacker is able to fully analyse any plain output event it has visibility of, while the contents of an encrypted request can only be inspected by a sufficiently strong attacker, who is able to decrypt the message. We assume here a randomized encryption scheme, whereby encrypting the same request twice always produces two different ciphertexts.2
This is a sound assumption for HTTPS, since it relies on the usage of short-term symmetric keys and attaches different sequence numbers to different messages.
Input events. The treatment of input events is similar, but subtler. Again, we start by introducing some notation. Let network responses (
Input events are then defined by the following self-explanatory productions:
We presuppose a further condition to rule out input events containing
We define similarity for input events as follows:
Intuitively,
(Visibility for inputs).
We define visibility for input events as follows:
In words, we just stipulate that
Formal results
Assuming the definitions of visibility and similarity for input and output events introduced above, we have our desired result.
(Noninterference).
EFF is noninterferent
We refer the interested reader to Appendix B for an intuition about the coinductive technique adopted in the proof, which approximately consists of 22K lines of Coq code. However, the result is interesting and important in itself, as it provides a certified guarantee of the effectiveness of the
Needless to say, the theorem only applies to web applications which apply the correct cookie flags. In the next section, we analyze the actual deployment of such mechanisms in existing systems, and describe our approach to enforce their use at the client side to secure them.
CookiExt: Strengthening web session security
We start with an analysis of the actual adoption of the security flags in existing systems: our results highlight a dangerous lack of protection, which supports the need for a client-side defense. We then describe the design of our solution, dubbed
Session cookie protection in the web
We conduct an analysis on the top 1000 websites of Alexa: we first present a heuristic for session cookie detection and then we apply it to the cookies set through the HTTP(S) headers by these websites. Based on this, we collect statistics aimed at understanding whether web developers put in place appropriate defenses for the session cookies set by their web applications.
A heuristic for session cookie detection
Session cookie flags in the gold set from [13]
Session cookie flags in the gold set from [13]
Since collecting session cookies in a reliable way is burdensome [13], but we do not want to draw any definite conclusion based on just 70 websites, we define a simple heuristic for session cookie detection and we apply it to extend our analysis to the top 1000 websites of Alexa. Inspired by previous work on client-side protection mechanisms [19,30,33], the heuristic marks a cookie as a session cookie if it satisfies either of the following two conditions:
its name matches the patterns ‘sess’, ‘sid’, ‘uid’, ‘user’, ‘auth’ or ‘key’; its value contains at least 10 characters and its index of coincidence
The index of coincidence is a statistical measure which can be effectively employed to estimate how likely a given text was randomly generated [22]. We consider here a variant which is not normalized by the alphabet size: given a string s of length N, let
Confusion matrix for the heuristic (gold set from [13])
Statistics about session cookie flags from Alexa top 1000
Statistics about session cookie flags from Alexa top 1000
Overall, we observe that the large majority of the session cookies we identified (71.4%) has no flag set: though this percentage may be partially biased by the adoption of a simple heuristic, it still provides clear indications of a limited practical deployment of the available protection mechanisms. We observe that, on average, web developers protect session cookies set over HTTPS more than session cookies set over HTTP. Perhaps surprisingly, we also notice that some cookies set over HTTP have the
We conducted a simple experiment aimed at estimating the extent of the actual HTTPS deployment. We found that 192 out of the 443 websites registering at least one session cookie (43.3%) support HTTPS transparently, i.e., they can be successfully accessed simply by replacing
Prior research has advocated the selective application of the
Overview
At a high level, the behaviour of if the response was sent over HTTP, all the identified session cookies are marked as if the response was sent over HTTPS, all the identified session cookies are marked as both
This simple picture, however, is significantly complicated by a number of issues which arise in practice and must be addressed to devise a usable implementation.
Supporting mixed content websites
Mixed content websites are websites which support HTTPS, but make some of their contents available only on HTTP [14]. This website structure is often adopted by e-commerce sites, which offer access to their private areas over HTTPS, but then make their catalogs available only on HTTP. These cases are problematic, as enforcing a redirection over HTTPS for the HTTP portion of the website would make the latter unavailable. Similarly, even assuming to be able to detect the absence of HTTPS support for some links, the adoption of a fallback to HTTP may break the user’s session: in fact, if session cookies are marked
In the original design of
Specifically, we observed that mixed content websites always provide HTTPS support at least for the initial authentication step, i.e., when the user’s password is sent from the browser to the server: this is a sensible practice, since passwords are (often reused) long-term credentials and their improper disclosure may have a much more severe impact than a session cookie leakage. The key for reliably ensuring protection is thus our choice of marking a session cookie as
Notice that the fallback mechanism never downgrades the security of the original website, i.e., it never removes the
Supporting sub-domains
Cookies registered by a website like
www.yahoo.com
can be set for
If a website relies on HTTP requests to a sub-domain for session tracking, a naive implementation of
Custom redirection rules
Custom redirection rules may be useful for two reasons. First, some websites that do not transparently support HTTPS may still provide their corresponding encrypted version on a different domain, hence a custom redirection rule would allow one to extend the protection offered by
Implementation details
The Google Chrome extension architecture requires to structure any extension in a number of different components, including zero or more content scripts and at most one background page [5]. Content scripts run with no privilege, but for the ability to communicate with the background page, and can be injected into downloaded web pages to interact with them; the background page, conversely, may request powerful privileges to the browser upon installation, but runs isolated from untrusted web contents.
Our extension consists of a content script and a background page. The content script is injected in any web page and it is used to detect the presence of login forms. This feature is implemented with a simple heuristic: roughly, when a form including a password field is detected on the page, a listener for later login attempts is registered by the extension [13]. The listener is used to check the protocol used for the password-based authentication step, so as to apply the most appropriate security policy on the received session cookies.
The background page requests and uses the following permissions:
Hosts permissions
Soundness of CookiExt
Careful readers will argue that our noninterference result, Theorem 1, predicates on (a Coq model of) a standard web browser rather than on a web browser extended with
Preliminaries
We first observe that the behaviour of
Also, it is worth noticing that the HTTPS redirection performed by
Based on the two observations above, it is possible to define the semantics of
Formal interpretation of CookiExt
Let
The relation
We extend the translation above from single input events to arbitrary input streams, by applying it pointwise to each stream component.
Extending the noninterference result
To generalize our noninterference result to a web browser patched with
(Extended input similarity).
Let
Intuitively,
We now observe that the relation
To show that
If
By a case analysis on the structure of i. □
In the end, we conclude that the relation
Let now
If
By induction on the derivation of
Finally, we can prove the main result of this section.
Let
The effectiveness of
Methodology
In our previous work [11], we performed a small scale experiment with
Overall, we collected a total of 733 cookies registered through HTTP(S) headers: 303 of them were marked as session cookies by our heuristics. For each session cookie we kept track of the original flags, as well as of the new flags which were assigned to it by
Evaluating protection
Original session cookie flags
Original session cookie flags
Secured session cookies
The table clearly highlights the improvement in protection. For instance, 92 session cookies (30.4%) were originally completely unprotected, while they can be secured against both web threats and network attacks. We also notice that 97 cookies (32.0%) can be protected at least against XSS attacks, while 19 cookies (6.3%) were originally protected against web attacks, but they can be effectively secured also against network threats. As a side-note to the table, we observe that 23 session cookies were originally marked as both
Redirected requests
In our experiments we navigated 1344 pages and we overall identified 322 HTTPS redirection attempts, among which 166 (51.5%) were successful: this suggests that many websites do not provide their pages over HTTPS, even though HTTPS support is actually available. Given the poor deployment of the
We also logged 158 HTTPS redirection attempts for sub-resources, like images or scripts, with only 4 failed redirections. Interestingly, 138 (87.3%) of these redirected requests were sent from the website www.fifa.com . The low number of sub-resource redirections highlights that web developers (except for a single website) normally do not include sub-resources in clear from the same website if the page is delivered over HTTPS: this is a sensible practice, since otherwise the sub-resource requests in clear may void the security provided by the HTTPS page.
One may wonder how effective
Based on this insight, we further investigated the numbers in Table 6 and we found that, with the use of
To further evaluate the security improvement granted by
Evaluating usability
The only way to understand the practical impact of the false positives of the heuristics is by testing and hands-on experience with the extension. In our experiments with
Apart from our experiments on the top 100 websites, we performed another empirical evaluation of the extension by having a small set of users install
Related work
Browser-side protection mechanisms
The idea of enforcing security at the browser side is certainly not new: below, we focus on a detailed comparison with the works which share direct similarities with our present proposal.
SessionShield [30] is a lightweight protection mechanism against session hijacking. SessionShield acts as a proxy between the browser and the network: incoming session cookies are stripped out from HTTP headers and stored in an external database; on later HTTP requests, the database is queried using the domain of the request as the key, and all the retrieved session cookies are attached to the outgoing request. We find the design of SessionShield very competent and we borrowed the idea of relying on a heuristic to identify session cookies in our implementation. On the other hand, SessionShield does not enforce any protection against network attacks and does not support HTTPS, since it is deployed as a stand-alone personal proxy external to the browser. The idea of identifying session cookies through a heuristic and selectively applying the
Another particularly relevant client-side defense is HTTPS Everywhere [34]. This is a browser extension which enforces communication with many major websites to happen only over HTTPS. The tool also offers support for setting the
We remark that both our theory and implementation just focus on the confidentiality of session cookies, which is a necessary precondition for thwarting the risks of session hijacking. However, several serious security threats against web sessions do not follow by confidentiality violations: for instance, classic CSRF vulnerabilities should rather be interpreted in terms of attacks on request integrity [26]. Several existing browser-based defenses mitigate the risk of other attacks against web sessions [10,17–19,29]. In a recent paper, we consider a strong definition of web session integrity and we discuss its browser-side enforcement [12].
Protecting against session hijacking
Session hijacking is surely the most dangerous threat against web sessions and researchers have proposed a number of different solutions against it. One-time cookies [15] use a session key and a HMAC construction to tie a unique authentication token to each request sent by the browser, so that the theft of a token does no harm, since it cannot be used to authenticate different requests. This is a good approach, since it tackles the root problem of session hijacking, but it requires web developers to implement a new session establishment protocol. Similarly, BetterAuth [25] is a novel authentication protocol for web applications, which aims at being secure by design, most notably by dispensing with the need of adopting cookies for authentication. A less invasive solution to the same problem is based on origin-bound certificates [20], which propose a small extension to the TLS protocol which allows browsers to establish strong authenticated channels with remote servers, by binding cookies only to these channels. Using origin-bound certificates, cookies can still be stolen, but they are of no use to an attacker.
Session hijacking can also be performed by fixating cookies known to the adversary in the user’s browser before the initial password-based authentication step, e.g., by exploiting an XSS vulnerability on the target website. If the target website does not refresh its cookies when the privilege level of the session changes, i.e., when the user submits her password, the session will be identified by a cookie chosen by the attacker, thus allowing him to impersonate the user at the website. Session fixation has been extensively studied by Johns et al. [24], who proposed different server-side solutions to the problem. At the browser side, session fixation can be prevented by Serene [19], a browser extension which keeps track of the session cookies registered through HTTP(S) headers and consequently strips from outgoing HTTP(S) requests any cookie which has not been seen before by the extension, thus preventing session cookies set by a script from reaching the target website and being used for authentication purposes.
Formal methods for web security
The importance of applying formal techniques to web security has been first recognised in a seminal paper by Akhawe et al. [1]. The work proposes a rigorous formalization of standard web concepts (browsers, servers, network messages…), a clear threat model and a precise specification of its security goals. The model is implemented in Alloy and applied to several case studies, exposing concrete attacks on web security mechanisms. Unfortunately, the bounded verification performed in Alloy is effective at finding attacks, but it fails at proving a security mechanism correct, which is what we are able to do in our work by relying on the Coq proof assistant.
A more recent research paper by Bansal et al. [3] introduces WebSpi, a ProVerif library which provides an applied pi-calculus encoding of a number of web features, including browsers, servers and a configurable threat model. The authors rely on the WebSpi library to perform an unbounded verification of several configurations of the OAuth authorization protocol through ProVerif, identifying some previously unknown attacks on authentication. Though interesting, the WebSpi library is much more abstract than Featherweight Firefox and not as easily extensible to include additional web features, since these must be encoded in the applied pi-calculus; moreover, ProVerif is a very powerful tool, but it still suffers from scalability and termination problems, which may potentially hinder other security analyses.
The Featherweight Firefox model has been proposed in [8] as a “blank slate” for researching new security policies and mechanisms for the browser. The original formulation consists of an executable OCaml model, which includes most of the features of the later Coq implementation [7]. The paper does not discuss any specific security property or application, and it just focuses on presenting the main features of the Featherweight Firefox model.
Reactive noninterference
The theory of reactive noninterference has been first developed by Bohannon et al. [9]. Aaron Bohannon’s doctoral dissertation [7] provides a mechanized proof of noninterference for a Coq implementation of the original Featherweight Firefox model [8] extended with a number of dynamic checks aimed at preventing information leakage. The considered information flow policy prevents cross-origin communication. In the present work we partially leverage the existing proof architecture to carry out our formal development, though we target a completely different information flow policy (for session cookie security).
Independently from Bohannon’s work, Bielova et al. [6] proposed an extension of the Featherweight Firefox model to enforce reactive noninterference through a dynamic technique known as secure multi-execution. In later work, De Groef et al. [16] built on this approach to develop FlowFox, a full-fledged web browser implementing fine-grained information flow control.
Conclusion
We have provided a formal view of web session security in terms of reactive noninterference and we showed that the protection mechanisms available in modern web browsers are effective at enforcing this notion. On the other hand, our practical experience highlighted that many web developers still fail at adequately protecting session cookies, hence we proposed
We imagine different directions for future work. First, we would like to further refine our formal model, to include additional concrete details which were initially left out from our study for the sake of simplicity; most notably, we would like to include sub-domains and domain cookies. Moreover, we plan to replace the current heuristic for session cookie detection with a more sophisticated solution based on machine learning techniques [13] to further improve the protection and the usability of our extension.
Footnotes
Acknowledgments
We would like to thank the anonymous referees for their valuable feedback, which helped us to significantly improve the original submission.
Coq implementation of the cookie flags
We present the Coq implementation of the
The function takes the source URL of the page where the script is running and the cookie jar as the input and returns all the non-
As to the
The function takes the destination URL of the HTTP(S) request and the cookie jar as the input and returns all the cookies which must be attached to the request. Specifically, the function passed as an argument to the
Noninterference proof
Following previous work [6,9], we prove our main result through an unwinding lemma, which provides a coinductive proof technique for reactive noninterference. However, we depart from previous proposals by developing a variant of the existing unwinding lemma based on a lockstep unwinding relation.
With respect to the original definition of unwinding relation, the main difference is in the last clause, where we require two related producer states to proceed in a lockstep fashion, even when they emit invisible output events. We can show that exhibiting a lockstep unwinding relation on the initial state of a reactive system is enough to prove noninterference.
By relying on a lockstep unwinding relation rather than on a standard unwinding relation, we can dramatically simplify the definition of the witness required by our proof technique and the proof itself, as we discuss below.
The browser state b in Featherweight Firefox is represented by a tuple, which contains several data structures modelling open windows, loaded pages, cookies, open network connections and a bunch of additional information needed for the browser to operate. We identify the set of consumer states with the space state generated by instantiating the set of these data structures in all possible ways. We then define producer states by pairing a consumer state b with a task list t: this list keeps track of the script expressions that the browser must evaluate before it can accept another input. State transitions are defined by the FF implementation: intuitively, the browser starts its execution in a consumer state and each input event fed to it will initialize the task list in a different way. Processing the task list moves the browser across producer states (possibly adding new tasks): when the task list is empty, the browser moves back to a consumer state and can process the next input.
To prove noninterference, we define our candidate lockstep unwinding relation
