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.