The process starts with developing a policy. The first policy is:

This natural-language policy must next be translated into XACML. The resulting XACML policy may be seen here. Note that the XACML policy is much more complicated than the natural-language policy. The author might be fearful that errors occurred while producing the XACML policy. Even if the natural-language policy is correctly translated into XAMCL, the author might still worry that the policy has unintended consequences.

To assuage these fears, the policy administrator can enumerate a set of properties that the policy must obey to be correct. In this policy the following properties are to hold:

1. There do not exist members of Student who can Assign ExternalGrades.
2. All members of Faculty can Assign both InternalGrades and ExternalGrades.
3. No combination of roles exists such that a user with those roles can both Receive and Assign the resource ExternalGrades.

Now all one must do is ensure that the properties hold under the given XACML policy. That is where Margrave steps in.

First one must load the XACML policy in question into Margrave. Assuming the that the base file (top most) of the XACML policy is xacmlA/RPSlist.xml, it can be loaded with the command:

(define Pol_1 (load-xacml-policy "xacmlA/RPSlist.xml"))

Note that if more than one policy had to be loaded (as will be the case with change-impact analysis), the command load-xacml-policies or the binding form let-xacml-policies should be used to load all the policies at once. Make sure to read documentation page for more information on correctly loading an XACML policy.

Next, one formalizes the properties that are to be verified by Margrave. The above properties are formalized for Margrave as (given in the same order as above):

1. (define (Pr_1 policy)
     (avc-false? (avc-and (restrict-policy-to-dec 'P policy)
   			(avc-and (make-avc 'Subject 'role 'Student)
   			         (make-avc 'Resource 'resource-class 'ExternalGrades)
   			         (make-avc 'Action 'command 'Assign)))))

   This ensures the no request falls into both the set of requests that include the role Student, resource-class ExternalGrades, and command Assign and the set of requests that are permitted. The expression (restrict-policy-to-dec 'P policy) returns the AVC (in this case, a representation of a set of requests) that corresponds to all the requests that are permitted under the policy policy. To get the set of all denied policies, replace the 'P with 'D. For the set of all requests to which the policy does not apply (i.e., would result in the decision of NotApplicable under this policy), use 'NA. The symbol 'E can be used for Excluded by Constraint. What that means will be explained shortly.

2. (define (Pr_2 policy)
     (avc-implication? (avc-and (make-avc 'Subject 'role 'Faculty)
                                (avc-or (make-avc 'Resource 'resource-class 'InternalGrades)
                                        (make-avc 'Resource 'resource-class 'ExternalGrades))
                                (make-avc 'Action 'command 'Assign))
                       (avc-or (restrict-policy-to-dec 'P policy)
                               (restrict-policy-to-dec 'E policy))))

   This is implemented by checking to ensure that all requests that include the role Faculty, either the resource-class InternalGrades or ExternalGrades and the command Assign are either within the set of permitted requests or the set of excluded requests. Although currently no requests are excluded, it is important to rule out the excluded requests in such properties since, as we will see shortly, not all requests matter. If we failed to deal with the excluded requests, the property might have failed since some request for say a faculty member assigning an external grades was not permitted, but rather excluded.

3. (define (Pr_3 policy)
      (let [ [assign (avc-and (restrict-policy-to-dec 'P policy)
                              (avc-and (make-avc 'Resource 'resource-class 'ExternalGrades)
   	                            (make-avc 'Action 'command 'Assign)))]
   	  [receive (avc-and (restrict-policy-to-dec 'P policy)
   			    (avc-and (make-avc 'Resource 'resource-class 'ExternalGrades)
   				     (make-avc 'Action 'command 'Receive)))] ]
        (avc-false? (avc-and (present-combo-attrValues 'Subject 'role assign)
   			  (present-combo-attrValues 'Subject 'role receive)))))

   This is implemented by first getting the set of requests that can Assign ExternalGrades (assign) and the set of requests that can Receive ExternalGrades (receive). Then we check that the intersection between the set of role combinations found in each set of requests is empty.

Margrave can now be used to verify that the properties hold or not. The following code will test the properties: (Pr_1 Pol_1) (Pr_2 Pol_1) (Pr_3 Pol_1). It shows that Pr_1 and Pr_3 do not hold. Knowing why the properties do not hold is the next step.

To see counterexamples to the properties the following Margrave queries may be used:

1. (define (find-Pr_1-counter-example policy)
   		    (avc-and (restrict-policy-to-dec 'P policy)
   			     (avc-and (make-avc 'Subject 'role 'Student)
   				      (make-avc 'Resource 'resource-class 'ExternalGrades)
   				      (make-avc 'Action 'command 'Assign))))

2. (define (find-Pr_2-counter-example policy)
   		    (avc-difference (avc-and (make-avc 'Subject 'role 'Faculty)
   					     (avc-or (make-avc 'Resource 'resource-class 'InternalGrades)
   						     (make-avc 'Resource 'resource-class 'ExternalGrades))
   					     (make-avc 'Action 'command 'Assign))
   				    (avc-or (restrict-policy-to-dec 'P policy)
   					    (restrict-policy-to-dec 'E policy))))

3. (define (find-Pr_3-counter-example policy)
   		    (let [ [assign (avc-and (restrict-policy-to-dec 'P policy)
   					    (avc-and (make-avc 'Resource 'resource-class 'ExternalGrades)
   						     (make-avc 'Action 'command 'Assign)))]
   			   [receive (avc-and (restrict-policy-to-dec 'P policy)
   					     (avc-and (make-avc 'Resource 'resource-class 'ExternalGrades)
   						      (make-avc 'Action 'command 'Receive)))] ]
   		      (avc-and (present-combo-attrValues 'Subject 'role assign)
   			       (present-combo-attrValues 'Subject 'role receive))))

Each of these will return the empty set if no counter-example can be found (and thus the property holds). They are applied to the policy as follows: (print-avc (find-Pr_1-counter-example Pol_1)) (print-avc (find-Pr_2-counter-example Pol_1)) (print-avc (find-Pr_3-counter-example Pol_1)). A file that holds all this code and shows how to combine it into an easy to use test suit is here.

As indicated above, (find-Pr_2-counter-example Pol_1) returns the empty set while the other two applications return actual counter-examples. The output for find-Pr_1-counter-example looks like:

 1:/Action, command, Receive/
 2:/Action, command, OTHER/
 3:/Resource, resource-class, ExternalGrades/
 4:/Resource, resource-class, OTHER/
 5:/Subject, role, Student/
 6:/Subject, role, OTHER/
 7:/Action, command, View/
 8:/Action, command, Assign/
 9:/Resource, resource-class, InternalGrades/
 10:/Subject, role, Faculty/

         1         
1234567890
{
0-1-1--1-1  
1-1-1--1--  

}

It consists of two parts: the key given above and the actually minterm representation of the counterexamples given below. The key lists all the variables created for the policy. For example, the first variable is 1:/Action, command, Receive/ this variable is has the value of

• '1' iff all requests in the represented set has the value of Receive associated with attribute command of the Action subtarget.
• '0' iff none of the requests in the represented set has the value of Receive associated with attribute command of the Action subtarget.
• '-' iff membership in the represented set does not depend on if the value of Receive is associated with attribute command of the Action subtarget. That is, this variable is irrelevant.

One can find the value of the variable in each by looking at the representation given below the key. This representation consists of a set of rows of '1's, '0's, and '-'s that are in between the '{' and '}'. The row of numbers above the '{' number the columns. The column with number i is associated with the variable numbered i. For example, in the above output, the value of '0' is below the number 1 in the first minterm row. Thus, since /Action, command, Receive/ is the variable assigned to the number 1 by the key, we know that no requests has the value Receive for Action command in this minterm. Similarly, the value of '1' is assigned to variable 3: /Resource, resource-class, ExternalGrades/ in this minterm. The value of '1' is also assigned to variable 1 in the second minterm.

Each minterm row represents a set of requests. The overall set of requests represented by the printout is the union of all the minterm sets of requests. A printout with no minterms represents the empty set.

Now that we know how to read the output, we can figure out what it tells us about the policy.

The counter-examples indicates that a student can request to receive an external grade (which Pol_1 permits) while simultaneously assigning an external grade (about which Pol_1 is silent, which implies access will not be granted). This is clear from the second minterm since there is a '1' under both variable 1 (/Action, command, Receive/) and 8 (/Action, command, Assign/). In effect, an illicit request is piggy-backing atop a legitimate one, and exploiting an underspecification in the policy. This reflects a subtlety of XACML: the language specification states that an attribute (here, the command attribute) represents an arbitrary set of values, not necessarily singletons.

The policy author must sometimes make the policy more elaborate to guard against such requests. In other cases, the author can presume that generated requests will include only a single value for certain attributes. To instruct Margrave about this presumption, the author can employ a general Margrave mechanism called an environment constraint. These are analogous to the environment models used in model checking, which bound the behaviors of the system by explicating details of the operating context in which the model will execute.

Returning to our example, we constrain the attributes governing the action and requested resource to be singletons (Pol_2) as follows:

(make-singleton-named-attribute 'Action 'command
                                 (make-singleton-named-attribute 'Resource 'resource-class
                                                                 Pol_1))

While this addresses the property violations above, this constrained policy still violates Pr_1 and Pr_3. The (sole) counter-example to Pr_3 shows that a member of Faculty can also be a Student:

 1:/Action, command, Receive/
 2:/Action, command, OTHER/
 3:/Resource, resource-class, ExternalGrades/
 4:/Resource, resource-class, OTHER/
 5:/Subject, role, Student/
 6:/Subject, role, OTHER/
 7:/Action, command, View/
 8:/Action, command, Assign/
 9:/Resource, resource-class, InternalGrades/
 10:/Subject, role, Faculty/

         1         
1234567890
{
----1----1  

}

This naturally triggers violations -- which is really a violation of the principle of separation-of-duty (SoD). Fortunately, this separation is easy to encode with another environment constraint:

(constrain-policy-disjoint (list (make-avc 'Subject 'role 'Faculty)
                                 (make-avc 'Subject 'role 'Student))
                           Pol_2)

The resulting policy Pol_3 satisfies all three properties.

For the next generation of policy, we add teaching assistants (TAs). Since TAs have some of a faculty member's privileges (while still being students), a careless implementation gives them the same rights as faculty. This implementation can be found in xacmlB/RPSlist.xml (see it here ). It is loaded and the constrained as above by the following command:

(define prePol_4 (load-xacml-policy "xacmlB/RPSlist.xml"))
(define Pol_4
   (constrain-policy-disjoint
		   (list (make-avc 'Subject 'role 'Faculty)
			 (make-avc 'Subject 'role 'Student))
		   (make-singleton-named-attribute
		    'Action
		    'command
		    (make-singleton-named-attribute
		     'Resource
		     'resource-class
                     prePol_4))))

Note that we first load the policy (and bind it to prePol_4) and then constrain it. This is since all policies must be loaded before any constraints are applied to any policy or AVCs made.

Margrave catches this error by reporting a violation of Pr_1 and Pr_3. The sole counter-example shows that a student with the freedom to assign external grades is also a TA but not a faculty member. Thus we define Pol_5 to be:

See the XACML policy here. Margrave establishes that this policy implementation (stored as xacmlC/RPSlist.xml) successfully satisfies all the properties.