Standard

Formal analysis of XACML policies using SMT. / Turkmen, Fatih; den Hartog, Jerry; Ranise, Silvio; Zannone, Nicola.

In: Computers and Security, Vol. 66, 01.05.2017, p. 185-203.

Research output: Scientific - peer-reviewArticle

Harvard

Turkmen, F, den Hartog, J, Ranise, S & Zannone, N 2017, 'Formal analysis of XACML policies using SMT' Computers and Security, vol 66, pp. 185-203. DOI: 10.1016/j.cose.2017.01.009

APA

Turkmen, F., den Hartog, J., Ranise, S., & Zannone, N. (2017). Formal analysis of XACML policies using SMT. Computers and Security, 66, 185-203. DOI: 10.1016/j.cose.2017.01.009

Vancouver

Turkmen F, den Hartog J, Ranise S, Zannone N. Formal analysis of XACML policies using SMT. Computers and Security. 2017 May 1;66:185-203. Available from, DOI: 10.1016/j.cose.2017.01.009

Author

Turkmen, Fatih; den Hartog, Jerry; Ranise, Silvio; Zannone, Nicola / Formal analysis of XACML policies using SMT.

In: Computers and Security, Vol. 66, 01.05.2017, p. 185-203.

Research output: Scientific - peer-reviewArticle

BibTeX

@article{c02756ed23014af0b39595454655565c,
title = "Formal analysis of XACML policies using SMT",
keywords = "Experimental evaluation, First-order logic, Logic encoding of policy analysis problems, Satisfiability modulo theories, XACML policy analysis",
author = "Fatih Turkmen and {den Hartog}, Jerry and Silvio Ranise and Nicola Zannone",
year = "2017",
month = "5",
doi = "10.1016/j.cose.2017.01.009",
volume = "66",
pages = "185--203",
journal = "Computers and Security",
issn = "0167-4048",

}

RIS

TY - JOUR

T1 - Formal analysis of XACML policies using SMT

AU - Turkmen,Fatih

AU - den Hartog,Jerry

AU - Ranise,Silvio

AU - Zannone,Nicola

PY - 2017/5/1

Y1 - 2017/5/1

N2 - 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.

AB - 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.

KW - Experimental evaluation

KW - First-order logic

KW - Logic encoding of policy analysis problems

KW - Satisfiability modulo theories

KW - XACML policy analysis

UR - http://www.scopus.com/inward/record.url?scp=85012256157&partnerID=8YFLogxK

U2 - 10.1016/j.cose.2017.01.009

DO - 10.1016/j.cose.2017.01.009

M3 - Article

VL - 66

SP - 185

EP - 203

JO - Computers and Security

T2 - Computers and Security

JF - Computers and Security

SN - 0167-4048

ER -

ID: 32863826