Access Control Policy Evaluator and Generator Acpeg

Software Available for DOWNLOAD below

Acpeg** is a tool for evaluating and generating access control policies. It can model check a model built from a script description of an access control policy, that is, a set of authorisation rules. The script is written in the RW language [1,2,3,4,5]. The script is written in the RW language. The language is based on first-order logic. It is machine readable. The RW language is for expressing access control policies modelled in the RW framework as well as properties of the model that are going to be checked. Through model checking potential security breaches caused by interactions of rules, co-operations between agents and multi-step actions may be found, whereas the same security breaches are harder to be identified by other approaches. These causes may make apparently integral authorisation rules powerless in achieving their security purposes.

A property of the model is expressed as the ability of a certain coalition of agents to read or overwrite certain information within the permissions the policy grants. The intention of the coalition to read or overwrite certain information is expressed by a goal. The ability of the coalition to achieve the goal is reflected by whether certain strategies are available to them. Each such strategy consists of a sequence of single reading or overwriting action that an agent in the coalition is able to carry out within the permissions the policy grants. The achievability of the goal reflects certain facts about the model, which, in turn, reflects certain facts about the policy. The existence of strategies for malicious goals suggests the fact that the policy contains security holes that can be exploited by the coalition to take advantages of the system. The failure of finding strategies for legitimate goals suggests that the policy has not granted the users of the system enough permissions to carry out their legitimate actions. Thus, the fitness of the policy of an access control system can be evaluated by the tool. The tool can also translate the policy written in the RW language to a policy file written in XACML. A real access control system can then be built using the XACML policy.

Releases and Download:

1. Acpeg 1.6 is the tool summarised in [1], which can check systems against specifications of the capabilities of users. Version 1.6 of the tool provides:
 

  • 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
To download it, Click here ! 

For installation and usage instruction please check the readme file.

2. Acpeg Lite : is a lite and improved version of Acpeg 1.6 . All the classes in Acpeg 1.6  relating to the RW model checking have been completely rewritten. As the results of that the source code of the classes have become more compact in  Acpeg Lite than they were in Acpeg 1.6. Functional speaking, only the necessary function in the RW model checking have been preserved in the new system, that is, the searching of strategies. The result is that the code of Acpeg Lite is much more easily readable and understandable than that of Acpeg 1.6.  

The functions preserved in Acpeg Lite are:

  • searching for strategies
  • translating from RW to XACML

All the code relating to the functions of searching for guessing strategies and abstraction, including CEGAR, have been removed. This decision was made at the beginning of the rewriting for several reasons. Originally, abstraction was introduced into the tool because of an error in the implementation. That error caused the searching of strategies in a large model unbearably slow. Abstraction was therefore added to the tool to speed up the checking of large models. Later, however, the error was pointed out by David Parker, and was corrected subsequently. After the correction, the performance of the tool was greatly improved. It seemed, from then on, the mechanisms of abstraction are not necessary any more. Besides this reason, from the experience with Acpeg 1.6, hundreds of meaningless strategies may be found by the tool while running in the abstraction modes. For these reasons abstraction was removed from Acpeg Lite . Because CEGAR only works under the abstraction modes, it was also removed.

For more details about you can read the release notes.

To download it, click here!

 For installation and usage instruction for Acpeg Lite   please click here.

 

Related Talks

 

Troubleshooting

We are interested in continuously improving Acpeg, so if you have any problems, please send us an e-mail. We will do our best to correct bugs or introduce some new features.

Credit

The creation of the tool was the collaboration of the four authors: Nan Zhang, Mark Ryan, Pierre-Yves Schobbens and Dimitar P. Guelev.

Referencesses

[1] 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 [This long paper summarises our results.]

[2] Nan Zhang. Generating Verified Access Control Policies through Model Checking. PhD thesis, School of Computer Science, University of Birmingham, 2005.

[3] 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 one defines our basic model and shows some of its properties.]

[4] 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 the basic model-checking algorithm for access control systems.]

[5] 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.[ This paper explains how access control systems defined in our model can be compiled into XACML code.]