Access control (AC) systems are among the most critical of information 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. It is common that 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 and more complex, and are deployed to manage a large amount of sensitive information and resources that are organized into sophisticated structures. Identifying discrepancies between policy specifications and their properties (intended function) are 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 provide such confidence, this project will develop a new generation of Access Control Policy Testing (ACPT) tool. The ACPT allows policy authors to conveniently specify access control models (such as RBAC and Multi-Level models) and rules as well as access control properties. From the specified models and rules, the ACPT automatically synthesizes deployable policies and comprehensively tests and verifies the policies against the specified properties, it then reports to the policy authors on the detected problems in the policies to prevent leaving security holes in the policies before deployment. The ACPT will be available to the nation’s policy authors in providing high security confidence levels for their policies.
To formally and precisely capture the security properties that access control should adhere to, AC models are usually written, bridging the rather wide gap in abstraction between policy and mechanism: users see an access control model as an unambiguous and precise expression of requirements; vendors and system developers see access control models as design and implementation requirements. Thus, techniques are required for verifying whether an AC models are correctly expressed in the AC policies and whether the properties are satisfied in the model. In practice, the same access control policies may express multiple different 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 non-trivial and critical task. However, the correct specification of access control 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.
ACPT allows users to specify access control (AC) models and rules or their combinations, as well as the expected properties through GUI. ACPT then performs logic check to verify if the specified properties conform to the specified models/rules. If not, non-conformance messages are returned to the user, otherwise, ACPT proceeds to generate test cases, which are ready for property verification testing of the AC application implemented according to the models/rules. ACPT is a reference implementation of the NIST’s research project: “Verification of Generic Access Control Model” with more extended capabilities. The following figure shows the architect of the ACPT.
ACPT is directly applicable to those types of access control policies whose profiles are already provided, such as (core and hierarchical) Role Based Access Control (RBAC), Chinese Wall, Multi-level, hierarchical-resource-based policies, web service policies, SAML, WS-Security policy, and privacy policies as well as other rule-based access control policies. For example, a firewall policy is a type of rule-based policies, being used to examine every incoming or outgoing packet and decide whether to permit or deny it. The results of the project will not only deeper our understanding of verifying access control policies against models/rules and their properties, but also provide a practical set of techniques and prototypes to support systematic conformance verification of access control policies.
In regard to cyber security, privacy, and information sharing, access control is one of the crucial elements in protecting the nation’s critical IT infrastructures for healthcare, transportation, financial, power grids, military, intelligence, and safety systems, etc. It is essential to have measurement technology such as ACPT for access control policy administrators and authors to ensure the safety and flexibility in composing their access control policies. Thus, the developing of ACPT meets the mission of Computer Security Division according to the Federal Information Security Management Act of 2002 (FISMA). NIST should develop this system, because so far, there is no project or research similar to the ACPT. And NIST has significant experience and has great success in developing and transferring access control technologies. This is reflected by performing research and development in this area for over 18 years.
Additional Technical Details:
http://nusmv.fbk.eu/ for NuSMV 2.2 Tutorial, a new symbolic model checker.
In addition to research papers (see Selected Publications), ACPT has been concept proved with a prototype implementation. Deployable version is under construction.
Lead Organizational Unit:itl
Related Programs and Projects:
For more information regarding the Automated Combinatorial Testing (ACTS), please visit the Computer Security Resource Center (CSRC).
Vincent C. Hu
100 Bureau Drive