Transcript pptx

Jean Yang, Travis Hance, Thomas H. Austin, Armando
Solar-Lezama, Cormac Flanagan, and Stephen Chong
PLDI 2016
Jean Yang / PLDI 2016
Precise, Dynamic
Information Flow
for DatabaseBacked
Applications
Jean Yang / PLDI 2016
An oil skimming operation works in a heavy oil slick after the
spill on April 1, 1989. (Photo from Huffington Post)
Jean Yang / PLDI 2016
Oil-covered otter. (Photo from the Human Impact Project)
Single hull
Double hull
Crude oil
Crude oil
Required by the Oil
Pollution Act of 1990.
Jean Yang / PLDI 2016
The Relationship Between
Design and Accidents
Jean Yang / PLDI 2016
But what about
information
leaks?
Single hull
Double hull
Sensitive data
Sensitive data
Research in language-based security looks at designs
for double hulls [Sabelfeld and Myers, JSAC 2003].
Our goal: make double hulls that are
as easy to construct as possible!
Jean Yang / PLDI 2016
Wanted: Double Hull for
Information Security
1.
Why it’s hard to prevent
information leaks.
2.
A programming model that
makes writing secure web
programs easier.
3.
How we support that
programming model in
database-backed applications.
Jean Yang / PLDI 2016
This Talk: Making It Easier to
Secure Web Programs
Social Calendar Example
Jean Yang / Jeeves
Let’s say Arjun and I want to throw a
surprise paper discussion party for Emery.
Challenge: Different Viewers
Should See Different Events
Surprise
discussion for
Emery at
Chuck E.
Cheese.
Guests
Pizza with
Arjun/Jean.
Private event
at Chuck E.
Cheese.
Strangers
Jean Yang / PLDI 2016
Emery
Policies May Depend on
Sensitive Values
Must be on guest list.
Policy for event
depends on policy
for guest list!
Guest List
Must be member of list and the
list must be finalized.
Finalized list
Jean Yang / PLDI 2016
Leaky enforcement:
when the programmer
neglects dependencies
of policies on sensitive
values.
A Story of Leaky Enforcement
1 We add Armando to
non-final guest list.
Guest List
4 Armando figures out
he was uninvited.
There was a
party on my
calendar…
2 Armando sees the
event on his calendar.
3 We run out of space
and remove Armando.
Guest List
Finalized list
Jean Yang / PLDI 2016
Finalized list
A Story of Leaky Enforcement
1 We add Armando to
non-final guest list.
4 Armando figures out
he was uninvited.
Problem: implementation for event
Guest List
was a
policy
neglected to take There
into
account
party on my
guest list policy.
calendar…
This arises
whenever we
sees the
2 Armando
3 We run out of space
trust
programmers
to getand remove Armando.
event
on his
calendar.
policy checks right!
Guest List
Finalized list
Jean Yang / PLDI 2016
Finalized list
Need to Track Policies and
Viewers Across the Code
Need to track how information flows
through derived values and where
derived values flow!
Update to
all
calendar
users
Jean Yang / PLDI 2016
“What is the
most popular
location among
friends 7pm
Tuesday?”
Conditional permissions
checks everywhere!
Jean Yang / PLDI 2016
“Policy Spaghetti” in HotCRP
Jacqueline Web Framework to
the Rescue!
Programmer specifies
information flow policies
separately from other
functionality.
3 Enhanced runtime
encompasses applications
and databases, preventing
leaks between the two.
Policy annotations
Sensitive data
2
Database
Runtime prevents information
leaks according to policy
annotations.
Jean Yang / PLDI 2016
1
Contributions
programming
model for database-backed web
applications.
• Semantics and proofs for policyagnostic programming that
encompasses SQL databases.
• Demonstration of practical
feasibility with Python
implementation and application
case studies.
Jean Yang / PLDI 2016
• Policy-agnostic
Jacqueline Web Framework
Policies
Enhanced runtime
Framework attaches
policies based on
annotations.
Jean Yang / PLDI 2016
Framework
shows
appropriate
values based
on viewer and
policies.
Object-relational
mapping propagates
policies and sensitive
values through
computations.
class Event(JacquelineModel):
name = CharField(max_length=256)
location = CharField(max_length=512)
time = DateTimeField()
description = CharField(max_length)=1024)
Base schema
@jacqueline
def has_host(self, host):
return EventHost.objects.get(
event=self, host=host) != None
@jacqueline
def has_guest(self, guest):
return EventGuest.objects.get(
event=self, host=host) != None
Policy helper
functions
@staticmethod
Information flow policy for location
@label_for(‘location’)
def restrict_event(event, ctxt):
return event.has_host(ctxt) or event.has_guest(ctxt)
@staticmethod
Public value for
def jacqueline_get_private_location(event):
return “Undisclosed location”
field
location field
Jean Yang / PLDI 2016
Coding in Jacqueline
Model
View
Centralized policies! No checks or
declassifications needed anywhere else!
Controller
Jean Yang / PLDI 2016
Centralized Policies in
Jacqueline
Closer Look at the PolicyAgnostic Runtime
Jeeves [Yang et al 2012, Austin et al 2013] uses facets
[Austin et al 2012] to simulate simultaneous multiple
executions.
propagates
values and
policies.
userCount = 0
if
2 Runtime
==
:
userCount += 1
return userCount
print {
}
1
solves for
values to show
based on
policies and
viewer.
print {
0
}
Jean Yang / Jeeves
1 Runtime
20
Labels Track Sensitive Values
to Prevent Leaks
if
==
:
c += 1
guest
if
true false :
c += 1
Emery can’t see secret
party information or
results of computations
on those values!
guest
c =
cold+1
Labels follow
values through
all computations,
including
conditionals and
assignments.
cold
Jean Yang / Jeeves
guest
21
Jean Yang / PLDI 2016
Jean Yang / PLDI 2016
The Dangers of Interacting
with Vanilla Databases
Queries
select * from Users
where location =
Application
All data
select * from Users
Database
Database
Database
queries can
leak
information!
Impractical
and potentially
slow!
Challenge: Support faceted execution when
interacting with an unmodified SQL database.
Need faceted queries!
Jean Yang / PLDI 2016
Application
Semantics of a Faceted
Database
)
Conceptual row
Primary key
1
select * from Users
where location =
Store facets
as strings?
Location
New
database
for each
label?
Too expensive! Too difficult to extend the
formal semantics!
Jean Yang / PLDI 2016
save(
SQL
Database
Solution: Use ORM to Map
Facets onto Database Rows
Jeeves key
Conceptual row
1
Location
a
Labels
1
{𝑎}
1
{¬𝑎}
select * from Users
where location =
Jeeves key
Location
1
Labels
{𝑎}
ORM refacets
Jeeves key
1
a
Location
NULL
Jean Yang / PLDI 2016
Primary key
Location
Jacqueline
Supports
SQL
ORM Implements
Implements
get
select
all
select
filter
select
sort
order by
refaceting Can use SQL
refaceting implementations
refaceting for many
queries!
refaceting
foreign keys
join
-
save
delete, insert turning a faceted value into
multiple rows
delete
delete
keeping track of which
facets to delete
Jean Yang / PLDI 2016
Supporting Queries in
Jacqueline
Jean Yang / PLDI 2016
Early Pruning Optimization
Policies
Optimization: Can
often explore fewer
possible paths!
Enhanced runtime
Jean Yang / PLDI 2016
Observation:
Framework can
often (but not
always) track
viewer.
Jean Yang / PLDI 2016
Review: Traditional NonInterference
Secret values should not affect public output.
==
:
if
guest
userCount += 1
==
:
userCount += 1
guest
1
0
print {
0
Challenge:
Compute labels from
program—may have
dependencies on
} secret values!
Jean Yang / Jeeves
if
guest
Policy-Agnostic NonInterference
guest
==
if
:
userCount += 1
==
:
userCount += 1
guest
1
0
print {
0
Theorem:
All executions where
guest must be
public produce
} equivalent outputs.
Can’t tell apart secret
values that require
guest to be public.
Jean Yang / Jeeves
if
guest
Jean Yang / PLDI 2016
Course
manager
Health
record
manager
Jacqueline reduces the number
of lines of policy code and has
reasonable overheads!
Conference
management
system
(deployed!)
Jean Yang / PLDI 2016
Application Case Studies
Jean Yang / PLDI 2016
Demo
Conference Management System
Running Times
All Papers*
0.15
0.1
0.05
0
0
500
1000
Papers in database
Jacqueline
Django
16
14
12
10
8
6
4
2
0
0
500
1000
Papers in database
Jacqueline
Django
Tests from Amazon AWS machine via HTTP requests from another machine.
*Different from numbers in paper.
Jean Yang / PLDI 2016
0.2
Time to show all papers (s)
Time to show page (s)
Single paper
Summary: Policy-Agnostic Web
Programming with Jacqueline
1
Programmer specifies
information flow policies
separately from other
functionality.
3 Enhanced runtime
encompasses applications
and databases, preventing
leaks between the two.
Policy annotations
2
Runtime prevents
information leaks according
to policy annotations.
Database
We have strong
formal
guarantees and
evidence that
this can be
practical!
Jean Yang / PLDI 2016
Sensitive data
You can factor out
information flow policies
from other code to avoid
policy spaghetti!
You can enforce policies
across the application and
database by using a
carefully-crafted ORM!
http://jeeveslang.org
http://github.com/jeanqasaur/jeeves
Jean Yang / PLDI 2016
You can build realistic
systems using this approach!