Analyzing access control policies with SMT

F. Turkmen; J.I. Hartog, den; N. Zannone

doi:10.1145/2660267.2662366

Analyzing access control policies with SMT

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

Onderzoeksoutput: Bijdrage aan congres › Poster

262 Downloads (Pure)

Samenvatting

The flexibility and expressiveness of eXtensible Access Control Markup Language (XACML) allows the specification of a wide range of policies in different access control models. However, XACML policies are often verbose and, thus, prone to errors. Several tools have been developed to assist policy authors for the verification and analysis of policies, but most of them are limited in the types of analysis they can perform. In particular, they are not able to rea- son about predicates of non-boolean variables and, even if they do, they do it inefficiently. In this paper, we present the X2S framework, a formal framework for the analysis of XACML policies that employs Satisfiability Modulo Theories (SMT) as the underlying reasoning mechanism. The use of SMT not only allows more fine-grained analysis of policies, but it also improves the performance of policy analysis significantly. Keywords: Access control, policy analysis and verification, property checking, SAT modulo theories

Originele taal-2	Engels
Pagina's	1508-1510
DOI's	https://doi.org/10.1145/2660267.2662366
Status	Gepubliceerd - 2014
Evenement	conference; 21st ACM Conference on Computer and Communications Security; 2014-11-03; 2014-11-07 - Duur: 3 nov. 2014 → 7 nov. 2014

Congres

Congres	conference; 21st ACM Conference on Computer and Communications Security; 2014-11-03; 2014-11-07
Periode	3/11/14 → 7/11/14
Ander	21st ACM Conference on Computer and Communications Security

Bibliografische nota

21st ACM Conference on Computer and Communications Security (CCS'14, Scottsdale AZ, USA, November 3-7, 2014)

Toegang tot document

10.1145/2660267.2662366

publishers versionDefinitieve gepubliceerde versie, 387 KB

Citeer dit

@conference{da1397d3eefc4b19a4f4bddcaaf22019,

title = "Analyzing access control policies with SMT",

abstract = "The flexibility and expressiveness of eXtensible Access Control Markup Language (XACML) allows the specification of a wide range of policies in different access control models. However, XACML policies are often verbose and, thus, prone to errors. Several tools have been developed to assist policy authors for the verification and analysis of policies, but most of them are limited in the types of analysis they can perform. In particular, they are not able to rea- son about predicates of non-boolean variables and, even if they do, they do it inefficiently. In this paper, we present the X2S framework, a formal framework for the analysis of XACML policies that employs Satisfiability Modulo Theories (SMT) as the underlying reasoning mechanism. The use of SMT not only allows more fine-grained analysis of policies, but it also improves the performance of policy analysis significantly. Keywords: Access control, policy analysis and verification, property checking, SAT modulo theories",

author = "F. Turkmen and {Hartog, den}, J.I. and N. Zannone",

note = "21st ACM Conference on Computer and Communications Security (CCS'14, Scottsdale AZ, USA, November 3-7, 2014); conference; 21st ACM Conference on Computer and Communications Security; 2014-11-03; 2014-11-07 ; Conference date: 03-11-2014 Through 07-11-2014",

year = "2014",

doi = "10.1145/2660267.2662366",

language = "English",

pages = "1508--1510",

}

TY - CONF

T1 - Analyzing access control policies with SMT

AU - Turkmen, F.

AU - Hartog, den, J.I.

AU - Zannone, N.

N1 - 21st ACM Conference on Computer and Communications Security (CCS'14, Scottsdale AZ, USA, November 3-7, 2014)

PY - 2014

Y1 - 2014

N2 - The flexibility and expressiveness of eXtensible Access Control Markup Language (XACML) allows the specification of a wide range of policies in different access control models. However, XACML policies are often verbose and, thus, prone to errors. Several tools have been developed to assist policy authors for the verification and analysis of policies, but most of them are limited in the types of analysis they can perform. In particular, they are not able to rea- son about predicates of non-boolean variables and, even if they do, they do it inefficiently. In this paper, we present the X2S framework, a formal framework for the analysis of XACML policies that employs Satisfiability Modulo Theories (SMT) as the underlying reasoning mechanism. The use of SMT not only allows more fine-grained analysis of policies, but it also improves the performance of policy analysis significantly. Keywords: Access control, policy analysis and verification, property checking, SAT modulo theories

AB - The flexibility and expressiveness of eXtensible Access Control Markup Language (XACML) allows the specification of a wide range of policies in different access control models. However, XACML policies are often verbose and, thus, prone to errors. Several tools have been developed to assist policy authors for the verification and analysis of policies, but most of them are limited in the types of analysis they can perform. In particular, they are not able to rea- son about predicates of non-boolean variables and, even if they do, they do it inefficiently. In this paper, we present the X2S framework, a formal framework for the analysis of XACML policies that employs Satisfiability Modulo Theories (SMT) as the underlying reasoning mechanism. The use of SMT not only allows more fine-grained analysis of policies, but it also improves the performance of policy analysis significantly. Keywords: Access control, policy analysis and verification, property checking, SAT modulo theories

U2 - 10.1145/2660267.2662366

DO - 10.1145/2660267.2662366

M3 - Poster

SP - 1508

EP - 1510

T2 - conference; 21st ACM Conference on Computer and Communications Security; 2014-11-03; 2014-11-07

Y2 - 3 November 2014 through 7 November 2014

ER -

Analyzing access control policies with SMT

Samenvatting

Congres

Bibliografische nota

Toegang tot document

Vingerafdruk

Citeer dit