Static support for capabilities
Vijay Saraswat
IBM TJ Watson Research Lab
(work done at Penn State)
Radha Jagadeesan
School of CTI, De Paul
http://www.cse.psu.edu/~saraswat/neighborhood.pdf
Outline


Capability languages
The problem of confinement


Object Reference Graph





Examples
Transformations
The basic idea: neighborhoods
Type rules for confined, contained.
Portals
Additional work: keys
Object-oriented Capability Languages

Objects


Encapsulated bundles of
state and action
May






Be Created
Stored/Retrieved
Transmitted
Be Acted on
Capability =def= object ref
Subject = object


Subject =def= source of
change/action in the
system.
Authority = possession of
capability


No static object designators


Authority =def= capacity to
perform an action
No ambient authority: only
connectivity begets
connectivity; must select
authority when performing
an access.
Types are interfaces


No closed world assumption
about known classes.
(Interfaces augmented with
assertions)
Example Languages: E, (statically typed) M (Java-)
Properties of Object-oriented Capability
Languages

No designation without
authority


To designate something
is to have the authority to
perform some actions on
it.



Dynamic subject
creation


Subjects (security
principals) are just other
objects
Open world assumption
Miller and Shapiro, ASIAN 2003
Subject-aggregated
authority management
Authorities are composable


No access control lists.
Subject has a list of
capabilities it can use.
The object pointed to by a
capability may itself
possess capabilities
Access controlled
delegation

X must have access to Y to
pass an authority to Y.
Confinement Problem


Capability copying +
check on access = *property violation
Alice (low)



Bob (high)



(loReader),loWriter
(hiWriter)
hiReader,(hiWriter)
loReader
Required: Bob should
not be able to write on
lo (exercise loWriter)
interface Reader {Object read();}
interface Writer {void write (Object a);}
interface ReaderWriter extends Reader,
Writer {}
…
// Alice
loWriter.write(loWriter);
…
// Bob
Object secret = hiReader.read();
Writer trapdoor =(Writer)loReader.read();
trapdoor.write(secret);
Problem: Alice can pass data, Bob can treat it as a capability and exercise it.
Confinement Problem: Other examples

You give 3d party Tax
software your data


Who has access?
Alice enters room
programmed by
untrusted Charlie.


Who can access rights to
talk to her?
(Harder) Can they do it
after she has left the
room?

Solution: Use factories.

Many drawbacks
Basic intuition

We can devise usable static type rules to
enforce confinement

Identify notion of private state




Based purely on graph-theoretic (connectivity) notions
Allow method to specify that received parameters
will circulate only to objects in private state
Thus: Type correctness => confinement
This can be done while supporting separate
compilation for classes.
(Cumulative) Object Reference Graph



(Typed) Nodes =objects
Edges = references
Four basic operations





Cumulative ORG: no delete
We will work with CORGs.
Easier to deal with statically.
Create
Give
Get
Delete
The effect of all programs
may be abstracted merely
by a sequence of these
transformations.
TOMS model: Motwani, Venkatsubramaniam, Panigrahy, Saraswat (STOC 2000)
Neighborhoods

Def: n(o), neighborhood of an
object o:

p in n(o) if






Remove from *(o) all elements
that have an incoming edge
from outside *(o).
o is a root of N.
Def: N is connected if it has an
incoming edge from outside N
Connected with dominators
N may hold outgoing edges.
n(o) may be empty
N and N’ overlap implies one is
contained in the other



Def: N is a neighborhood if
N=n(o), for some o.


Properties
Finding neighborhoods:


for any q st q->p, q=o or q in
n(o)
o -*-> p


Thus neighborhoods may be
nested.
n(p) subset N if p in N
(non-empty) N is connected iff
it does not contain one of its
roots.
A connected neighborhood has
a unique root.
Free and confined objects

We label each object in the
(C)ORG with an object




o(p) is read as: object p is
the label for object o.
Label is established when
an object is created, and
does not change during its
lifetime.
Think: label is stored in a
final field on the object.
An object o is free =def=
o(o)

An object that is not free is
said to be confined.


A reference to a free object
p(p) is said to be contained
in n(o) if it is accepted by a
free object o(o) and can be
propagated only through
confined links.
Edges will be labeled as
well:


f: free (the original kind)
c: confined
Example: Information leakage revisited


If Alice is not to be able to
propagate loWriter freely,
then loWriter must be
communicated to Alice at a
confined type.
Now loWriter cannot be
communicated to any free
object:

interface Reader {Object read();}
interface Writer {void write (Object a);}
interface ReaderWriter extends Reader,
Writer {}
…
// Alice
contained Writer loWriter = …
loWriter.write(loWriter); // FAILS
…
confined objects cannot
// Bob
be passed as args to
method invocations on
confined objects
Object secret = hiReader.read();
Writer trapdoor =(Writer)loReader.read();
trapdoor.write(secret);
Confined edges

Transformation rules

Free




Confined




Create
Give
Get
Create
Give
Get
Not permitted:

Cannot give/get
confined object
into/from a free object
Confined edges approximate neighborhoods.
Basic Theorem


Let G0 be a single node graph a0(a0).
Let G=G0,G1,G2 be a sequence of graphs
obained by applying these rules. Then in any
Gn:



a(o) –c c(q) implies o=q
a(o) –c c(q) implies all edges into c(q) are
confined edges.
a(o) implies a in {o} u n(o)
Contained edges
b(b)
a(o)

a creates b
f
b(p)
f
b(p)
a(o)
f
f|
f|
t
t

f
a(o)
c(q)
c(q)
a gives b to c
Introduce contained edges
(t)
Transformation rules:

a gets b from c
b(o)
a(o)
a creates confined b

b(p)
a(o)
c
c
x
a(o)
x
(x=) c | f | t
(x=) c | f | t
c(q)
f
b(p)
t

b(p)
a(o)
t
t
c(q)
a gives b to c
a gets b from confined c
f|
f|
t
a(o)
c(q)
f
a gives b to confined c
b(p)
c(q)
a gets b from c
Contained edges stay within the neighborhood.
Contained edges may be
created through give or get
(on any edge).
Contained edges may be
propagated (via give/get)
only through confined
edges.
Free edges (not confined or
contained edges) may be
propagated through
contained edges.
Basic Theorem: Confinement


Associate each contained edge with the set s of
nodes responsible for its creation.
Confinement Theorem: In any Gn (defined as
before):


a(o) –t(s) b(q) implies label of each object in s is o.
a(o) –t(s) b(q) cannot cause the introduction of an
edge into b(q) other than a contained edge.
Need for portals: Vector iterators

Consider a vector
implementation


Cells representing
elements should be
considered to be in the
private state of the vector
However a
VectorIterator
should be allowed
access to these cells.

A portal for an object o
is an object p (labeled
with o) that may access
objects in n(o), but may
be propagated freely
outside n(o).
Multi-neighborhoods

Def: n(s), neighborhood of a
set of objects s:



for any q st q->p, q in s u
n(s)
*(s) contains n(s)

Note:


Intuition:
p in n(s) if




n(o) = n({o})
n({})={}

Multi-neighborhoods are
disjunctive neighborhoods.
We should not permit two
neighborhoods to be joined:
this loses containment.
Instead, we permit objects
in a neighborhood to be
“freed”.
Def: A neighborhood n(s) is
said to be generated by o if
all objects in s are labeled
by o.
Portals into multi-neighborhoods
b(b)
a(o)
a creates b
f
b(p)
f
f
Confined nodes may “leak”
free references (e.g.
iterators)
But a free reference cannot
be used to access
contained state.
Confinement Theorem
unchanged!
t
t

b(p)
a(o)
f|
f|
Allow an object to possess
a free reference to itself
(this).
f
a(o)

c(q)
c(q)
a gives b to c
a gets b from c
b(o)
a(o)
a creates confined b
x
b(p)
c
c
x
a(o)
(x=) c | f | t
(x=) c | f | t
a(o)
c(q)
c(q)
t
b(p)
b(p)
a(o)
t
f|
f|
f
f

a gets b from confined c
a gives b to confined c
a(o)
b(p)
t
t
c(q)
c(q)
a gives b to c at contained type

a gets b from c at contained type
a(o)
a(o)
a inserts this
Contained edges stay within the neighborhood, even with portals.
Future work

Compare with



Information Flow –
introduce confined(k), for
k an object.
SFKASI – different way
of getting protection
domains in Java.
Alias control, ownership
types, containment types

Similar intuitions … but
their development is
complicated!

Develop static analysis
for other capability
programming patterns.


Exploit ORG!
Understand connection
with BI logic.
b(b)
a(o)
a creates b
f
b(p)
f
b(p)
a(o)
f
f|
f|
f
a(o)
t
t
c(q)
c(q)
a gives b to c
a gets b from c
b(o)
a(o)
a creates confined b
x
b(p)
c
c
x
a(o)
(x=) c | f | t
(x=) c | f | t
a(o)
c(q)
c(q)
a gets b from confined c
a gives b to confined c
t
b(p)
f|
f|
t
t
c(q)
c(q)
a gives b to c at contained type
a gets b from c at contained type
a(o)
a(o)
a inserts this
Introducing Portals.
b(p)
a(o)
f
f
t
a(o)
b(p)
Descargar

Infrastructure for Mass Computing