- XACML Analysis with SMT (click here for more information)
The flexibility 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. XACML-SMT tool assists policy authors for the verification and analysis of policies. It employs Satisfiability Modulo Theories (SMT) as the underlying reasoning mechanism. The use of SMT not only allows more fine-grained analysis of policies (e.g. reasoning about non-boolean attributes) compared to existing tools, but it also improves the performance of policy analysis significantly.
- Stateful UAQ Solver (click here for download)
The User Authorization Query (UAQ) Problem for Role- Based Access Control (RBAC) amounts to determining a set of roles to be activated in a given session in order to achieve some permissions while satisfying a collection of authorization constraints governing the activation of roles. Techniques ranging from greedy algorithms to reduction to (variants of) the propositional satisfiability (SAT) problem have been used to tackle the UAQ problem. Unfortunately, available techniques su er two major limitations that seem to question their practical usability. On the one hand, authorization constraints over multiple sessions or histories are not considered. On the other hand, the experimental evaluations of the various techniques are not satisfactory since they do not seem to scale to larger RBAC policies.
In this project, we developed a SAT-based technique to solve the UAQ problem which overcomes these limitations. We first showed how authorization constraints over multiple sessions and histories can be supported. Second, we carefully tuned the reduction to the SAT problem so that most of the clauses need not to be generated at run-time but only in a pre-processing step. An extensive experimental evaluation of an implementation of our techniques on a significant set of UAQ problem instances shows the practical viability of our approach; e.g., problems with 300 roles are solved in less than a second.
The implementation includes a RBAC policy (state-based) generator and a SAT translator for answering authorization queries. More information on UAQ problem and the relevant concepts of this project can be found in .
- RBACSimulator (click here for download)
The notion of "session" created a considerable debate in access control.
Recent research demonstrated that many access control constraints can
not be verified statically at design time. The user behavior during an
active session is uncertain, sessions are concurrent and some
authorization decision parameters (i.e. conditions) are only available
at runtime. However, similarly to what is done in software verification,
it is possible to give static indications about the run-time behavior of
the access control system, by analyzing a finite number of
approximations that model both the user behavior and the decision
parameters. Moreover, constraints (e.g. history-based ones) can be
analyzed in combination rather than individually. RBACSimulator is a
framework tailored to offline verification of run-time constraints
and security properties (e.g. mutually exclusive roles) for role based
access control systems. It uses actors to mimic active
entities at runtime and creates activity entropies from a set
of permission and role activations.
The software model representing
RBAC run-time is fed to a software model checker for (exhaustive) state
space exploration and any violation of the given constraints at any state is reported. A security administrator can obtain
a set of run-time trajectories with a finite number of simulations that
can be used to verify the desired properties. More details on this work can be found in .
- Efficiency XACML PDP Engines (click here for the relevant code)
eXtensible Access Control Markup Language (XACML), an OASIS standard, is the most widely used policy specification language for access control. Its simplicity in syntax and strength in coverage makes it suitable for diverse environments such as Service Oriented Architectures (SOAs) and P2P systems. There are different implementations of XACML available. Some of these implementations are open source and some others are proprietary. In this project we intended to shed some lights to the performance issues of XACML engines. We tested 3 open source XACML implementations with different policy/request settings. Our experiments revealed some important points to be taken into consideration when deploying an XACML based access control system. Besides, our results can be used as hints by policy writers and system developers for deploying efficient authorization services. This work is related to .