Verifying Models of Access Control Systems

In a world in which computers are ever-more interconnected, access control systems are of increasing importance in order to guarantee that resources are accessible by their intended users, and not by other possibly malicious users. Access control systems are used to regulate access to resources such as files, database entries, printers, web pages, and web services. They may also be used in less obvious applications, such as to determine whether incoming mail has access to its destination mailbox (spam filtering), or incoming IP packets to their destination computers (firewalls).

We are developing a model of access control which has among others the following features:

• Access control may be dependent on the values of data to which access is being controlled. This is useful in many applications in which the decision of whether access is allowed depends on the state of the system. For example, patient health records and employee databases are systems of this kind. Sometimes this feature is called conditional authorisation.
• Delegation of access control is easily expressed. This helps to avoid the root bottleneck, whereby root or the owner of a resource is required in order to make access control changes, and the insecurity caused by investing too much power in a single agent.
• Permissions for coalitions of users to act jointly can be expressed.

A key feature of our model is that permissions are functions of state variables, and therefore may change with the state.  Because the ability to change the state is itself controlled by permissions, one can, in particular, express permissions about permissions. This allows us easily to devolve authority downwards, thus avoiding the root bottleneck, and to express delegation.

We have developed a software tool for verifying access control systems, which can check systems against specifications of the capabilities of users. The tar file includes a manual and full documentation. Version 1.6 of the tool supports:

• improved query syntax
• searching for strategies
• searching for guessing strategies
• checking both nested goals and simple goals
• Counter-example guided abstraction refinement (CEGAR)
• selective running of rounds
• other optimization on efficiency
• translating from RW to XACML

Please view the releases for more information and to download the software.

We present a framework for evaluating and generating access control policies. The framework contains a modelling formalism called RW, which is supported by a model checking tool.  RW is designed for modelling access control policies, and verifying their properties.  The RW language is very expressive, allowing us to model complex access conditions which can depend on data values, other permissions, and agent roles.

A property expresses the capability of a coalition of agents to achieve a goal, which may include reading and overwriting certain information. 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 within the permissions the policy provides.  In the case that the goal is achievable, the algorithm outputs strategies which may be used by the coalition to achieve the goal.

The unachievability of legitimate goals may suggest that the policy does not provide the users enough permissions to carry out their actions. The achievability of malicious goals may reveal certain security holes in the policy. When malicious goals are achievable, the resulting 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. An access control system can then be built on the converted policy file.

• Nan Zhang, Dimitar P. Guelev and Mark Ryan. Synthesising Verified Access Control Systems through Model Checking. Journal of Computer Security 16(1):1-61. 2007

Some earlier papers may also be interesting.

This one defines our basic model and shows some of its properties.

• Dimitar P. Guelev, Mark D. Ryan and Pierre-Yves Schobbens. Model-checking Access Control Policies.  Seventh Information Security Conference (ISC’04). Lecture Notes in Computer Science, Springer-Verlag, 2004. 16 pages.

This paper explains the basic model-checking algorithm for access control systems.

• Nan Zhang, Mark D. Ryan and Dimitar Guelev, Evaluating Access Control Policies Through Model Checking. Eighth Information Security Conference (ISC’05). Lecture Notes in Computer Science, Springer-Verlag, 2005.

This paper explains how access control systems defined in our model can be compiled into XACML code.

• Nan Zhang, Mark Ryan, and Dimitar P. Guelev, Synthesising Verified Access Control Systems in XACML. 2nd ACM Workshop on Formal Methods in Security Engineering, LNCS, Springer-Verlag, 2004. 10 pages.

• Dimitar Guelev, Bulgarian Academy of Sciences
• Nan Zhang, University of Birmingham
  
• Pierre Yves Schobbens, University of Namur, Belgium
• Hasan Qunoo, University of Birmingham
• Masoud Koleini, University of Birmingham