Sciweavers

Share
STTT
2008

Automated verification of access control policies using a SAT solver

11 years 6 months ago
Automated verification of access control policies using a SAT solver
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. Key words: access control, automated verification
Graham Hughes, Tevfik Bultan
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2008
Where STTT
Authors Graham Hughes, Tevfik Bultan
Comments (0)
books