Analysis of XACML policies with SMT

F. Turkmen, J.I. Hartog, den, S. Ranise, N. Zannone

Research output: Book/ReportReportAcademic

Abstract

The eXtensible Access Control Markup Language (XACML) is an extensible and flexible XML language for the specification of access control policies. However, the richness and flexibility of the language (along with the verbose syntax of XML) come with a price: errors are easy to make and difficult to detect when policies grow in size. If these errors are not detected and rectified, they can result in serious data leakage and/or privacy violations leading to significant legal and financial consequences. To assist policy authors in the analysis of their policies, several policy analysis tools have been proposed based on different underlying formalisms. However, most of these tools either abstract away functions over non-Boolean domains (hence they cannot provide information about them) or produce very large encodings which hinder the performance. In this paper, we present a generic policy analysis framework that employs SMT as the underlying reasoning mechanism. The use of SMT does not only allow more fine-grained analysis of policies but also improves the performance. We demonstrate that a wide range of security properties proposed in the literature can be easily modeled within the framework. A prototype implementation and its evaluation are also provided.
LanguageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Number of pages25
StatePublished - 2014

Publication series

NameComputer science reports
Volume1408
ISSN (Print)0926-4515

Fingerprint

Surface mount technology
Access control
XML
Markup languages
Specifications

Cite this

Turkmen, F., Hartog, den, J. I., Ranise, S., & Zannone, N. (2014). Analysis of XACML policies with SMT. (Computer science reports; Vol. 1408). Eindhoven: Technische Universiteit Eindhoven.
Turkmen, F. ; Hartog, den, J.I. ; Ranise, S. ; Zannone, N./ Analysis of XACML policies with SMT. Eindhoven : Technische Universiteit Eindhoven, 2014. 25 p. (Computer science reports).
@book{4471e193f91a4f0ebbc96f648c421f0d,
title = "Analysis of XACML policies with SMT",
abstract = "The eXtensible Access Control Markup Language (XACML) is an extensible and flexible XML language for the specification of access control policies. However, the richness and flexibility of the language (along with the verbose syntax of XML) come with a price: errors are easy to make and difficult to detect when policies grow in size. If these errors are not detected and rectified, they can result in serious data leakage and/or privacy violations leading to significant legal and financial consequences. To assist policy authors in the analysis of their policies, several policy analysis tools have been proposed based on different underlying formalisms. However, most of these tools either abstract away functions over non-Boolean domains (hence they cannot provide information about them) or produce very large encodings which hinder the performance. In this paper, we present a generic policy analysis framework that employs SMT as the underlying reasoning mechanism. The use of SMT does not only allow more fine-grained analysis of policies but also improves the performance. We demonstrate that a wide range of security properties proposed in the literature can be easily modeled within the framework. A prototype implementation and its evaluation are also provided.",
author = "F. Turkmen and {Hartog, den}, J.I. and S. Ranise and N. Zannone",
year = "2014",
language = "English",
series = "Computer science reports",
publisher = "Technische Universiteit Eindhoven",

}

Turkmen, F, Hartog, den, JI, Ranise, S & Zannone, N 2014, Analysis of XACML policies with SMT. Computer science reports, vol. 1408, Technische Universiteit Eindhoven, Eindhoven.

Analysis of XACML policies with SMT. / Turkmen, F.; Hartog, den, J.I.; Ranise, S.; Zannone, N.

Eindhoven : Technische Universiteit Eindhoven, 2014. 25 p. (Computer science reports; Vol. 1408).

Research output: Book/ReportReportAcademic

TY - BOOK

T1 - Analysis of XACML policies with SMT

AU - Turkmen,F.

AU - Hartog, den,J.I.

AU - Ranise,S.

AU - Zannone,N.

PY - 2014

Y1 - 2014

N2 - The eXtensible Access Control Markup Language (XACML) is an extensible and flexible XML language for the specification of access control policies. However, the richness and flexibility of the language (along with the verbose syntax of XML) come with a price: errors are easy to make and difficult to detect when policies grow in size. If these errors are not detected and rectified, they can result in serious data leakage and/or privacy violations leading to significant legal and financial consequences. To assist policy authors in the analysis of their policies, several policy analysis tools have been proposed based on different underlying formalisms. However, most of these tools either abstract away functions over non-Boolean domains (hence they cannot provide information about them) or produce very large encodings which hinder the performance. In this paper, we present a generic policy analysis framework that employs SMT as the underlying reasoning mechanism. The use of SMT does not only allow more fine-grained analysis of policies but also improves the performance. We demonstrate that a wide range of security properties proposed in the literature can be easily modeled within the framework. A prototype implementation and its evaluation are also provided.

AB - The eXtensible Access Control Markup Language (XACML) is an extensible and flexible XML language for the specification of access control policies. However, the richness and flexibility of the language (along with the verbose syntax of XML) come with a price: errors are easy to make and difficult to detect when policies grow in size. If these errors are not detected and rectified, they can result in serious data leakage and/or privacy violations leading to significant legal and financial consequences. To assist policy authors in the analysis of their policies, several policy analysis tools have been proposed based on different underlying formalisms. However, most of these tools either abstract away functions over non-Boolean domains (hence they cannot provide information about them) or produce very large encodings which hinder the performance. In this paper, we present a generic policy analysis framework that employs SMT as the underlying reasoning mechanism. The use of SMT does not only allow more fine-grained analysis of policies but also improves the performance. We demonstrate that a wide range of security properties proposed in the literature can be easily modeled within the framework. A prototype implementation and its evaluation are also provided.

M3 - Report

T3 - Computer science reports

BT - Analysis of XACML policies with SMT

PB - Technische Universiteit Eindhoven

CY - Eindhoven

ER -

Turkmen F, Hartog, den JI, Ranise S, Zannone N. Analysis of XACML policies with SMT. Eindhoven: Technische Universiteit Eindhoven, 2014. 25 p. (Computer science reports).