Mohawk

Automatic Verification of Access-Control Policies

 


Mohawk is a tool for automatically verifying the correctness of access-control policies.


Mohawk accepts an ARBAC policy and a safety query as inputs, and reports an error if it finds one. Otherwise, Mohawk terminates and reports that it could not find any errors.


Mohawk uses an abstraction-refinement based technique and bounded model checking for quickly identifying errors. The basic idea behind the approach is that it is efficient to verify an abstract policy than the full policy. Mohawk operation comprises multiple steps. In the first step, Mohawk creates an initial abstraction, by aggressively removing parts of the policy. Subsequently, Mohawk looks for errors in the abstract policy, and refines it by adding more information. Both the abstraction and refinement steps use a heuristic that tries to retain the error.


*New*: A new version of Mohawk will be available for download soon in

its google code website.




http://mohawk.googlecode.com





Karthick Jayaraman

Mahesh Tripunitara

Vijay Ganesh

Martin Rinard

Steve J. Chapin




Automatic Error Finding for Access-Control Policies.

Karthick Jayaraman, Vijay Ganesh, Mahesh Tripunitara, Martin Rinard, Steve Chapin

Proc. of the ACM Conf. on Computer and Communications Security (CCS 2011)

(PDF)


All the experimental data are available in the google code website.

(link)


Case Study:

ARBAC Policy for a Large Multi-National Bank.

Karthick Jayaraman, Vijay Ganesh, Mahesh Tripunitara, Martin Rinard, Steve Chapin

(PDF)


Case study policies

What is Mohawk?

Where is the source code?

People

Publications