# Semantics

We now present the formal semantics of our language:

TC and TG are vector 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 to show the relation between the values of lattice elements (things will be clearer in the examples).

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
}
EXCEPT
DENY {
Actors = Bob
Resources = EMAIL
}


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 (look at the 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!

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

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 jus by checking this one we know that $$⊥ ∈ TG ⨅ TC$$. So our last clause is also valid in our node.