Enabling Verification and conformance testing for access control model

Verification and testing are the important step for software assurance. However, such crucial and yet challenging tasks have not been widely adopted in building access control systems. In this paper we propose a methodology to support automatic analysis and conformance testing for access control systems, integrating those features to Assurance Management Framework (AMF). Our methodology attempts to verify formal specifications of a role-based access control model and corresponding policies with selected security properties. Also, we systematically articulate testing cases from formal specifications and validate conformance to the system design and implementation using those cases. In addition, we demonstrate feasibility and effectiveness of our methodology using SAT and Alloy toolset.