Context
In this paper, we take a first step towards building a comprehensive formal foundation for web security
- threat models and web attacks are abstracted
- five case studies are presented
Threat models
Web attacker
- operates a malicious web site and may use a browser, but has no visibility into the network beyond requests or responses directed towards the hosts it operates
- The web attacker controls at least one web server and can respond to HTTP requests with arbitrary content
- The web attacker controls some number of DNS names, which the attacker can point to any server
- the attacker can host malicious content at URLs like
https://attacker.com/ - the web attacker can neither eavesdrop on messages to other recipients nor forge messages
- this threat model typically frame phishing or clickjacking: an user is tricked into browsing a malicious website
Network attacker
- has all the abilities of a web attacker plus the ability to HTTP eavesdropping, block, and forge network messages
- These HTTP requests do not need to comply with the HTTP specification, nor must the attacker process the responses in the usual way (although the attacker can simulate a browser locally if desired)
- read, control, and block the contents of all unencrypted network traffic
Gadget attacker
- has all the abilities of a web attacker as well as the ability to inject some limited kinds of content into honest web sites
- the easiest injection and the most common is hyperlink (e.g., link to a malicious website)
- a gadget attacker can often inject images, or other HTML tags
- he can also inject fully executable scripts
Security goal/objectives/concepts taken for granted
- “Don’t break the web” (no regression principle): new features/mechanisms in the web should not violate any of the invariants a web site rely upon (e.g., the GET method would never be replaced by another method with another name)
- Session integrity: the sever should not be tricked into performing sensitive actions. When a server takes action based on receiving an HTTP request the server takes for granted that the request was generated by a trusted user and not an attacker. Attacks such as CSRF (cross-site request forgery) are a violation of this principle
Monotonic and non-monotonic models of web apps
- A web attacker can undertake an action at one point in time, so the action is always available (motonony)
- A network attacker deals with a non-monotonic system, because once the system is, for instance, at the step 2, the attacker can no longer cause the system to accept an HTTP message expected in step 1
Network requests Requests generated by XMLHttpRequest can be sent only to the same origin (in the absence of CORS (Cross-Origin Resource Sharing)), whereas requests generated by HTML forms can be sent to any origin but can contain only certain methods and headers.
Approach
We implement a subset of our formal model in the Alloy modeling language
- expressing our model in an executable form ensures that our model has precise, testable semantics
- In creating the model, we found a number of errors by running simple checks. Modeling an assumption makes it clearer
- Alloy lets us express a model of unbounded size and then later specify a size bound when checking properties.