Consider an example from the wikipedia XSRF article:
The attack works by including a link or script in a page that accesses a site to which the user is known (or is supposed) to have authenticated. For example, one user, Bob, might be browsing a chat forum where another user, Mallory, has posted a message. Suppose that Mallory has crafted an HTML image element that references a script on Bob's bank's website (rather than an image file), e.g.,
<img src="http://bank.example/withdraw?account=bob&amount=1000000&for=mallory">If Bob's bank keeps his authentication information in a cookie, and if the cookie hasn't expired, then the attempt by Bob's browser to load the image will submit the withdrawal form with his cookie, thus authorizing a transaction without Bob's approval.
Lets look at the bank's (faulty) reasoning. The bank takes withdrawl requests from forms:
@forAll AMT, A1, A2.
{
?Q formParam [ paramName "account"; paramValue ?ACCT ],
[ paramName "amount"; paramValue AMT ],
[ paramName "for"; paramValue ?FOR ].
A1 accountName ?ACCT.
A2 accountName ?FOR.
} => { ?Q c:says { A1 debit AMT. A2 credit AMT. } }.
Note that the bank is not careful to distinguish between GET and POST requests. While this is architecturally unsound by itself,
- The practice is quite common, and
- It's not critical to the argument; the problem occurs with POST requests as well. Do XSRF attacks with POST always rely on JavaScript? Gotta read up on that...
The bank accepts cookies as sufficient credentials for all requests that the user is authorized to make:
{
?USER cookie ?COOKIE.
?Q ht:headers [ list:member [
ht:fieldName "Cookie";
ht:fieldValue ?COOKIE ]].
} => { ?Q c:speaks_for ?USER }.
TODO:clarify
And bob is logged in, so he has a current cookie:
bob cookie "s3lkw3lij4wl3i".
And Bob and Mallory have accounts:
bobAccount accountName "bob". malloryAccount accountName "mallory".
Then the request from Bob's browser comes in:
Q1 ht:absoluteURI "http://bank.example/withdraw?account=bob&amount=1000000&for=mallory"; ht:headers ( [ ht:fieldName "Cookie"; ht:fieldValue "s3lkw3lij4wl3i" ]).
next para needs clarification
We know that Q1 speaks for mallory, not bob, but the cookie authentication rule leads to the wrong conclusion:
Q1 speaks_for bob.
and hence:
bob c:says { bobAccount debit "1000000". malloryAccount credit "1000000" }.
If you're so-inclined, see the XSRF proof. Amounts are expressed as numeral strings; we could convert to integers or decimal numbers, but it would complicate the rules a bit and it's not essential to the argument.
Suppose we have a page from fedex that wants to (that is: claims it may) call back to fedex:
@prefix sop: <scriptorigin#>.
fedexConnection ht:connectionAuthority "fedex.com";
ht:requests (q2).
q2 ht:absoluteURI "http://fedex.com/track.js";
ht:methodName "GET";
ht:resp a2.
a2 ht:statusCodeNumber "200";
hs:messageEntity { xhr1 sop:contactsOrigin "fedex.com" }.
The browser, as the point of enforcement, must see that there is a valid argument that:
xhr1 sop:contactsOrigin "fedex.com".
From the premises above, the same origin policy leads to:
<http://fedex.com/track.js> sop:origin "fedex.com" . <http://fedex.com/track.js> c:controls_subject ( sop:contactsOrigin "fedex.com" ) .
Then our theory of HTTP speech acts leads to these steps:
fedexConnection c:says {
<http://fedex.com/track.js>
hs:information { xhr1 sop:contactsOrigin "fedex.com" . } .
} .
<http://fedex.com/track.js> :information
{ xhr1 sop:contactsOrigin "fedex.com" . } .
Layering the HTTP social constraint, we get:
<http://fedex.com/track.js>
c:says { xhr1 sop:contactsOrigin "fedex.com" . } .
Combining this with the information we got from the same origin policy about what <track.js> controls, the browser concludes that xhr1 is authorized:
xhr1 sop:contactsOrigin "fedex.com".
This line of reasoning is detailed in a same origin proof.