Theory Primitive_Abstract
theory Primitive_Abstract
imports
Common_Primitive_toString
Transform
Conntrack_State_Transform
begin
section‹Abstracting over Primitives›
text‹Abstract over certain primitives. The first parameter is a function
@{typ "'i::len common_primitive negation_type ⇒ bool"} to select the primitives to be abstracted over.
The @{typ "'i::len common_primitive"} is wrapped in a @{typ "'i::len common_primitive negation_type"} to let the function
selectively abstract only over negated, non-negated, or both kinds of primitives.
This functions requires a @{const normalized_nnf_match}.
›
fun abstract_primitive
:: "('i::len common_primitive negation_type ⇒ bool) ⇒ 'i common_primitive match_expr ⇒ 'i common_primitive match_expr"
where
"abstract_primitive _ MatchAny = MatchAny" |
"abstract_primitive disc (Match a) =
(if
disc (Pos a)
then
Match (Extra (common_primitive_toString ipaddr_generic_toString a))
else
(Match a))" |
"abstract_primitive disc (MatchNot (Match a)) =
(if
disc (Neg a)
then
Match (Extra (''! ''@common_primitive_toString ipaddr_generic_toString a))
else
(MatchNot (Match a)))" |
"abstract_primitive disc (MatchNot m) = MatchNot (abstract_primitive disc m)" |
"abstract_primitive disc (MatchAnd m1 m2) = MatchAnd (abstract_primitive disc m1) (abstract_primitive disc m2)"
text‹For example, a simple firewall requires that no negated interfaces and protocols occur in the
expression.›
definition abstract_for_simple_firewall :: "'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr"
where "abstract_for_simple_firewall ≡ abstract_primitive (λr. case r
of Pos a ⇒ is_CT_State a ∨ is_L4_Flags a
| Neg a ⇒ is_Iiface a ∨ is_Oiface a ∨ is_Prot a ∨ is_CT_State a ∨ is_L4_Flags a)"
lemma abstract_primitive_preserves_normalized:
"normalized_src_ports m ⟹ normalized_src_ports (abstract_primitive disc m)"
"normalized_dst_ports m ⟹ normalized_dst_ports (abstract_primitive disc m)"
"normalized_src_ips m ⟹ normalized_src_ips (abstract_primitive disc m)"
"normalized_dst_ips m ⟹ normalized_dst_ips (abstract_primitive disc m)"
"normalized_nnf_match m ⟹ normalized_nnf_match (abstract_primitive disc m)"
by(induction disc m rule: abstract_primitive.induct) (simp_all)
lemma abstract_primitive_preserves_nodisc:
"¬ has_disc disc' m ⟹ (∀str. ¬ disc' (Extra str)) ⟹ ¬ has_disc disc' (abstract_primitive disc m)"
by(induction disc m rule: abstract_primitive.induct)(simp_all)
lemma abstract_primitive_preserves_nodisc_nedgated:
"¬ has_disc_negated disc' neg m ⟹ (∀str. ¬ disc' (Extra str)) ⟹ ¬ has_disc_negated disc' neg (abstract_primitive disc m)"
by(induction disc m arbitrary: neg rule: abstract_primitive.induct) simp+
lemma abstract_primitive_nodisc:
"∀x. disc' x ⟶ disc (Pos x) ∧ disc (Neg x) ⟹ (∀str. ¬ disc' (Extra str)) ⟹ ¬ has_disc disc' (abstract_primitive disc m)"
by(induction disc m rule: abstract_primitive.induct) auto
lemma abstract_primitive_preserves_not_has_disc_negated:
"∀a. ¬ disc (Extra a)⟹ ¬ has_disc_negated disc neg m ⟹ ¬ has_disc_negated disc neg (abstract_primitive sel_f m)"
by(induction sel_f m arbitrary: neg rule: abstract_primitive.induct) simp+
lemma abstract_for_simple_firewall_preserves_nodisc_negated:
"∀a. ¬ disc (Extra a)⟹ ¬ has_disc_negated disc False m ⟹ ¬ has_disc_negated disc False (abstract_for_simple_firewall m)"
unfolding abstract_for_simple_firewall_def
using abstract_primitive_preserves_nodisc_nedgated by blast
text‹The function @{const ctstate_assume_state} can be used to fix a state and hence remove all state matches from the ruleset.
It is therefore advisable to create a simple firewall for a fixed state, e.g. with @{const ctstate_assume_new} before
calling to @{const abstract_for_simple_firewall}.›
lemma not_hasdisc_ctstate_assume_state: "¬ has_disc is_CT_State (ctstate_assume_state s m)"
by(induction m rule: ctstate_assume_state.induct) (simp_all)
lemma abstract_for_simple_firewall_hasdisc: fixes m :: "'i::len common_primitive match_expr"
shows "¬ has_disc is_CT_State (abstract_for_simple_firewall m)"
and "¬ has_disc is_L4_Flags (abstract_for_simple_firewall m)"
unfolding abstract_for_simple_firewall_def
apply(induction "(λr:: 'i common_primitive negation_type. case r of Pos a ⇒ is_CT_State a | Neg a ⇒ is_Iiface a ∨ is_Oiface a ∨ is_Prot a ∨ is_CT_State a)" m rule: abstract_primitive.induct)
apply(simp_all)
done
lemma abstract_for_simple_firewall_negated_ifaces_prots: fixes m :: "'i::len common_primitive match_expr"
shows "normalized_nnf_match m ⟹ ¬ has_disc_negated (λa. is_Iiface a ∨ is_Oiface a) False (abstract_for_simple_firewall m)"
and "normalized_nnf_match m ⟹ ¬ has_disc_negated is_Prot False (abstract_for_simple_firewall m)"
unfolding abstract_for_simple_firewall_def
apply(induction "(λr:: 'i common_primitive negation_type. case r of Pos a ⇒ is_CT_State a | Neg a ⇒ is_Iiface a ∨ is_Oiface a ∨ is_Prot a ∨ is_CT_State a)" m rule: abstract_primitive.induct)
apply(simp_all)
done
context
begin
private lemma abstract_primitive_in_doubt_allow_Allow:
"primitive_matcher_generic β ⟹ normalized_nnf_match m ⟹
matches (β, in_doubt_allow) m action.Accept p ⟹
matches (β, in_doubt_allow) (abstract_primitive disc m) action.Accept p"
by(induction disc m rule: abstract_primitive.induct)
(simp_all add: bunch_of_lemmata_about_matches(1) primitive_matcher_generic.Extra_single)
private lemma abstract_primitive_in_doubt_allow_Allow2:
"primitive_matcher_generic β ⟹ normalized_nnf_match m ⟹
¬ matches (β, in_doubt_allow) m action.Drop p ⟹
¬ matches (β, in_doubt_allow) (abstract_primitive disc m) action.Drop p"
proof(induction disc m rule: abstract_primitive.induct)
case(5 m1 m2) thus ?case by (auto simp add: bunch_of_lemmata_about_matches(1))
qed(simp_all add: bunch_of_lemmata_about_matches(1) primitive_matcher_generic.Extra_single)
private lemma abstract_primitive_in_doubt_allow_Deny:
"primitive_matcher_generic β ⟹ normalized_nnf_match m ⟹
matches (β, in_doubt_allow) (abstract_primitive disc m) action.Drop p ⟹
matches (β, in_doubt_allow) m action.Drop p"
apply(induction disc m rule: abstract_primitive.induct)
apply (simp_all add: bunch_of_lemmata_about_matches(1))
apply(auto simp add: primitive_matcher_generic.Extra_single primitive_matcher_generic.Extra_single_not split: if_split_asm)
done
private lemma abstract_primitive_in_doubt_allow_Deny2:
"primitive_matcher_generic β ⟹ normalized_nnf_match m ⟹
¬ matches (β, in_doubt_allow) (abstract_primitive disc m) action.Accept p ⟹
¬ matches (β, in_doubt_allow) m action.Accept p"
apply(induction disc m rule: abstract_primitive.induct)
apply (simp_all add: bunch_of_lemmata_about_matches(1))
apply(auto simp add: primitive_matcher_generic.Extra_single primitive_matcher_generic.Extra_single_not split: if_split_asm)
done
theorem abstract_primitive_in_doubt_allow_generic:
fixes β::"('i::len common_primitive, ('i, 'a) tagged_packet_scheme) exact_match_tac"
assumes generic: "primitive_matcher_generic β"
and n: "∀ r ∈ set rs. normalized_nnf_match (get_match r)"
and simple: "simple_ruleset rs"
defines "γ ≡ (β, in_doubt_allow)" and "abstract disc ≡ optimize_matches (abstract_primitive disc)"
shows "{p. γ,p⊢ ⟨abstract disc rs, Undecided⟩ ⇒⇩α Decision FinalDeny} ⊆ {p. γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalDeny}"
(is ?deny)
and "{p. γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow} ⊆ {p. γ,p⊢ ⟨abstract disc rs, Undecided⟩ ⇒⇩α Decision FinalAllow}"
(is ?allow)
proof -
from simple have "good_ruleset rs" using simple_imp_good_ruleset by fast
from optimize_matches_simple_ruleset simple simple_imp_good_ruleset have
good: "good_ruleset (optimize_matches (abstract_primitive disc) rs)" by fast
let ?γ="(β, in_doubt_allow) :: ('i::len common_primitive, ('i, 'a) tagged_packet_scheme) match_tac"
have abstract_primitive_in_doubt_allow_help1:
"approximating_bigstep_fun γ p (optimize_matches (abstract_primitive disc) rs) Undecided = Decision FinalAllow"
if prem: "approximating_bigstep_fun γ p rs Undecided = Decision FinalAllow" for p
proof -
from simple have "wf_ruleset γ p rs" using good_imp_wf_ruleset simple_imp_good_ruleset by fast
from this simple prem n show ?thesis
unfolding γ_def
proof(induction ?γ p rs Undecided rule: approximating_bigstep_fun_induct_wf)
case (MatchAccept p m a rs)
from MatchAccept.prems
abstract_primitive_in_doubt_allow_Allow[OF generic] MatchAccept.hyps have
"matches ?γ (abstract_primitive disc m) action.Accept p" by simp
thus ?case
apply(simp add: MatchAccept.hyps(2))
using optimize_matches_matches_fst by fastforce
next
case (Nomatch p m a rs) thus ?case
proof(cases "matches ?γ (abstract_primitive disc m) a p")
case False with Nomatch show ?thesis
apply(simp add: optimize_matches_def)
using simple_ruleset_tail by blast
next
case True
from Nomatch.prems(1) have "a = action.Accept ∨ a = action.Drop" by(simp add: simple_ruleset_def)
from Nomatch.hyps(1) Nomatch.prems(3) abstract_primitive_in_doubt_allow_Allow2[OF generic] have
"a = action.Drop ⟹ ¬ matches ?γ (abstract_primitive disc m) action.Drop p" by simp
with True ‹a = action.Accept ∨ a = action.Drop› have "a = action.Accept" by blast
with True show ?thesis
using optimize_matches_matches_fst by fastforce
qed
qed(simp_all add: simple_ruleset_def)
qed
have abstract_primitive_in_doubt_allow_help2:
"approximating_bigstep_fun γ p rs Undecided = Decision FinalDeny"
if prem: "approximating_bigstep_fun γ p (optimize_matches (abstract_primitive disc) rs) Undecided = Decision FinalDeny"
for p
proof -
from simple have "wf_ruleset γ p rs" using good_imp_wf_ruleset simple_imp_good_ruleset by fast
from this simple prem n show ?thesis
unfolding γ_def
proof(induction ?γ p rs Undecided rule: approximating_bigstep_fun_induct_wf)
case Empty thus ?case by(simp add: optimize_matches_def)
next
case (MatchAccept p m a rs)
from MatchAccept.prems abstract_primitive_in_doubt_allow_Allow[OF generic] MatchAccept.hyps have
1: "matches ?γ (abstract_primitive disc m) action.Accept p" by simp
with MatchAccept have "approximating_bigstep_fun ?γ p
(Rule (abstract_primitive disc m) action.Accept # (optimize_matches (abstract_primitive disc) rs)) Undecided = Decision FinalDeny"
using optimize_matches_matches_fst by metis
with 1 have False by(simp)
thus ?case ..
next
case (Nomatch p m a rs) thus ?case
proof(cases "matches ?γ (abstract_primitive disc m) a p")
case False
with Nomatch.prems(2) have "approximating_bigstep_fun ?γ p (optimize_matches (abstract_primitive disc) rs) Undecided = Decision FinalDeny"
by(simp add: optimize_matches_def split: if_split_asm)
with Nomatch have IH: "approximating_bigstep_fun ?γ p rs Undecided = Decision FinalDeny"
using simple_ruleset_tail by auto
with Nomatch(1) show ?thesis by simp
next
case True
from Nomatch.prems(2) True have 1: "approximating_bigstep_fun ?γ p
(Rule (abstract_primitive disc m) a # (optimize_matches (abstract_primitive disc) rs)) Undecided = Decision FinalDeny"
using optimize_matches_matches_fst by metis
from Nomatch.prems(1) have "a = action.Accept ∨ a = action.Drop" by(simp add: simple_ruleset_def)
from Nomatch.hyps(1) Nomatch.prems(3) abstract_primitive_in_doubt_allow_Allow2[OF generic] have
"a = action.Drop ⟹ ¬ matches ?γ (abstract_primitive disc m) action.Drop p" by simp
with True ‹a = action.Accept ∨ a = action.Drop› have "a = action.Accept" by blast
with 1 True have False by simp
thus ?thesis ..
qed
qed(simp_all add: simple_ruleset_def)
qed
from good approximating_semantics_iff_fun_good_ruleset abstract_primitive_in_doubt_allow_help1 ‹good_ruleset rs› show ?allow
unfolding abstract_def by fast
from good approximating_semantics_iff_fun_good_ruleset abstract_primitive_in_doubt_allow_help2 ‹good_ruleset rs› γ_def show ?deny
unfolding abstract_def by fast
qed
corollary abstract_primitive_in_doubt_allow:
assumes "∀ r ∈ set rs. normalized_nnf_match (get_match r)" and "simple_ruleset rs"
defines "γ ≡ (common_matcher, in_doubt_allow)" and "abstract disc ≡ optimize_matches (abstract_primitive disc)"
shows "{p. γ,p⊢ ⟨abstract disc rs, Undecided⟩ ⇒⇩α Decision FinalDeny} ⊆ {p. γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalDeny}"
and "{p. γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow} ⊆ {p. γ,p⊢ ⟨abstract disc rs, Undecided⟩ ⇒⇩α Decision FinalAllow}"
unfolding γ_def abstract_def
using assms abstract_primitive_in_doubt_allow_generic[OF primitive_matcher_generic_common_matcher] by blast+
end
context
begin
private lemma abstract_primitive_in_doubt_deny_Deny:
"primitive_matcher_generic β ⟹ normalized_nnf_match m ⟹
matches (β, in_doubt_deny) m action.Drop p ⟹
matches (β, in_doubt_deny) (abstract_primitive disc m) action.Drop p"
by(induction disc m rule: abstract_primitive.induct)
(simp_all add: bunch_of_lemmata_about_matches(1) primitive_matcher_generic.Extra_single)
private lemma abstract_primitive_in_doubt_deny_Deny2:
"primitive_matcher_generic β ⟹ normalized_nnf_match m ⟹
¬ matches (β, in_doubt_deny) m action.Accept p ⟹
¬ matches (β, in_doubt_deny) (abstract_primitive disc m) action.Accept p"
proof(induction disc m rule: abstract_primitive.induct)
case(5 m1 m2) thus ?case by (auto simp add: bunch_of_lemmata_about_matches(1))
qed(simp_all add: bunch_of_lemmata_about_matches(1) primitive_matcher_generic.Extra_single)
private lemma abstract_primitive_in_doubt_deny_Allow:
"primitive_matcher_generic β ⟹ normalized_nnf_match m ⟹
matches (β, in_doubt_deny) (abstract_primitive disc m) action.Accept p ⟹
matches (β, in_doubt_deny) m action.Accept p"
apply(induction disc m rule: abstract_primitive.induct)
apply (simp_all add: bunch_of_lemmata_about_matches(1))
apply(auto simp add: primitive_matcher_generic.Extra_single primitive_matcher_generic.Extra_single_not split: if_split_asm)
done
private lemma abstract_primitive_in_doubt_deny_Allow2:
"primitive_matcher_generic β ⟹ normalized_nnf_match m ⟹
¬ matches (β, in_doubt_deny) (abstract_primitive disc m) action.Drop p ⟹
¬ matches (β, in_doubt_deny) m action.Drop p"
apply(induction disc m rule: abstract_primitive.induct)
apply (simp_all add: bunch_of_lemmata_about_matches(1))
apply(auto simp add: primitive_matcher_generic.Extra_single primitive_matcher_generic.Extra_single_not split: if_split_asm)
done
theorem abstract_primitive_in_doubt_deny_generic:
fixes β::"('i::len common_primitive, ('i, 'a) tagged_packet_scheme) exact_match_tac"
assumes generic: "primitive_matcher_generic β"
and n: "∀ r ∈ set rs. normalized_nnf_match (get_match r)"
and simple: "simple_ruleset rs"
defines "γ ≡ (β, in_doubt_deny)" and "abstract disc ≡ optimize_matches (abstract_primitive disc)"
shows "{p. γ,p⊢ ⟨abstract disc rs, Undecided⟩ ⇒⇩α Decision FinalAllow} ⊆ {p. γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow}"
(is ?allow)
and "{p. γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalDeny} ⊆ {p. γ,p⊢ ⟨abstract disc rs, Undecided⟩ ⇒⇩α Decision FinalDeny}"
(is ?deny)
proof -
from simple have "good_ruleset rs" using simple_imp_good_ruleset by fast
from optimize_matches_simple_ruleset simple simple_imp_good_ruleset have
good: "good_ruleset (optimize_matches (abstract_primitive disc) rs)" by fast
let ?γ="(β, in_doubt_deny) :: ('i::len common_primitive, ('i, 'a) tagged_packet_scheme) match_tac"
have abstract_primitive_in_doubt_deny_help1:
"approximating_bigstep_fun γ p (optimize_matches (abstract_primitive disc) rs) Undecided = Decision FinalDeny"
if prem: "approximating_bigstep_fun γ p rs Undecided = Decision FinalDeny" for p
proof -
from simple have "wf_ruleset γ p rs" using good_imp_wf_ruleset simple_imp_good_ruleset by fast
from this simple prem n show ?thesis
unfolding γ_def
proof(induction ?γ p rs Undecided rule: approximating_bigstep_fun_induct_wf)
case (MatchDrop p m a rs)
from MatchDrop.prems abstract_primitive_in_doubt_deny_Deny[OF generic] MatchDrop.hyps have
"matches ?γ (abstract_primitive disc m) action.Drop p" by simp
thus ?case
apply(simp add: MatchDrop.hyps(2))
using optimize_matches_matches_fst by fastforce
next
case (Nomatch p m a rs) thus ?case
proof(cases "matches ?γ (abstract_primitive disc m) a p")
case False with Nomatch show ?thesis
apply(simp add: optimize_matches_def)
using simple_ruleset_tail by blast
next
case True
from Nomatch.prems(1) have "a = action.Accept ∨ a = action.Drop" by(simp add: simple_ruleset_def)
from Nomatch.hyps(1) Nomatch.prems(3) abstract_primitive_in_doubt_deny_Deny2[OF generic] have
"a = action.Accept ⟹ ¬ matches ?γ (abstract_primitive disc m) action.Accept p" by(simp)
with True ‹a = action.Accept ∨ a = action.Drop› have "a = action.Drop" by blast
with True show ?thesis using optimize_matches_matches_fst by fastforce
qed
qed(simp_all add: simple_ruleset_def)
qed
have abstract_primitive_in_doubt_deny_help2:
"approximating_bigstep_fun γ p rs Undecided = Decision FinalAllow"
if prem: "approximating_bigstep_fun γ p (optimize_matches (abstract_primitive disc) rs) Undecided = Decision FinalAllow"
for p
proof -
from simple have "wf_ruleset ?γ p rs" using good_imp_wf_ruleset simple_imp_good_ruleset by fast
from this simple prem n show ?thesis
unfolding γ_def
proof(induction ?γ p rs Undecided rule: approximating_bigstep_fun_induct_wf)
case Empty thus ?case by(simp add: optimize_matches_def)
next
case (MatchAccept p m a rs) thus ?case by auto
next
case (MatchDrop p m a rs)
from MatchDrop.prems abstract_primitive_in_doubt_deny_Deny[OF generic] MatchDrop.hyps have
1: "matches ?γ (abstract_primitive disc m) action.Drop p" by simp
from MatchDrop have "approximating_bigstep_fun ?γ p
(Rule (abstract_primitive disc m) action.Drop # (optimize_matches (abstract_primitive disc) rs)) Undecided = Decision FinalAllow"
using optimize_matches_matches_fst 1 by fastforce
with 1 have False by(simp)
thus ?case ..
next
case (Nomatch p m a rs) thus ?case
proof(cases "matches ?γ (abstract_primitive disc m) a p")
case False
with Nomatch.prems(2) have "approximating_bigstep_fun ?γ p (optimize_matches (abstract_primitive disc) rs) Undecided = Decision FinalAllow"
by(simp add: optimize_matches_def split: if_split_asm)
with Nomatch have IH: "approximating_bigstep_fun ?γ p rs Undecided = Decision FinalAllow"
using simple_ruleset_tail by auto
with Nomatch(1) show ?thesis by simp
next
case True
from Nomatch.prems(2) True have 1: "approximating_bigstep_fun ?γ p
(Rule (abstract_primitive disc m) a # (optimize_matches (abstract_primitive disc) rs)) Undecided = Decision FinalAllow"
using optimize_matches_matches_fst by metis
from Nomatch.prems(1) have "a = action.Accept ∨ a = action.Drop" by(simp add: simple_ruleset_def)
from Nomatch.hyps(1) Nomatch.prems(3) abstract_primitive_in_doubt_deny_Deny2[OF generic] have
"a = action.Accept ⟹ ¬ matches ?γ (abstract_primitive disc m) action.Accept p" by simp
with True ‹a = action.Accept ∨ a = action.Drop› have "a = action.Drop" by blast
with 1 True have False by force
thus ?thesis ..
qed
qed(simp_all add: simple_ruleset_def)
qed
from good approximating_semantics_iff_fun_good_ruleset abstract_primitive_in_doubt_deny_help1 ‹good_ruleset rs› show ?deny
unfolding abstract_def by fast
from good approximating_semantics_iff_fun_good_ruleset abstract_primitive_in_doubt_deny_help2 ‹good_ruleset rs› show ?allow
unfolding abstract_def by fast
qed
end
end