Semantics

We now present the formal semantics of our language:

TC and TG are vectors of sets of lattice elements, representing respectively a clause during policy evaluation and the label of a node in the data dependency graph. As we've seen before, the data dependency graph is just a graph that shows the relation between the values of lattice elements (the examples should help make this concept clearer).

The partial order TG ⊑ TC is defined as:

\(TG ⊑ TC = ∀ x . TG_x ⊑_x TC_x\)
\(TG_x ⊑_x TC_x = ∀ v ∈ TG_x ∃ v' ∈ TC_x . v ≤_x v'\)

Where \(≤_x\) is the partial order associated with the lattice of attribute \(x\).

We also define an intersection operator \(⨅_x\):

\(TG_x ⨅_x TC_x = { ∀ v ∈ TG_x v ∧_x v' | v' ∈ TC_x }\)

Where \(∧_x\) is the meet operator for the attribute \(x\).

Last we define the notation:

\(⊥ ∈ TG ⨅ TC = ∃ x . ⊥ ∈ TG_x ⨅_x TC_x\)

Basically we want to check if there's an attribute \(x\) such that \(v ∧_x v' = ⊥\) for every \(v ∈ TG_x\) and \(v' ∈ TC_x\).

This whole thing might sound too abstract, so let’s look at some examples to clarify.

Examples

This is a walk-through example over the following policy:

main = 
  DENY
  EXCEPT {
    ALLOW {
      Actors: Analyst
      Resources: EMAIL
      Actions: Reads
    } EXCEPT {
      DENY {
        Actors: Bob
        Resources: EMAIL
        Actions: Reads
      }
    }
  };

It will be represented as a triple (operation, attributes, except_list):

clauses = [
   ("DENY", {'Actors': {"Top"}, 'Resources': {"Top"}, 'Actions': {"Top"}}, [
       ("ALLOW", {'Actors': {"Analyst"}, 'Resources': {"ip"}, "Actions": {"reads"}}, [
           ("DENY", {'Actors': {"Bob"}, 'Resources': {"ip"}, "Actions": {"reads"}}, [])
       ])
   ])
]

And the following data dependency graph with only one node:

[{Actors: {“Bob”}, Actions: {“Reads”}, Resources: {“EMAIL”}}]

That means, we want to answer the following query: can Bob perform Reads operation in the EMAIL resource?

Well, the first clause is an empty DENY (denies everything), so we must look if at least one of its EXCEPT clauses allow our node.

For the EXCEPT ALLOW clause, Bob ≤ Analyst, EMAIL ≤ EMAIL and Reads ≤ Reads (reference lattices), so OK! Then it is allowed right? No, we have to check if all of its deny clauses are valid as well.

For the last EXCEPT DENY clause, Bob ∧ Bob = Bob, EMAIL ∧ EMAIL = EMAIL, Reads ∧ Reads = Reads, therefore \(⊥ ∈ TG ⨅ TC\) is false and our policy result denies our node.

In other words, Bob can’t read emails!

Let’s try another node now, what about this one:

[{Actors: {“Alice”}, Actions: {“Reads”}, Resources: {“EMAIL”}}]

Which is equivalent to asking: can “Alice” perform the “Reads” operation on the “EMAIL” resource?

For the first DENY it’ll be the same.

In the EXCEPT ALLOW clause, Alice ≤ Analyst, EMAIL ≤ EMAIL and Reads ≤ Reads, OK! So, let’s check our DENY clause.

EXCEPT DENY, Alice ∧ Bob = ⊥ … wait a moment, we already have it! I doesn’t really matter the other attributes because just by checking this one we know that \(⊥ ∈ TG ⨅ TC\). So our last clause is also valid in our node.

That means that Alice can read emails!

Hapi

Semantics

Examples