theory exercise_rulesetinduction_sol
imports firewall (*http://www.net.in.tum.de/pub/netzanalyse/2014/firewall.thy*)
begin
(*
It is common knowledge that enhanced packets have an evil bit.
*)
record enhanced_packet = enhanced_src_addr :: string
enhanced_dst_addr :: string
evil_bit :: bool
value "\ enhanced_src_addr = ''Alice'', enhanced_dst_addr = ''Bob'', evil_bit = False \"
value "evil_bit \ enhanced_src_addr = ''Alice'', enhanced_dst_addr = ''Bob'', evil_bit = True \"
(*
You are a young, flexible, dynamic startup which wants to sell a static analysis tool for firewalls.
Your product checks firewall rulesets and makes sure that the firewall does not allow any packets with the evil bit set.
*)
definition filters_evil :: "enhanced_packet rule \ bool" where
"filters_evil r \ \p. evil_bit p \ r p = Deny"
fun filters_all_evil :: "enhanced_packet ruleset \ bool" where
"filters_all_evil DefaultDeny = True" |
"filters_all_evil DefaultAllow = False" |
"filters_all_evil (r \ rs) = (filters_evil r \ filters_all_evil rs)"
(*
Your tool is an offline analysis tool, i.e. it verifies correctness statically of the firewall rule set.
It can thus detect ruleset errors before the firewall ruelset is actually deployed!
Now verify that your tool fulfills what it promises!
*)
lemma "filters_all_evil rs \ (\p. evil_bit p \ firewall rs p = Deny)"
proof(induction rs)
case DefaultAllow
assume a: "filters_all_evil DefaultAllow"
hence "False" by(simp_all add: filters_evil_def)
thus ?case ..
next
case DefaultDeny
show "\p. evil_bit p \ firewall DefaultDeny p = Deny"
by(simp_all add: filters_evil_def)
next
case (Rule r rs)
assume IH: "filters_all_evil rs \ \p. evil_bit p \ firewall rs p = Deny"
assume prems: "filters_all_evil (r \ rs)"
from prems have "filters_evil r \ filters_all_evil rs" by simp
hence 1:"filters_evil r" and 2: "filters_all_evil rs" by simp_all
from 1 have prems': "\p. evil_bit p \ r p = Deny" by(simp add: filters_evil_def)
from 2 IH have IH': "\p. evil_bit p \ firewall rs p = Deny" by simp
show "\p. evil_bit p \ firewall (r \ rs) p = Deny"
proof(clarify)
fix p::enhanced_packet
assume a: "evil_bit p"
from a prems' have 1: "r p = Deny" by simp
from a IH' have 2: "firewall rs p = Deny" by simp
from 1 2 show "firewall (r \ rs) p = Deny" by(simp)
qed
qed
(*
You have a competitor who also sells a similar but way cheaper product.
*)
fun filters_all_evil_cheap :: "enhanced_packet ruleset \ bool" where
"filters_all_evil_cheap _ = False"
(*
Can he guarantee correctness too?
*)
lemma "filters_all_evil_cheap rs \ \p. evil_bit p \ firewall rs p = Deny" by simp
(*
However, your filters_all_evil analysis tool can also certify rulesets, a thing filters_all_evil_cheap cannot do.
*)
lemma "\rs p. firewall rs p = Allow \ filters_all_evil rs"
apply(rule_tac x="(\p. if evil_bit p then Deny else Allow) \ DefaultDeny" in exI)
apply(simp add: filters_evil_def)
apply(rule_tac x="\ enhanced_src_addr = ''Alice'', enhanced_dst_addr = ''Bob'', evil_bit = False \" in exI)
apply(simp)
done
(*
Why does your filters_all_evil reject the following ruleset: (\p. if evil_bit p then Deny else Pass) \ DefaultAllow
*)
(*
We define other_firewall. In every Rule-step, the firewall makes sure that there exist a combination of rule and packet that can evaluate to True.
Does this make sense? Does it exhibit different behaviour than our firewall?
*)
fun other_firewall :: "'p ruleset \ 'p \ action" where
"other_firewall DefaultDeny _ = Deny" |
"other_firewall DefaultAllow _ = Allow" |
"other_firewall (r\rs) p = (if r p \ Pass \ (\(p'::'p) (r'::'p rule). r' p' = Allow) then r p else other_firewall rs p)"
(*Show that other_firewall and firewall are actually equivalent. I.e. (\p' r'. r' p' = Allow) does not make any sense!*)
lemma "other_firewall rs p = firewall rs p"
proof(induction rs)
case DefaultAllow thus ?case by simp
next
case DefaultDeny thus ?case by simp
next
case (Rule r rs)
assume IH: "other_firewall rs p = firewall rs p"
have ex: "\(p'::'p) (r'::'p rule). r' p' = Allow" by fast
show "other_firewall (r \ rs) p = firewall (r \ rs) p"
proof(cases "r p")
case Allow
from ex Allow show "other_firewall (r \ rs) p = firewall (r \ rs) p" by simp
next
case Deny
from this ex show "other_firewall (r \ rs) p = firewall (r \ rs) p" by auto
next
case Pass
from this IH show "other_firewall (r \ rs) p = firewall (r \ rs) p" by simp
qed
qed
(*our proof from the course*)
lemma mehrhilfslemma: "(\(p'::'p) (r'::'p rule). r' p' = Allow)" by fast
(*Show that other_firewall and firewall are actually equivalent. I.e. (\p' r'. r' p' = Allow) does not make any sense!*)
lemma hilfslemma: "other_firewall rs p = firewall rs p"
proof(induction rs)
case DefaultAllow
show "other_firewall DefaultAllow p = firewall DefaultAllow p" by simp
next
case(Rule r rs)
assume IH: "other_firewall rs p = firewall rs p"
have 1: "firewall (r \ rs) p =
(case r p of Allow \ Allow | Deny \ Deny | Pass \ firewall rs p)"
by(simp)
have "other_firewall (r \ rs) p =
(if r p \ Pass \ (\p' r'. r' p' = Allow) then r p else other_firewall rs p)"
by auto
hence 2: "other_firewall (r \ rs) p =
(if r p \ Pass then r p else other_firewall rs p)" using mehrhilfslemma by auto
have 3: "(case r p of Allow \ Allow | Deny \ Deny | Pass \ firewall rs p) =
(if r p \ Pass then r p else firewall rs p)"
by(simp split: action.split)
from 1 2 3 IH show "other_firewall (r \ rs) p = firewall (r \ rs) p" by simp
qed(simp)
theorem "other_firewall = firewall"
apply(simp add: fun_eq_iff)
apply(clarify, rename_tac rs p)
using hilfslemma by fast
(*the function which removes shadowed rules from a ruleset*)
fun rmshadow :: "'p ruleset \ 'p set \ 'p ruleset" where
"rmshadow DefaultDeny _ = DefaultDeny" |
"rmshadow DefaultAllow _ = DefaultAllow" |
"rmshadow (r \ rs) P = (if (\p\P. r p = Pass)
then
rmshadow rs P
else
r \ rs (*(rmshadow rs) {p \P. r p = Pass}*))"
value "rmshadow (allow_HTTP \ DefaultDeny) UNIV"
lemma hilfslemmaX: "p \ P \ firewall rs p = firewall (rmshadow rs P) p"
apply(induction rs arbitrary: p P)
apply(simp_all)
done
lemma hilfslemmaX2:
"p \ P \ firewall rs p = firewall (((\x. rmshadow x P)^^n) rs) p"
apply(induction n)
apply(simp_all)
using hilfslemmaX by fast
definition "rmallshadowed rs \ ((\x. rmshadow x UNIV)^^(size rs)) rs"
theorem "firewall rs p = firewall (rmallshadowed rs) p"
unfolding rmallshadowed_def
using hilfslemmaX2 by fastforce
(*maybe our tool is no so good, ...*)
lemma "rmallshadowed (deny_UDP \ deny_UDP \ DefaultAllow) = deny_UDP \ deny_UDP \ DefaultAllow"
apply(simp add: rmallshadowed_def deny_UDP_def allow_DNS_def)
by (metis packet.select_convs(3))
(*but it can do a bit, ...*)
lemma "rmallshadowed ((\p. Pass) \ deny_UDP \ DefaultAllow) = deny_UDP \ DefaultAllow"
apply(simp add: rmallshadowed_def deny_UDP_def allow_DNS_def)
by (metis packet.select_convs(3))
end