Analyzing access control policies with SMT

Research output: Contribution to conferencePosterAcademic

99 Downloads (Pure)

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
Original languageEnglish
Pages1508-1510
DOIs
Publication statusPublished - 2014
Eventconference; 21st ACM Conference on Computer and Communications Security; 2014-11-03; 2014-11-07 -
Duration: 3 Nov 20147 Nov 2014

Conference

Conferenceconference; 21st ACM Conference on Computer and Communications Security; 2014-11-03; 2014-11-07
Period3/11/147/11/14
Other21st ACM Conference on Computer and Communications Security

Bibliographical note

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

Fingerprint Dive into the research topics of 'Analyzing access control policies with SMT'. Together they form a unique fingerprint.

Cite this