Suppose we had defined the same sequence of policies, but did not have formal properties to help identify problems introduced at each stage. What can change impact analysis tell us? Remarkably, simply by examining the output of change analysis closely, we can find most of the errors found by formal property analysis.

Since change-impact analysis is meant for use on extensions to stable code, we begin with policy Pol_3, the initial Faculty and Student policy constrained with the singleton and SoD conditions. A user can perform change analysis on this policy against Pol_4 (the buggy addition of TAs) as follows:

(let-xacml-policies ( [prePol_3 "xacml-code/xacmlA/RPSlist.xml"]
                      [prePol_4 "xacml-code/xacmlB/RPSlist.xml"] )
       (let ( [Pol_3 (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_3)))]
              [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)))] )
         (print-comparison-changes (compare-policies Pol_3 Pol_4))))

Note that one must use the two step pattern of first loading the XACML files and then constraining policies. Code of the form:

(let ( [Pol_3 (constraint-policy-disjoint ... (load-xacml-policy "xacml-code/xacmlA/RPSlist.xml"))]
       [Pol_4 (constraint-policy-disjoint ... (load-xacml-policy "xacml-code/xacmlB/RPSlist.xml"))] )
	   ...)

will NOT work since it does not load all the XACML policy files at once. (It makes two calls to load-xacml-policy in one program.)

The output produced from the above code is as follows:

 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/
 11:/Subject, role, TA/

         1         
12345678901
{
00000-01101  N->P
00000-10101  N->P
00001-01101  N->P
00001-10101  N->P
00100-01001  N->P
00100-10001  N->P
00101-01001  N->P
00101-10001  N->P

}

This output is read almost in the exactly same way as the output from the counterexamples in Part I. The only difference is now there is a symbol to the right of each minterm saying to what set the requests in that minterm belong. In the above output, all the minterms belong to the N->P or the NotApplicable goes to Permit set. Other possible sets include P->D (Permit to Deny) and E->P (Excluded by Constraint to Permit). Note that not all requests belong to one these minterm sets. This is since those requests that do not change from one decision to another are not shown. If one used print-comparison to include these requests in the output. They would each get mapped to P->P, D->D, N->N, or E->E.

Now it is clear that all eight changes grant new access since all the minterms have N->P next to the them. Furthermore, four of these changes involve ExternalGrades as indicated by the last four minterms having a '1' under the variable numbered 3 (/Resource, resource-class, ExternalGrades/). A vigilant user would immediately notice something awry, since adding TAs should not have affected external grades in any way. Thus, even in the absence of formal properties, a policy deployer can potentially detect a dangerous leakage of access and make the changes that lead to the correct Pol_5.

Repeating this analysis on Pol_3 and Pol_5 shows changes that involve only TAs and internal grades. Since the changes all correctly grant new permissions, we can now be confident that the TA role in Pol_5 was added correctly to Pol_3.

Since adding TAs should not have involved any changes to ExternalGrades, the user could make this a formal property as was done in verification. Now, however, instead of verifying a property of a policy, he will be verifying a property of the change.

This property of the change can be written as:

(define (external-grades-no-change comp)  
  (avc-false? (avc-and (get-combo-attrVal-involved-in-change 'Resource 'resource-class comp)
                       (make-avc 'Resource 'resource-class 'ExternalGrades))))

The function get-combo-attrVal-involved-in-change returns an AVC representing the set of all combinations of values associated with the attribute resource-class such that that combination shows up in a request whose decision changed from one policy to the next. Thus, we see that AVCs can represent more than just requests. The function then checks that none of these combinations include the value of ExternalGrades

After defining this function, it can be used inside the body of the let-xacml-policies statement where print-comparison-changes was used before.