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 two software tools for verifying access control policies: PoliVer and AcPeg. These tools are able to check systems against required specifications. These tools demonstrate two policy evaluations methods. Both of them are 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 following table compares the features PoliVer and AcPeg:
| PoliVer | AcPeg | |
| Nested query support | ✔ | ✔ |
| Searching forn guessing strategies | ✔ | ✔ |
| Bulk variable update | ✔ | |
| Translating to XACML | ✔ | |
| Selective running of rounds | ✔ | ✔ |
| Counterexample guided abstraction refinement (CEGAR) | ✔ | |
| Support for memoryful knowledge | ✔ |
Please view the links for more information and to download the tools.