资 源 简 介
Mohawk is tool for verifying 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 The latest version of Mohawk uses novel methods for calculating the diameter of an ARBAC policy and uses that as the bound when using the bound
