# What should be verified?

We want the policies implemented with the Hapi tool to be Consistent and Secure. By Consistency we mean that we want the policies to be correct, running without errors; and by Security we mean that we want the policies to represent the real intentions of the user who implements them.

In order to ensure that the policies implemented in Hapi comply with the above, we verify two properties: collision and permissiveness, defined below:

Definitions:

• Collision: Each sensitive data must be governed by a single policy, (i.e., no two policies should overlap over sensitive data).

• Permissivenes: given two similar policies, they are compared to determine the relationship and degree of permissiveness between them, that is, which policy allows a greater number of users to access certain resources.

### Consistency

Consistency is one of the most important properties that an Access Policy System must have, and with it we want to ensure that the policies created here are running, individually or together, correctly. For that, the policies need to be in agreement with each other, without Conflict restrictions, or Redundancy.

To be consistent, access policies need to satisfy 3 properties: Totality, Unicity and Collision. As explained in Section 2.2 Grammar , the Hapi language ensures the properties of 'Totality' and 'Unicity' by construction. Therefore, regarding consistency, it remains to verify the property of Collision.

The verification of Collision aims to ensure that two different policies (in separeted files) will deal with different sensitive datas, thus avoiding redundancy or conflicts between different policies. For example, in a case where access to a resource could be guaranteed in one policy but is denied in another:

#Policy_A                               |#Policy_B
----------------------------------------|---------------------------------------
data: [EMAIL, CCN]                      |data: [EMAIL, CCN]
rules:                                  |rules:
- identities:                         |  - identities:
users: Alice                      |      users: Alice
data: [CCN, EMAIL]              |        data: [CCN]
----------------------------------------|---------------------------------------
Note that in Policy_A Alice can Update the Resource EMAIL, but in Policy_B, she can't.


This scenario cannot exist. And even if the policies did not conflict, i.e., both policies allowing Alice to perform the Updates action under Resource EMAIL, this would be redundant, which should also not occur in a consistent set of access policies.

Moreover, this is a property that our client, Cyral, determined that should be guaranteed, as can be seen in the following note:

### Security

Although access policies are developed precisely for the security of a system's data, the user who creates these policies may, at any given time, make a mistake or may lose control of a policy as time passes and the number of associated users to your system increases.

In order to assist the user when it comes to remodeling a policy aiming at a more restrictive system, we have incorporated into the Hapi tool, a Permissiveness check between two Policies.

The verification of Permissiveness seeks to warn the user if an access Policy_A is less-equally Permissive than an access Policy_B:

#Policy_A                               |#Policy_B
----------------------------------------|---------------------------------------
main =                                  |main =
DENY                                  |  DENY
EXCEPT                                |  EXCEPT
ALLOW {                             |    ALLOW {
Actors = Professor, Assistants    |      Actors
Resources                         |      Resources
Actions                           |      Actions
}                                   |    }
ALLOW {                             |    EXCEPT
Actors = Students                 |      DENY {
Resources = Exam.pdf              |        Actors = Students
Note that Policy_B prohibits Students from accessing Exam Answers (Answers.pdf)
(Actors <null>), which can give access to users other than teachers,

When comparing these Policies, it will be returned that  Policy_A is less permissive than  Policy_B and, therefore Policy_B does not represent the real intentions of the user who creates the Policies. Policy_A being the least permissive, it is the ideal model for a Restrictive system; that in the item Security, is what is expected.