Automated Verification of Access Control Policies

Managing access control policies in modern computer systems can bechallenging and error-prone, especially when multiple access policiesare combined to form new policies, possibly introducing unintendedconsequences. In this paper we present a framework for automatedverification of access control policies. We introduce a formal modelfor systematically specifying access to resources. We show that theaccess control policies in the XACML access control language can betranslated to a simple form which partitions the input domain to fourclasses: permit, deny, error, and not-applicable. We present severalordering relations for access control policies which can be used tospecify the properties of policies and the relationships among them. Wethen show how to automatically check these ordering relations using anexisting automated analysis tool. In particular, we translate XACMLpolicies to the Alloy language and check their properties using theAlloy Analyzer. Our experimental results demonstrate that automatedverification of XACML policies is feasible.