Theory No_Spoof
theory No_Spoof
imports Common_Primitive_Lemmas
Ipassmt
begin
section‹No Spoofing›
text‹assumes: @{const simple_ruleset}›
subsection‹Spoofing Protection›
text‹
No spoofing means:
Every packet that is (potentially) allowed by the firewall and comes from an interface ‹iface›
must have a Source IP Address in the assigned range ‹iface›.
``potentially allowed'' means we use the upper closure.
The definition states: For all interfaces which are configured, every packet that comes from this
interface and is allowed by the firewall must be in the IP range of that interface.
›
text‹We add @{typ "'pkt_ext itself"} as a parameter to have the type of a generic, extensible packet
in the definition.›
definition no_spoofing :: "'pkt_ext itself ⇒ 'i::len ipassignment ⇒ 'i::len common_primitive rule list ⇒ bool" where
"no_spoofing TYPE('pkt_ext) ipassmt rs ≡ ∀ iface ∈ dom ipassmt. ∀p :: ('i,'pkt_ext) tagged_packet_scheme.
((common_matcher, in_doubt_allow),p⦇p_iiface:=iface_sel iface⦈⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow) ⟶
p_src p ∈ (ipcidr_union_set (set (the (ipassmt iface))))"
text ‹This is how it looks like for an IPv4 simple packet: We add @{type unit} because a
@{typ "32 tagged_packet"} does not have any additional fields.›
lemma "no_spoofing TYPE(unit) ipassmt rs ⟷
(∀ iface ∈ dom ipassmt. ∀p :: 32 tagged_packet.
((common_matcher, in_doubt_allow),p⦇p_iiface:=iface_sel iface⦈⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow)
⟶ p_src p ∈ (ipcidr_union_set (set (the (ipassmt iface)))))"
unfolding no_spoofing_def by blast
text‹The definition is sound (if that can be said about a definition):
if @{const no_spoofing} certifies your ruleset, then your ruleset prohibits spoofing.
The definition may not be complete:
@{const no_spoofing} may return @{const False} even though your ruleset prevents spoofing
(should only occur if some strange and unknown primitives occur)›
text‹Technical note: The definition can can be thought of as protection from OUTGOING spoofing.
OUTGOING means: I define my interfaces and their IP addresses. For all interfaces,
only the assigned IP addresses may pass the firewall.
This definition is simple for e.g. local sub-networks.
Example: @{term "[Iface ''eth0'' ↦ {(ipv4addr_of_dotdecimal (192,168,0,0), 24)}]"}
If I want spoofing protection from the Internet, I need to specify the range of the Internet IP addresses.
Example: @{term "[Iface ''evil_internet'' ↦ {everything_that_does_not_belong_to_me}]"}.
This is also a good opportunity to exclude the private IP space, link local, and probably multicast space.
See @{const all_but_those_ips} to easily specify these ranges.
See examples below. Check Example 3 why it can be thought of as OUTGOING spoofing.›
context
begin
text‹The set of any ip addresses which may match for a fixed ‹iface› (overapproximation)›
private definition get_exists_matching_src_ips :: "iface ⇒ 'i::len common_primitive match_expr ⇒ 'i word set" where
"get_exists_matching_src_ips iface m ≡ let (i_matches, _) = (primitive_extractor (is_Iiface, iiface_sel) m) in
if (∀ is ∈ set i_matches. (case is of Pos i ⇒ match_iface i (iface_sel iface)
| Neg i ⇒ ¬ match_iface i (iface_sel iface)))
then
(let (ip_matches, _) = (primitive_extractor (is_Src, src_sel) m) in
if ip_matches = []
then
UNIV
else
⋂ ips ∈ set (ip_matches). (case ips of Pos ip ⇒ ipt_iprange_to_set ip | Neg ip ⇒ - ipt_iprange_to_set ip))
else
{}"
lemma "primitive_extractor (is_Src, src_sel)
(MatchAnd (Match (Src (IpAddrNetmask (0::ipv4addr) 30))) (Match (IIface (Iface ''eth0'')))) =
([Pos (IpAddrNetmask 0 30)], MatchAnd MatchAny (Match (IIface (Iface ''eth0''))))" by eval
private lemma get_exists_matching_src_ips_subset:
assumes "normalized_nnf_match m"
shows "{ip. (∃p :: ('i::len, 'a) tagged_packet_scheme. matches (common_matcher, in_doubt_allow) m a (p⦇p_iiface:= iface_sel iface, p_src:= ip⦈))} ⊆
get_exists_matching_src_ips iface m"
proof -
let ?γ="(common_matcher, in_doubt_allow)"
{ fix ip_matches rest src_ip i_matches rest2 and p :: "('i, 'a) tagged_packet_scheme"
assume a1: "primitive_extractor (is_Src, src_sel) m = (ip_matches, rest)"
and a2: "matches ?γ m a (p⦇p_iiface := iface_sel iface, p_src := src_ip⦈)"
let ?p="(p⦇p_iiface := iface_sel iface, p_src := src_ip⦈)"
from primitive_extractor_negation_type_matching1[OF wf_disc_sel_common_primitive(3) assms a1 a2]
match_simplematcher_SrcDst[where p = ?p] match_simplematcher_SrcDst_not[where p="?p"]
have ip_matches: "(∀ip∈set (getPos ip_matches). p_src ?p ∈ ipt_iprange_to_set ip) ∧
(∀ip∈set (getNeg ip_matches). p_src ?p ∈ - ipt_iprange_to_set ip)" by simp
from ip_matches have "∀x ∈ set ip_matches. src_ip ∈ (case x of Pos x ⇒ ipt_iprange_to_set x | Neg ip ⇒ - ipt_iprange_to_set ip)"
apply(simp)
apply(simp split: negation_type.split)
apply(safe)
using NegPos_set apply fast+
done
} note 1=this
{ fix ip_matches rest src_ip i_matches rest2 and p :: "('i, 'a) tagged_packet_scheme"
assume a1: "primitive_extractor (is_Iiface, iiface_sel) m = (i_matches, rest2)"
and a2: "matches ?γ m a (p⦇p_iiface := iface_sel iface, p_src := src_ip⦈)"
let ?p="(p⦇p_iiface := iface_sel iface, p_src := src_ip⦈)"
from primitive_extractor_negation_type_matching1[OF wf_disc_sel_common_primitive(5) assms a1 a2]
primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher, where p = ?p]
primitive_matcher_generic.Iface_single_not[OF primitive_matcher_generic_common_matcher, where p = ?p]
have iface_matches: "(∀i∈set (getPos i_matches). match_iface i (p_iiface ?p)) ∧
(∀i∈set (getNeg i_matches). ¬ match_iface i (p_iiface ?p))" by simp
hence 2: "(∀x∈set i_matches. case x of Pos i ⇒ match_iface i (iface_sel iface) | Neg i ⇒ ¬ match_iface i (iface_sel iface))"
apply(simp add: split: negation_type.split)
apply(safe)
using NegPos_set apply fast+
done
} note 2=this
from 1 2 show ?thesis
unfolding get_exists_matching_src_ips_def
by(clarsimp)
qed
lemma common_primitive_not_has_primitive_expand:
"¬ has_primitive (m::'i::len common_primitive match_expr) ⟷
¬ has_disc is_Dst m ∧
¬ has_disc is_Src m ∧
¬ has_disc is_Iiface m ∧
¬ has_disc is_Oiface m ∧
¬ has_disc is_Prot m ∧
¬ has_disc is_Src_Ports m ∧
¬ has_disc is_Dst_Ports m ∧
¬ has_disc is_MultiportPorts m ∧
¬ has_disc is_L4_Flags m ∧
¬ has_disc is_CT_State m ∧
¬ has_disc is_Extra m"
apply(induction m)
apply(simp_all)
apply(rename_tac x, case_tac x, simp_all)
by blast
lemma "¬ has_primitive m ∧ matcheq_matchAny m ⟷ (if ¬ has_primitive m then matcheq_matchAny m else False)"
by simp
text‹The set of ip addresses which definitely match for a fixed ‹iface› (underapproximation)›
private definition get_all_matching_src_ips :: "iface ⇒ 'i::len common_primitive match_expr ⇒ 'i word set" where
"get_all_matching_src_ips iface m ≡ let (i_matches, rest1) = (primitive_extractor (is_Iiface, iiface_sel) m) in
if (∀ is ∈ set i_matches. (case is of Pos i ⇒ match_iface i (iface_sel iface)
| Neg i ⇒ ¬ match_iface i (iface_sel iface)))
then
(let (ip_matches, rest2) = (primitive_extractor (is_Src, src_sel) rest1) in
if ¬ has_primitive rest2 ∧ matcheq_matchAny rest2
then
if ip_matches = []
then
UNIV
else
⋂ ips ∈ set (ip_matches). (case ips of Pos ip ⇒ ipt_iprange_to_set ip | Neg ip ⇒ - ipt_iprange_to_set ip)
else
{})
else
{}"
private lemma get_all_matching_src_ips:
assumes "normalized_nnf_match m"
shows "get_all_matching_src_ips iface m ⊆
{ip. (∀p::('i::len, 'a) tagged_packet_scheme. matches (common_matcher, in_doubt_allow) m a (p⦇p_iiface:= iface_sel iface, p_src:= ip⦈))}"
proof
fix ip
assume a: "ip ∈ get_all_matching_src_ips iface m"
obtain i_matches rest1 where select1: "primitive_extractor (is_Iiface, iiface_sel) m = (i_matches, rest1)" by fastforce
show "ip ∈ {ip. ∀p :: ('i, 'a) tagged_packet_scheme. matches (common_matcher, in_doubt_allow) m a (p⦇p_iiface := iface_sel iface, p_src := ip⦈)}"
proof(cases "∀ is ∈ set i_matches. (case is of Pos i ⇒ match_iface i (iface_sel iface)
| Neg i ⇒ ¬match_iface i (iface_sel iface))")
case False
have "get_all_matching_src_ips iface m = {}"
unfolding get_all_matching_src_ips_def
using select1 False by auto
with a show ?thesis by simp
next
case True
let ?γ="(common_matcher, in_doubt_allow) :: ('i::len common_primitive, ('i, 'a) tagged_packet_scheme) match_tac"
let ?p="λp::('i, 'a) tagged_packet_scheme. p⦇p_iiface := iface_sel iface, p_src := ip⦈"
obtain ip_matches rest2 where select2: "primitive_extractor (is_Src, src_sel) rest1 = (ip_matches, rest2)" by fastforce
let ?noDisc="¬ has_primitive rest2"
have get_all_matching_src_ips_caseTrue: "get_all_matching_src_ips iface m =
(if ?noDisc ∧ matcheq_matchAny rest2
then if ip_matches = []
then UNIV
else ⋂((case_negation_type ipt_iprange_to_set (λip. - ipt_iprange_to_set ip) ` (set ip_matches)))
else {})"
unfolding get_all_matching_src_ips_def
by(simp add: True select1 select2)
from True have "(∀m∈set (getPos i_matches). matches ?γ (Match (IIface m)) a (?p p)) ∧
(∀m∈set (getNeg i_matches). matches ?γ (MatchNot (Match (IIface m))) a (?p p))"
for p :: "('i, 'a) tagged_packet_scheme"
by(simp add: negation_type_forall_split
primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher]
primitive_matcher_generic.Iface_single_not[OF primitive_matcher_generic_common_matcher])
hence matches_iface: "matches ?γ (alist_and (NegPos_map IIface i_matches)) a (?p p)"
for p :: "('i,'a) tagged_packet_scheme"
by(simp add: matches_alist_and NegPos_map_simps)
show ?thesis
proof(cases "?noDisc ∧ matcheq_matchAny rest2")
case False
assume F: "¬ (?noDisc ∧ matcheq_matchAny rest2)"
with get_all_matching_src_ips_caseTrue have "get_all_matching_src_ips iface m = {}" by presburger
with a have False by simp
thus ?thesis ..
next
case True
assume F: "?noDisc ∧ matcheq_matchAny rest2"
with get_all_matching_src_ips_caseTrue have "get_all_matching_src_ips iface m =
(if ip_matches = []
then UNIV
else ⋂((case_negation_type ipt_iprange_to_set (λip. - ipt_iprange_to_set ip) ` (set ip_matches))))" by presburger
from primitive_extractor_correct[OF assms wf_disc_sel_common_primitive(5) select1] have
select1_matches: "matches ?γ (alist_and (NegPos_map IIface i_matches)) a p ∧ matches ?γ rest1 a p ⟷ matches ?γ m a p"
and normalized1: "normalized_nnf_match rest1" for p :: "('i,'a) tagged_packet_scheme"
apply -
apply fast+
done
from select1_matches matches_iface have
rest1_matches: "matches ?γ rest1 a (?p p) ⟷ matches ?γ m a (?p p)" for p :: "('i, 'a) tagged_packet_scheme" by blast
from primitive_extractor_correct[OF normalized1 wf_disc_sel_common_primitive(3) select2] have
select2_matches: "matches ?γ (alist_and (NegPos_map Src ip_matches)) a p ∧ matches ?γ rest2 a p ⟷
matches ?γ rest1 a p" for p :: "('i, 'a) tagged_packet_scheme"
by fast
with F matcheq_matchAny have "matches ?γ rest2 a p" for p :: "('i, 'a) tagged_packet_scheme" by metis
with select2_matches rest1_matches have ip_src_matches:
"matches ?γ (alist_and (NegPos_map Src ip_matches)) a (?p p) ⟷ matches ?γ m a (?p p)"
for p :: "('i, 'a) tagged_packet_scheme" by simp
have case_nil: "⋀p. ip_matches = [] ⟹ matches ?γ (alist_and (NegPos_map Src ip_matches)) a p"
by(simp add: bunch_of_lemmata_about_matches)
have case_list: "⋀p. ∀x∈set ip_matches. (case x of Pos i ⇒ ip ∈ ipt_iprange_to_set i
| Neg i ⇒ ip ∈ - ipt_iprange_to_set i) ⟹
matches ?γ (alist_and (NegPos_map Src ip_matches)) a (p⦇p_iiface := iface_sel iface, p_src := ip⦈)"
apply(simp add: matches_alist_and NegPos_map_simps)
apply(simp add: negation_type_forall_split match_simplematcher_SrcDst_not match_simplematcher_SrcDst)
done
from a show "ip ∈ {ip. ∀p :: ('i, 'a) tagged_packet_scheme. matches (common_matcher, in_doubt_allow) m a (p⦇p_iiface := iface_sel iface, p_src := ip⦈)}"
unfolding get_all_matching_src_ips_caseTrue
proof(clarsimp split: if_split_asm)
fix p :: "('i, 'a) tagged_packet_scheme"
assume "ip_matches = []"
with case_nil have "matches ?γ (alist_and (NegPos_map Src ip_matches)) a (?p p)" by simp
with ip_src_matches show "matches ?γ m a (?p p)" by simp
next
fix p :: "('i, 'a) tagged_packet_scheme"
assume "∀x∈set ip_matches. ip ∈ (case x of Pos x ⇒ ipt_iprange_to_set x | Neg ip ⇒ - ipt_iprange_to_set ip)"
hence "∀x∈set ip_matches. case x of Pos i ⇒ ip ∈ ipt_iprange_to_set i | Neg i ⇒ ip ∈ - ipt_iprange_to_set i"
by(simp_all split: negation_type.split negation_type.split_asm)
with case_list have "matches ?γ (alist_and (NegPos_map Src ip_matches)) a (?p p)" .
with ip_src_matches show "matches ?γ m a (?p p)" by simp
qed
qed
qed
qed
private definition get_exists_matching_src_ips_executable
:: "iface ⇒ 'i::len common_primitive match_expr ⇒ 'i wordinterval" where
"get_exists_matching_src_ips_executable iface m ≡ let (i_matches, _) = (primitive_extractor (is_Iiface, iiface_sel) m) in
if (∀ is ∈ set i_matches. (case is of Pos i ⇒ match_iface i (iface_sel iface)
| Neg i ⇒ ¬match_iface i (iface_sel iface)))
then
(let (ip_matches, _) = (primitive_extractor (is_Src, src_sel) m) in
if ip_matches = []
then
wordinterval_UNIV
else
l2wi_negation_type_intersect (NegPos_map ipt_iprange_to_interval ip_matches))
else
Empty_WordInterval"
lemma get_exists_matching_src_ips_executable:
"wordinterval_to_set (get_exists_matching_src_ips_executable iface m) = get_exists_matching_src_ips iface m"
apply(simp add: get_exists_matching_src_ips_executable_def get_exists_matching_src_ips_def)
apply(case_tac "primitive_extractor (is_Iiface, iiface_sel) m")
apply(case_tac "primitive_extractor (is_Src, src_sel) m")
apply(simp)
apply(simp add: l2wi_negation_type_intersect)
apply(simp add: NegPos_map_simps)
apply(safe)
apply(simp_all add: ipt_iprange_to_interval)
apply(rename_tac i_matches rest1 a b x xa)
apply(case_tac xa)
apply(simp_all add: NegPos_set)
using ipt_iprange_to_interval apply fast+
apply(rename_tac i_matches rest1 a b x aa ab ba)
apply(erule_tac x="Pos aa" in ballE)
apply(simp_all add: NegPos_set)
using NegPos_set(2) by fastforce
lemma "(get_exists_matching_src_ips_executable (Iface ''eth0'')
(MatchAnd (MatchNot (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24)))) (Match (IIface (Iface ''eth0''))))) =
RangeUnion (WordInterval 0 0xC0A7FFFF) (WordInterval 0xC0A80100 0xFFFFFFFF)" by eval
private definition get_all_matching_src_ips_executable
:: "iface ⇒ 'i::len common_primitive match_expr ⇒ 'i wordinterval" where
"get_all_matching_src_ips_executable iface m ≡ let (i_matches, rest1) = (primitive_extractor (is_Iiface, iiface_sel) m) in
if (∀ is ∈ set i_matches. (case is of Pos i ⇒ match_iface i (iface_sel iface)
| Neg i ⇒ ¬match_iface i (iface_sel iface)))
then
(let (ip_matches, rest2) = (primitive_extractor (is_Src, src_sel) rest1) in
if ¬ has_primitive rest2 ∧ matcheq_matchAny rest2
then
if ip_matches = []
then
wordinterval_UNIV
else
l2wi_negation_type_intersect (NegPos_map ipt_iprange_to_interval ip_matches)
else
Empty_WordInterval)
else
Empty_WordInterval"
lemma get_all_matching_src_ips_executable:
"wordinterval_to_set (get_all_matching_src_ips_executable iface m) = get_all_matching_src_ips iface m"
apply(simp add: get_all_matching_src_ips_executable_def get_all_matching_src_ips_def)
apply(case_tac "primitive_extractor (is_Iiface, iiface_sel) m")
apply(simp, rename_tac i_matches rest1)
apply(case_tac "primitive_extractor (is_Src, src_sel) rest1")
apply(simp)
apply(simp add: l2wi_negation_type_intersect)
apply(simp add: NegPos_map_simps)
apply(safe)
apply(simp_all add: ipt_iprange_to_interval)
apply(rename_tac i_matches rest1 a b x xa)
apply(case_tac xa)
apply(simp_all add: NegPos_set)
using ipt_iprange_to_interval apply fast+
apply(rename_tac i_matches rest1 a b x aa ab ba)
apply(erule_tac x="Pos aa" in ballE)
apply(simp_all add: NegPos_set)
apply(erule_tac x="Neg aa" in ballE)
apply(simp_all add: NegPos_set)
done
lemma "(get_all_matching_src_ips_executable (Iface ''eth0'')
(MatchAnd (MatchNot (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24)))) (Match (IIface (Iface ''eth0''))))) =
RangeUnion (WordInterval 0 0xC0A7FFFF) (WordInterval 0xC0A80100 0xFFFFFFFF)" by eval
text‹The following algorithm sound but not complete.›
private fun no_spoofing_algorithm
:: "iface ⇒ 'i::len ipassignment ⇒ 'i common_primitive rule list ⇒ 'i word set ⇒ 'i word set ⇒ bool" where
"no_spoofing_algorithm iface ipassmt [] allowed denied1 ⟷
(allowed - denied1) ⊆ ipcidr_union_set (set (the (ipassmt iface)))" |
"no_spoofing_algorithm iface ipassmt ((Rule m Accept)#rs) allowed denied1 = no_spoofing_algorithm iface ipassmt rs
(allowed ∪ get_exists_matching_src_ips iface m) denied1" |
"no_spoofing_algorithm iface ipassmt ((Rule m Drop)#rs) allowed denied1 = no_spoofing_algorithm iface ipassmt rs
allowed (denied1 ∪ (get_all_matching_src_ips iface m - allowed))" |
"no_spoofing_algorithm _ _ _ _ _ = undefined"
private fun no_spoofing_algorithm_executable
:: "iface ⇒ (iface ⇀ ('i::len word × nat) list) ⇒ 'i common_primitive rule list
⇒ 'i wordinterval ⇒ 'i wordinterval ⇒ bool" where
"no_spoofing_algorithm_executable iface ipassmt [] allowed denied1 ⟷
wordinterval_subset (wordinterval_setminus allowed denied1) (l2wi (map ipcidr_to_interval (the (ipassmt iface))))" |
"no_spoofing_algorithm_executable iface ipassmt ((Rule m Accept)#rs) allowed denied1 = no_spoofing_algorithm_executable iface ipassmt rs
(wordinterval_union allowed (get_exists_matching_src_ips_executable iface m)) denied1" |
"no_spoofing_algorithm_executable iface ipassmt ((Rule m Drop)#rs) allowed denied1 = no_spoofing_algorithm_executable iface ipassmt rs
allowed (wordinterval_union denied1 (wordinterval_setminus (get_all_matching_src_ips_executable iface m) allowed))" |
"no_spoofing_algorithm_executable _ _ _ _ _ = undefined"
lemma no_spoofing_algorithm_executable: "no_spoofing_algorithm_executable iface ipassmt rs allowed denied ⟷
no_spoofing_algorithm iface ipassmt rs (wordinterval_to_set allowed) (wordinterval_to_set denied)"
proof(induction iface ipassmt rs allowed denied rule: no_spoofing_algorithm_executable.induct)
case (1 iface ipassmt allowed denied1)
have "(⋃a∈set (the (ipassmt iface)). case ipcidr_to_interval a of (x, xa) ⇒ {x..xa}) =
(⋃x∈set (the (ipassmt iface)). uncurry ipset_from_cidr x)"
by(simp add: ipcidr_to_interval_def uncurry_def ipset_from_cidr_ipcidr_to_interval)
with 1 show ?case by(simp add: ipcidr_union_set_uncurry l2wi)
next
case 2 thus ?case by(simp add: get_exists_matching_src_ips_executable get_all_matching_src_ips_executable)
next
case 3 thus ?case by(simp add: get_exists_matching_src_ips_executable get_all_matching_src_ips_executable)
qed(simp_all)
private definition "nospoof TYPE('pkt_ext) iface ipassmt rs = (∀p :: ('i::len,'pkt_ext) tagged_packet_scheme.
(approximating_bigstep_fun (common_matcher, in_doubt_allow) (p⦇p_iiface:=iface_sel iface⦈) rs Undecided = Decision FinalAllow) ⟶
p_src p ∈ (ipcidr_union_set (set (the (ipassmt iface)))))"
private definition "setbydecision TYPE('pkt_ext) iface rs dec = {ip. ∃p :: ('i::len,'pkt_ext) tagged_packet_scheme. approximating_bigstep_fun (common_matcher, in_doubt_allow)
(p⦇p_iiface:=iface_sel iface, p_src := ip⦈) rs Undecided = Decision dec}"
private lemma nospoof_setbydecision:
fixes rs :: "'i::len common_primitive rule list"
shows "nospoof TYPE('pkt_ext) iface ipassmt rs ⟷
setbydecision TYPE('pkt_ext) iface rs FinalAllow ⊆ (ipcidr_union_set (set (the (ipassmt iface))))"
proof
assume a: "nospoof TYPE('pkt_ext) iface ipassmt rs"
have packet_update_iface_simp: "p⦇p_iiface := iface_sel iface, p_src := x⦈ = p⦇p_src := x, p_iiface := iface_sel iface⦈"
for p::"('i::len, 'p) tagged_packet_scheme" and x by simp
from a show "setbydecision TYPE('pkt_ext) iface rs FinalAllow ⊆ ipcidr_union_set (set (the (ipassmt iface)))"
apply(simp add: nospoof_def setbydecision_def)
apply(safe)
apply(rename_tac x p)
apply(erule_tac x="p⦇p_iiface := iface_sel iface, p_src := x⦈" in allE)
apply(simp)
apply(simp add: packet_update_iface_simp)
done
next
assume a1: "setbydecision TYPE('pkt_ext) iface rs FinalAllow ⊆ ipcidr_union_set (set (the (ipassmt iface)))"
show "nospoof TYPE('pkt_ext) iface ipassmt rs"
unfolding nospoof_def
proof(safe)
fix p :: "('i::len,'pkt_ext) tagged_packet_scheme"
assume a2: "approximating_bigstep_fun (common_matcher, in_doubt_allow) (p⦇p_iiface := iface_sel iface⦈) rs Undecided = Decision FinalAllow"
let ?setbydecision_fix_p="{ip. approximating_bigstep_fun (common_matcher, in_doubt_allow)
(p⦇p_iiface := iface_sel iface, p_src := ip⦈) rs Undecided = Decision FinalAllow}"
from a1 a2 have 1: "?setbydecision_fix_p ⊆ ipcidr_union_set (set (the (ipassmt iface)))" by(simp add: nospoof_def setbydecision_def) blast
from a2 have 2: "p_src p ∈ ?setbydecision_fix_p" by simp
from 1 2 show "p_src p ∈ ipcidr_union_set (set (the (ipassmt iface)))" by blast
qed
qed
private definition "setbydecision_all TYPE('pkt_ext) iface rs dec = {ip. ∀p :: ('i::len,'pkt_ext) tagged_packet_scheme.
approximating_bigstep_fun (common_matcher, in_doubt_allow) (p⦇p_iiface:=iface_sel iface, p_src := ip⦈) rs Undecided = Decision dec}"
private lemma setbydecision_setbydecision_all_Allow:
"(setbydecision TYPE('pkt_ext) iface rs FinalAllow - setbydecision_all TYPE('pkt_ext) iface rs FinalDeny) =
setbydecision TYPE('pkt_ext) iface rs FinalAllow"
apply(safe)
apply(simp add: setbydecision_def setbydecision_all_def)
done
private lemma setbydecision_setbydecision_all_Deny:
"(setbydecision TYPE('pkt_ext) iface rs FinalDeny - setbydecision_all TYPE('pkt_ext) iface rs FinalAllow) =
setbydecision TYPE('pkt_ext) iface rs FinalDeny"
apply(safe)
apply(simp add: setbydecision_def setbydecision_all_def)
done
private lemma setbydecision_append:
"simple_ruleset (rs1 @ rs2) ⟹
setbydecision TYPE('pkt_ext) iface (rs1 @ rs2) FinalAllow =
setbydecision TYPE('pkt_ext) iface rs1 FinalAllow ∪ {ip. ∃p :: ('i::len,'pkt_ext) tagged_packet_scheme. approximating_bigstep_fun (common_matcher, in_doubt_allow)
(p⦇p_iiface:=iface_sel iface, p_src := ip⦈) rs2 Undecided = Decision FinalAllow ∧
approximating_bigstep_fun (common_matcher, in_doubt_allow) (p⦇p_iiface:=iface_sel iface, p_src := ip⦈) rs1 Undecided = Undecided}"
apply(simp add: setbydecision_def)
apply(subst Set.Collect_disj_eq[symmetric])
apply(rule Set.Collect_cong)
apply(subst approximating_bigstep_fun_seq_Undecided_t_wf)
apply(simp add: simple_imp_good_ruleset good_imp_wf_ruleset)
by blast
private lemma not_FinalAllow: "foo ≠ Decision FinalAllow ⟷ foo = Decision FinalDeny ∨ foo = Undecided"
apply(cases foo)
apply simp_all
apply(rename_tac x2)
apply(case_tac x2)
apply(simp_all)
done
private lemma setbydecision_all_appendAccept: "simple_ruleset (rs @ [Rule r Accept]) ⟹
setbydecision_all TYPE('pkt_ext) iface rs FinalDeny = setbydecision_all TYPE('pkt_ext) iface (rs @ [Rule r Accept]) FinalDeny"
apply(simp add: setbydecision_all_def)
apply(rule Set.Collect_cong)
apply(subst approximating_bigstep_fun_seq_Undecided_t_wf)
apply(simp add: simple_imp_good_ruleset good_imp_wf_ruleset)
apply(simp add: not_FinalAllow)
done
private lemma setbydecision_all_append_subset: "simple_ruleset (rs1 @ rs2) ⟹
setbydecision_all TYPE('pkt_ext) iface rs1 FinalDeny ∪ {ip. ∀p :: ('i::len,'pkt_ext) tagged_packet_scheme.
approximating_bigstep_fun (common_matcher, in_doubt_allow) (p⦇p_iiface:=iface_sel iface, p_src := ip⦈) rs2 Undecided = Decision FinalDeny ∧
approximating_bigstep_fun (common_matcher, in_doubt_allow) (p⦇p_iiface:=iface_sel iface, p_src := ip⦈) rs1 Undecided = Undecided}
⊆
setbydecision_all TYPE('pkt_ext) iface (rs1 @ rs2) FinalDeny"
unfolding setbydecision_all_def
apply(subst Set.Collect_disj_eq[symmetric])
apply(rule Set.Collect_mono)
apply(subst approximating_bigstep_fun_seq_Undecided_t_wf)
apply(simp add: simple_imp_good_ruleset good_imp_wf_ruleset)
apply(simp add: not_FinalAllow)
done
private lemma "setbydecision_all TYPE('pkt_ext) iface rs1 FinalDeny ∪
{ip. ∀p :: ('i::len,'pkt_ext) tagged_packet_scheme.
approximating_bigstep_fun (common_matcher, in_doubt_allow) (p⦇p_iiface := iface_sel iface, p_src := ip⦈) rs1 Undecided = Undecided}
⊆
- setbydecision TYPE('pkt_ext) iface rs1 FinalAllow"
unfolding setbydecision_all_def
unfolding setbydecision_def
apply(subst Set.Collect_neg_eq[symmetric])
apply(subst Set.Collect_disj_eq[symmetric])
apply(rule Set.Collect_mono)
by(simp)
private lemma Collect_minus_eq: "{x. P x} - {x. Q x} = {x. P x ∧ ¬ Q x}" by blast
private lemma setbydecision_all_append_subset2:
"simple_ruleset (rs1 @ rs2) ⟹
setbydecision_all TYPE('pkt_ext) iface rs1 FinalDeny ∪
(setbydecision_all TYPE('pkt_ext) iface rs2 FinalDeny -
setbydecision TYPE('pkt_ext) iface rs1 FinalAllow)
⊆ setbydecision_all TYPE('pkt_ext) iface (rs1 @ rs2) FinalDeny"
unfolding setbydecision_all_def
unfolding setbydecision_def
apply(subst Collect_minus_eq)
apply(subst Set.Collect_disj_eq[symmetric])
apply(rule Set.Collect_mono)
apply(subst approximating_bigstep_fun_seq_Undecided_t_wf)
apply(simp add: simple_imp_good_ruleset good_imp_wf_ruleset; fail)
apply(intro impI allI)
apply(simp add: not_FinalAllow)
apply(case_tac "approximating_bigstep_fun (common_matcher, in_doubt_allow) (p⦇p_iiface := iface_sel iface, p_src := x⦈) rs1 Undecided")
subgoal by(elim disjE) simp_all
apply(rename_tac x2)
apply(case_tac x2)
prefer 2
apply simp
apply(elim disjE)
apply(simp)
by blast
private lemma "setbydecision_all TYPE('pkt_ext) iface rs FinalDeny ⊆ - setbydecision TYPE('pkt_ext) iface rs FinalAllow"
apply(simp add: setbydecision_def setbydecision_all_def)
apply(subst Set.Collect_neg_eq[symmetric])
apply(rule Set.Collect_mono)
apply(simp)
done
private lemma no_spoofing_algorithm_sound_generalized:
fixes rs1 :: "'i::len common_primitive rule list"
shows "simple_ruleset rs1 ⟹ simple_ruleset rs2 ⟹
(∀r ∈ set rs2. normalized_nnf_match (get_match r)) ⟹
setbydecision TYPE('pkt_ext) iface rs1 FinalAllow ⊆ allowed ⟹
denied1 ⊆ setbydecision_all TYPE('pkt_ext) iface rs1 FinalDeny ⟹
no_spoofing_algorithm iface ipassmt rs2 allowed denied1 ⟹
nospoof TYPE('pkt_ext) iface ipassmt (rs1@rs2)"
proof(induction iface ipassmt rs2 allowed denied1 arbitrary: rs1 allowed denied1 rule: no_spoofing_algorithm.induct)
case (1 iface ipassmt)
from 1 have "allowed - denied1 ⊆ ipcidr_union_set (set (the (ipassmt iface)))"
by(simp)
with 1 have "setbydecision TYPE('pkt_ext) iface rs1 FinalAllow - setbydecision_all TYPE('pkt_ext) iface rs1 FinalDeny
⊆ ipcidr_union_set (set (the (ipassmt iface)))"
by blast
thus ?case
by(simp add: nospoof_setbydecision setbydecision_setbydecision_all_Allow)
next
case (2 iface ipassmt m rs)
from 2(2) have simple_rs1: "simple_ruleset rs1" by(simp add: simple_ruleset_def)
hence simple_rs': "simple_ruleset (rs1 @ [Rule m Accept])" by(simp add: simple_ruleset_def)
from 2(3) have simple_rs: "simple_ruleset rs" by(simp add: simple_ruleset_def)
with 2 have IH: "⋀rs' allowed denied1.
simple_ruleset rs' ⟹
setbydecision TYPE('pkt_ext) iface rs' FinalAllow ⊆ allowed ⟹
denied1 ⊆ setbydecision_all TYPE('pkt_ext) iface rs' FinalDeny ⟹
no_spoofing_algorithm iface ipassmt rs allowed denied1 ⟹ nospoof TYPE('pkt_ext) iface ipassmt (rs' @ rs)"
by(simp)
from 2(5) have "setbydecision TYPE('pkt_ext) iface (rs1 @ [Rule m Accept]) FinalAllow ⊆
(allowed ∪ {ip. ∃p :: ('i::len,'pkt_ext) tagged_packet_scheme. matches (common_matcher, in_doubt_allow) m Accept (p⦇p_iiface := iface_sel iface, p_src := ip⦈)})"
apply(simp add: setbydecision_append[OF simple_rs'])
by blast
with get_exists_matching_src_ips_subset 2(4) have allowed: "setbydecision TYPE('pkt_ext) iface (rs1 @ [Rule m Accept]) FinalAllow ⊆ (allowed ∪ get_exists_matching_src_ips iface m)"
by fastforce
from 2(6) setbydecision_all_appendAccept[OF simple_rs', where 'pkt_ext = 'pkt_ext] have denied1:
"denied1 ⊆ setbydecision_all TYPE('pkt_ext) iface (rs1 @ [Rule m Accept]) FinalDeny" by simp
from 2(7) have no_spoofing_algorithm_prems: "no_spoofing_algorithm iface ipassmt rs
(allowed ∪ get_exists_matching_src_ips iface m) denied1"
by(simp)
from IH[OF simple_rs' allowed denied1 no_spoofing_algorithm_prems] have "nospoof TYPE('pkt_ext) iface ipassmt ((rs1 @ [Rule m Accept]) @ rs)" by blast
thus ?case by(simp)
next
case (3 iface ipassmt m rs)
from 3(2) have simple_rs1: "simple_ruleset rs1" by(simp add: simple_ruleset_def)
hence simple_rs': "simple_ruleset (rs1 @ [Rule m Drop])" by(simp add: simple_ruleset_def)
from 3(3) have simple_rs: "simple_ruleset rs" by(simp add: simple_ruleset_def)
with 3 have IH: "⋀rs' allowed denied1.
simple_ruleset rs' ⟹
setbydecision TYPE('pkt_ext) iface rs' FinalAllow ⊆ allowed ⟹
denied1 ⊆ setbydecision_all TYPE('pkt_ext) iface rs' FinalDeny ⟹
no_spoofing_algorithm iface ipassmt rs allowed denied1 ⟹ nospoof TYPE('pkt_ext) iface ipassmt (rs' @ rs)"
by(simp)
from 3(5) simple_rs' have allowed: "setbydecision TYPE('pkt_ext) iface (rs1 @ [Rule m Drop]) FinalAllow ⊆ allowed "
by(simp add: setbydecision_append)
have "{ip. ∀p :: ('i,'pkt_ext) tagged_packet_scheme. matches (common_matcher, in_doubt_allow) m Drop (p⦇p_iiface := iface_sel iface, p_src := ip⦈)} ⊆
setbydecision_all TYPE('pkt_ext) iface [Rule m Drop] FinalDeny" by(simp add: setbydecision_all_def)
with 3(5) have "setbydecision_all TYPE('pkt_ext) iface rs1 FinalDeny ∪ ({ip. ∀p :: ('i,'pkt_ext) tagged_packet_scheme. matches (common_matcher, in_doubt_allow) m Drop (p⦇p_iiface := iface_sel iface, p_src := ip⦈)} - allowed) ⊆
setbydecision_all TYPE('pkt_ext) iface rs1 FinalDeny ∪ (setbydecision_all TYPE('pkt_ext) iface [Rule m Drop] FinalDeny - setbydecision TYPE('pkt_ext) iface rs1 FinalAllow)"
by blast
with 3(6) setbydecision_all_append_subset2[OF simple_rs', of iface] have
"denied1 ∪ ({ip. ∀p :: ('i,'pkt_ext) tagged_packet_scheme. matches (common_matcher, in_doubt_allow) m Drop (p⦇p_iiface := iface_sel iface, p_src := ip⦈)} - allowed) ⊆
setbydecision_all TYPE('pkt_ext) iface (rs1 @ [Rule m Drop]) FinalDeny"
by blast
with get_all_matching_src_ips 3(4) have denied1:
"denied1 ∪ (get_all_matching_src_ips iface m - allowed) ⊆ setbydecision_all TYPE('pkt_ext) iface (rs1 @ [Rule m Drop]) FinalDeny"
by force
from 3(7) have no_spoofing_algorithm_prems: "no_spoofing_algorithm iface ipassmt rs allowed
(denied1 ∪ (get_all_matching_src_ips iface m - allowed))"
apply(simp)
done
from IH[OF simple_rs' allowed denied1 no_spoofing_algorithm_prems] have "nospoof TYPE('pkt_ext) iface ipassmt ((rs1 @ [Rule m Drop]) @ rs)" by blast
thus ?case by(simp)
next
case "4_1" thus ?case by(simp add: simple_ruleset_def)
next
case "4_2" thus ?case by(simp add: simple_ruleset_def)
next
case "4_3" thus ?case by(simp add: simple_ruleset_def)
next
case "4_4" thus ?case by(simp add: simple_ruleset_def)
next
case "4_5" thus ?case by(simp add: simple_ruleset_def)
next
case "4_6" thus ?case by(simp add: simple_ruleset_def)
next
case "4_7" thus ?case by(simp add: simple_ruleset_def)
qed
definition no_spoofing_iface :: "iface ⇒ 'i::len ipassignment ⇒ 'i common_primitive rule list ⇒ bool" where
"no_spoofing_iface iface ipassmt rs ≡ no_spoofing_algorithm iface ipassmt rs {} {}"
lemma[code]: "no_spoofing_iface iface ipassmt rs =
no_spoofing_algorithm_executable iface ipassmt rs Empty_WordInterval Empty_WordInterval"
by(simp add: no_spoofing_iface_def no_spoofing_algorithm_executable)
private corollary no_spoofing_algorithm_sound: "simple_ruleset rs ⟹ ∀r∈set rs. normalized_nnf_match (get_match r) ⟹
no_spoofing_iface iface ipassmt rs ⟹ nospoof TYPE('pkt_ext) iface ipassmt rs"
unfolding no_spoofing_iface_def
apply(rule no_spoofing_algorithm_sound_generalized[of "[]" rs iface "{}" "{}", simplified])
apply(simp_all)
apply(simp add: simple_ruleset_def)
apply(simp add: setbydecision_def)
done
text‹The @{const nospoof} definition used throughout the proofs corresponds to checking @{const no_spoofing} for all interfaces›
private lemma nospoof: "simple_ruleset rs ⟹ (∀iface ∈ dom ipassmt. nospoof TYPE('pkt_ext) iface ipassmt rs) ⟷ no_spoofing TYPE('pkt_ext) ipassmt rs"
unfolding nospoof_def no_spoofing_def
apply(drule simple_imp_good_ruleset)
apply(subst approximating_semantics_iff_fun_good_ruleset)
apply(simp_all)
done
theorem no_spoofing_iface: "simple_ruleset rs ⟹ ∀r∈set rs. normalized_nnf_match (get_match r) ⟹
∀iface ∈ dom ipassmt. no_spoofing_iface iface ipassmt rs ⟹ no_spoofing TYPE('pkt_ext) ipassmt rs"
by(auto dest: nospoof no_spoofing_algorithm_sound)
text‹Examples›
text‹Example 1:
Ruleset: Accept all non-spoofed packets, drop rest.
›
lemma "no_spoofing_iface
(Iface ''eth0'')
[Iface ''eth0'' ↦ [(ipv4addr_of_dotdecimal (192,168,0,0), 24)]]
[Rule (MatchAnd (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24))) (Match (IIface (Iface ''eth0'')))) action.Accept,
Rule MatchAny action.Drop]" by eval
lemma "no_spoofing TYPE('pkt_ext)
[Iface ''eth0'' ↦ [(ipv4addr_of_dotdecimal (192,168,0,0), 24)]]
[Rule (MatchAnd (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24))) (Match (IIface (Iface ''eth0'')))) action.Accept,
Rule MatchAny action.Drop]"
apply(rule no_spoofing_iface)
apply(simp_all add: simple_ruleset_def)
by eval
text‹Example 2:
Ruleset: Drop packets from a spoofed IP range, allow rest.
Handles negated interfaces correctly.
›
lemma "no_spoofing TYPE('pkt_ext)
[Iface ''eth0'' ↦ [(ipv4addr_of_dotdecimal (192,168,0,0), 24)]]
[Rule (MatchAnd (Match (IIface (Iface ''wlan+''))) (Match (Extra ''no idea what this is''))) action.Accept,
Rule (MatchNot (Match (IIface (Iface ''eth0+'')))) action.Accept,
Rule (MatchAnd (MatchNot (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24)))) (Match (IIface (Iface ''eth0'')))) action.Drop,
Rule MatchAny action.Accept]
"
apply(rule no_spoofing_iface)
apply(simp_all add: simple_ruleset_def)
by eval
text‹Example 3:
Accidentally, matching on wlan+, spoofed packets for eth0 are allowed.
First, we prove that there actually is no spoofing protection. Then we show that our algorithm finds out.
›
lemma "¬ no_spoofing TYPE('pkt_ext)
[Iface ''eth0'' ↦ [(ipv4addr_of_dotdecimal (192,168,0,0), 24)]]
[Rule (MatchNot (Match (IIface (Iface ''wlan+'')))) action.Accept,
Rule (MatchAnd (MatchNot (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24)))) (Match (IIface (Iface ''eth0'')))) action.Drop,
Rule MatchAny action.Accept]
"
apply(simp add: no_spoofing_def)
apply(rule_tac x="p⦇p_src := 0⦈" in exI)
apply(simp add: range_0_max_UNIV ipcidr_union_set_def)
apply(intro conjI)
apply(subst approximating_semantics_iff_fun_good_ruleset)
apply(simp add: good_ruleset_def; fail)
apply(simp add: bunch_of_lemmata_about_matches
match_simplematcher_SrcDst_not
primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher]
primitive_matcher_generic.Iface_single_not[OF primitive_matcher_generic_common_matcher])
apply eval
done
lemma "¬ no_spoofing_iface
(Iface ''eth0'')
[Iface ''eth0'' ↦ [(ipv4addr_of_dotdecimal (192,168,0,0), 24)]]
[Rule (MatchNot (Match (IIface (Iface ''wlan+'')))) action.Accept,
Rule (MatchAnd (MatchNot (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24)))) (Match (IIface (Iface ''eth0'')))) action.Drop,
Rule MatchAny action.Accept]
" by eval
text‹Example 4:
Ruleset: Drop packets coming from the wrong interface, allow the rest.
Warning: this does not prevent spoofing for eth0!
Explanation: someone on eth0 can send a packet e.g. with source IP 8.8.8.8
The ruleset only prevents spoofing of 192.168.0.0/24 for other interfaces
›
lemma "¬ no_spoofing TYPE('pkt_ext) [Iface ''eth0'' ↦ [(ipv4addr_of_dotdecimal (192,168,0,0), 24)]]
[Rule (MatchAnd (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24))) (MatchNot (Match (IIface (Iface ''eth0''))))) action.Drop,
Rule MatchAny action.Accept]"
apply(simp add: no_spoofing_def)
apply(rule_tac x="p⦇p_src := 0⦈" in exI)
apply(simp add: range_0_max_UNIV ipcidr_union_set_def)
apply(intro conjI)
apply(subst approximating_semantics_iff_fun_good_ruleset)
apply(simp add: good_ruleset_def; fail)
apply(simp add: bunch_of_lemmata_about_matches
primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher]
primitive_matcher_generic.Iface_single_not[OF primitive_matcher_generic_common_matcher])
apply eval
done
text‹Our algorithm detects it.›
lemma "¬ no_spoofing_iface
(Iface ''eth0'')
[Iface ''eth0'' ↦ [(ipv4addr_of_dotdecimal (192,168,0,0), 24)]]
[Rule (MatchAnd (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24))) (MatchNot (Match (IIface (Iface ''eth0''))))) action.Drop,
Rule MatchAny action.Accept]" by eval
text‹Example 5:
Spoofing protection but the algorithm fails.
The algorithm @{const no_spoofing_iface} is only sound, not complete.
The ruleset first drops spoofed packets for TCP and then drops spoofed packets for ‹¬ TCP›.
The algorithm cannot detect that ‹TCP ∪ ¬TCP› together will match all spoofed packets.›
lemma "no_spoofing TYPE('pkt_ext) [Iface ''eth0'' ↦ [(ipv4addr_of_dotdecimal (192,168,0,0), 24)]]
[Rule (MatchAnd (MatchNot (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24))))
(MatchAnd (Match (IIface (Iface ''eth0'')))
(Match (Prot (Proto TCP))))) action.Drop,
Rule (MatchAnd (MatchNot (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24))))
(MatchAnd (Match (IIface (Iface ''eth0'')))
(MatchNot (Match (Prot (Proto TCP)))))) action.Drop,
Rule MatchAny action.Accept]" (is "no_spoofing TYPE('pkt_ext) ?ipassmt ?rs")
proof -
have 1: "∀p. (common_matcher, in_doubt_allow),p⊢ ⟨?rs, Undecided⟩ ⇒⇩α Decision FinalAllow ⟷
approximating_bigstep_fun (common_matcher, in_doubt_allow) p ?rs Undecided = Decision FinalAllow"
by(subst approximating_semantics_iff_fun_good_ruleset) (simp_all add: good_ruleset_def)
show ?thesis
unfolding no_spoofing_def
apply(simp add: 1 ipcidr_union_set_def)
apply(simp add: bunch_of_lemmata_about_matches
primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher]
primitive_matcher_generic.Iface_single_not[OF primitive_matcher_generic_common_matcher])
apply(simp add: match_iface.simps match_simplematcher_SrcDst_not
primitive_matcher_generic.Prot_single[OF primitive_matcher_generic_common_matcher]
primitive_matcher_generic.Prot_single_not[OF primitive_matcher_generic_common_matcher])
done
qed
text‹Spoofing protection but the algorithm cannot certify spoofing protection.›
lemma "¬ no_spoofing_iface
(Iface ''eth0'')
[Iface ''eth0'' ↦ [(ipv4addr_of_dotdecimal (192,168,0,0), 24)]]
[Rule (MatchAnd (MatchNot (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24))))
(MatchAnd (Match (IIface (Iface ''eth0'')))
(Match (Prot (Proto TCP))))) action.Drop,
Rule (MatchAnd (MatchNot (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24))))
(MatchAnd (Match (IIface (Iface ''eth0'')))
(MatchNot (Match (Prot (Proto TCP)))))) action.Drop,
Rule MatchAny action.Accept]" by eval
end
lemma "no_spoofing_iface (Iface ''eth1.1011'')
([Iface ''eth1.1011'' ↦ [(ipv4addr_of_dotdecimal (131,159,14,0), 24)]]:: 32 ipassignment)
[Rule (MatchNot (Match (IIface (Iface ''eth1.1011+'')))) action.Accept,
Rule (MatchAnd (MatchNot (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (131,159,14,0)) 24)))) (Match (IIface (Iface ''eth1.1011'')))) action.Drop,
Rule MatchAny action.Accept]" by eval
text‹We only check accepted packets.
If there is no default rule (this will never happen if parsed from iptables!), the result is unfinished.›
lemma "no_spoofing_iface (Iface ''eth1.1011'')
([Iface ''eth1.1011'' ↦ [(ipv4addr_of_dotdecimal (131,159,14,0), 24)]]:: 32 ipassignment)
[Rule (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (127, 0, 0, 0)) 8))) Drop]" by eval
end