Access control systems are among the most critical security components. Faulty policies, misconfigurations, or flaws in software implementation can result in serious vulnerabilities. The specification of access control policies is often a challenging problem. Often a system’s privacy and security are compromised due to the misconfiguration of access control policies instead of the failure of cryptographic primitives or protocols. This problem becomes increasingly severe as software systems become more complex, and are deployed to manage a large amount of sensitive information and resources organized into sophisticated structures. Identifying discrepancies between policy specifications and their properties (intended function) is crucial because correct implementation and enforcement of policies by applications is based on the premise that the policy specifications are correct. As a result, policy specifications must undergo rigorous verification and validation through systematic testing to ensure that the policy specifications truly encapsulate the desires of the policy authors.

To formally and precisely capture the security properties that access control should adhere to, access control models are usually written to bridge the rather wide gap in abstraction between policy and mechanism. Thus, an access control model provides unambiguous and precise expression as well as reference for design and implementation of security requirements. Techniques are required for verifying whether an access control model is correctly expressed in the access controls policies and whether the properties are satisfied in the model. In practice, the same access control policies may express multiple access control models or express a single model in addition to extra access control constraints outside of the model. Ensuring the conformance of access control models and policies is a nontrivial and critical task.

Started in 2009, NIST CSD developed a prototype system, Access Control Policy Tool (ACPT), which allows a user to compose, verify, test, and generate access control policies. ACPT provides (1) GUI templates for composing AC policies, (2) property checking for AC policy models through an SMV (Symbolic Model Verification) model checker, (3) complete test suite generated by NIST’s combinatorial testing tool ACTS, and (4) XACML policy generation as output of verified model. Through the four major functions, ACPT performs all the syntactic and semantic verifications as well as the interface for composing and combining AC rules for AC policies. In addition, CSD published research papers related to ACPT.

Most research on AC model or policy verification techniques are focused on one particular model, and almost all of the research is in applied methods, which require the completed AC policies as the input for verification or test processes to generate fault reports. Even though correct verification is achieved and counter examples may be generated along with found faults, those methods provide no information about the source of rule faults that might allow conflicts in privilege assignment, leakage of privileges, or conflict of interest permissions. The difficulty in finding the source of faults is increased especially when the AC rules are intricately covering duplicated variables to a degree of complexity. The complexity is due to the fact that a fault might not be caused by one particular rule; for example, rule x grants subject/attribute s access to object/attribute o, and rule y denies the group subject/attribute g, which s is a member of, access to object o. Such conflict can only be resolved by removing either rule x or y, or the g membership of s from the policy. But removing x or yaffects other rules that depend on them (e.g., a member of subject group g k is granted access to object o), and removing s’s membership in g will disable g‘s legitimate access to other objects/attributes through the membership. Thus, it requires manually analyzing each rule in the policy in order to find the correct solution for the fault.

To address the issue, CSD researched the AC Rule Logic Circuit Simulation (ACRLCS) technique, which enables the AC authors to detect a fault when the fault-causing AC rule is added to the policy, so the fixing can be implemented in real time before adding other rules that further complicate the detecting effort. Rather than checking by retracing the interrelations between rules after the policy is completed, the policy author needs only check the newly added rule against previous “correct” ones. In ACRLCS, AC rules are represented in a Simulated Logic Circuit (SLC). The use of simulation may restrict ACRLCS implementation on a physical electronic circuit; however, the concept can be implemented and computed through simulated software.

In addition to AC tools, this paper presents a result of evaluating generic AC policy verification mechanisms. The evaluation is based on a set of reference metrics for analyzing and sets of oracles and test cases for empirically checking of the run-time capability and performance of AC verification tools.