Abstract

Dynamic constraints such as Separation of Duty (SoD) prevent the possibility of frauds and enable flexible protection of sensitive resources appearing in active contexts. They are enforced in various ways depending on the access control model and the application. Role based access control (RBAC) employs restrictions on the activation of roles and the exercise of permissions by individuals for enforcing the constraints. However, whether a constraint specification correctly enforces a given dynamic policy is an open research question. This is mainly due to the nature of the dynamic constraint enforcement: a constraint satisfied at a state can be violated at a future state as a result of the event sequences occurred in between. Moreover, the support of dynamic enforcement usually imposes low level extensions to the implementation, which in return requires another level of verification. In the approaches that tackle this problem at run-time, efficiency is a key concern. In this dissertation, we present two approaches for analyzing and enforcing dynamic constraints. The first is employed on-line and is based on software testing features available in software model checkers. The relevant components of an access control system are modeled as a software and the execution of this software mimics the RBAC run-time. A software model checker is used to check some properties that represent constraint specifications and the actual authorization policies encoded in eXtensible Access Control Language (XACML). We demonstrate our approach by using an open source software model checker, Java Path Finder (JPF), and its sub-projects for dierent testing scenarios. In this first approach, efficiency is not the main concern but coverage is. The second approach relies on a propositional satisability (SAT) based run-time procedure to replace the conventional policy evaluation in RBAC systems. Efficiency and flexibility are the prominent features of this approach. Efficiency is obtained by dividing the steps involved in policy evaluation into on-line and off-line. On-line steps correspond to request answering in conventional policy evaluation and have to be done at run-time. On-line steps can be performed as pre-processing or post-processing of the on-line steps and have no effect on policy evaluation performance. We experimentally show that our approach is efficient and scales well in realistic scenarios. The final chapter of the thesis presents an extensive study of XACML policy evaluation performance. Policy evaluation corresponds to a function, Eval(Policy,Request), that takes a policy and a request as input, and produces an access control decision. Our experimental results show that the Eval function can create a bottleneck in application domains where the number of policies and rules is large. We present a list of optimization techniques that can speed up the evaluation performance.