On the Use of SMT Solving for XACML Policy Evaluation
- 1 December 2016
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE) in 2016 IEEE International Conference on Cloud Computing Technology and Science (CloudCom)
Abstract
eXtensible Access Control Markup Language (XACML) allows for flexible management of authorisations and is particularly useful in settings where permissions change dynamically. However, it has been shown that policy evaluation in XACML may have scalability problems when policies become large and sophisticated in content. Among several proposals for designing efficient policy decision points for XACML policies, decision diagram (DD) based procedures still represent the state-of-the-art. In this paper, we present an alternative approach to policy evaluation that employs Satisfiability Modulo Theories (SMT) solving instead of DDs. The approach does not only represent a feasible policy evaluation procedure in terms of performance but also easily lends itself to different application areas such as verification at run-time during authorization query answering. We discuss various scenarios in which SMT-based policy evaluation would be more practical compared to DD-based procedures. A preliminary experimental evaluation of our policy evaluation procedure against real-world policies is also provided in the paper.Keywords
This publication has 10 references indexed in Scilit:
- Analysis of XACML Policies with SMTPublished by Springer Science and Business Media LLC ,2015
- Z3-str: a z3-based string solver for web application analysisPublished by Association for Computing Machinery (ACM) ,2013
- Multi-data-types interval decision diagrams for XACML evaluation enginePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2013
- Anomaly discovery and resolution in web access control policiesPublished by Association for Computing Machinery (ACM) ,2011
- Designing Fast and Scalable XACML Policy Evaluation EnginesIEEE Transactions on Computers, 2010
- Performance evaluation of XACML PDP implementationsPublished by Association for Computing Machinery (ACM) ,2008
- Automated verification of access control policies using a SAT solverInternational Journal on Software Tools for Technology Transfer, 2008
- Verification and change-impact analysis of access-control policiesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- Symbolic model checking using SAT procedures instead of BDDsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Symbolic Model Checking without BDDsPublished by Defense Technical Information Center (DTIC) ,1999