XACML-SMT is an analysis framework that allows formal verification of XACML policies (v2 and v3). Most of the existing policy analysis tools either cannot efficiently reason about non-Boolean attributes, which often appear in XACML policies, or restrict the analysis to a small set of properties. XACML-SMT employs SAT modulo theories (SMT) as the underlying reasoning mechanism to address these drawbacks. It offers an intuitive syntax to specify properties, and provides models (if property is satisfiable) and proofs (if property is not satisfiable). By being able to reason over non-Boolean attributes, XACML-SMT allows a fine-grained policy analysis while relieving policy authors of the burden of defining an appropriate level of granularity of the analysis.
The tool is experimental, so the "use with your own risk" state holds. The current version is released as a jar file (find here). Z3 Java instructions are available here (just beware the use of --java flag for Java bindings, --x64 for 64-bit configuration). Following these instructions, you will need to rename the generated Z3 jar as "z3-4.4.1.jar" (sorry due to maven stuff), and place the generated dynamic libraries as described below. Do not hesitate to contact me in case you drive into problems...
Assuming the executable jar file of the tool (XACMLSMT.jar) is located under “bin” directory (or any directory you like), then XACML-SMT tool assumes that the external libraries to be in the “lib” directory at the same level with "bin". Moreover, Z3 DLLs (libz3 and libz3java) need to be in the same directory from where the tool is launched. The general syntax for running the tool is as follows:
java -jar bin/XACMLSMT.jar -p [p1 p2 p3 …] -q QUERY [optional parameters]
Note : Use -h flag to see the help/options...
The authorization spaces of policies are denoted as P (permit), D (deny), IN (Indeterminate) and NA (NotApplicable). In a given set of policies {p1, p2,…,pn}, each policy is referred with the index that represents the order it is provided. Thus the deny space (D) of the second policy is referred as D_2 while indeterminate space (IN) of the first policy is referred as IN_1. Note here also that you need to escape the backslash (i.e. \ --> \\) when you actually input the query to the tool.
Currently Supported Datatypes: Integer, Double (more precisely Reals in Z3), Boolean, String (converted to enumerated data types).
Supported Operators: \WEDGE (Conjunction), \VEE (Disjunction), \NEG (Negation), \IMPLIES (Simple Implication), \FORALL (Universal Quantifier), \EXISTS (Existential Quantifier), \INS (Request Instantiation), \REST (Restriction), and the operators: { (, ), =} as defined conventionally.
Future/ongoing extensions: The operators {-,+,%,*,/,^} will also be supported in the next release.
"\NEG ( ( P_1 \IMPLIES P_2 ) \WEDGE ( D_1 \IMPLIES D_2 ) )" : Does the second policy refine the first policy?
role = Manager \WEDGE experience = 10 : The attribute role is set to value “Manager” (this reads as “Manager” \in role), and the attribute experience is set to 10.
Number of Solutions: Certain property types require the enumeration of solutions in a satisfiable property instance, e.g. change-impact. The specification of enumeration requirement is provided at the beginning of the query.
XACML standard defines around ~250 functions for the specification of policies. The following functions are readily supported by the XACML-SMT tool while many functions can be easily integrated.
Equality and Simple Match functions: string-equal, double-equal, integer-equal and boolean-equal
Arithmetic (Comparison) Functions: Greater-than, less-than, greater-or-equal, less-or-equal
Arithmetic Functions: integer-add, less-than, greater-or-equal, less-or-equal
Set Functions: At-least-one-member-of (this is encoded with the expression X ∩ Y ≠ ∅)
Logic Functions: And, or, not
Bag Functions: (type)-one-and-only, string-bag, is-in
Non-numeric Comparison: Time-in-range (handled as integer conversion and comparison)
In the current versions of the tool, string manipulation (concat etc) is not supported. We plan to support them through external tools such as z3str however (to our knowledge) no string theory solver that integrates with Z3 exists yet.
The tool considers mainly AttributeDesignators for identifying attributes and AttributeSelectors are partially supported. AttributeId of an AttributeDesignator is the principal identifier that separates an attribute of a particular policy from the attribute of another policy. For instance, if the attribute “role” is used in two policies p1 and p2 that are analyzed then there will be one variable with the domain that contains all values (i.e. roles).
Here the issue is the negation of the models are added with conjunction to the original formula F as follows
F /\ ¬(m1) /\ ¬(m2) ...
The cases of \FORALL and \EXISTS need to be tested. There is (most probably) an error in the code for the case that if the quantified variable does not exist in the policy then its sort cannot be found through policy scanning. This will throw an exception.
A possibility to disable model pruning during analysis (now it adds the additional formula in every cases) needs to be added.
Even the query parser can handle the syntactic sugar \INS from the language, it should be removed since it can be encoded with \WEDGE by the user…
Credits: Fatih Turkmen, Jerry den Hartog, Silvio Ranise and Nicola Zannone