Automated verification of access control policies using a SAT solver |
| |
Authors: | Graham Hughes Tevfik Bultan |
| |
Affiliation: | (1) Computer Science Department, University of California, Santa Barbara, CA 93106, USA |
| |
Abstract: | Managing access control policies in modern computer systems can be challenging and error-prone. Combining multiple disparate
access policies can introduce unintended consequences. In this paper, we present a formal model for specifying access to resources,
a model that encompasses the semantics of the xacml access control language. From this model we define several ordering relations on access control policies that can be used
to automatically verify properties of the policies. We present a tool for automatically verifying these properties by translating
these ordering relations to Boolean satisfiability problems and then applying a sat solver. Our experimental results demonstrate that automated verification of xacml policies is feasible using this approach.
This work is supported by NSF grants CCF-0614002 and CCF-0716095. |
| |
Keywords: | Access control Automated verification |
本文献已被 SpringerLink 等数据库收录! |