Hasan Qunoo
CSRG seminar on 20th March 2007 at 14:00
Room 245, School of Computer Science

Generating Verified Access Control Policies through Model-Checking

Access control systems are increasingly important. Large-scale, heterogeneous and decentralized systems are needed in order to protect resources and information. Current access control models have limited autonomy, are hard to administer, and are too inflexible. Adding new users, updating users' roles or changing a security policy can be expensive and needs to be done in an ad-hoc fashion. An access control framework for evaluating and generating access control policies is extremely needed. Recently, many access control frameworks and policy languages has been developed. One of those frameworks is presented by Zhang et. al.

Zhang's framework contains a modelling formalism (RW formalism), a machine-readable language (RW language), a model-checking algorithm and a tool (AcPeg) implemented in java. The RW formalism is for modelling access control policies. The RW language is for expressing policies modelled in the RW formalism and security properties to be verified.  A property defines a goal, a coalition of agents and some conditions. Given a model built based on a policy and a property, the model checking algorithm decides whether the goal defined by the property is achievable by the coalition with the permissions the policy provides.


The conditions defined by the property serve as pre-requirements based on which the checking is performed. In the case that the goal is achievable, the algorithm outputs strategies that may be used by the coalition to achieve the goal. The un-achievability of legitimate goals may suggest that the policy does not provide the users enough permission to carry out their actions. The achievability of malicious goals may reveal certain security holes in the policy, among which are security holes caused by interaction of rules, co-operation between agents (including changing of each other's privileges) and multi-step actions. When malicious goals are achievable, the outputting strategies help to provide clues on amending the policy. The tool implements the algorithm and thus performs the RW model-checking. It can also convert a policy written in the RW language into a policy file in XACML. A real access control system can then be built on the converted policy file.  

In this talk, I will present Zhang's framework in details and demonstrate a domo to run the RW checker and AcPeg tools with an appropriate examples.