Inconsistent access control policies checking using TLA+

[knnik...@gmail.com]

Hi All,

Is it possible to identify inconsistent access policies using TLA+?

Inconsistent access policies are one of the following:

users= {u1, u2}

dataTypes= {T1, T2}

permission= {u1 -> T1, u2 -> T2} // u1 and u2 can access T1 and T2 respectively

restriction= {u1 -> T2} // u1 can not access T2

Then we define some access policy P1:

P1 = {∀ t ∈ dataTypes u2 -> t => u1 -> t} // This tells, u1 can acces all dataTypes that u2 can access. This is an inconsistent defenition according to permission and restriction set.

I am trying to ask that, is it possible to identify these type of inconsistent definitions using TLA+?

- Thaks and Regards

Nikhila K N

[Hillel Wayne]

Yup, this is something TLA+ can handle. It'd look something like this:

VARIABLE permissions, restrictions
Users == {"u1", "u2"}
DataTypes == {"T1", "T2"}

ConsistentPolicy ==
  \A u \in Users:
    \A d \in DataTypes:
      \/ d \notin permissions[u]
      \/ d \notin restrictions[u]

AssignPermissions(from, to) ==
  /\ permissions' = [permissions EXCEPT ![to] = @ \cup permissions[from]]
  /\ UNCHANGED <<restrictions>>
 
Init ==
  /\ permissions = [u1 |-> {"T1"}, u2 |-> {"T2"}]
  /\ restrictions = [u1 |-> {"T2"}, u2 |-> {}]

Next ==
  \/ \E u, v \in Users:
    \/ AssignPermissions(u, v)

Spec == Init /\ [][Next]_<<permissions, restrictions>>

Where this fails on action AssignPermissions("u1", "u2").

[knnik...@gmail.com]

Thanks, Hillel Wayne.   This helps me to write spec :-)

[Roger Bigger]

Hi Hillel Wayne,

How did this go? I've got a similar project (lots of complex access rules) and would like to know how your project went.