Abstract
Automated Verification of Access Control Policies
by: Graham Hughes and Tevfik Bultan
Abstract:
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.
Keywords:
access controls, verification
Date:
September 2004
Document: 2004-22
