source: doc/design @ da73657

mei_rt2mei_rt2_fix_1
Last change on this file since da73657 was 2efdff5, checked in by Mei <mei@…>, 12 years ago

1) fix the missing check for 'This' rt2.y when called from creddy/prover

combo

2) patch up the stringify of abac_term that is of time type.
3) update the testing to reflect the changes to baseline output

  • Property mode set to 100644
File size: 11.5 KB
Line 
1OVERVIEW
2
3ABAC proves attributes about principals.
4
5libabac is comprised of three main types of objects: credentials, roles/osets,
6and contexts.
7
8A typical use of ABAC is:
9
10    - create a context
11    - load some certificates
12    - add more certificates, possibly presented by another party
13    - make a query 'does principal B have the role A.r1?'
14         or a query 'is object B part of the oset A.o1?'
15
16CREDENTIAL
17
18An ABAC credential is the most basic unit of an ABAC proof.
19
20It is a signed assertion by a principal A that some other entity has a
21role r1.  Abstractly, it is one of the following (A, B principals;
22r1, r2, r3 roles):
23
24    A.r1 <- B
25    A.r1 <- B.r2
26    A.r1 <- B.r2.r3
27
28It is a signed assertion by a principal A that some other entity is
29an object of oset o1. (A, B principals; r1 role; o1, o2 osets; O object):
30
31    A.o1 <- O
32    A.o1 <- B.o2
33    A.o1 <- B.r1.o2
34
35
36When interacting with libabac, a credential is represented by an X509
37attribute certificates and the associated issuer X509 identity
38certificate.
39
40A principal is represented by the SHA1 hash of the public key of its
41identity certificate. Therefore when a credential is encoded in an
42attribute certificate, it will look something along the lines of:
43
44    e65aace9237833ec775253cfde97f59a0af5bc3d.frobnicate <-
45        e93547826455a80d9488825a1d083ef6ef264107
46
47ROLE
48
49ABAC roles are the atomic units that form the head and tail of a
50credential. The head will always be a proper role, which is to say it
51takes form:
52
53    A.r1
54
55As seen in the CREDENTIAL section, the tail of a role can take one of
56three forms:
57
58    principal:      B
59    role:           B.r2
60    linking role:   B.r2.r3
61
62For more information about the different types of roles, refer to
63[Li03rt].
64
65OSET
66
67ABAC osets are the atomic units that form the head and tail of a
68credential. See the RT2 description for how osets and roles differ.
69The head will always be a proper oset, which is to say it
70takes form:
71
72    A.o1
73
74As seen in the CREDENTIAL section, the tail of a oset can take one of
75three forms:
76
77    object:         O
78    oset:           B.o2
79    linking oset:   B.r2.o3
80
81
82CONTEXT
83
84An ABAC context object encapsulates a set of ABAC credentials and its
85associated YAP clause db. The context supports the following operations:
86
87    - load X509 identity certificate
88    - load X509 attribute certificate
89    - list all the credentials (attribute identity certificate pairs)
90    - query whether a principal has a given role
91    - query whether an object belongs to a given o-set
92
93RT2
94
95RT2 is a more expressive logic than the original RT0 logic that ABAC
96supported.
97
98The RT2 specification extends the existing RT0 notation in 5 ways:
99
100        * More general principal specification to allow room for other
101          identity providers
102        * Explicit syntax for specifying RT2 objects
103        * Explicit type information to differentiate roles and o-sets.
104        * Explicit type information for RT1 and RT2 parameters
105        * Syntax for constraints
106
107These additions make the syntax both much less terse and much less
108ambiguous.
109
110A few words about RT1 and RT2 before we describe syntax.  RT1 parameterizes
111roles, that is, it attaches ordered, typed data to roles.  It also adds
112matching requirements to role derivations, including constraints.  The
113RT1 rule
114
115A.r(?x, ?y) <- A.s(1, ?y:[1..3]) & A.t(?y, ?x)
116
117requires that all instances of ?x and ?y on the right side have the same
118type and that the constraints on ?y in the first term are valid for that
119type.  There's no explicit typing in the rule notation of the papers,
120which this specification addresses.
121
122The data types in the papers inlcude integers, floats, dates, closed
123enumerations, and open enumerations.  Closed enumerations are things
124like C or C++ enums, with boolean being a specific example.  Open
125enumerations include things like principals.  For tractability we're
126going to want to define a specific set of data types, which we do
127below.
128
129RT2 allows principals to label data in the same way that they label
130principals.  The ABAC authors helpfully use the exact same syntax for
131assigining a label to a data object as they do for assigning a role to a
132principal, but the semantics are slightly different.  We add syntax
133that clarfies when data is being labelled and when principals are being
134labelled.  These "data roles" are called o-sets.
135
136On with the specification, from the basic chunks up to rules.
137
138Principal Names
139
140We've been using self-signed X.509 identity certificates as identities,
141and that's been a useful way to get started, but it would be nice to be
142able to use other identities in the future.  Now a principal name is not
143marked in the representation at all.  New principal IDs will be of the
144form: [idtype:A].  The idtype will define what valid characters in A
145will be, but in any event "]" must be escaped with a backslash.
146
147The current id's will be of idtype 'keyid', so only applying the
148principal extensions, the role A.r would be written [keyid:A].r, where A
149is the sha1 hash of the public key.  keyid principal names can include
150[0-9a-fA-F] (hex digits).
151
152I'm going to continue to use [keyid:A] here so not everything runs off
153the page.
154
155Data Objects
156
157The RT1 and RT2 parameters are loosely data objects.  RT1 allows one to
158reason about them, RT2 adds the ability to have principals make
159statements about these data objects.  Just as we need to represent
160principals including their type, we need to represent objects with their
161type.  We support following types:
162
163        int: 32-bit signed integers
164        float: floats in the range of an IEEE float.
165        time: a time expressed as yyyymmddThhmmss where the lower case
166                letters are digits and the T is a T.  Zulu time,
167                everything after the T is optional
168        boolean: true or false
169        urn: a resource named by a URN
170        string: a UTF-8 string.  This is a free space for people to
171                define local free-form attributes
172
173A particular object is specified by:
174
175[ type: name]
176
177Objects are always specified this way, because rules and assignments may
178come from many places and the typing information must mesh.
179
180Examples:
181
182        [boolean: true]
183        [int: 3454]
184        [float: -323.0] also [ float: 1]
185        [time: 20111109T122300] also [ time: 20101010T]
186        [urn:"file:///usr/local/bin/ls"]
187        [urn:"uuid://106c0cdd-0afb-11e1-90d8-14feb5e4012d"]
188        [string:"a string"]
189
190Roles and O-Sets
191
192In the ABAC papers, roles and o-sets look exactly alike, and one may
193have trouble understanding that they are different.  This spec
194explicitly types them for clarity.  Roles are prefixed by "role:" and
195o-sets by "oset:".
196
197The rule that places principal P in role A.r is written in the paper as
198
199A.r <- P
200
201In our notation:
202
203[keyid:A].role:r <- [keyid:P]
204
205The rule that places file P in o-set A.r is written in the paper as
206
207A.r <- P
208
209In our notation:
210
211[keyid:A].oset:r <- ["urn:file://P"]
212
213Similarly derivation rules like:
214
215A.r <- B.r
216
217become
218
219[keyid:A].role:r <- [keyid:B].role:r
220
221or
222
223[keyid:A].oset:r <- [keyid:B].oset:r
224
225depending on their intent.  It is an error to try (or probably to think):
226
227[keyid:A].oset:r <- [keyid:B].role:r
228
229Note also that
230
231[keyid:A].oset:os <- [keyid:B].role:r.oset:os
232
233Is the only valid linking credential for assigning o-sets.
234[keyid:B].role:r is a set of principals that may have defined an o-set
235(oset:os), but the members of an o-set could not have done so.
236
237Variables
238
239Both RT1 and RT2 allow rules defining roles or o-sets to match
240parameters using variable bindings.  We illustrate with roles here,
241though all of this holds for o-sets.  The variables may be named to
242specify connections between the role to be defined and the roles used to
243define it.
244
245For example the rule (in paper notation):
246
247A.evaluatorOf(?x) <- A.managerOf(?x)
248
249means that if
250
251A.managerOf(mikeryan) <- faber
252
253then
254
255A.evaluatorOf(mikeryan) <- faber
256
257is also true.  The two ?x es bind to the same thing.  For more complex
258rules, we have to make sure that the types are also consistent:
259
260A.example(?x) <- A.isInteger(?x) & A.isFloat(?x)
261
262?x is not allowed to match an integer-typed data object in the first
263clause and a float-typed one in the second.  The papers say this is an
264invalid rule, but without knowing the types of the parameters it cannot
265be checked.
266
267We adopt the same variable naming convention, but require them to be
268prefixed with the types above.  Variable names start with a ?, followed
269by a capitalized character and can contain [_\-a-zA-Z0-9], that is,
270alphanumerics, underscore and the hyphens.  ? is a valid anonymous
271variable name.  Multiple instances of ? in the same rule can bind to
272different types.
273
274This is OK:
275
276[keyid:A].role:weird([urn:?X]) <- [keyid:B].role:a([urn:?X], [int:?]) &
277        [keyid:C].role:b([urn:?X], [boolean:?])
278
279Other examples:
280
281[keyid:A].role:example([int:?X]) <- [keyid:A].role:isInteger([int:?X]) &
282        [keyid:A].role:isFloat([int:?X])
283
284is valid
285
286[keyid:A].role:example([int:?X]) <- [keyid:A].role:isInteger([int:?X]) &
287        [keyid:A].role:isFloat([float:?X])
288
289is not, because the types of ?X are different.
290
291
292In addition to the data object types, the "principal" type is allowed as
293well, indicating that the variable must match an ABAC principal.  The
294first example in this section is written:
295
296[keyid:A].role:evaluatorOf([principal:?X]) <-
297        [keyid:A].role:managerOf([principal:?X])
298
299A special keyword "this" for principal type can be used as a data term.
300It is translated into an implicit principal variable and all appearances
301of "this" data term refer to the same binding within the credential.
302
303Constraints
304
305A constraint is a static (RT1) or dynamic (RT2) set of valid choices for
306a parameter.  There are two kinds of constraint sets, static and
307dynamic.  A dynamic constraint set is an o-set or role.  Static
308constraint sets are a list of valid values.  Constraints are separated
309from a variable name by a colon (:).
310
311We specify a static set by enclosing the values in [] separated by
312commas.  Because the set is bound to a typed variable, the values
313in the set can omit the [type:], so we write:
314
315[keyid:A].role:r([int:?X:[1,3,5])
316
317not
318
319[keyid:A].role:r([int:?X:[[int:1],[int:3],[int:5]]])
320
321For ordered sets like integers, floats and dates, the .. sequence
322specifies a range:
323
324[keyid:A].role:r(int:?X:[1..5])
325
326in static constraint sets, commas, elipses (..), and the bracket
327characters [, ] must be escaped using a backslash (\) prefix.
328
329The constraint can also be an o-set (for objects) or a role (for a principal).
330Variable name is not syntactically separated from o-set/role constraint
331with a colon.
332
333[keyid:A].role:r([principal:?X[[keyid:A].role:r1])
334[keyid:A].role:r([urn:?X[[keyid:A].oset:o1])
335
336A Complex Example
337
338The example on p. 10 of "Design of a Role-Based Trust Management
339Framework" starts with the rule
340
341Alpha.fileAc(read, ?F:Alpha.documents(?proj)) <- Alpha.team(?proj)
342
343and says that given
344
345Alpha.documents(proj1) <- fileA
346Alpha.team(proj1) <- Bob
347
348one can conclude
349
350Alpha.fileAc(read, fileA) <- Bob
351
352In our notation the initial rule is encoded (note the mingling of o-sets
353and roles)
354
355[keyid:Alpha].role:fileAc([string:"read"],
356        [string:?F:[keyid:Alpha].oset:documents([string:?proj])])
357                <- [keyid:Alpha].role:team([string:?proj])
358
359and given
360
361[keyid:Alpha].oset:documents([string:"proj1"]) <- [string:"fileA"]
362[keyid:Alpha].role:team([string:"proj1"]) <- [keyid:Bob]
363
364one can conclude
365
366[keyid:Alpha].role:fileAc([string:"read"], [string:"fileA"]) <- [keyid:Bob]
367
368It is more verbose, but draws out the different roles and o-sets in
369play. 
370
371REFERENCES
372
373[Li03rt]
374    Li, N. and Mitchell, J. C. RT: A role-based trust-management
375    framework. In Proceedings of the Third DARPA Information
376    Survivability Conference and Exposition. IEEE Computer Society
377    Press, 201­212.
378
379
380
381http://groups.geni.net/geni/wiki/TIEDABACModel
382
383http://groups.geni.net/geni/wiki/TIEDABACDemo
Note: See TracBrowser for help on using the repository browser.