Theory Normalisation
section‹Policy Transformations›
theory
Normalisation
imports
SeqComposition
ParallelComposition
begin
text‹
This theory provides the formalisations required for the transformation of UPF policies.
A typical usage scenario can be observed in the firewall case
study~\<^cite>‹"brucker.ea:formal-fw-testing:2014"›.
›
subsection‹Elementary Operators›
text‹
We start by providing several operators and theorems useful when reasoning about a list of
rules which should eventually be interpreted as combined using the standard override operator.
›
text‹
The following definition takes as argument a list of rules and returns a policy where the
rules are combined using the standard override operator.
›
definition list2policy::"('a ↦ 'b) list ⇒ ('a ↦ 'b)" where
"list2policy l = foldr (λ x y. (x ⨁ y)) l ∅"
text‹
Determine the position of element of a list.
›
fun position :: "'α ⇒ 'α list ⇒ nat" where
"position a [] = 0"
|"(position a (x#xs)) = (if a = x then 1 else (Suc (position a xs)))"
text‹
Provides the first applied rule of a policy given as a list of rules.
›
fun applied_rule where
"applied_rule C a (x#xs) = (if a ∈ dom (C x) then (Some x)
else (applied_rule C a xs))"
|"applied_rule C a [] = None"
text ‹
The following is used if the list is constructed backwards.
›
definition applied_rule_rev where
"applied_rule_rev C a x = applied_rule C a (rev x)"
text‹
The following is a typical policy transformation. It can be applied to any type of policy and
removes all the rules from a policy with an empty domain. It takes two arguments: a semantic
interpretation function and a list of rules.
›
fun rm_MT_rules where
"rm_MT_rules C (x#xs) = (if dom (C x)= {}
then rm_MT_rules C xs
else x#(rm_MT_rules C xs))"
|"rm_MT_rules C [] = []"
text ‹
The following invariant establishes that there are no rules with an empty domain in a list
of rules.
›
fun none_MT_rules where
"none_MT_rules C (x#xs) = (dom (C x) ≠ {} ∧ (none_MT_rules C xs))"
|"none_MT_rules C [] = True"
text‹
The following related invariant establishes that the policy has not a completely empty domain.
›
fun not_MT where
"not_MT C (x#xs) = (if (dom (C x) = {}) then (not_MT C xs) else True)"
|"not_MT C [] = False"
text‹
Next, a few theorems about the two invariants and the transformation:
›
lemma none_MT_rules_vs_notMT: "none_MT_rules C p ⟹ p ≠ [] ⟹ not_MT C p"
apply (induct p)
apply (simp_all)
done
lemma rmnMT: "none_MT_rules C (rm_MT_rules C p)"
apply (induct p)
apply (simp_all)
done
lemma rmnMT2: "none_MT_rules C p ⟹ (rm_MT_rules C p) = p"
apply (induct p)
apply (simp_all)
done
lemma nMTcharn: "none_MT_rules C p = (∀ r ∈ set p. dom (C r) ≠ {})"
apply (induct p)
apply (simp_all)
done
lemma nMTeqSet: "set p = set s ⟹ none_MT_rules C p = none_MT_rules C s"
apply (simp add: nMTcharn)
done
lemma notMTnMT: "⟦a ∈ set p; none_MT_rules C p⟧ ⟹ dom (C a) ≠ {}"
apply (simp add: nMTcharn)
done
lemma none_MT_rulesconc: "none_MT_rules C (a@[b]) ⟹ none_MT_rules C a"
apply (induct a)
apply (simp_all)
done
lemma nMTtail: "none_MT_rules C p ⟹ none_MT_rules C (tl p)"
apply (induct p)
apply (simp_all)
done
lemma not_MTimpnotMT[simp]: "not_MT C p ⟹ p ≠ []"
apply (auto)
done
lemma SR3nMT: "¬ not_MT C p ⟹ rm_MT_rules C p = []"
apply (induct p)
apply (auto simp: if_splits)
done
lemma NMPcharn: "⟦a ∈ set p; dom (C a) ≠ {}⟧ ⟹ not_MT C p"
apply (induct p)
apply (auto simp: if_splits)
done
lemma NMPrm: "not_MT C p ⟹ not_MT C (rm_MT_rules C p)"
apply (induct p)
apply (simp_all)
done
text‹Next, a few theorems about applied\_rule:›
lemma mrconc: "applied_rule_rev C x p = Some a ⟹ applied_rule_rev C x (b#p) = Some a"
proof (induct p rule: rev_induct)
case Nil show ?case using Nil
by (simp add: applied_rule_rev_def)
next
case (snoc xs x) show ?case using snoc
apply (simp add: applied_rule_rev_def if_splits)
by (metis option.inject)
qed
lemma mreq_end: "⟦applied_rule_rev C x b = Some r; applied_rule_rev C x c = Some r⟧ ⟹
applied_rule_rev C x (a#b) = applied_rule_rev C x (a#c)"
by (simp add: mrconc)
lemma mrconcNone: "applied_rule_rev C x p = None ⟹
applied_rule_rev C x (b#p) = applied_rule_rev C x [b]"
proof (induct p rule: rev_induct)
case Nil show ?case
by (simp add: applied_rule_rev_def)
next
case (snoc ys y) show ?case using snoc
proof (cases "x ∈ dom (C ys)")
case True show ?thesis using True snoc
by (auto simp: applied_rule_rev_def)
next
case False show ?thesis using False snoc
by (auto simp: applied_rule_rev_def)
qed
qed
lemma mreq_endNone: "⟦applied_rule_rev C x b = None; applied_rule_rev C x c = None⟧ ⟹
applied_rule_rev C x (a#b) = applied_rule_rev C x (a#c)"
by (metis mrconcNone)
lemma mreq_end2: "applied_rule_rev C x b = applied_rule_rev C x c ⟹
applied_rule_rev C x (a#b) = applied_rule_rev C x (a#c)"
apply (case_tac "applied_rule_rev C x b = None")
apply (auto intro: mreq_end mreq_endNone)
done
lemma mreq_end3: "applied_rule_rev C x p ≠ None ⟹
applied_rule_rev C x (b # p) = applied_rule_rev C x (p)"
by (auto simp: mrconc)
lemma mrNoneMT: "⟦r ∈ set p; applied_rule_rev C x p = None⟧ ⟹
x ∉ dom (C r)"
proof (induct p rule: rev_induct)
case Nil show ?case using Nil
by (simp add: applied_rule_rev_def)
next
case (snoc y ys) show ?case using snoc
proof (cases "r ∈ set ys")
case True show ?thesis using snoc True
by (simp add: applied_rule_rev_def split: if_split_asm)
next
case False show ?thesis using snoc False
by (simp add: applied_rule_rev_def split: if_split_asm)
qed
qed
subsection‹Distributivity of the Transformation.›
text‹
The scenario is the following (can be applied iteratively):
\begin{itemize}
\item Two policies are combined using one of the parallel combinators
\item (e.g. P = P1 P2) (At least) one of the constituent policies has
\item a normalisation procedures, which as output produces a list of
\item policies that are semantically equivalent to the original policy if
\item combined from left to right using the override operator.
\end{itemize}
›
text‹
The following function is crucial for the distribution. Its arguments are a policy, a list
of policies, a parallel combinator, and a range and a domain coercion function.
›
fun prod_list :: "('α ↦'β) ⇒ (('γ ↦'δ) list) ⇒
(('α ↦'β) ⇒ ('γ ↦'δ) ⇒ (('α × 'γ) ↦ ('β × 'δ))) ⇒
(('β × 'δ) ⇒ 'y) ⇒ ('x ⇒ ('α × 'γ)) ⇒
(('x ↦ 'y) list)" (infixr ‹⨂⇩L› 54) where
"prod_list x (y#ys) par_comb ran_adapt dom_adapt =
((ran_adapt o_f ((par_comb x y) o dom_adapt))#(prod_list x ys par_comb ran_adapt dom_adapt))"
| "prod_list x [] par_comb ran_adapt dom_adapt = []"
text‹
An instance, as usual there are four of them.
›
definition prod_2_list :: "[('α ↦'β), (('γ ↦'δ) list)] ⇒
(('β × 'δ) ⇒ 'y) ⇒ ('x ⇒ ('α × 'γ)) ⇒
(('x ↦ 'y) list)" (infixr ‹⨂⇩2⇩L› 55) where
"x ⨂⇩2⇩L y = (λ d r. (x ⨂⇩L y) (⨂⇩2) d r)"
lemma list2listNMT: "x ≠ [] ⟹ map sem x ≠ []"
apply (case_tac x)
apply (simp_all)
done
lemma two_conc: "(prod_list x (y#ys) p r d) = ((r o_f ((p x y) o d))#(prod_list x ys p r d))"
by simp
text‹
The following two invariants establish if the law of distributivity holds for a combinator
and if an operator is strict regarding undefinedness.
›
definition is_distr where
"is_distr p = (λ g f. (∀ N P1 P2. ((g o_f ((p N (P1 ⨁ P2)) o f)) =
((g o_f ((p N P1) o f)) ⨁ (g o_f ((p N P2) o f))))))"
definition is_strict where
"is_strict p = (λ r d. ∀ P1. (r o_f (p P1 ∅ ∘ d)) = ∅)"
lemma is_distr_orD: "is_distr (⨂⇩∨⇩D) d r"
apply (simp add: is_distr_def)
apply (rule allI)+
apply (rule distr_orD)
apply (simp)
done
lemma is_strict_orD: "is_strict (⨂⇩∨⇩D) d r"
apply (simp add: is_strict_def)
apply (simp add: policy_range_comp_def)
done
lemma is_distr_2: "is_distr (⨂⇩2) d r"
apply (simp add: is_distr_def)
apply (rule allI)+
apply (rule distr_or2)
by simp
lemma is_strict_2: "is_strict (⨂⇩2) d r"
apply (simp only: is_strict_def)
apply simp
apply (simp add: policy_range_comp_def)
done
lemma domStart: "t ∈ dom p1 ⟹ (p1 ⨁ p2) t = p1 t"
apply (simp add: map_add_dom_app_simps)
done
lemma notDom: "x ∈ dom A ⟹ ¬ A x = None"
apply auto
done
text‹
The following theorems are crucial: they establish the correctness of the distribution.
›
lemma Norm_Distr_1: "((r o_f (((⨂⇩1) P1 (list2policy P2)) o d)) x =
((list2policy ((P1 ⨂⇩L P2) (⨂⇩1) r d)) x))"
proof (induct P2)
case Nil show ?case
by (simp add: policy_range_comp_def list2policy_def)
next
case (Cons p ps) show ?case using Cons
proof (cases "x ∈ dom (r o_f ((P1 ⨂⇩1 p) ∘ d))")
case True show ?thesis using True
by (auto simp: list2policy_def policy_range_comp_def prod_1_def
split: option.splits decision.splits prod.splits)
next
case False show ?thesis using Cons False
by (auto simp: list2policy_def policy_range_comp_def map_add_dom_app_simps(3) prod_1_def
split: option.splits decision.splits prod.splits)
qed
qed
lemma Norm_Distr_2: "((r o_f (((⨂⇩2) P1 (list2policy P2)) o d)) x =
((list2policy ((P1 ⨂⇩L P2) (⨂⇩2) r d)) x))"proof (induct P2)
case Nil show ?case
by (simp add: policy_range_comp_def list2policy_def)
next
case (Cons p ps) show ?case using Cons
proof (cases "x ∈ dom (r o_f ((P1 ⨂⇩2 p) ∘ d))")
case True show ?thesis using True
by (auto simp: list2policy_def prod_2_def policy_range_comp_def
split: option.splits decision.splits prod.splits)
next
case False show ?thesis using Cons False
by (auto simp: policy_range_comp_def list2policy_def map_add_dom_app_simps(3) prod_2_def
split: option.splits decision.splits prod.splits)
qed
qed
lemma Norm_Distr_A: "((r o_f (((⨂⇩∨⇩A) P1 (list2policy P2)) o d)) x =
((list2policy ((P1 ⨂⇩L P2) (⨂⇩∨⇩A) r d)) x))"
proof (induct P2)
case Nil show ?case
by (simp add: policy_range_comp_def list2policy_def)
next
case (Cons p ps) show ?case using Cons
proof (cases "x ∈ dom (r o_f ((P1 ⨂⇩∨⇩A p) ∘ d))")
case True show ?thesis using True
by (auto simp: policy_range_comp_def list2policy_def prod_orA_def
split: option.splits decision.splits prod.splits)
next
case False show ?thesis using Cons False
by (auto simp: policy_range_comp_def list2policy_def map_add_dom_app_simps(3) prod_orA_def
split: option.splits decision.splits prod.splits)
qed
qed
lemma Norm_Distr_D: "((r o_f (((⨂⇩∨⇩D) P1 (list2policy P2)) o d)) x =
((list2policy ((P1 ⨂⇩L P2) (⨂⇩∨⇩D) r d)) x))"
proof (induct P2)
case Nil show ?case
by (simp add: policy_range_comp_def list2policy_def)
next
case (Cons p ps) show ?case using Cons
proof (cases "x ∈ dom (r o_f ((P1 ⨂⇩∨⇩D p) ∘ d))")
case True show ?thesis using True
by (auto simp: policy_range_comp_def list2policy_def prod_orD_def
split: option.splits decision.splits prod.splits)
next
case False show ?thesis using Cons False
by (auto simp: policy_range_comp_def list2policy_def map_add_dom_app_simps(3) prod_orD_def
split: option.splits decision.splits prod.splits)
qed
qed
text ‹Some domain reasoning›
lemma domSubsetDistr1: "dom A = UNIV ⟹ dom ((λ(x, y). x) o_f (A ⨂⇩1 B) o (λ x. (x,x))) = dom B"
apply (rule set_eqI)
apply (rule iffI)
apply (auto simp: prod_1_def policy_range_comp_def dom_def
split: decision.splits option.splits prod.splits)
done
lemma domSubsetDistr2: "dom A = UNIV ⟹ dom ((λ(x, y). x) o_f (A ⨂⇩2 B) o (λ x. (x,x))) = dom B"
apply (rule set_eqI)
apply (rule iffI)
apply (auto simp: prod_2_def policy_range_comp_def dom_def
split: decision.splits option.splits prod.splits)
done
lemma domSubsetDistrA: "dom A = UNIV ⟹ dom ((λ(x, y). x) o_f (A ⨂⇩∨⇩A B) o (λ x. (x,x))) = dom B"
apply (rule set_eqI)
apply (rule iffI)
apply (auto simp: prod_orA_def policy_range_comp_def dom_def
split: decision.splits option.splits prod.splits)
done
lemma domSubsetDistrD: "dom A = UNIV ⟹ dom ((λ(x, y). x) o_f (A ⨂⇩∨⇩D B) o (λ x. (x,x))) = dom B"
apply (rule set_eqI)
apply (rule iffI)
apply (auto simp: prod_orD_def policy_range_comp_def dom_def
split: decision.splits option.splits prod.splits)
done
end