Software‎ > ‎

XACML-SMT

News:

[07/11/16] New version of XACML-SMT is available...  

[10/6/15] Small update on model generation (type cast bug)

[18/5/15] XACML-SMT version 1.0 is released (in the form of jar file).


What is XACML-SMT? 

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.


Download 

The tool is still experimental, so the "use with your own risk" state still holds. The current version is released as a jar file (find below XACMLSMT.jar). 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... 

Requirements/Dependencies

  • Apache Commons CLI (commons-cli-1.2)
  • Commons Lang (v2.1) 
  • Commons Math (v3-3.3) 
  • Z3 (v4.4.1) 


Running 

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...


Query Language 

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.


Example queries:

  • "\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.


Currently Supported XACML Functions

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

(Note: Equality functions are mapped to set membership predicates for enumerated types such as strings, while they are mapped to proper equality predicates for integers, double/reals and booleans)

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).


Known Issues and TODO:

(1)  Model generation as it is in the implementation misses some models. Think about the following example, with "role" attribute and possible values {Employee, Manager, Clerk}.

- Assume the first model is   ==>  m1:  Employee  role

- We add the clause "Employee ∉ role" and obtain another model   ==>  m2 : Manager ∈ role, and so on...

Here the issue is the negation of the models are added with conjunction to the original formula F as follows

F /\ ¬(m1) /\ ¬(m2) ...

one at a time at each run. From here, there is no possibility to obtain a model that contains {Employee,Manager} ⊆ role .  While it should be possible to have a model m3: role={Clerk,Manager}

(2)  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.

(3)  A possibility to disable model pruning during analysis (now it adds the additional formula in every cases) needs to be added.

(4)  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 


Publications

[1] F Turkmen, J den Hartog, S Ranise, N Zannone, "Formal analysis of XACML policies using SMT", Computers & Security (COSE) , 185-203

[2] F. Turkmen, J.d. Hartog, S. Ranise, N. Zannone,  "Analysis of XACML Policies with SMT", 4th Conference on Principles of Security and Trust (POST) 2015: 115-134

[3] F. Turkmen, J. D. Hartog, N. Zannone, "Analyzing Access Control Policies with SMT"21st ACM Conference on Computer and Communications Security (CCS), 2014 (Poster).


Contact 

fturkmen[AT]gmail(DOT)com   


ċ
XACMLSMT.jar
(221k)
Fatih Turkmen,
Nov 7, 2016, 5:14 AM
Comments