Access Control Policy Tool (ACPT), An Assurance Tool That Combines Symbolic Model Checking with Combinatorial Coverage

Presented as part of the 2013 HCSS conference.

ABSTRACT

The correct specification of access control (AC) policies is a very challenging problem. This problem becomes increasingly severe as a system becomes more and more complex, and is deployed to manage a large amount of sensitive or private information and resources. Thus, it is important to provide a tool, which can thoroughly and automatically check the syntactic and semantic faults of AC policies before deploying them for operation. This presentation demonstrates NIST’s effort of developing the tool – Access Control Policy Tool (ACPT), which 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; ACPT assures the efficiency of specified AC policies, and eliminates the possibility of making faulty AC policies that leak the privacy information or prohibit legitimate information sharing.