Enabling verification and conformance testing for access control model

Abstract

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 sys-tems. In this paper we propose a methodology to sup-port automatic analysis and conformance testing for ac-cess control systems, integrating those features to Assur-ance Management Framework (AMF). Our methodology at-tempts to verify formal specifications of a role-based access control model and corresponding policies with selected se-curity 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.