Formal analysis of XACML policies using SMT. Issue 66 (May 2017)

• Record Type: Journal Article
• Authors: Turkmen, Fatih; den Hartog, Jerry; Ranise, Silvio; Zannone, Nicola
• Is Part Of: Computers & security. Issue 66(2017)
• Page Start: 185
• Page End: 203
• Publication Date: 2017-05
• Subjects: XACML policy analysis -- Logic encoding of policy analysis problems -- First-order logic -- Satisfiability modulo theories -- Experimental evaluation; Computer security -- Periodicals; Electronic data processing departments -- Security measures -- Periodicals; 005.805
• DOI: 10.1016/j.cose.2017.01.009
• Languages: English
• ISSNs: 0167-4048

Abstract

Abstract: The eXtensible Access Control Markup Language (XACML) has attracted significant attention from both industry and academia, and has become the de facto standard for the specification of access control policies. However, its XML-based verbose syntax and rich set of constructs make the authoring of XACML policies difficult and error-prone. Several automated tools have been proposed to analyze XACML policies before their actual deployment. However, most of the existing tools either cannot efficiently reason about non-Boolean attributes, which often appear in XACML policies, or restrict the analysis to a small set of properties. This work presents a policy analysis framework for the verification of XACML policies based on SAT modulo theories (SMT). We show how XACML policies can be encoded into SMT formulas, along with a query language able to express a variety of well-known security properties, for policy analysis. By being able to reason over non-Boolean attributes, our SMT-based policy analysis framework allows a fine-grained policy analysis while relieving policy authors of the burden of defining an appropriate level of granularity of the analysis. An evaluation of the framework shows that it is computationally efficient and requires less memory compared to existing approaches.