The exibility 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 reason 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. Copyright is held by the owner/author(s).

Original languageEnglish
Title of host publicationCCS'14
Subtitle of host publicationProceedings of the 2014 ACM Conference on Computer and Communications Security
Place of PublicationNew York
PublisherAssociation for Computing Machinery (ACM)
Number of pages3
ISBN (Electronic)9781450329576
StatePublished - 3 Nov 2014
Externally publishedYes
Event21st ACM Conference on Computer and Communications Security, CCS 2014 - Scottsdale, United States
Duration: 3 Nov 20147 Nov 2014


Conference21st ACM Conference on Computer and Communications Security, CCS 2014
CountryUnited States

    Research areas

  • Access control, Policy analysis and verification, Property checking, SAT modulo theories

ID: 32864732