MOHAWK: Abstraction-refinement and bound-estimation for verifying access control policies

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

Research output: Contribution to journalArticlepeer-review

26 Scopus citations


Verifying that access-control systems maintain desired security properties is recognized as an important problem in security. Enterprise access-control systems have grown to protect tens of thousands of resources, and there is a need for verification to scale commensurately. We present techniques for abstractionrefinement and bound-estimation for bounded model checkers to automatically find errors in Administrative Role-Based Access Control (ARBAC) security policies. ARBAC is the first and most comprehensive administrative scheme for Role-Based Access Control (RBAC) systems. In the abstraction- refinement portion of our approach, we identify and discard roles that are unlikely to be relevant to the verification question (the abstraction step). We then restore such abstracted roles incrementally (the refinement steps). In the boundestimation portion of our approach, we lower the estimate of the diameter of the reachability graph from the worst-case by recognizing relationships between roles and state-change rules. Our techniques complement one another, and are used with conventional bounded model checking. Our approach is sound and complete: an error is found if and only if it exists.We have implemented our technique in an access-control policy analysis tool called MOHAWK. We show empirically that MOHAWK scales well to realistic policies, and provide a comparison with prior tools.

Original languageEnglish (US)
Article number18
JournalACM Transactions on Information and System Security
Issue number4
StatePublished - Apr 2013

ASJC Scopus subject areas

  • General Computer Science
  • Safety, Risk, Reliability and Quality


Dive into the research topics of 'MOHAWK: Abstraction-refinement and bound-estimation for verifying access control policies'. Together they form a unique fingerprint.

Cite this