On the use of SMT solving for XACML policy evaluation

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.