How is it being verified?

All of our checks are integrated into our Tests framework. Currently they are executed manually: the user needs to determine, via command line, the file under which verification will be performed. Automating this process is a work in progress.

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 Legalease.

How does it happen?

To better explain how verification occurs, we will present examples of use cases for each property being verified and then describe how the code will be executed for this example, according to the implementation of the code.

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


Given two policies (A and B), all possible input queries are determined, with the help of the CVC4 SMT solver. Each set of allowed queries is then added to a corresponding list. Both lists are compared according to their items. It follows that: if all items in policy A are contained in policy B, but not all items in policy B are contained in policy 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.

Permissiveness verification is done using two auxiliary functions that were created within the verification file itself. They are:

  • The function Get_list(Policy):
def Get_list(Policy):
 Models_list = []

 while slv.checkSat()._name == 'sat':
   Models_list.append((slv.getValue(Actors), slv.getValue(Action), slv.getValue(Resources)))
 return Models_list

Function that receives an access policy defined with the CVC4 API and obtains all combinations of Actor, Resource, and Action that satisfy the policy, that is, all accepted input queries; returning a list.

  • The function Check_permissiveness(list1, list2):
# check if list2 contains all elements of list1
   # list1 -> list2?
   implication_1 =  all(elem in list2  for elem in list1)

   # check if list1 contains all elements of list2
   # list2 -> list1?
   implication_2 =  all(elem in list1  for elem in list2)

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

The one that receives the two lists obtained from the policies to be compared and checks whether list_1 implies list2, that is, whether all elements of list_1 are contained in list_2, and the opposite too (list_2 implies list_1).

In the case of our example, Alpha -> Beta, we will have that the implication_1 will be false so, not all accesses allowed by Alfa are allowed by Beta. And the implication_2 will be true (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_permissivenes_test None


All the policies, that are already created, needs to be specified to execute this verification. Then, the datas treated in each policy are stored in sets. We then check whether the sets are disjoint or not. If they are not, there will be an intersection between different sets, and respective policies. There is our Collision. Actually theres only one way to verify the Collision, that is manually. Making this verification occurs automatically, where for each new Policy created in Hapi the test is executed, it is a future project.

User X was given the task of defining Resource access: ID, PRODUCTS, EMAIL for Actors Alice and Bob. In user X's system there are hundreds of defined Policies that work perfectly. A Policy A that defines Resources: SSN, EMAIL and CCN already exists in the system, expressed as follows:

data: [SSN, EMAIL, CCN]
  - identities:
      users: Alice
        data: [CCN, EMAIL]
        data: [CCN, EMAIL]
  - identities:
      users: Bob
        data: [CCN, EMAIL]
        data: [EMAIL]

However, not knowing about the existence of such a policy, and that it already governed what happened with Resource EMAIL, user X decides to create a new Policy B to define what happens with all the Resources requested in the task. This new policy being expressed as follows:

  - identities:
      users: Alice
        data: [PRODUCTS, ID]
        data: [PRODUCTS, ID]
  - identities:
      users: Bob
        data: [PRODUCTS, EMAIL]
        data: [PRODUCTS]

As you can see, both Policies A and B define different access restrictions under Resource EMAIL, which can generate errors in the system since the Policies overlap. With the collision verification being performed, the user will receive a warning as it follows:


Indicating the conflicting Resource: EMAIL; and also the two Policies in which this Resource is defined: Policies A and B. Then he will need to correct this error if he wants to maintain the Consitency of the system.

The verification of the Collision property occurs with multiple YAML Policy files being passed as a reference in the Verification Call.

Within the plugin, the framework reads every policy and stores all Resources (data) that are treated in each one in different Sets (One set for each Policy):

#...While there is policies...

with open("fixtures/yaml/first-deny.yaml", "r") as ymlfile: #Opening the policy
      cfg = yaml.load(ymlfile)

  Policy_name_1 = set(cfg["data"]) #Getting the defined Resources

Finally, all the Sets containing the Resources that are treated in each policy, are added to a list. In this way, we obtain a list of Sets.

In the second moment, we used two Loops while, to compare all the sets stored in the List. If two sets are 'disjunct', that is, without similar elements, the loop advances to compare the next set:

while iterator < len(list_of_policiess):
    aux = iterator + 1
    while aux < len(list_of_policiess):

        if not list_of_policiess[iterator].isdisjoint(list_of_policiess[aux]):
            overlapped_resources = list_of_policiess[iterator].intersection(list_of_policiess[iterator+1])
            collision_boolean = True
        aux += 1

    if collision_boolean == True:
    iterator += 1

If there are similar elements in two different sets: the loops are closed, the names of the Policies corresponding to each Set are stored in an auxiliary variable, and these two sets are intersected, that will return the similar elements.

After the loop, an auxiliary variable called collision_boolean is used to indicate whether a 'collision' has occurred or not. Being 'True', the test returns the Conflict Policies and Resources governed by both simultaneously. Being 'False', the test passes, telling the user that there are no conflicting policies.

Pre-built execution test: python -collision_verifier None

Updates and improvements are being made so that the use of these features will be easy and intuitive, for users of the Hapi tool.