Theory TopoS_Stateful_Policy_impl
theory TopoS_Stateful_Policy_impl
imports TopoS_Composition_Theory_impl TopoS_Stateful_Policy_Algorithm
begin
section‹Stateful Policy -- List Implementaion›
record 'v stateful_list_policy =
hostsL :: "'v list"
flows_fixL :: "('v ×'v) list"
flows_stateL :: "('v ×'v) list"
definition stateful_list_policy_to_list_graph :: "'v stateful_list_policy ⇒ 'v list_graph" where
"stateful_list_policy_to_list_graph 𝒯 = ⦇ nodesL = hostsL 𝒯, edgesL = (flows_fixL 𝒯) @ [e ← flows_stateL 𝒯. e ∉ set (flows_fixL 𝒯)] @ [e ← backlinks (flows_stateL 𝒯). e ∉ set (flows_fixL 𝒯)] ⦈"
lemma stateful_list_policy_to_list_graph_complies:
"list_graph_to_graph (stateful_list_policy_to_list_graph ⦇ hostsL = V, flows_fixL = E⇩f, flows_stateL = E⇩σ ⦈) =
stateful_policy_to_network_graph ⦇ hosts = set V, flows_fix = set E⇩f, flows_state = set E⇩σ ⦈"
by(simp add: stateful_list_policy_to_list_graph_def stateful_policy_to_network_graph_def all_flows_def list_graph_to_graph_def backlinks_correct, blast)
lemma wf_list_graph_stateful_list_policy_to_list_graph:
"wf_list_graph G ⟹ distinct E ⟹ set E ⊆ set (edgesL G) ⟹ wf_list_graph (stateful_list_policy_to_list_graph ⦇hostsL = nodesL G, flows_fixL = edgesL G, flows_stateL = E⦈)"
apply(simp add: wf_list_graph_def stateful_list_policy_to_list_graph_def)
apply(rule conjI)
apply(simp add: backlinks_distinct)
apply(rule conjI)
apply(simp add: backlinks_set)
apply(blast)
apply(rule conjI)
apply(simp add: backlinks_set)
apply(blast)
apply(simp add: wf_list_graph_axioms_def)
apply(rule conjI)
apply(simp add: backlinks_set)
apply(force)
apply(simp add: backlinks_set)
apply(clarsimp)
apply(erule disjE)
apply(auto)[1]
apply(erule disjE)
apply(auto)[1]
by force
subsection‹Algorithms›
fun filter_IFS_no_violations_accu :: "'v list_graph ⇒ 'v SecurityInvariant list ⇒ ('v × 'v) list ⇒ ('v × 'v) list ⇒ ('v × 'v) list" where
"filter_IFS_no_violations_accu G M accu [] = accu" |
"filter_IFS_no_violations_accu G M accu (e#Es) = (if
all_security_requirements_fulfilled (TopoS_Composition_Theory_impl.get_IFS M) (stateful_list_policy_to_list_graph ⦇ hostsL = nodesL G, flows_fixL = edgesL G, flows_stateL = (e#accu) ⦈)
then filter_IFS_no_violations_accu G M (e#accu) Es
else filter_IFS_no_violations_accu G M accu Es)"
definition filter_IFS_no_violations :: "'v list_graph ⇒ 'v SecurityInvariant list ⇒ ('v × 'v) list" where
"filter_IFS_no_violations G M = filter_IFS_no_violations_accu G M [] (edgesL G)"
lemma filter_IFS_no_violations_accu_distinct: "⟦ distinct (Es@accu) ⟧ ⟹ distinct (filter_IFS_no_violations_accu G M accu Es)"
apply(induction Es arbitrary: accu)
by(simp_all)
lemma filter_IFS_no_violations_accu_complies:
"⟦∀ (m_impl, m_spec) ∈ set M. SecurityInvariant_complies_formal_def m_impl m_spec;
wf_list_graph G; set Es ⊆ set (edgesL G); set accu ⊆ set (edgesL G); distinct (Es@accu) ⟧ ⟹
filter_IFS_no_violations_accu G (get_impl M) accu Es = TopoS_Stateful_Policy_Algorithm.filter_IFS_no_violations_accu (list_graph_to_graph G) (get_spec M) accu Es"
proof(induction Es arbitrary: accu)
case Nil
thus ?case by(simp add: get_impl_def get_spec_def)
next
case (Cons e Es)
let ?caseDistinction = "all_security_requirements_fulfilled (TopoS_Composition_Theory_impl.get_IFS (get_impl M)) (stateful_list_policy_to_list_graph ⦇ hostsL = nodesL G, flows_fixL = edgesL G, flows_stateL = (e#accu) ⦈)"
from get_IFS_get_ACS_select_simps(2)[OF Cons.prems(1)] have get_impl_zip_simp: "(get_impl (zip (TopoS_Composition_Theory_impl.get_IFS (get_impl M)) (TopoS_Composition_Theory.get_IFS (get_spec M)))) = TopoS_Composition_Theory_impl.get_IFS (get_impl M)" by simp
from get_IFS_get_ACS_select_simps(3)[OF Cons.prems(1)] have get_spec_zip_simp: "(get_spec (zip (TopoS_Composition_Theory_impl.get_IFS (get_impl M)) (TopoS_Composition_Theory.get_IFS (get_spec M)))) = TopoS_Composition_Theory.get_IFS (get_spec M)" by simp
from Cons.prems(3) Cons.prems(4) have "set (e # accu) ⊆ set (edgesL G)" by simp
from Cons.prems(4) have "set (accu) ⊆ set (edgesL G)" by simp
from Cons.prems(5) have "distinct (e # accu)" by simp
from Cons.prems(3) have "set Es ⊆ set (edgesL G)" by simp
from Cons.prems(5) have "distinct (Es @ accu)" by simp
from Cons.prems(5) have "distinct (Es @ (e # accu))" by simp
from Cons.prems(2) have validLG: "wf_list_graph (stateful_list_policy_to_list_graph ⦇hostsL = nodesL G, flows_fixL = edgesL G, flows_stateL = e # accu⦈)"
apply(rule wf_list_graph_stateful_list_policy_to_list_graph)
apply(fact ‹distinct (e # accu)›)
apply(fact ‹set (e # accu) ⊆ set (edgesL G)›)
done
from get_IFS_get_ACS_select_simps(1)[OF Cons.prems(1)]
have "∀ (m_impl, m_spec) ∈ set (zip (get_IFS (get_impl M)) (TopoS_Composition_Theory.get_IFS (get_spec M))). SecurityInvariant_complies_formal_def m_impl m_spec" .
from all_security_requirements_fulfilled_complies[OF this] have all_security_requirements_fulfilled_eq_rule:
"⋀G. wf_list_graph G ⟹
TopoS_Composition_Theory_impl.all_security_requirements_fulfilled (TopoS_Composition_Theory_impl.get_IFS (get_impl M)) G =
TopoS_Composition_Theory.all_security_requirements_fulfilled (TopoS_Composition_Theory.get_IFS (get_spec M)) (list_graph_to_graph G)"
by(simp add: get_impl_zip_simp get_spec_zip_simp)
have case_impl_spec: "?caseDistinction ⟷ TopoS_Composition_Theory.all_security_requirements_fulfilled (TopoS_Composition_Theory.get_IFS (get_spec M)) (stateful_policy_to_network_graph ⦇ hosts = set (nodesL G), flows_fix = set (edgesL G), flows_state = set (e#accu) ⦈)"
apply(subst all_security_requirements_fulfilled_eq_rule[OF validLG])
by(simp add: stateful_list_policy_to_list_graph_complies)
show ?case
proof(case_tac ?caseDistinction)
assume cTrue: ?caseDistinction
from cTrue have g1: "TopoS_Stateful_Policy_impl.filter_IFS_no_violations_accu G (get_impl M) accu (e # Es) = TopoS_Stateful_Policy_impl.filter_IFS_no_violations_accu G (get_impl M) (e # accu) Es" by simp
from cTrue[simplified case_impl_spec] have g2: "TopoS_Stateful_Policy_Algorithm.filter_IFS_no_violations_accu (list_graph_to_graph G) (get_spec M) accu (e # Es) =
TopoS_Stateful_Policy_Algorithm.filter_IFS_no_violations_accu (list_graph_to_graph G) (get_spec M) (e#accu)Es"
by(simp add: list_graph_to_graph_def)
show ?case
apply(simp only: g1 g2)
using Cons.IH[OF Cons.prems(1) Cons.prems(2) ‹set Es ⊆ set (edgesL G)› ‹set (e # accu) ⊆ set (edgesL G)› ‹distinct (Es @ (e # accu))›] by simp
next
assume cFalse: "¬ ?caseDistinction"
from cFalse have g1: "TopoS_Stateful_Policy_impl.filter_IFS_no_violations_accu G (get_impl M) accu (e # Es) = TopoS_Stateful_Policy_impl.filter_IFS_no_violations_accu G (get_impl M) accu Es" by simp
from cFalse[simplified case_impl_spec] have g2: "TopoS_Stateful_Policy_Algorithm.filter_IFS_no_violations_accu (list_graph_to_graph G) (get_spec M) accu (e # Es) =
TopoS_Stateful_Policy_Algorithm.filter_IFS_no_violations_accu (list_graph_to_graph G) (get_spec M) accu Es"
by(simp add: list_graph_to_graph_def)
show ?case
apply(simp only: g1 g2)
using Cons.IH[OF Cons.prems(1) Cons.prems(2) ‹set Es ⊆ set (edgesL G)› ‹set accu ⊆ set (edgesL G)› ‹distinct (Es @ accu)›] by simp
qed
qed
lemma filter_IFS_no_violations_complies:
"⟦ ∀ (m_impl, m_spec) ∈ set M. SecurityInvariant_complies_formal_def m_impl m_spec; wf_list_graph G ⟧ ⟹
filter_IFS_no_violations G (get_impl M) = TopoS_Stateful_Policy_Algorithm.filter_IFS_no_violations (list_graph_to_graph G) (get_spec M) (edgesL G)"
apply(unfold filter_IFS_no_violations_def TopoS_Stateful_Policy_Algorithm.filter_IFS_no_violations_def)
apply(rule filter_IFS_no_violations_accu_complies)
apply(simp_all)
apply(simp add: wf_list_graph_def)
done
fun filter_compliant_stateful_ACS_accu :: "'v list_graph ⇒ 'v SecurityInvariant list ⇒ ('v × 'v) list ⇒ ('v × 'v) list ⇒ ('v × 'v) list" where
"filter_compliant_stateful_ACS_accu G M accu [] = accu" |
"filter_compliant_stateful_ACS_accu G M accu (e#Es) = (if
e ∉ set (backlinks (edgesL G)) ∧ (∀F ∈ set (implc_get_offending_flows (get_ACS M) (stateful_list_policy_to_list_graph ⦇ hostsL = nodesL G, flows_fixL = edgesL G, flows_stateL = (e#accu) ⦈)). set F ⊆ set (backlinks (e#accu)))
then filter_compliant_stateful_ACS_accu G M (e#accu) Es
else filter_compliant_stateful_ACS_accu G M accu Es)"
definition filter_compliant_stateful_ACS :: "'v list_graph ⇒ 'v SecurityInvariant list ⇒ ('v × 'v) list" where
"filter_compliant_stateful_ACS G M = filter_compliant_stateful_ACS_accu G M [] (edgesL G)"
lemma filter_compliant_stateful_ACS_accu_complies:
"⟦∀ (m_impl, m_spec) ∈ set M. SecurityInvariant_complies_formal_def m_impl m_spec;
wf_list_graph G; set Es ⊆ set (edgesL G); set accu ⊆ set (edgesL G); distinct (Es@accu) ⟧ ⟹
filter_compliant_stateful_ACS_accu G (get_impl M) accu Es = TopoS_Stateful_Policy_Algorithm.filter_compliant_stateful_ACS_accu (list_graph_to_graph G) (get_spec M) accu Es"
proof(induction Es arbitrary: accu)
case Nil
thus ?case by(simp add: get_impl_def get_spec_def)
next
case (Cons e Es)
let ?caseDistinction = "e ∉ set (backlinks (edgesL G)) ∧ (∀F ∈ set (implc_get_offending_flows (get_ACS (get_impl M)) (stateful_list_policy_to_list_graph ⦇ hostsL = nodesL G, flows_fixL = edgesL G, flows_stateL = (e#accu) ⦈)). set F ⊆ set (backlinks (e#accu)))"
have backlinks_simp: "(e ∉ set (backlinks (edgesL G))) ⟷ (e ∉ backflows (set (edgesL G)))"
by(simp add: backlinks_correct)
have "⋀ G X. (∀F∈set (implc_get_offending_flows (TopoS_Composition_Theory_impl.get_ACS (get_impl M)) G). set F ⊆ X) =
(∀F∈set ` set (implc_get_offending_flows (TopoS_Composition_Theory_impl.get_ACS (get_impl M)) G). F ⊆ X)" by blast
also have "⋀ G X. wf_list_graph G ⟹ (∀F∈set ` set (implc_get_offending_flows (TopoS_Composition_Theory_impl.get_ACS (get_impl M)) G). F ⊆ X) =
(∀F∈get_offending_flows (TopoS_Composition_Theory.get_ACS (get_spec M)) (list_graph_to_graph G). F ⊆ X)"
using implc_get_offending_flows_complies[OF get_IFS_get_ACS_select_simps(4)[OF Cons.prems(1)], simplified get_IFS_get_ACS_select_simps[OF Cons.prems(1)]] by simp
finally have implc_get_offending_flows_simp_rule: "⋀G X. wf_list_graph G ⟹
(∀F∈set (implc_get_offending_flows (TopoS_Composition_Theory_impl.get_ACS (get_impl M)) G). set F ⊆ X) = (∀F∈get_offending_flows (TopoS_Composition_Theory.get_ACS (get_spec M)) (list_graph_to_graph G). F ⊆ X)" .
from Cons.prems(3) Cons.prems(4) have "set (e # accu) ⊆ set (edgesL G)" by simp
from Cons.prems(4) have "set (accu) ⊆ set (edgesL G)" by simp
from Cons.prems(5) have "distinct (e # accu)" by simp
from Cons.prems(3) have "set Es ⊆ set (edgesL G)" by simp
from Cons.prems(5) have "distinct (Es @ accu)" by simp
from Cons.prems(5) have "distinct (Es @ (e # accu))" by simp
from Cons.prems(2) have validLG: "wf_list_graph (stateful_list_policy_to_list_graph ⦇hostsL = nodesL G, flows_fixL = edgesL G, flows_stateL = e # accu⦈)"
apply(rule wf_list_graph_stateful_list_policy_to_list_graph)
apply(fact ‹distinct (e # accu)›)
apply(fact ‹set (e # accu) ⊆ set (edgesL G)›)
done
have "set (backlinks (e # accu)) = backflows (insert e (set accu))"
by(simp add: backlinks_set backflows_def)
have case_impl_spec: "?caseDistinction ⟷ (
e ∉ backflows (set (edgesL G)) ∧ (∀F ∈ get_offending_flows (TopoS_Composition_Theory.get_ACS (get_spec M)) (stateful_policy_to_network_graph ⦇ hosts = set (nodesL G), flows_fix = set (edgesL G), flows_state = set (e#accu) ⦈). F ⊆ (backflows (set (e#accu)))))"
apply(simp add: backlinks_simp)
apply(simp add: implc_get_offending_flows_simp_rule[OF validLG])
apply(simp add: stateful_list_policy_to_list_graph_complies)
by(simp add: ‹set (backlinks (e # accu)) = backflows (insert e (set accu))›)
show ?case
proof(case_tac ?caseDistinction)
assume cTrue: ?caseDistinction
from cTrue have g1: "TopoS_Stateful_Policy_impl.filter_compliant_stateful_ACS_accu G (get_impl M) accu (e # Es) = TopoS_Stateful_Policy_impl.filter_compliant_stateful_ACS_accu G (get_impl M) (e#accu) Es" by simp
from cTrue[simplified case_impl_spec] have g2: "TopoS_Stateful_Policy_Algorithm.filter_compliant_stateful_ACS_accu (list_graph_to_graph G) (get_spec M) accu (e # Es) =
TopoS_Stateful_Policy_Algorithm.filter_compliant_stateful_ACS_accu (list_graph_to_graph G) (get_spec M) (e#accu) Es"
by(simp add: list_graph_to_graph_def)
show ?case
apply(simp only: g1 g2)
using Cons.IH[OF Cons.prems(1) Cons.prems(2) ‹set Es ⊆ set (edgesL G)› ‹set (e # accu) ⊆ set (edgesL G)› ‹distinct (Es @ (e # accu))›] by simp
next
assume cFalse: "¬ (?caseDistinction)"
from cFalse have g1: "TopoS_Stateful_Policy_impl.filter_compliant_stateful_ACS_accu G (get_impl M) accu (e # Es) = TopoS_Stateful_Policy_impl.filter_compliant_stateful_ACS_accu G (get_impl M) accu Es" by force
from cFalse[simplified case_impl_spec] have g2: "TopoS_Stateful_Policy_Algorithm.filter_compliant_stateful_ACS_accu (list_graph_to_graph G) (get_spec M) accu (e # Es) =
TopoS_Stateful_Policy_Algorithm.filter_compliant_stateful_ACS_accu (list_graph_to_graph G) (get_spec M) accu Es"
apply(simp add: list_graph_to_graph_def) by fast
show ?case
apply(simp only: g1 g2)
using Cons.IH[OF Cons.prems(1) Cons.prems(2) ‹set Es ⊆ set (edgesL G)› ‹set accu ⊆ set (edgesL G)› ‹distinct (Es @ accu)›] by simp
qed
qed
lemma filter_compliant_stateful_ACS_cont_complies:
"⟦ ∀ (m_impl, m_spec) ∈ set M. SecurityInvariant_complies_formal_def m_impl m_spec; wf_list_graph G; set Es ⊆ set (edgesL G); distinct Es ⟧ ⟹
filter_compliant_stateful_ACS_accu G (get_impl M) [] Es = TopoS_Stateful_Policy_Algorithm.filter_compliant_stateful_ACS (list_graph_to_graph G) (get_spec M) Es"
apply(unfold filter_compliant_stateful_ACS_def TopoS_Stateful_Policy_Algorithm.filter_compliant_stateful_ACS_def)
apply(rule filter_compliant_stateful_ACS_accu_complies)
apply(simp_all)
done
lemma filter_compliant_stateful_ACS_complies:
"⟦ ∀ (m_impl, m_spec) ∈ set M. SecurityInvariant_complies_formal_def m_impl m_spec; wf_list_graph G ⟧ ⟹
filter_compliant_stateful_ACS G (get_impl M) = TopoS_Stateful_Policy_Algorithm.filter_compliant_stateful_ACS (list_graph_to_graph G) (get_spec M) (edgesL G)"
apply(unfold filter_compliant_stateful_ACS_def TopoS_Stateful_Policy_Algorithm.filter_compliant_stateful_ACS_def)
apply(rule filter_compliant_stateful_ACS_accu_complies)
apply(simp_all)
apply(simp add: wf_list_graph_def)
done
definition generate_valid_stateful_policy_IFSACS :: "'v list_graph ⇒ 'v SecurityInvariant list ⇒ 'v stateful_list_policy" where
"generate_valid_stateful_policy_IFSACS G M = (let filterIFS = filter_IFS_no_violations G M in
(let filterACS = filter_compliant_stateful_ACS_accu G M [] filterIFS in ⦇ hostsL = nodesL G, flows_fixL = edgesL G, flows_stateL = filterACS ⦈))"
fun inefficient_list_intersect :: "'a list ⇒ 'a list ⇒ 'a list" where
"inefficient_list_intersect [] bs = []" |
"inefficient_list_intersect (a#as) bs = (if a ∈ set bs then a#(inefficient_list_intersect as bs) else inefficient_list_intersect as bs)"
lemma inefficient_list_intersect_correct: "set (inefficient_list_intersect a b) = (set a) ∩ (set b)"
apply(induction a)
by(simp_all)
definition generate_valid_stateful_policy_IFSACS_2 :: "'v list_graph ⇒ 'v SecurityInvariant list ⇒ 'v stateful_list_policy" where
"generate_valid_stateful_policy_IFSACS_2 G M =
⦇ hostsL = nodesL G, flows_fixL = edgesL G, flows_stateL = inefficient_list_intersect (filter_IFS_no_violations G M) (filter_compliant_stateful_ACS G M) ⦈"
lemma generate_valid_stateful_policy_IFSACS_2_complies: "⟦∀ (m_impl, m_spec) ∈ set M. SecurityInvariant_complies_formal_def m_impl m_spec;
wf_list_graph G;
valid_reqs (get_spec M);
TopoS_Composition_Theory.all_security_requirements_fulfilled (get_spec M) (list_graph_to_graph G);
𝒯 = (generate_valid_stateful_policy_IFSACS_2 G (get_impl M))⟧ ⟹
stateful_policy_compliance ⦇hosts = set (hostsL 𝒯), flows_fix = set (flows_fixL 𝒯), flows_state = set (flows_stateL 𝒯) ⦈ (list_graph_to_graph G) (get_spec M)"
apply(rule_tac edgesList="edgesL G" in generate_valid_stateful_policy_IFSACS_2_stateful_policy_compliance)
apply(simp)
apply (metis wf_list_graph_def wf_list_graph_iff_wf_graph)
apply(simp)
apply(simp add: list_graph_to_graph_def)
apply(simp add: TopoS_Stateful_Policy_Algorithm.generate_valid_stateful_policy_IFSACS_2_def TopoS_Stateful_Policy_impl.generate_valid_stateful_policy_IFSACS_2_def)
apply(simp add: list_graph_to_graph_def inefficient_list_intersect_correct)
apply(thin_tac "𝒯 = _")
apply(frule(1) filter_compliant_stateful_ACS_complies)
apply(frule(1) filter_IFS_no_violations_complies)
apply(thin_tac "_")
apply(thin_tac "_")
apply(thin_tac "_")
apply(thin_tac "_")
apply(simp)
by (metis list_graph_to_graph_def)
end