Rule Based Systems and the Intersection of Formal Methods and Testing

Abstract:

Methods for generating tests from formal models often use model checkers or simulation to serve as a test oracle that determines expected results for a set of test inputs. We describe the derivation of complete test cases from formal access control rules converted to k- DNF structure, using a constraint solver and covering array generator. Two arrays are constructed such that every test in each array should produce the same result, with variations indicating an error. The method has been implemented for testing access control systems with binary grant/deny outputs, but may be generalized for verifying other adaptive rule based systems with a small number of discrete outputs. An interesting aspect of the method is the manner in which the structure of the problem is used to eliminate the need for a conventional test oracle.

Attribute based access control (ABAC) is a method of controlling authorization using rules that include a subject's attributes and possibly changing attributes of the operating environment such as time. For example, a rule may allow access to a resource if the subject's attributes include employee and US_citizen. How should an ABAC system be tested? Confirming that access will be granted for users with any set of rule- specified attributes is easy: we can simply read off the attribute conditions for each grant expression and verify that the access control system returns an authorization in each case. However, with possibly hundreds of attributes, it is much more difficult to ensure that rules have not been implemented such that an unspecified combination of attributes results in authorization that should not be permitted.

To resolve this problem, we use covering arrays of attributes from ABAC policies that have been converted to k-DNF form using a constraint solver. A fixed-value covering array of m variables with v values each - denoted by CA(N, v^m, k) - is an N x m matrix of elements from a set of v symbols {0, 1, ..., (v - 1)} such that every set of k columns contains each possible k-tuple of elements at least once, where the positive integer k is the strength of the covering array (the extension of this definition for variables with different numbers of symbols is straightforward). A disjunctive normal form expression where no term contains more than k literals is referred to as k-DNF. Recall that a term is a conjunction of one or more literals within the disjunction. For example, abc + de contains two terms, one with three literals and one with two, so the expression is in 3-DNF form. The covering array will contain all k-way combinations of variable values. Where an expression is in k-DNF, any term containing k literals that resolves to true will clearly result in the full expression being evaluated to true. Because a covering array of strength k contains every possible setting of all k-tuples and j-tuples for j < k, it contains every combination of values of any k attribute values. For the set of access control rules denoted by R, an array for grant conditions is produced such that each test will instantiate only one term to true. A Deny array is generated as a covering array of strength k, for the set of attributes included in R, with constraints specified by ~R to eliminate from the Deny array all terms that should evaluate to grant. This construction results in an array containing all possible conditions for which the access control system should produce an output of deny.

The structure of access control rule evaluation makes it possible to compress a large number of test conditions into a few tests. Rules for grant conditions are checked in series, then a deny issued only after all grant conditions have been evaluated. Each test in the Grant array contains only one term that results in a grant decision, ensuring that the presence of one grant term does not mask testing another such term in the same test. Terms that should produce a deny, however, can be combined in a single test. For m variables with at most k attribute values in each term, up to terms can be evaluated in each test. If any test in the Deny array produces a grant response, an error has been discovered, which can be repaired before running the test set again.

Because the number of rows in a covering array grows only with log n for n attributes at a given number of attributes and values, the process scales easily to systems with a large number of attributes for k-DNF rules with k < 7 (currently). For example, it is possible to cover all 3-way combinations of 100 boolean attributes with 45 tests, increasing only to 57 tests for 300 attributes. (Variables with more than two values may also be used.) This method has been implemented for rule sets with binary decisions, and we are extending it to cases where more than two outputs are possible.

Bio:

Rick Kuhn is a computer scientist in the Computer Security Division of the National Institute of Standards and Technology. He has authored more than 100 publications on information security, empirical studies of software failure, and software assurance, and is a senior member of the IEEE. He co-developed the role based access control model (RBAC) used throughout industry and led the effort establishing RBAC as an ANSI standard. Before joining NIST, he worked as a systems analyst with NCR Corporation and the Johns Hopkins University Applied Physics Laboratory. He received an MS in computer science from the University of Maryland College Park.