Web Attacks
This model shows a store and provides a number of requests to modify the store. It then shows how
to use the store with a good user Alice and have a bad user Eve that do not give any credentials.
Eve should therefore never be able to login or buy anything.
Preamble
Order the Token and State sigs which will be used later. (The includes (open) must come first.)
We also define Item and Token which are needed later but only used for their identity. We
require some of them to be there because otherwise you run into the really nasty problem
that any comprehension seems to succeed because it misses atoms for one of the variables.
module store
open util/ordering[Token] as tk
open util/ordering[State] as st
some sig Item, Token {}
Actions
We later create a serial trace of actions that are performed in the store. The following actions are defined:
enum Action {
INIT,
BUY,
LOGIN,
STUTTER
}
The STUTTER action is necessary to not block the trace. I.e. if there are no more items and
everybody is logged in then there are no alternative actions so then stutter can fill the gap.
Authentication
We use a simple userid to digest table. The digest (total) function calculates a digest. In this case
we use the same atom for ease of use but this should be a one-way hash function like the SHA-x
algorithm.
We add the credentials for Alice but no credentials for Eve. That is, Eve has no access to the store.
fun digest[password : String ] : String { password }
pred authenticate[userid,password : String] {
userid->digest[password] in
("Alice" -> digest["Bob123"])
}
State
We need to create a trace of actions. We maintain this state in, ehh, State. For convenience
this State maintains the state for both the browser (the cookies) and the server (the stock,
token generator, etc.).
Notice that the order is very relevant here because it defines how the sig is displayed in the
table view. You should try to create ‘sentences’ with the order. For example, Eve BUY item
It is important to realize that the cookies are shared state. This means that the browser is free to ignore or violete the contract of cookies. We can therefore not create any facts that rely in the cookies.
sig State {
browser : lone Browser,
action : Action,
bought : lone Item,
// Reflects the browser state
cookies : Browser -> Token,
// Reflects the server state
stock : set Item,
cart : Token -> (Item+String),
token : lone Token,
nextToken : Token,
}
Action Predicates
Later we define a trace of actions. A trace is a sequence of State atoms. We require
that the trace is constrained by the action predicates. That is, going from Staten to
Staten+1 requires that one of the action predicates is true.
Login
The first action predicate is login. A browser gives us a userid and a password. These credentials
must be authenticated before the login succeeds.
If this login is successful then we require a cookie with a token. This token is a capability, a browser that has that token can then buy in the store.
The login fails if the user is already logged in. It might be interesting to succeed a failed attempt due to lack of proper credentials. This would then record the attack in the trace. That is not done here.
In the cart we record the user id as the first bought item, this is a bit hackish. It records the name of the user of that cart, but it also creates at least one entry in the cart. I.e. it activates the cart. (Never realized you could hack in models?)
pred login[ s, s' : lone State ] {
let browser = s'.browser,
userid = browser.userid,
password = browser.password {
one userid
one password
no s.cart.userid
authenticate[ userid,password ]
s'.action = LOGIN
s'.nextToken = s.nextToken.next
s'.stock = s.stock
s'.cart = s.cart + (s.nextToken->userid)
s'.token = s.nextToken
s'.bought = none
s'.cookies = s.cookies + (browser->s.nextToken)
}
}
Buy
After login the browser has a cookie with a token. We use this token to record the sale in the corresponding cart.
pred buy[ s, s' : State ] {
let item = s'.bought,
tkn = s'.token {
some item
item in s.stock
one tkn
some s.cart[tkn]
s'.action = BUY
s'.nextToken = s.nextToken
s'.stock = s.stock-item
s'.cart = s.cart + (tkn -> item)
s'.token = tkn
s'.bought = item
s'.cookies = s.cookies
}
}
Stutter
A stutter action is there to fill gaps. If the trace cannot make progress then it can always
provide a stutter step. They are kind of annoying because a trace with just stutters is
then a perfectly valid solution. You have to filter out those solutions with your run command.
For check commands they are generally irrelevant.
pred stutter[s, s' : State ] {
s'.action = STUTTER
s'.nextToken = s.nextToken
s'.stock = s.stock
s'.cart = s.cart
s'.browser = none
s'.token = none
s'.bought = none
s'.cookies = s.cookies
}
The Clients
We’re now ready to define the client side. Our model is that we have a Browser, a.k.a the User Agent.
We’re cheating a bit because we do not record the cookies in the browser, we rely on the shared state to store the cookies. (This is dangerous because it is now easy to make facts that assume the server knows about the browser.)
We are also defining two users: Alice and Eve. Alice is the good girl and gets a password. Eve is evil and we do not constrain her use of credentials. In practice, this means that Alloy will use all possible credentials for Eve.
abstract sig Browser {
userid : String,
password : String
}
one sig Alice extends Browser {} {
userid = "Alice"
password = "Bob123"
}
one sig Eve extends Browser {}
Trace
We now create a trace of every combination of all possible actions. We constrain
the actions to those allowed by the action predicates login, buy, and stutter.
That is, each action predicate is used to constrain Staten -> Staten+1
fact {
st/first.nextToken = tk/first
st/first.stock = Item
no st/first.bought
no st/first.cart
no st/first.browser
no st/first.cookies
st/first.action = INIT
all s' : State - first, s : s'.prev {
login[s,s']
or
buy[s,s']
or
stutter[s,s']
}
}
Checking
We do not want Eve to be able to buy anything, only Alice’s credentials are recorded in the password database so Eve should not be able to login nor buy anything.
So we can check that Eve can never buy anything nor can she login:
assert Evil {
no s : State | s.browser = Eve
}
check Evil for 4
If we run this then it gives us the following output.
┏━━━━━━━━━━┳━━━━━━━┳━━━━━━━━┳━━━━━━┳━━━━━━━━━━━┳━━━━━┳━━━━━━━━━━━━━━┳━━━━━━┳━━━━━━━━━┓
┃this/State┃browser┃action ┃bought┃cookies ┃stock┃cart ┃token ┃nextToken┃
┠──────────╊━━━━━━━╋━━━━━━━━╋━━━━━━╋━━━━━━━━━━━╋━━━━━╋━━━━━━━━━━━━━━╋━━━━━━╋━━━━━━━━━┫
┃State⁰ ┃ ┃INIT⁰ ┃ ┃ ┃Item⁰┃ ┃ ┃Token⁰ ┃
┠──────────╊━━━━━━━╋━━━━━━━━╋━━━━━━╋━━━━━━━━━━━╋━━━━━╋━━━━━━━━━━━━━━╋━━━━━━╋━━━━━━━━━┫
┃State¹ ┃ ┃STUTTER⁰┃ ┃ ┃Item⁰┃ ┃ ┃Token⁰ ┃
┠──────────╊━━━━━━━╋━━━━━━━━╋━━━━━━╋━━━━━━━━━━━╋━━━━━╋━━━━━━━━━━━━━━╋━━━━━━╋━━━━━━━━━┫
┃State² ┃ ┃STUTTER⁰┃ ┃ ┃Item⁰┃ ┃ ┃Token⁰ ┃
┠──────────╊━━━━━━━╋━━━━━━━━╋━━━━━━╋━━━━┯━━━━━━╋━━━━━╋━━━━━━┯━━━━━━━╋━━━━━━╋━━━━━━━━━┫
┃State³ ┃Eve⁰ ┃LOGIN⁰ ┃ ┃Eve⁰│Token⁰┃Item⁰┃Token⁰│"Alice"┃Token⁰┃Token¹ ┃
┗━━━━━━━━━━┻━━━━━━━┻━━━━━━━━┻━━━━━━┻━━━━┷━━━━━━┻━━━━━┻━━━━━━┷━━━━━━━┻━━━━━━┻━━━━━━━━━┛
You can see this also in the Browser table. We see that Eve has stolen the credentials of Alice.
┏━━━━━━━━━━━━┳━━━━━━━┳━━━━━━━━┓
┃this/Browser┃userid ┃password┃
┠────────────╊━━━━━━━╋━━━━━━━━┫
┃Alice⁰ ┃"Alice"┃"Bob123"┃
┠────────────╊━━━━━━━╋━━━━━━━━┫
┃Eve⁰ ┃"Alice"┃"Bob123"┃
┗━━━━━━━━━━━━┻━━━━━━━┻━━━━━━━━┛
Attacks
This is a bit of a conumdrum but it shows the power of Alloy. This immediately shows how fragile passwords are. In the real world we demand from the users that they keep their passwords secret. We therefore record this (stupid!) assumption in a fact.
fact NoSharedPassword {
// all disj b1, b2 : Browser | b1.userid = b2.userid => b1.password != b2.password
}
Uncomment the previous fact and the run the EveBuying command again. This gives the following output
┏━━━━━━━━━━┳━━━━━━━┳━━━━━━━━┳━━━━━━┳━━━━━━━━━━━━━┳━━━━━┳━━━━━━━━━━━━━━┳━━━━━━┳━━━━━━━━━┓
┃this/State┃browser┃action ┃bought┃cookies ┃stock┃cart ┃token ┃nextToken┃
┠──────────╊━━━━━━━╋━━━━━━━━╋━━━━━━╋━━━━━━━━━━━━━╋━━━━━╋━━━━━━━━━━━━━━╋━━━━━━╋━━━━━━━━━┫
┃State⁰ ┃ ┃INIT⁰ ┃ ┃ ┃Item⁰┃ ┃ ┃Token⁰ ┃
┠──────────╊━━━━━━━╋━━━━━━━━╋━━━━━━╋━━━━━━━━━━━━━╋━━━━━╋━━━━━━━━━━━━━━╋━━━━━━╋━━━━━━━━━┫
┃State¹ ┃ ┃STUTTER⁰┃ ┃ ┃Item⁰┃ ┃ ┃Token⁰ ┃
┠──────────╊━━━━━━━╋━━━━━━━━╋━━━━━━╋━━━━━━┯━━━━━━╋━━━━━╋━━━━━━┯━━━━━━━╋━━━━━━╋━━━━━━━━━┫
┃State² ┃Alice⁰ ┃LOGIN⁰ ┃ ┃Alice⁰│Token⁰┃Item⁰┃Token⁰│"Alice"┃Token⁰┃Token¹ ┃
┠──────────╊━━━━━━━╋━━━━━━━━╋━━━━━━╋━━━━━━┿━━━━━━╋━━━━━╋━━━━━━┿━━━━━━━╋━━━━━━╋━━━━━━━━━┫
┃State³ ┃Eve⁰ ┃BUY⁰ ┃Item⁰ ┃Alice⁰│Token⁰┃ ┃Token⁰│"Alice"┃Token⁰┃Token¹ ┃
┃ ┠───────╂────────╂──────╂──────┴──────┨ ┃ ├───────╂──────╂─────────┨
┃ ┃ ┃ ┃ ┃ ┃ ┃ │Item⁰ ┃ ┃ ┃
┗━━━━━━━━━━┻━━━━━━━┻━━━━━━━━┻━━━━━━┻━━━━━━━━━━━━━┻━━━━━┻━━━━━━┷━━━━━━━┻━━━━━━┻━━━━━━━━━┛
Since Eve can no longer succeed in using Alice’s credentials, it tries to steal the token that the server handed to Alice’s browser. It can do this by sniffing in on a wireless network at Starbucks when Alice uses normal HTTP, not encrypted HTTPS.
It is interesting to see that the item ends up in Alice’s cart.
So we need to record a fact that our model can assume that in the real world the cookies are protected using HTTPS and cannot be guessed. In our model that means we can ‘trust’ the cookies to be protected. (Another indication of the fragility of the web.)
Again uncomment for making it active.
fact HTTPS {
// all s : State | one s.token implies s.token = s.cookies[s.browser]
}
Instead of doing a run, we now want to make sure Eve cannot buy anything ever … So if you run the check again it should fail to find a counter example.
So now we know the web is safe! #not