Re: Inconsistent access control policies checking using TLA+

[Hillel Wayne <hwa...@xxxxxxxxx>]

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").

On Tuesday, 6 March 2018 08:49:20 UTC-6, knni...@xxxxxxxxx wrote:

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