| margrave |
| Base Module | mzscheme |
| Description | The module holding query functions. Use the Scheme command "(require "Margrave/analysis/margrave.scm")" to include it in your query files. |
|
  
1 Constants |
|
|
| list-of-decision-const |
| Form | list-of-decision-const |
| Description | A list of constants (symbols) used for the decisions.
This include 'P for permit, 'D for deny, 'N for not applicable, and 'E for excluded by constraint |
|
| list-of-change-const |
| Form | list-of-change-const |
| Description | A list of constants that represent all the possible terminals in a comparison
that correspond to a change. For example, 'PD corresponds to the change "Permit goes to Deny".
Note that "changes" like 'PP (permit stays permit) are not in the list since these "changes"
are not really changes. |
|
| list-of-real-change-const |
| Form | list-of-real-change-const |
| Description | Like the list-of-change-const, but only list those changes that will change the
behavior of the PEP. For example, 'ND (not applicable goes to deny) is not in this
list despite being in list-of-change-const since the PEP must reject any request
that yields either not applicable or deny, so the PEP will do the same thing either way. |
|
2 Loading XACML files. |
| There are three ways to load XACML policies into Margrave. Only one
of these ways may be used in any one program due to memory sharing and
assumptions that Margrave use to create a bounded universe of requests.
You must load all the XACML policies that are to be used before using any
of the other Margrave functions.
Use load-xacml-policy if you only have one policy total to load during the
the entire run of the program. Use either load-xacml-policies or
load-xacml-policies-list if you would like to load more than one.
If you are loading more than one, you must load them all in one
application of load-xacml-policies or load-xacml-policies-list. |
|
| load-xacml-policy |
| Form | (load-xacml-policy policy) |
| Type | (string | ast) -> policy |
| Description | Returns one XACML policy ADD after loading it.
Only use if you have exactly one XACML policy to
load during the entire run of the program. |
|
| load-xacml-policies |
| Form | (load-xacml-policies . policies) |
| Type | (string | ast)* -> (listof policy) |
| Description | Returns a list of policies given
some number of policies locations (either file paths or abstract syntax trees). |
|
| let-xacml-policies |
| Form | (let-xacml-policies ( [name loc] ...) body ...)) |
| Type | SYNTAX |
| Description | Syntax that binds identifiers to policies within its body.
The identifies are not bound out side of the bind-xacml-policies's body.
Furthermore, the values to which they are bound (policy ADDs) and any other
ADD values made within the body, cannot be used outside the body.
For example, using set! to bind a policy ADD to an identifier that is
in scope outside of the body, will result in unspecified behavior.
For example:
(let-xacml-policies [ [pol1 "file1.xml"]
[pol2 ast2]
[pol3 "file3.xml"] ]
body-expr_1
body-expr_2
...
body-expr_n)
(define let-xacml-policies 2) ; hack for schemedocs, real def/n below |
|
3 Creating AVCs. |
| Functions for creating attribute value constraints. |
|
| avc-true |
| Form | (avc-true) |
| Description | The constant true AVC. |
|
| avc-false |
| Form | (avc-false) |
| Description | The constant false AVC. |
|
| make-avc |
| Form | (make-avc subtarget attributeId value) |
| Type | (| (sym sym sym -> avc) (sym sym sym sym -> avc) (string -> avc)) |
| Description | Creates an AVC with the given attribute assignments.
If three symbols are given, it assigns the value given as the third argument,
to the attribute given as the second in the subtarget (namespace) given as the first.
This can be seen as representing the set of requests in which the given attribute has
the given value.
If four symbols are given, it returns the AVC in which the attribute of the first two arguments
shares a value with the attribute given in the second two. This can be seen as the set of
requests in which the two given attributes have value in common.
If just a string is given, then that string will create the AVC in which for each '1'
in the string the variable in that position will be true; each '0', false; each '-',
a don't care (i.e., it will include both those with and without it). This is mostly
only useful for pasting in lines from the command print-avc and creating an AVC
represents that one minterm. |
|
| make-avc-singleton |
| Form | (make-avc-singleton subtarget attrId attrValue) |
| Description | Returns the AVC that contains exactly one request,
specifically the request that has only the given attribute value
associated with the given attribute id in the given
subtarget, and no other associations. |
|
| match->avc |
| Form | (match->avc match) |
| Description | Given a match, it will return the corresponding AVC.
Note that (make-avc aSubtarget anAttrId anAttrValue) does return
the same AVC as (match->avc (make-match aSubtarget anAttrId anAttrValue)) |
|
| match->avc-singleton |
| Form | (match->avc-singleton . match-list) |
| Description | Like make-avc-singleton but takes a match instead. |
|
4 AVC Connectives. |
| These mirror the Boolean connectives.
One might find it easier to think of these as set operations
where each AVC is a set of requests or matches.
For example, avc-or may be thought of as a union. |
|
| avc-not |
| Form | (avc-not avc) |
| Type | avc -> avc |
| Description | Returns that complement of the given AVC. |
|
| avc-or |
| Form | (avc-or . l) |
| Type | avc* -> avc |
| Description | Returns the union of the given AVCs. |
| See also | list version | avc-or* |
|
| avc-or* |
| Form | (avc-or* l) |
| Type | (listof avc) -> avc |
| Description | Like avc-or but takes a list of AVCs. |
| See also | non-list version | avc-or |
|
| avc-and |
| Form | (avc-and . l) |
| Type | avc* -> avc |
| Description | Returns the intersection of the given AVCs. |
| See also | list version | avc-and* |
|
| avc-and* |
| Form | (avc-and* l) |
| Type | (listof avc) -> avc |
| Description | Like avc-and but takes a list of AVCs. |
| See also | non-list version | avc-and |
|
| avc-implies |
| Form | (avc-implies if-avc else-avc) |
| Type | avc avc -> avc |
| Description | Returns the avc that implies if an element is in if-avc, then it is in else-avc.
The set of avc that are in else-avc or not in if-avc. |
| See also | closely related | avc-difference |
|
| avc-difference |
| Form | (avc-difference base-avc removed-avc) |
| Type | avc avc -> avc |
| Description | Returns the AVC that is the difference between base-avc and removed-avc.
Removes the elements of removed-avc from base-avc.
{x in base-avc | x not in removed-avc} = base-avc intersect (compl removed-avc) |
| See also | closely related | avc-implies |
|
| disjoint-set |
| Form | (disjoint-set . avc-list) |
| Type | avc* -> avc |
| Description | Produces the AVC that holds all requests that fall into
no more than one of the AVCs given. |
| See also | list version | disjoint-set* |
|
| disjoint-set* |
| Form | (disjoint-set* avc-list) |
| Type | (listof avc) -> avc |
| Description | Produces the AVC that holds all requests that fall into
no more than one of the AVCs given in the list. |
| See also | non-list version | disjoint-set |
|
| partition-set |
| Form | (partition-set . avc-list) |
| Type | avc* -> avc |
| Description | Produces the AVC that holds all requests that fall into
exactly one of the AVCs given. |
| See also | list version | partition-set* |
|
| partition-set* |
| Form | (partition-set* avc-list) |
| Type | (listof avc) -> avc |
| Description | Produces the AVC that holds all requests that fall into
exactly one of the AVCs given in the list. |
| See also | non-list version | partition-set |
|
5 Predicates over AVCs. |
| These check for basic properties of AVCs. |
|
| avc-false? |
| Form | (avc-false? avc) |
| Type | avc -> bool |
| Description | Returns true iff the given AVC is the constant false.
One can view such an AVC as being empty. |
|
| avc-equal? |
| Form | (avc-equal? l r) |
| Type | avc avc -> bool |
| Description | Returns true iff the two given AVCs are equal. |
|
| avc-implication? |
| Form | (avc-implication? l r) |
| Type | avc avc -> bool |
| Description | Returns true iff l implies r.
That is, returns true when l holds all the match sets that r holds (and maybe some more).
One can view this as returning true iff l is a subset of r. |
|
6 Other Predicates. |
|
|
| policy-equal? |
| Form | (policy-equal? l r) |
| Type | policy policy -> bool |
| Description | Tests for the equality of two policies. |
|
| comparison-equal? |
| Form | (comparison-equal? l r) |
| Type | comparison comparison -> bool |
| Description | Test for the equality of two comparisons. |
|
7 Creating Comparisons. |
|
|
| compare-policies |
| Form | (compare-policies policy1 policy2) |
| Type | policy policy -> comparison |
| Description | Compares two policies.
Given two policies, it will merge
the two policies into a comparison that
will list all of the differences between the two
policies. The comparison will be done in the
order in which the policies are provided.
For example:
(compare p1 p2) where p1 denies all requests and p2 permits all requests that would yield a comparison in which everything is mapped to 'DP, the symbol for "deny goes to permits". |
|
8 Quantification. |
| Performs quantification over a match. |
|
| there-exists-for |
| Form | (there-exists-for avc . match-list) |
| Type | avc match* -> avc |
| Description | Makes a BADD badd into E b in bool such that badd[avc -> b].
Existential quantification over an avc:
does there exist a value for this match (has it or does not have it)
such that true is yielded. Maybe a better name would be "don't-care-out-match". |
| See also | list version | there-exists-for* |
|
| there-exists-for* |
| Form | (there-exists-for* avc match-list) |
| Type | avc (listof match) -> avc |
| Description | Makes the given AVC into E b in bool s.t. badd[avc -> b]
Existential quantification over an avc,
does there exist a value for this match (has it or does not have it)
such that true is yielded. |
| See also | non-list version | there-exists-for |
|
| for-all |
| Form | (for-all avc . match-list) |
| Type | avc match* -> avc |
| Description | Like there-exits-for, but performs the for-all* operation. |
| See also | list version | for-all* |
|
| for-all* |
| Form | (for-all* avc match-list) |
| Type | avc (listof match) -> avc |
| Description | Universal quantification over an avc. |
| See also | non-list version | for-all |
|
9 Evaluating Requests. |
| These allow Margrave to act as a PDP or to view things as a PEP does. |
|
| PEP-view |
| Form | (PEP-view policy) |
| Type | policy -> policy |
| Description | The way the policy is enforced by a PEP
(with NA being treated as a deny) |
|
| PDP |
| Form | (PDP policy request) |
| Type | policy * avc -> decision |
| Description | Takes a policy and a request and yields the response a PDP would yield. |
| Returns | A symbol, either 'P, 'D, 'N, 'E, for permit, deny, not applicable, or excluded by constraint, respectively. |
|
10 Restriction. |
| Get the AVC that corresponds to the terminal in which you are interested from a policy or comparison.
If for example you would like to know which requests are mapped to 'P (permit) in a policy named Pol,
you can restrict the policy to 'P with (restrict-policy-to-dec 'P Pol). This will yield the AVC that
holds all the requests that would yield 'P. |
|
| restrict-policy-to-dec |
| Form | (restrict-policy-to-dec decision policy) |
| Type | policy decision -> avc |
| Description | Get the AVC that corresponds to the terminal in which you are interested from a policy or comparison. |
| Parameters | "decision" | "Should be 'P for Permit, 'D for Deny, 'N for NotApplicable, and 'E for ExcludedByConstraint" |
|
| restrict-comparison-to-change |
| Form | (restrict-comparison-to-change change comparison) |
| Type | comparison decision -> avc |
| Description | Get the AVC that corresponds to the terminal in which you are interested from a policy or comparison. |
| Parameters | "change" | "Should be one of the symbols of the form XY where X and Y each P, D, N, or E. The change of PD, for example, means a change from permit to deny." |
|
11 Constraining Policies. |
| Rule some requests out of consideration by introducing environment constraints. |
|
| constrain-policy |
| Form | (constrain-policy request-set policy) |
| Type | policy avc -> policy |
| Description | Constrain a policy to a given request-set.
All requests that are not in the request-set are mapped to EC. |
|
| constrain-policy-disjoint |
| Form | (constrain-policy-disjoint avc-list policy) |
| Type | (listof avc) policy -> policy |
| Description | Returns the policy that applies if only one of the
listed avcs is possible at once. |
|
| constrain-policy-partition |
| Form | (constrain-policy-partition avc-list policy) |
| Type | (listof avc) policy -> policy |
| Description | Like disjoint, but all requests must lay in one of the give avcs. |
| See also | | constrain-policy-disjoint |
|
| make-named-attribute |
| Form | (make-named-attribute subtarget attrId policy) |
| Type | subtarget sym policy -> policy |
| Description | Makes the attribute only associated with values named in the loaded policies.
Rules out the possibility of having the attribute id associated with
values that are not named (given) in any of the loaded policies. These values are represented
by one special value: OTHER. Removes the possibility of that attribute
having the special value of OTHER. Maybe a better name for this function would be
make-named-values-only-attribute. |
|
| make-nonmulti-named-attribute |
| Form | (make-nonmulti-named-attribute subtarget attrId policy) |
| Type | subtarget sym policy -> policy |
| Description | Make-nonmulti-attribute will constrain out any request that associates more than one attribute value
with the given attribute id.
Also constrains out the possibility of the special value OTHER being associates with the given attribute id.
OTHER is constrained out since OTHER actually stands for any natural number of other values, not just one.
For example:
You know that every request will have at most one value associated with the resource-id attribute so place a make-nonmulti-attribute constraint on the policy Pol with "(make-nonmulti-attribute 'Resource 'resource-id Pol)". |
| See also | list version | make-nonmulti-attribute* |
| implies | make-named-attribute |
|
| make-nonmulti-named-attribute* |
| Form | (make-nonmulti-named-attribute* list-s-id policy) |
| Type | (listof (pair subtarget sym)) policy -> policy |
| Description | |
| See also | non-list version | make-nonmulti-attribute |
| implies | make-named-attribute |
|
| make-singleton-named-attribute |
| Form | (make-singleton-named-attribute subtarget attrId policy) |
| Type | policy subtarget sym -> policy |
| Description | Make-single-valued-attribute will constrain out any request that does not associate exactly one attribute value
with the given attribute id.
Also constrains out the possibility of the special value OTHER being associates with the given attribute id.
OTHER is constrained out since OTHER actually stands for any positive number of other values, not just one.
For example:
You know that every request will have exactly one value associates with the resource-id attribute so place a make-nonmulti-attribute constraint on the policy Pol with "(make-singleton-attribute 'Resource 'resource-id Pol)". |
| See also | list version | make-singleton-attribute* |
| implies | make-named-attribute |
|
| make-singleton-named-attribute* |
| Form | (make-singleton-named-attribute* list-s-id policy) |
| Type | (listof (pair subtarget sym)) policy -> policy |
| Description | |
| See also | non-list version | make-singleton-attribute |
| implies | make-named-attribute |
|
12 Reducing AVCs. |
| Reduce an AVC to the parts in which you are interested. |
|
| present-combo-attrValues |
| Form | (present-combo-attrValues subtarget attrId avc) |
| Type | subtarget attrId avc -> avc |
| Description | Returns an AVC representing all the combinations of attribute values found
for the given attribute in the given AVC. |
|
| get-combo-attrVal-involved-in |
| Form | (get-combo-attrVal-involved-in subtarget attrId change cadd) |
| Type | subtarget attrId terminal (| policy comparison) -> avc |
| Description | Returns an AVC representing all the combination of attribute values found
for the given attribute in the given comparison that are involved in the given change. |
| See also | list version | get-combo-attrVal-involved-in* |
|
| get-combo-attrVal-involved-in* |
| Form | (get-combo-attrVal-involved-in* subtarget attrId change-list cadd) |
| Type | subtarget attrId (listof terminal) (| policy comparison) -> avc |
| Description | Returns an AVC representing all the combination of attribute values found
for the given attribute in the given comparison that are involved in any of the given changes. |
| See also | non-list version | get-combo-attrVal-involved-in |
|
| get-combo-attrVal-involved-in-change |
| Form | (get-combo-attrVal-involved-in-change subtarget attrId cadd) |
| Type | cadd subtarget attrId change -> avc |
| Description | Returns an AVC representing all the combination of attribute values found
for the given attribute in the given comparison that are involved in a change |
| See also | list of | list-of-change-const |
|
| get-combo-attrVal-involved-in-real-change |
| Form | (get-combo-attrVal-involved-in-real-change subtarget attrId cadd) |
| Type | cadd subtarget attrId change -> avc |
| Description | Returns an AVC representing all the combination of attribute values found
for the given attribute in the given comparison that are involved in a change
that can effect the action taken by a PEP: |
| See also | list of | list-of-real-change-const |
|
13 Test Functions. |
| These functions are for testing properties of an AVC. These functions mirror the predicates over AVCs.
If a predicate holds, they return true. Otherwise, they yield counter-examples in the form of an AVC.
If an optional fail-func is provided, they will call the fail-func with the counter-examples
if the predicate fails to hold (instead of just returning the counter-examples).
These functions are useful in testing a large number of properties since you can have the return value
of true be ignored while having the fail-func print out which test failed and the counter-example. |
|
| avc-false-test |
| Form | avc-false-test |
| Type | (avc -> #t | avc) | (avc (avc -> a) -> #t | a) |
| Description | If the AVC is not false it calls the fail-func with the given AVC, else true is returned.
(If the AVC is not false, it is itself a counter-example.)
The default fail-func is the identity function, so by default, the non-false AVC is returned. |
| See also | mirrored predicate | avc-false? |
|
| avc-not-empty-test |
| Form | avc-not-empty-test |
| Type | (avc -> #t | avc) | (avc (avc -> a) -> #t | a) |
| Description | If the AVC is false it calls the fail-func with the given AVC, else true is returned.
(If the AVC is false, it is itself a counter-example.)
The default fail-func is the identity function, so by default, the false AVC is returned. |
|
| avc-equal-test |
| Form | avc-equal-test |
| Type | (avc avc -> #t | avc) | (avc avc (avc -> a) -> #t | a) |
| Description | If the two AVCs are equal it calls the fail-func with the difference of the two AVCs,
else true is returned.
The default fail-func is the identity function, so by default, the difference AVC is returned. |
| See also | mirrored predicate | avc-equal? |
|
| avc-implication-test |
| Form | avc-implication-test |
| Type | (avc avc -> #t | avc) | (avc avc (avc -> a) -> #t | a) |
| Description | If the first AVC does not imply the second AVC, the fail-func is called with the difference of the two AVCs,
else true is returned.
The default fail-func is the identity function, so by default, the difference AVC is returned. |
| See also | mirrored predicate | avc-implication? |
|
14 Output. |
Functions for printing string representations of AVCs, policies, and comparisons.
The functions print-avc print-policy print-comparison and print-comparison-changes
all print string representations ADDs to standard output. Since each node in an ADD
has a number corresponding to its place in the ordering of nodes, they all print
the ADD with nodes in order and numbered by that number. First, a list of these nodes
is printed in order giving to what match each node corresponds. Second, list of rows are
printed. Each row consists of list of "0"s, "1"s, and "-"s. The "0"s correspond to the
false (or else) branch of the node whose number is equal to the column number of that symbol
(see the column key at the top of the print out). The "1"s correspond to the true (then) branches
and the "-"s to don't-care. Each row ends in a terminal. A sequence of matches that fit the pattern
of "0"s, "1"s, "-"s in a row is mapped to the terminal at the end of the row.
For example,
1:/Resource, resource-class, paper/
2:/Resource, , review/
3:/
12
{
00 N
01 P
1- D
}
states that a request without the attribute match of resource-class to paper or to review will
receive NotApplicable, one with just the match of resource-class to review will be Permitted,
and one with a match of resource-class to paper will be Denied regardless whether it matches
review or not. |
|
| print-avc |
| Form | (print-avc avc) |
| Type | avc -> |
| Description | Prints an AVC to the standard output port. |
| Returns | void |
|
| print-policy |
| Form | (print-policy policy) |
| Type | policy -> |
| Description | Prints a policy to the standard output port. |
| Returns | void |
|
| print-comparison |
| Form | (print-comparison comparison) |
| Type | comparison -> |
| Description | Prints a comparison to the standard output port. |
| Returns | void |
|
| print-comparison-changes |
| Form | (print-comparison-changes comparison) |
| Type | comparison -> |
| Description | Prints only the parts of a comparison that deal with changes to the standard output port. |
| Returns | void |
|
| print-with-names |
| Form | (print-with-names xradd) |
| Type | xradd -> |
| Description | Prints a XRADD in a different more verbose format.
Note that it takes a long time and great deal of memory.
Thus, it is best to only use on "small" XRADDs,
i.e., ones with few disjuncts (rows when printed with the above methods). |
|
| get-all-attributeIds |
| Form | (get-all-attrIds) |
| Type | -> (listof (listof attrId)) |
| Description | Return a list of lists, where the first list is for subjects,
the second for resources, the third for actions.
Each of these lists holds all the attribute ids found in that subtarget
in one of the policies loaded. |
|
| get-all-attributeValues |
| Form | (get-all-attrValues) |
| Type | -> (listof (listof (pairof attrId, (listof attrValues)))) |
| Description | Return a list of lists, where the first list is for subjects,
the second for resources, the third for actions.
Each these lists hold pairs.
The first element of each pair is an attribute id
and second is a list of all the values associated with that attribute id
somewhere in one of policies loaded. |
|
| get-all-vars |
| Form | (get-all-vars) |
| Description | Returns a list of all the ADD variables made from the parsed policies. |
|
15 Extracting Invariants |
|
|
| print-always-false-vars |
| Form | (print-always-false-vars avc) |
| Description | Given an AVC it will print what constraints on that AVC
always does not hold. |
|
| print-always-true-vars |
| Form | (print-always-true-vars avc) |
| Description | Given an AVC it will print what constraints on that AVC
always hold. |
|
| print-always-irrelevant-vars |
| Form | (print-always-irrelevant-vars avc) |
| Description | Given an AVC it will print what constraints on that AVC
are always irrelevant. I.e., those which are always "don't cares"
This function seems to broken. |
|
16 Measuring Performance. |
|
|
| print-add-resource-use |
| Form | print-add-resource-use |
| Description | Prints the memory usage and size of the ADDs.
Does not give all memory use. Only that which
is being used by the AVC in the underlying CUDD implementation.
Prints to the terminal (not DrScheme). |
|