Static Checking of Dynamically-Varying
Security Policies in Database-Backed
Applications
Adam Chlipala
OSDI 2010

Beyond Code Injection
1.Injection
2.Cross Site Scripting

AnDependent
applicationonincludes
an
application­specific
unintended
run­time
authentication
and program
access control
interpreter
regimes!

3.Broken Authentication and Session Mgmt.
4.Insecure Direct Object References
5.Cross Site Request Forgery
6.Security Misconfiguration
7.Insecure Cryptographic Storage
....

2

Authentication Snafus

3

Roads to Security
Attack vector #1
Attack vector #2

Audit
Resource

Surprise attack

Audit

Security Policy
Attack vector #3

Audit

Information flow:
who can learn what
Access control:
who can change what

4

Dynamic Checking
Output to User

Database

Program
Variable

Sensitive
Datum

Program
Variable

Store security information with values

Program
Variable

Check before interaction with environment.

Pros
●Easy to add to existing programs
●Flexibility in coding security checks
Cons
●Bugs are only found for program paths that are tested.
●Performance overhead

5

Sensitive
Datum

Database

Static
Checking
High Security
Low Security

Type

Type

Program
Variable
Type
Program
Variable

Type

Output to User

Type
Program
Variable

Subtyping check

Pros
●Checks all program paths at compile time
●No changes to run-time behavior required
Cons
●Usually requires extensive program annotation
●Limited policy expressiveness

6

The Best of Both Worlds
Like Dynamic Checking:
●No program annotations
required
●Flexible and
programmer-accessible
policy language (SQL)

The

UrFlow
analysis

Like Security Typing:
●Checks all program paths
statically
●No run-time overhead

for the
Ur/Web
programming
language

7

A Word About Ur/Web
Integrated parsing and
queryX (SELECT * FROM t) type-checking of SQL
and HTML
(fn row => <xml><tr>

<td>{[row.T.A]}</td>
<td>{[row.T.B]}</td>
<td>{[row.T.C]}</td>
<td>{[row.T.D]}</td>
<td><form><submit
action={delete row.T.A}
value="Delete"/>
</form></td>
</tr></xml>);

8

Simple Policies
Secrets
Id Name

Secret

Client may learn
anything this query
could return.

policy sendClient
(SELECT Id, Name
FROM Secrets)
9

Reasoning About Knowledge
Secrets
Id Name

Secret

Code

policy sendClient
(SELECT *
FROM Secrets
WHERE known(Code))
10

What is “known”?
App source

Web page that generated this request

Cookies

AUTH

“foo”

n

known: “foo”
(“foo”, n)

(Username, Password)
= (U, P)

v

42

42

n

(42, v)

v

(U, P)
U

((42, v), P)

P
11

Multi-Table Policies
Secrets

Users

Id Name Secret Owner

Id Name Password

policy sendClient
(SELECT Secret
FROM Secrets, Users
WHERE Owner = Users.Id
AND known(Password))

12

Understanding SQL Usage

Program Execution

...
...
(U, P) = readCookie(AUTH);
pass = SELECT Password
known (U, P)
FROM Users
WHERE Id = U;
if (pass != P) abort();
...
∃ u ∈ Users. u.Id = U ∧ u.Password = P
...
...
rows = SELECT Secret
FROM Secrets
WHERE Owner = U;
// Send rows to client....
...
∀ v. mightSend(v) ⇒ ∃ s ∈ Secrets.

s.Owner = U ∧ v = s.Secret

13

Understanding SQL Usage
policy sendClient
(SELECT Secret
FROM Secrets, Users
WHERE Owner = Users.Id
AND (U,
known(Password))
known
P)
∀ s ∈ Secrets. ∀ u ∈ Users.
s.Owner = u.Id ∧ known(u.Password)
⇒ allowed(s.Secret)
∃ u ∈ Users. u.Id = U ∧ u.Password = P

Prove:
∀ v. mightSend(v)
⇒ allowed(v)

∧
∧
∧

∀ v. mightSend(v) ⇒ ∃ s ∈ Secrets.
s.Owner = U ∧ v = s.Secret

14

UrFlow Sketch
Program Code

Policies (SQL)

Finite set of
execution paths
Symbolic
executions
State:
P1
P2
P3
...
PN

Policies
(First-Order Logic)

Automated
Theorem-Prover

Check:
Q1
Q2
...
P2 /\ policies => Q1

15

Fancier Policies
Messages

ACL

Users

Forum Body

Forum User Level

Id Password

policy sendClient
(SELECT Body
FROM Messages, ACL, Users
WHERE ACL.Forum = Messages.Forum
AND ACL.User = User.Id
AND known(Password)
16
AND Level >= 42)

Write Policies
Secrets

Users

Id Name Secret Owner

Id Name Password

policy mayInsert
(SELECT *
FROM Secrets AS New, Users
WHERE New.Owner = Users.Id
AND known(Password)
AND known(New.Secret))

17

Case Studies

18

Progress
Imperative programs are too
hard to analyze!
Just use declarative
languages, and your life will be
so much easier.

Programming
Languages
Researchers

Maybe later. I'm going to get back to
coding my web application, which
does almost nothing besides SQL
queries.

Practitioners
App

UrFlow

Database

19

Ur/Web Available At:
http://www.impredicative.com/ur/

Including online demos with syntax-highlighted source code

20