close

Se connecter

Se connecter avec OpenID

A Formal Foundation for XrML

IntégréTéléchargement
A Formal Foundation for XrML
Vicky Weissman
Joint work with: Joseph Halpern
The big picture


A policy says that under certain
conditions an action, such as
downloading a file, is permitted or
forbidden.
Digital content providers want


to write policies about how their works
may be accessed, and
they want their policies enforced.
2
Example - Entertainment


Music/movie industries want to enforce
policies that amount to `if the client has
not paid to access the content, then she
may not access it’.
Industries might need this capability.

British Video Association estimated that
this year, 1.67million people downloaded
illegal film/TV files; more than double last
year’s estimate.
3
It’s not just about money
Because we can’t regulate access to
online content with precision:



Digital libraries can’t put certain content
online; it might violate IP laws.
The Greek Orthodox Archdiocese of
America is wary of defamation.
Cultural traditions aren’t respected.
(Australian Aboriginal communities often
restrict access to a clan or gender.)
4
XrML to the rescue



XrML is a language for writing policies.
Syntax is XML-based.
Semantics is given in 2 ways.
1. An English interpretation of the syntax.
2. An English description of an algorithm
that says if a set of XrML policies imply a
permission.

Bottom line: write policies in XrML,
enforce using the algorithm.
5
Industry likes XrML



XrML endorsed by Adobe, Hewlett-Packard,
Microsoft, Xerox, Barnesandnoble.com, MPEG
International Standards Committee…
Microsoft and others plan to make XrMLcompliant products.
Will tomorrow’s OS, DVD player, … enforce
XrML policies?
6
XrML Shortcomings

No formal semantics.



Policies can be ambiguous.
The interpretation of the syntax doesn’t
quite match the algorithm.
The algorithm’s behavior on some
(realistic) input is unintuitive and
unintended by language designers.

E.g. If Alice is a student and any student
may eat lunch, may Alice? Alg. says no. 7
Improving XrML



Fix the algorithm to match developers’ intent.
Translate XrML policies to formulas in modal
first-order logic.
Prove our translation matches the algorithm.


Algorithm says policies imply a permission iff
translated policies imply translated permission.
Why translate?


Gives XrML formal semantics (no ambiguity).
Lets us compare XrML with languages in CS
literature, borrow complexity results, extensions,…
8
First step:
Present XrML syntax

XrML is an XML-based language.


XrML policies are verbose.
So, we present a syntax that is


more concise and
easy to map to XrML syntax.
9
XrML Syntax

Language includes a set of principals.



Primitive principals are agents
(e.g., Alice, Bob).
Set of principals is closed under union
(e.g., Alice  Bob is a principal; often
written as {Alice, Bob}).
According to the XrML doc, {p1,.., pn}
represents agents p1, …, pn “acting
together as one holistic identified entity”.

But what does this mean?
10
Groups/members relationship


Suppose that agent p has property Prp and
group {p, …} has property Prg.
What should we infer?



Option 1: nothing.
Option 2: {p, …} has property Prp.
Option 3: p has property Prg.
11
Groups/members relationship


Suppose that agent p has property Prp and
group {p, …} has property Prg.
What should we infer?




Option 1: nothing.
Option 2: {p, …} has property Prp.
Option 3: p has property Prg.
XrML chooses each of these options (at
different points in the specification).
12
Groups/members relationship


Suppose that agent p has property Prp and
group {p, …} has property Prg.
What should we infer?




Option 1: nothing.
Option 2: {p, …} has property Prp.
Option 3: p has property Prg.
XrML chooses each of these options (at
different points in the specification).
No formal semantics  language is inconsistent!
13
Our fix

Since XrML is inconsistent…


We do not assume that a group has the
properties of its members or vice-versa.
But can easily write policies to force either
relationship (or both).
14
Syntax (cont.)

Resources


Rights


Digital content (e.g., a movie, an article)
Actions (e.g., play, edit)
Properties

Describe a principal (e.g., adult, trusted).
15
Syntax (cont.)

Conclusions



conc ::= Pr(p) | Perm(p, r, s)
Pr(p) means principal p has property pr.
Perm(p, r, s) means p is permitted to
exercise right r over resource s.
16
Syntax (cont.)

Conclusions



conc ::= Pr(p) | Perm(p, r, s)
Pr(p) means principal p has property pr.
Perm(p, r, s) means p is permitted to
exercise right r over resource s.
17
Syntax (cont.)

Conclusions



conc ::= Pr(p) | Perm(p, r, s)
Pr(p) means principal p has property pr.
Perm(p, r, s) means p is permitted to
exercise right r over resource s.
18
Syntax (cont.)

Conclusions




conc ::= Pr(p) | Perm(p, r, s)
Pr(p) means principal p has property pr.
Perm(p, r, s) means p is permitted to
exercise right r over resource s.
Conditions

cond ::= true | conc | cond  cond.
19
Syntax (cont.)

grant ::= x1…xn (cond  conc).



If cond holds, then conc holds.
In our fragment, grants are closed
(no free variables).
license ::= (grant, principal)

(g, p) means p issues/says g.
20
Examples

Can write:



`Joe is a SPYCE member’ as
true  SPYCE(Joe),
Andre says`Joe is a SPYCE member’ as
(true  SPYCE(Joe), Andre).
Vicky says `Any SPYCE member who gives
a talk may have a cookie’ as
(x (SPYCE(x)  GivesTalk(x) 
Perm(x, eat, cookie)), Vicky).
21
Examples

Can write:



`Joe is a SPYCE member’ as
true  SPYCE(Joe),
Andre says`Joe is a SPYCE member’ as
(true  SPYCE(Joe), Andre).
Vicky says `Any SPYCE member who gives
a talk may have a cookie’ as
(x (SPYCE(x)  GivesTalk(x) 
Perm(x, eat, cookie)), Vicky).
22
Examples

Can write:



`Joe is a SPYCE member’ as
true  SPYCE(Joe),
Andre says`Joe is a SPYCE member’ as
(true  SPYCE(Joe), Andre).
Vicky says `Any SPYCE member who gives
a talk may have a cookie’ as
(x (SPYCE(x)  GivesTalk(x) 
Perm(x, eat, cookie)), Vicky).
23
Examples

Can write:



`Joe is a SPYCE member’ as
true  SPYCE(Joe),
Andre says`Joe is a SPYCE member’ as
(true  SPYCE(Joe), Andre).
Vicky says `Any SPYCE member who gives
a talk may have a cookie’ as
(x (SPYCE(x)  GivesTalk(x) 
Perm(x, eat, cookie)), Vicky).
24
The syntax given here is
a fragment of XrML.
(See paper for details.)
25
XrML Algorithm


Let L be a set of licenses; G is a set of
grants that implicitly hold.
Auth algorithm



In: L, G, and a closed conclusion e.
Out: true iff e “follows” from L and G.
Auth calls Holds algorithm


Holds in: L and a closed condition d.
Out: true iff d “follows” from L.
26
Auth(e, L, G) overview

Recall
e is a closed conclusion.
 L is the set of issued licenses.
 G is set of grants that hold implicitly.


R is the grants that hold relative to L and G

G{g | (g, p)L, “LG  Perm(p, issue, g)”}

D is {d | gR. “gd  e”}.

Auth(e, L, G) returns
dD Holds(d, L).
27
Problem



Let g = true  Student(Alice),
g’ = x (Student(x)  Perm(x, eat, lunch))
May Alice eat lunch?
Auth(Perm(Alice, eat, lunch), , {g, g’})



Auth sets R, the grants that hold, to {g, g’}.
Auth sets D = {Student(Alice)}, since g’ implies
Perm(Alice, eat, lunch) if Student(Alice) holds.
Auth calls Holds(Student(Alice), ), which returns
false, since Student(Alice) doesn’t follow from .
Auth says no!
28
The fix


To correct the problem, pass G to Holds
and modify Holds to use the new info.
Notice: Bug is easy to find and easy to
fix, but still made it into the released
March 2003 version of the spec.
29
Another bug

Auth(e, , {x (Perm(p, issue, x)  e)})




The set of grants is infinite.



Sets R={x ( Perm(p, issue, x)  e)}
Sets D={Perm(p, issue, g) | g is a grant}
Calls Holds on each dD.
g0 = true  Student(Alice)
gi = true  Perm(Bob, issue, gi-1), i = 1, …
D is infinite. Auth doesn’t terminate.
30
Our fix

Restrict the grants in the language.



If a grant g has a condition d, d mentions
a resource variable x, and x is free in d,
then x is free in g’s conclusion.
Can make an empirical argument for why
this restriction is okay.
Alternative: Restrict the language so
that the set of grants is finite.
31
But that’s not all…
In this small fragment of XrML, there
are 2 other bugs. See paper for
details.
32
The translation


The translation relies on which licenses have
been issued and which grants implicitly hold.
Let sL,G be the translation of any string s wrt
the input parameters L and G.
33
Translation (cont.)

(g, p)L,G = Issued(p, cg).



Assume a constant cg for each grant g.
Perm(p, issue, g)L,G = Perm(p, issue, cg)
Except for grants, rest of translation is
straightforward.
L,G = d L,G  d L,G,
 (d1  d )
1
2
2

Pr(p)L,G = Pr(p), and

trueL,G = true
34
Translating grants

x1…xn(d  e)L,G =
x1…xn (Holds(d, L, G)  eL,G)


Holds(d, L, G) returns true iff d is a logical
consequence of L and G.
Define a modal operator Val, where Val() is
true in a model m iff  is true in all models.
Holds(d, L, G)=Val(L L,G  gG gL,G  dL,G )
35
Correctness

Definition: A good model satisfies



union properties (p1p2 = p2p1, …), and
if Issued(p, g)  Perm(p, issue, g) holds,
then g holds.
Thm: the fixed Auth(e, L, G) returns
true iff LL,G  gG gL,G  eL,G is
true in every good model.
36
Complexity

Determining if a set of XrML grants
imply a conclusion is NP-hard.


This is because the language supports sets
of primitive principals.
If we remove  from the language…


XrML translates (essentially) to Datalog,
which is a well-known tractable language.
Given the translation, finding a tractable,
fairly expressive fragment is easy.
37
Summary


Industry wants to implement XrML but …
XrML has no formal semantics



We give formal semantics to a representative
fragment of XrML.
Even a small fragment is intractable.


and needs them!
We can leverage results in the CS literature to find
fairly expressive, tractable options.
Next step: Add negation to XrML.
38
talk ends on preceding slide
39
Sample XrML policy


Consider the policy `anyone may play
the movie `Big Hit’ for $2 (per use)’.
We could write this policy in XrML as…
40
<license>
<grant> <forAll varName="anyone" />
<!-- This is saying that anyone can use this grant. -->
<principal varRef="anyone" />
<!-- The right to play the movie is granted -->
<cx:play />
<!-- This is the movie that we are giving access to. -->
<cx:digitalWork>
<cx:title>Big Hit </cx:title>
</cx:digitalWork>
<!-- $2.00 each -->
<sx:fee>
<sx:paymentPerUse>
<sx:rate currency="USD">2.00</ sx:rate>
</sx:paymentPerUse
</sx:fee>
</grant>
</license>
41
Auteur
Документ
Catégorie
Без категории
Affichages
4
Taille du fichier
198 Кб
Étiquettes
1/--Pages
signaler