Unit Four Analyze of Web Security Model Mechanisms
The Web，indispensable in modern commerce，entertainment，and social interaction，is a complex delivery platform for sophisticated distributed applications with multifaceted security requirements.However，most web browsers，servers，network protocols，browser extensions，and their security mechanisms were designed without analytical foundations.Further complicating matters，the Web continues to evolve with new browser features，protocols，and standards added at a rapid pace.The specifications of new features are often complex，lack clear threat models，and involve unstated and unverified assumptions about other components of the Web.As a result，new features can introduce new vulnerabilities and break security invariants assumed by web applications.Just as formal models and tools have proven useful in evaluating the security of network protocols，we believe that abstract yet informed models of the web platform，web applications，and web security mechanisms will be amenable to automation，reveal practical attacks，and support useful evaluation of alternate designs.
The web security model consists of a selection of web concepts，precise threat models，and two broadly applicable security goals.These design choices are informed by previous experience de-signingand evaluating web security mechanisms，such as preventing cross-site request forgery，securingbrowser frame communication，preventing DNS rebinding，and protecting high security Web sites from network attacks.These and other previous studies suggest that a few central modeling concepts will prove useful for evaluating a wide range of mechanisms.
Model Mechanisms
There are many threats associated with web browsing and web applications，including phishing，drive-by downloads，blog spam，account takeover，and click fraud.Although some of these threats revolve around exploiting implementation vulnerabilities，on ways in which an attacker can abuse web functionality that exists by design.Web sites use a number of different strategies to defend themselves against CSRF，but it lack a scientifically rigorous methodology of studying thesedefenses.By formulating an accurate model of the web，it can evaluate the security of these defensesand determine how they interact with extensions to the web platform.
A core idea in our model is to describe what could occur if a user navigates the web and visits sites in the ways that the web is designed to be used.For example，the user could choose to type any web address into the address bar and visit any site，or click on a link provided by one site to visit another.Because browsers support the“back”button，returning the user to a previously visited page，many sites in effect allow a user to click on all of the links presented on a page，notjust one.When the user visits a site，the site could serve a page with any number of characteristics，possibly setting a cookie，or redirecting the user to another site.The set of events that could occur，therefore，includes browser requests，responses，cookies，redirects，and so on，transmitted over HTTP or HTTPS.
The model has three main parts：web concepts，threat models，and security goals.The web concepts represent the conceptual universe defined by web standards.The formalization of these concepts includes a set of browsers，operated by potential victims，each with its user and abrowsing history，interacting with an arbitrary number of web servers that receive and send HTTP requests and responses，possibly encrypted using SSL/TLS.The model considers a spectrum of threats，rangingfrom a web attacker to a network attacker to a gadget attacker.
（1）Web concepts
The central concepts of the Web are common to virtually every web security mechanism we wish to analyze.For example，web mechanisms involve a web browser that interacts with one or more web servers via a series of HTTP requests and responses.The browser，server，and network behavior form the“backbone”of the model，much in the same way that cryptographic primitives provide the backbone of network protocols.Many of the surprising behaviors of the web platform，which lead to attack against security mechanisms，arise from the complex interaction between these concepts.By modeling these concepts precisely，we can check their interactions automatically.
①Non-Linear Time：Use a branching notion of time because of the browser's“back”button.Instead，if a user could click on either of two links，then use the back button to click on theother，it represent this as two actions that are unordered in time.In effect，temporal order represents necessary“happens before”relations between events.Instead of regarding thesebranchesas possible futures.In addition to conceptual economy，abstracting from the accidental linear order can reduce the number of possible states in need of exploration.
②Browser：The user's web browser，of course，plays a central role in our model of websecurity.However，the key question is what level of abstraction to use for the browser.Instead，it can abstract the browser into three key pieces.
Script Context.A script context represents all the scripts running in the browser on behalf of the origin of a single web.The browser does not provide any isolation guarantees between content within an origin—all the same origin scripts“share fate.”Correspondingly，we group the various scripts running in different web pages with an origin into a single script context and imagine them acting in unison.
Security UI.Some parts of the browser's user interface have security properties.For example，the browser guarantees that the location bar accurately displays the URL of the top-level frame.Model includes these elements in model and imbues them with their security properties.Inaddition，we model a forest of frames，in which each frame is associated with a script context and each tree of frames is associated with a constellation of security indicators.We assume that eachframe can overwrite or display（but not read）the pixels drawn by the frame below it in the hierarchy，modeling（at a high level）how web pages are drawn.
State Storage.Finally，the browser contains some amount of persistent storage，such as a cookie store and a password database.Assuming that confidential information contained in these state stores is associated with an origin and can be read by a script context running on behalf of that origin.To keep the model monotonic，it models these state stores as“append only，”which is not entirely accurate but simplifies the model considerably.
③Servers：It models web servers as existing at network locations（which are an abstraction of IP addresses）.Each web server is owned by a single principal，who controls the way of server responding to network messages.Servers are controlled by“honest”principals follow the specification，but a server might not be controlled by a malicious principal.Servers have a many-to-many relation to DNS names，which they exist in a delegation hierarchy.Holding servers in a many-to-many relation with DNS names is essential for modeling various tricky situations，such as DNS rebinding，where the attacker points a malicious DNS name at an honest server.
④Network：Finally，browsers and servers communicate by a way of network.In contrast to traditional models of network security，our model of the network has significant internal structure.Browsers issue HTTP requests to URLs，which are mapped to servers via DNS.The requests containa method and a set of HTTP headers.Individual headers carry semantics.It is an important part of security mechanisms，such as CSRF defenses that the referer header is set by the browser and not controlled by content rendered in the browser.
（2）Threat models
When evaluating the security of web applications，we are concerned with a spectrum of threats.The weakest threat is a web attacker—a malicious principal who operates a web site visited by the user.Starting with the web attacker as a base，it can consider more advanced threats，such as an active network attacker and a gadget attacker.
①Web attacker：Although the informal notion of a web attacker has appeared，it articulates the web attacker's abilities precisely.
Web Server.The web attacker controls at least one web server and can respond to HTTPrequestswith arbitrary content.Intuitively，we imagine the web attacker as having“root access”to these web servers.The web attacker controls some number of DNS names，which the attacker canpoint to any server.Canonically，we imagine the DNS named attacker.com referring to the attacker smain web server.The web attacker can obtain a HTTPs certificate for domains owned by theattackerfrom certificate authorities trusted by the user's browser.Using these certificates，theattackercan host malicious content at URLs.
Network.The web attacker has no special network privileges.The web attacker can respond only to HTTP requests directed at his or her own servers.However，the attacker can send HTTP requests to honest servers from attacker-controlled network endpoints.These HTTP requests need neither comply with the HTTP specification，nor must the attacker process the responses in theusualway（although the attacker can simulate a browser locally if desired）.For example，attacker can send an arbitrary value in the referer header and need not follow HTTP redirects.Notice that the web attacker's abilities are decidedly weaker than the usual network attacker considered in studies of network security，because the web attacker can neither eavesdrop on messages to other recipients nor forge messages from other senders.
Browser.When the user visits the attacker's web site，the attacker is“ introduced”to theuser'sbrowser.Once introduced，the attacker has access to the browser's web APIs.For example，the attacker can create new browser windows by calling the window.Open API.Weassumethe attacker's use of these APIs is constrained by the browser's security policy，that is，the attacker usesonly the privileges afforded to every web site.One of the most useful browser APIs，from the attacker'spoint of view，is the ability to generate cross-origin HTTPs requests via hyperlinks or the HTML form element.Attacks often use these APIs in preference to directlysending HTTP requests because the requests contain the user's cookies and the responses are interpreted by the user's browser.
A subtle consequence of these assumptions is that（once introduced）the attacker canmaintaina persistent thread of control in the user's browser.This thread of control，easily achieved in practice to use a widely known web application programming technique，can communicate freely with（and receive instructions from）the attacker's servers.We do not model this thread of control directly.Instead，we abstract these details by imagining a single coherent attacker operating at servers and can generate specific kinds of events in the user's browser.
②Network Attacker：An active network attacker has all the abilities of a web attacker as well as the ability to read，control，and block the contents of all unencrypted network traffic.Inparticular，the active network attacker need not be present at a network endpoint to send or receive messages at that endpoint.We assume the attacker cannot corrupt HTTPs traffic between honest principals，because trusted certificate authorities are unwilling to issue the attacker certificates for honest DNS names.Although these certificate authorities are willing to issue the attacker HTTPs certificates for malicious DNS names and the attacker can，of course，always self sign a certificate for an honest DNS name.Without the appropriate certificates，we assume the attacker cannot read or modify the contents of HTTPs requests or responses.
③User Behavior：The most delicate part of our threat model is how to constrain user behavior.If we do not constrain user behavior at all，the user could simply send his or herpasswordto the attacker，and defeat most web security mechanisms.
（3）Security goals
Although different web security mechanisms have different security goals，there are two security goals that seem to be fairly common：
①Security Invariants.The web contains a large number of existing web applications that make assumptions about web security.For example，some applications assume that a user's browser will never generate a cross-origin HTTP request with DELETE method because that property isensured by today's browsers.When analyzing the security of new elements of the web platform，it is essentialto check that these elements respect these（implicit）security invariants and“don't break the web”.
②Session Integrity.When a server takes action based on receiving an HTTP request，the server often wishes to ensure that the request was generated by a trusted principal and not anattacker.For example，traditional cross-site request forgery vulnerability results from failing to meet this goal.
Implementation
It implements a subset of formal model in the Alloy modeling language.Although incomplete，its implementation contains the bulk of the networking and scripting concepts and is sufficiently powerful to find new and previously known vulnerabilities in our case studies.Expressing model in Alloy has several benefits.First，expressing model in an executable form ensures that model has precise，testable semantics.Second，Alloy lets express a model of unbounded size and then later specify a size bound when checking properties.Finally，Alloy translates high-level，declarative，relational expression of the model into a SAT instance that can be solved by state-of-the-art SAT solvers，letting us leverage recent advances in the SAT solving community.
（1）An introduction
Alloy is a declarative language based on first order relational logic.All data types are represented as relations and are defined by their type signatures—each type signature plays the role of a type or subtype in the type system.A type signature declaration consists of the type name，the declarations of fields，and an optional signature fact constraining elements of the signature.A sub signature is a type signature that extends another，and is represented as a subset of the basesignature.The immediate sub signatures of a signature are disjoint.A top-level signature is asignaturethat does not extend any other signature.An abstract signature，marked abstract，representsa classification of elements that is intended to be refined further by more“concrete”sub signatures.
In Alloy，a fact is a constraint that must always hold.A function is a named expression with declaration parameters and a declaration expression as a result.A predicate is a named logical formula with declaration parameters.An assertion is a constraint that is intended to follow from the facts of a model.
Alloy Analyzer is a software tool that can be used to analyze models written in Alloy.The Alloycode is first translated into a satisfying problem.SAT solvers are then invoked to exhaustively search for satisfying models or counterexamples to assertions within a bounded scope.The scope is determined jointly by the user and the Alloy Analyzer.More specifically，the user can specify anumericbound for each type signature，and any type signature not bounded by the user is given a bound computed by the Alloy Analyzer.The bounds limit the number of elements in each set represented by a type signature，hence making the finite search.
（2）Realization
Many of the concepts in our general model have direct realizations in our implementation.For example，we define types as representing Principals，Network Endpoints，and Network Events.A Network Event represents a type of network message that has a sender and a recipient.It is a sub signature of Event；hence it also inherits all fields of Event.
In addition to being located in a particular Browser，a Script Context also has an Origin and a set of HTTP Transactions.The Origin is used by various browser APIs to implement the so-called“same origin”policy.For example，the XMLHTTP Request object（a subtype of Request API）prevents the Script Context from initiating HTTP Requests to a foreign origin.The transactions property of Script Context is the set of HTTP Transactions generated by the Script Context.
（3）Assertions
It finds that it is convenient to model the browser's cookie store on using fact statements about cookies，rather than declares a new type signature for it.It requires that HTTP Requests from Browsers contain only appropriate cookies from previous Set Cookie Headers.Selecting the appropriate cookies uses a rule that has a number of cases reflecting the complexity of cookie policies in practice，part of which is shown below.More explicitly，a browser attaches a cookie to an HTTP Request only if the cookie is set in a previous HTTP Response and the servers of the HTTPRequest and HTTP Response have the same DNS label.