Given two policies (A and B), all possible input queries are determined, with the help of the CVC4 SMT solver. Both policies are compared in the form of Boolean expressions, using the implication and logical negation provided by the SMT solver, to determine whether one policy (expression) implies the other. It follows that: if all models accepted in policy A are accepted in policy B, i.e. A implies B, but not all models accepted in policy B are accepted in policy A, i.e B not implies A ; A is less permissive than B.


To simulate an use-case to this check, imagine the scenario of a fast-growing company:

Every day new employees are hired, new actors are created and added to groups of the company and, consequently, these new actors receive access to various files of the Company, thanks to their association with such groups.

With such rapid growth, regulating and controlling that each added actor has the proper permissions can be a complicated task and therefore failures can occur in the process.

Thinking mainly of a hierarchical class system: New actors can be added to Subgroup C (red circle), which in turn will be associated with a Subgroup B (gray circle), which is associated with group A (black circle).


  Actors = Group_A
  Actions = Reads, Updates, Deletes

These new actors will inherit all permissions given to group A, which can cause a leak of sensitive data.

Identifying this situation, the user of the HAPI Tool can reformulate the policy that grants access to group A:

  Actors = Group_A
  Actions = Reads, Updates, Deletes
  DENY {
    Actors = Group_B
    Actions = Reads, Updates, Deletes

When performing the test using as parameters: 'Alpha Policy (old) -> Beta Policy (new)', it will be reported that the Beta Policy is less permissive than the Alpha Policy:


That is, Alpha -> Beta = False (Alpha does not implies Beta) but, Beta -> Alpha = True (Beta imply Alpha), which was expected. The user will then choose to use the Beta Policy at the end.


We use the CVC4 SMT Solver for the Permissivenes check. The check has the following code snippet in its implementation:

    task_command = ["gradle", "generateCVC4",
    subprocess.check_call(task_command, shell=True, cwd='../src/legalease'))*

This code snippet corresponds to the command given to the system so that our translator can be executed over the Legalease policy files, passed as verification parameters. In addition, every CVC4 verification check needs two special imports:

  • PyCVC4 - A python API for the CVC4 SMT solver.
  • CVC4_Statements - A file containing general utilities (definitions of actors, resources, actions ...) to deal with access policies created in Hapi language.

Permissiveness verification is done basicaly using one auxiliar function that were created within the verification file itself: The Permissivenes(Policy_A, Policy_B) function, given as follows:

  • def Permissivenes(Policy_A, Policy_B):
   implication_aux = slv.mkTerm(kinds.Implies, Policy_A, Policy_B)
   implication_1 = slv.mkTerm(kinds.Not, implication_aux)

   implication_aux = slv.mkTerm(kinds.Implies, Policy_B, Policy_A)
   implication_2 = slv.mkTerm(kinds.Not, implication_aux)

   if (str(slv.checkSatAssuming(implication_1)) == "unsat") and (str(slv.checkSatAssuming(implication_2)) == "sat"):
       return "The First Policy is less permissive than the Second"
   elif (str(slv.checkSatAssuming(implication_1)) == "sat") and (str(slv.checkSatAssuming(implication_2)) == "unsat"):
       return "The Second Policy is less permissive than the First"
   elif (str(slv.checkSatAssuming(implication_1)) == "unsat") and (str(slv.checkSatAssuming(implication_2)) == "unsat"):
       return "The two Policies are equally permissive"
       return "The test doens't aply. There's different accepted models in each Policy"

It receives the two Policies covered in the verification. Three auxiliary variables are used: implication_aux, implication_1 e implication_2.

In Boolean logic, we want to know if A implies B AND B NOT implies A. This is equivalent to using only the expression: B NOT implies A. Thus, the variable implication_aux is used to store the Boolean implication. And the variables implication_`` 1 and 2 store the negations of the implications. According to the satisfiability of the expressions generated, the corresponding result is returned at the end of the verification, indicating whether one policy is equally-less permissive than the other.

In the case of our example, implication_1 = Beta -/> Alpha is valid so, not all accesses allowed by Alfa are allowed by Beta. And the implication_2 = Alpha -/> Beta is invalid (all accesses allowed by Beta are allowed by Alpha). The end result is that "The Second Policy(Beta) is less permissive than the First(Alpha)".

Pre-built execution test: python -cvc4_permissiveness_test None

Note: To run the "Pre-builted execution tests" you need to be on the '../hapi/test' folder