Policy expressions and the bottom-up design of computing policies

Abstract

A policy is a sequence of rules, where each rule consists of a predicate and a decision, and where each decision is either “accept” or “reject”. A policy P is said to accept (or reject, respectively) a request iff the decision of the first rule in P, that matches the request is “accept” (or “reject”, respectively). Examples of computing policies are firewalls, routing policies and software-defined networks in the Internet, and access control policies. In this paper, we present a generalization of policies called policy expressions. A policy expression is specified using one or more policies and the three policy operators: “not”, “and”, and “or”. We show that policy expressions can be utilized to support bottom-up methods for designing policies. We also show that each policy expression can be represented by a set of special types of policies, called slices. We present several algorithms that use the slice representation of given policy expressions to verify whether the given policy expressions satisfy logical properties such as adequacy, implication, and equivalence. Finally, we present 19 equivalence laws of policy expressions.

A proofs of equivalence laws

Proof of Elementary Law 1: (${\varvec{PE_1}}$and${\varvec{FE}}) = ({\varvec{FE}}$):

No request is accepted by the policy expression (FE). Thus, the reject rules in each slice in the base of (FE) covers the accept rule of that slice. Hence, the reject rules in each slice in the base of ($PE_1$ and FE) covers the accept rule of that slice. Therefore, no request is accepted by ($PE_1$ and FE). Thus, the two expressions ($PE_1$ and FE) and (FE) are equivalent.

Proofs of Elementary Laws 2, 3, and 4 are similar and are presented in [15].

Proof of Idempotence Law 1: (not(not (${\varvec{PE_1}}))) = ({\varvec{PE_1}}$):

Our proof is by induction on the rank of the policy expression $PE_1$. (Recall that the rank of a policy expression is defined in the proof of Theorem 1.) The induction proof consists of two parts: a base case and an induction step.

Base Case: We prove that if the rank of $PE_1$ is 0 then the two policy expressions (not(not($PE_1$))) and ($PE_1$) are equivalent. This proof proceeds as follows. Because the rank of $PE_1$ is 0 then $PE_1$ is either of the form complete policy P or of the form complete policy not(P). If $PE_1$ is of the form complete policy P, then the two policy expressions (not(not(P))) and (P) are equivalent. On the other hand, if $PE_1$ is of the form complete policy not(P), then the two policy expressions not(not(P)) and (P) are equivalent and the two policy expressions (not(not(not(P)))) and (not(P)) are equivalent.

Induction Step: We assume that for every $PE_1$ of rank $k_1$ or less, the two policy expressions (not(not($PE_1$))) and ($PE_1$) are equivalent.

We then use this assumption (often called the Induction Hypothesis) to prove that for every $PE_1$ of rank ($k_1$ + 1), the two policy expressions (not(not(PE1))) and (PE1) are equivalent. Let $PE_1$ be any policy expression of rank ($k_1$ + 1). In this case, $PE_1$ is either of the form ($PE_2$ or $PE_3$) or of the form ($PE_2$ and $PE_3$), where the rank $k_2$ of $PE_2$ is $k_1$ or less and the rank $k_3$ of $PE_3$ is $k_1$ or less. In the rest of this proof, we focus on the case where $PE_1$ is of the form ($PE_2$ or $PE_3$). (The proof for the case where $PE_1$ is of the form ($PE_2$ and $PE_3$) is similar.) We have to prove that the two policy expressions (not(not($PE_2$ or $PE_3$))) and ($PE_2$ or $PE_3$) are equivalent. The induction step proceeds as follows:

• (1) From the definition of not($\langle$ a policy expression$\rangle$), the two policy expressions not($PE_2$ or $PE_3$) and (not($PE_2$) and not($PE_3$)) are equivalent.

• (2) From (1) and the definition of not($\langle$ a policy expression$\rangle$), the two policy expressions (not(not($PE_2$ or $PE_3$))) and (not(not($PE_2$)) or not(not($PE_3$))) are equivalent.

• (3) From the induction hypothesis, the two policy expressions (not(not($PE_2$))) and ($PE_2$) are equivalent and the two policy expressions (not(not($PE_3$))) and ($PE_3$) are equivalent.

• (4) From (2) and (3), the two policy expressions (not(not($PE_2$ or $PE_3$))) and ($PE_2$ or $PE_3$) are equivalent.

Proofs of Idempotence Laws 2, 3, 4, and 5 are similar and are presented in [15].

Proof of Symmetry Law 1: (${\varvec{PE_1}}$and${\varvec{PE_2}}) = ({\varvec{PE_2}}$and${\varvec{PE_1}}$):

The base of ($PE_1$ and $PE_2$) is identical to the base of ($PE_2$ and $PE_1$). Thus, the request set associated with ($PE_1$ and $PE_2$) is identical to the request set associated with ($PE_2$ and $PE_1$). Therefore, the two policy expressions ($PE_1$ and $PE_2$) and ($PE_2$ and $PE_1$) are equivalent.

Proof of Symmetry Law 2 is similar and is presented in [15].

Proof of Absorption Law 1: (${\varvec{PE_1}}$and (${\varvec{PE_1}}$or${\varvec{PE_2}})) = ({\varvec{PE_1}}$):

We need to prove two cases: (1) if ($PE_1$ and ($PE_1$ or $PE_2$)) accepts a request rq then ($PE_1$) accepts rq, and (2) if ($PE_1$) accepts a request rq then ($PE_1$ and ($PE_1$ or $PE_2$)) accepts rq.

Proof of Case (1): Assume that ($PE_1$ and ($PE_1$ or $PE_2$)) accepts a request rq. Thus, rq is accepted by a slice sl in the base of ($PE_1$ and ($PE_1$ or $PE_2$)). Slice sl is the intersection of two slices $sl'$ in the base of ($PE_1$) and $sl''$ in the base of ($PE_1$ or $PE_2$). Hence, rq is accepted by slice $sl'$ in the base of ($PE_1$). Therefore ($PE_1$) accepts rq.

Proof of Case (2): Assume that ($PE_1$) accepts a request rq. Thus, rq is accepted by a slice sl in the base of ($PE_1$). Because slice sl is also in the base of ($PE_1$ or $PE_2$), rq is accepted by a slice sl in the base of ($PE_1$ or $PE_2$). Slice sl can be viewed as the intersection of the two slices sl in the base of ($PE_1$) and sl in the base of ($PE_1$ or $PE_2$). Hence, rq is accepted by slice sl which is in the base of ($PE_1$ and ($PE_1$ or $PE_2$)). Therefore, ($PE_1$ and ($PE_1$ or $PE_2$)) accepts rq.

Proof of Absorption Law 2 is similar and is presented in [15].

Proof of De-Morgan’s Law 1: (not(${\varvec{PE_1}}$and${\varvec{PE_2}}))$ = (not(${\varvec{PE_1}}$) ornot(${\varvec{PE_2}}$)):

From definition of not($\langle$ a policy expression$\rangle$), the two policy expressions (not($PE_1$ and $PE_2$)) and (not($PE_1$) or not($PE_2$)) are equivalent.

The proof of De-Morgan’s Law 2 is similar and is presented in [15].

Proof of Distribution Law 1: (${\varvec{PE_1}}$and (${\varvec{PE_2}}$or${\varvec{PE_3}})) = (({\varvec{PE_1}}$and${\varvec{PE_2}}$) or (${\varvec{PE_1}}$and${\varvec{PE_3}}$)):

We need to prove two cases: (1) if ($PE_1$ and ($PE_2$ or $PE_3$)) accepts a request rq then (($PE_1$ and $PE_2$) or ($PE_1$ and $PE_3$)) accepts rq, and (2) if (($PE_1$ and $PE_2$) or ($PE_1$ and $PE_3$)) accepts a request rq then ($PE_1$ and ($PE_2$ or $PE_3$)) accepts rq.

Proof of Case (1): Assume that ($PE_1$ and ($PE_2$ or $PE_3$)) accepts a request rq. Thus, rq is accepted by a slice sl in the base of ($PE_1$ and ($PE_2$ or $PE_3$)). Slice sl is the intersection of two slices $sl'$ in the base of ($PE_1$) and $sl''$ in the base of ($PE_2$ or $PE_3$). Since slice $sl''$ is in the base of ($PE_2$ or $PE_3$), so $sl''$ is also in the base of ($PE_2$) or is in the base of ($PE_3$). If $sl''$ is in the base of ($PE_2$), then slice sl is also in the base of ($PE_1$ and $PE_2$). If $sl''$ is in the base of ($PE_3$), then slice sl is also in the base of ($PE_1$ and $PE_3$). Therefore slice sl is in the base of (($PE_1$ and $PE_2$) or ($PE_1$ and $PE_3$)). Thus, rq is accepted by slice sl in the base of (($PE_1$ and $PE_2$) or ($PE_1$ and $PE_3$)). Therefore (($PE_1$ and $PE_2$) or ($PE_1$ and $PE_3$)) accepts rq.

Proof of Case (2): Assume that (($PE_1$ and $PE_2$) or ($PE_1$ and $PE_3$)) accepts a request rq. Thus, rq is accepted by a slice sl in the base of (($PE_1$ and $PE_2$) or ($PE_1$ and $PE_3$)). Hence, slice sl is in the base of ($PE_1$ and $PE_2$) or is in the base of ($PE_1$ and $PE_3$). If slice sl is in the base of ($PE_1$ and $PE_2$), sl is the intersection of two slices $sl'$ in the base of ($PE_1$) and $sl''$ in the base of ($PE_2$). Because slice $sl''$ is also in the base of ($PE_2$ or $PE_3$), slice sl is in the base of ($PE_1$ and ($PE_2$ or $PE_3$)). If slice sl is in the base of ($PE_1$ and $PE_3$), sl is the intersection of two slices $sl'$ in the base of ($PE_1$) and $sl''$ in the base of ($PE_3$). Because slice $sl''$ is also in the base of ($PE_2$ or $PE_3$), slice sl is in the base of ($PE_1$ and ($PE_2$ or $PE_3$)). Thus, rq is accepted by a slice in the base of ($PE_1$ and ($PE_2$ or $PE_3$)). Therefore, ($PE_1$ and ($PE_2$ or $PE_3$)) accepts rq.

Proof of Distribution Law 2 is similar and is presented in [15].

Proof of Associativity Law 1: (${\varvec{PE_1}}$and (${\varvec{PE_2}}$and${\varvec{PE_3}})) = (({\varvec{PE_1}}$and${\varvec{PE_2}}$) and${\varvec{PE_3}}$):

We need to prove two cases: (1) if ($PE_1$ and ($PE_2$ and $PE_3$)) accepts a request rq then (($PE_1$ and $PE_2$) and $PE_3$) accepts rq, and (2) if (($PE_1$ and $PE_2$) and $PE_3$) accepts a request rq then ($PE_1$ and ($PE_2$ and $PE_3$)) accepts rq.

Proof of Case (1): Assume that ($PE_1$ and ($PE_2$ and $PE_3$)) accepts a request rq. Thus, rq is accepted by a slice sl in the base of ($PE_1$ and ($PE_2$ and $PE_3$)). Slice sl is the intersection of two slices $sl'$ in the base of ($PE_1$) and $sl''$ in the base of ($PE_2$ and $PE_3$). Also, slice $sl''$ is the intersection of two slices $sl_1''$ in the base of ($PE_2$) and $sl_2''$ in the base of ($PE_3$). Since slice sl accepts rq, rq is accepted by $sl'$ and $sl''$. Also rq is accepted by $sl_1''$ and $sl_2''$. Hence, rq is accepted by the intersection slice $s_1$ of the two slices $sl'$ and $sl_1'$, which is in the base of ($PE_1$ and $PE_2$). Moreover, rq is accepted by the intersection slice $s_2$ of the two slices $s_1$ and $sl_2''$, which is in the base of (($PE_1$ and $PE_2$) and $PE_3$). Therefore, (($PE_1$ and $PE_2$) and $PE_3$) accepts rq.

Proof of Case (2): Assume that (($PE_1$ and $PE_2$) and $PE_3$) accepts a request rq. Thus, rq is accepted by a slice sl in the base of (($PE_1$ and $PE_2$) and $PE_3$). Slice sl is the intersection of two slices $sl'$ in the base of ($PE_1$ and $PE_2$) and $sl''$ in the base of ($PE_3$). Also, slice $sl'$ is the intersection of two slices $sl_1'$ in the base of ($PE_1$) and $sl_2'$ in the base of ($PE_2$). Since slice sl accepts rq, rq is accepted by $sl'$ and $sl''$. Also rq is accepted by $sl_1'$ and $sl_2'$. Hence, rq is accepted by the intersection slice $s_1$ of the two slices $sl_2'$ and $sl''$, which is in the base of ($PE_2$ and $PE_3$). Moreover, rq is accepted by the intersection slice $s_2$ of the two slices $sl_1'$ and $s_1$, which is in the base of ($PE_1$ and ($PE_2$ and $PE_3$)). Therefore, ($PE_1$ and ($PE_2$ and $PE_3$)) accepts rq.

Proof of Associativity Law 2 is similar and is presented in [15].