People's Newsroom

FORMAL WEB SECURITY MODELING AND CHECKING

The design of Web security mechanisms is complex: the behavior of (same-origin and cross-origin) browser requests, server responses and redirects, cookie and session management, as well as the often implicit threat models of Web security can lead to subtle security bugs in new features or countermeasures. In order to evaluate proposals for new Web mechanisms more rigorously,  proposed a model of the Web infrastructure, formalized in Alloy. The base model is some 2000 lines of Alloy source code, describing (1) the essential characteristics of browsers, Web servers, cookie management and the HTTP protocol, and (2) a collection of relevant threat models for the Web. The Alloy Analyzer – a bounded-scope model checker – can then produce counterexamples that violate intended security properties if they exist in a specified finite scope. 

MODELING OUR COUNTERMEASURE

A WEBATTACKER is a malicious user who can control malicious Web servers but has no extended networking capabilities. The concept of Origin is used to differentiate between origins, which correspond to domains in the real world. An origin is linked with a server on the Web, that can be controlled by a principal. The browsing context, modeled as a ScriptContext, is also associated with an origin, that represents the origin of the currently loaded page, also known as the referrer. A ScriptContext can be the source of a set of HTTPTransaction objects, which are a pair of an HTTPRequest and HTTPResponse. An HTTP request and response are also associated with their remote destination origin. Both an HTTP request and response can have headers, where respectively the CookieHeader and SetCookieHeader are the most relevant ones. An HTTP request also has a method, such as GET or POST, and a queryString, representing URI parameters.

An HTTP response has a statusCode, such as c200 for a content result or c302 for a redirect. Finally, an HTTP transaction has a cause, which can be none, such as the user opening a new page, a RequestAPI, such as a scripting API, or another HTTPTransaction, in case of a redirect.

Client-side State. Web introduced a new signature CSState that represents a client-side state. Such a state is associated with an Origin and contains a set of Cookie objects. To associate a client-side state with a given request or response and a given point in time, we have opted to extend the HTTPTransaction from the original model into a CSStateHTTPTransaction. Such an extended transaction includes a beforeState and afterState, respectively representing the accessible client-side state at the time of sending the request and the updated client-side state after having received the response. The afterState is equal to the beforeState, with the potential addition of new cookies, set in the response.

Trusted-delegation Assumption. Web model the trusted-delegation assumption as a fact, that honest servers do not send a POST or parametrized redirect to Web attackers.

USING MODEL CHECKING FOR SECURITY AND FUNCTIONALITY

Web formally define a CSRF attack as the possibility for a Web attacker (defined in the base model) to inject a request with at least one existing cookie attached to it (this cookie model the session/authentication information attached to requests) in a session between a user and an honest server.

Web provided the Alloy Analyzer with a universe of at most 9 HTTP events and where an attacker can control up to 3 origins and servers. In such a universe, no examples of an attacker injecting a request through the user’s browser were found. This gives strong assurance that the countermeasure does indeed protect against CSRF under the trusted delegation assumption. Web also modeled the non-malicious scenarios, and the Alloy Analyzer reports that these scenarios are indeed permitted. From this, we can also conclude that extension of the base model is consistent.

Back to top button