Theory Semantics
theory Semantics
imports Main Firewall_Common "Common/List_Misc" "HOL-Library.LaTeXsugar"
begin
section‹Big Step Semantics›
text‹
The assumption we apply in general is that the firewall does not alter any packets.
›
text‹A firewall ruleset is a map of chain names
(e.g., INPUT, OUTPUT, FORWARD, arbitrary-user-defined-chain) to a list of rules.
The list of rules is processed sequentially.›
type_synonym 'a ruleset = "string ⇀ 'a rule list"
text‹A matcher (parameterized by the type of primitive @{typ 'a} and packet @{typ 'p})
is a function which just tells whether a given primitive and packet matches.›
type_synonym ('a, 'p) matcher = "'a ⇒ 'p ⇒ bool"
text‹Example: Assume a network packet only has a destination street number
(for simplicity, of type @{typ "nat"}) and we only support the following match expression:
Is the packet's street number within a certain range?
The type for the primitive could then be @{typ "nat × nat"} and a possible implementation
for @{typ "(nat × nat, nat) matcher"} could be
@{term "match_street_number (a,b) p ⟷ p ∈ {a .. b}"}.
Usually, the primitives are a datatype which supports interfaces, IP addresses, protocols,
ports, payload, ...›
text‹Given an @{typ "('a, 'p) matcher"} and a match expression, does a packet of type @{typ 'p}
match the match expression?›
fun matches :: "('a, 'p) matcher ⇒ 'a match_expr ⇒ 'p ⇒ bool" where
"matches γ (MatchAnd e1 e2) p ⟷ matches γ e1 p ∧ matches γ e2 p" |
"matches γ (MatchNot me) p ⟷ ¬ matches γ me p" |
"matches γ (Match e) p ⟷ γ e p" |
"matches _ MatchAny _ ⟷ True"
inductive iptables_bigstep :: "'a ruleset ⇒ ('a, 'p) matcher ⇒ 'p ⇒ 'a rule list ⇒ state ⇒ state ⇒ bool"
("_,_,_⊢ ⟨_, _⟩ ⇒ _" [60,60,60,20,98,98] 89)
for Γ and γ and p where
skip: "Γ,γ,p⊢ ⟨[], t⟩ ⇒ t" |
accept: "matches γ m p ⟹ Γ,γ,p⊢ ⟨[Rule m Accept], Undecided⟩ ⇒ Decision FinalAllow" |
drop: "matches γ m p ⟹ Γ,γ,p⊢ ⟨[Rule m Drop], Undecided⟩ ⇒ Decision FinalDeny" |
reject: "matches γ m p ⟹ Γ,γ,p⊢ ⟨[Rule m Reject], Undecided⟩ ⇒ Decision FinalDeny" |
log: "matches γ m p ⟹ Γ,γ,p⊢ ⟨[Rule m Log], Undecided⟩ ⇒ Undecided" |
empty: "matches γ m p ⟹ Γ,γ,p⊢ ⟨[Rule m Empty], Undecided⟩ ⇒ Undecided" |
nomatch: "¬ matches γ m p ⟹ Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ Undecided" |
decision: "Γ,γ,p⊢ ⟨rs, Decision X⟩ ⇒ Decision X" |
seq: "⟦Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ t; Γ,γ,p⊢ ⟨rs⇩2, t⟩ ⇒ t'⟧ ⟹ Γ,γ,p⊢ ⟨rs⇩1@rs⇩2, Undecided⟩ ⇒ t'" |
call_return: "⟦ matches γ m p; Γ chain = Some (rs⇩1@[Rule m' Return]@rs⇩2);
matches γ m' p; Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ⟧ ⟹
Γ,γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided" |
call_result: "⟦ matches γ m p; Γ chain = Some rs; Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ t ⟧ ⟹
Γ,γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ t"
text‹
The semantic rules again in pretty format:
\begin{center}
@{thm[mode=Axiom] skip [no_vars]}\\[1ex]
@{thm[mode=Rule] accept [no_vars]}\\[1ex]
@{thm[mode=Rule] drop [no_vars]}\\[1ex]
@{thm[mode=Rule] reject [no_vars]}\\[1ex]
@{thm[mode=Rule] log [no_vars]}\\[1ex]
@{thm[mode=Rule] empty [no_vars]}\\[1ex]
@{thm[mode=Rule] nomatch [no_vars]}\\[1ex]
@{thm[mode=Rule] decision [no_vars]}\\[1ex]
@{thm[mode=Rule] seq [no_vars]} \\[1ex]
@{thm[mode=Rule] call_return [no_vars]}\\[1ex]
@{thm[mode=Rule] call_result [no_vars]}
\end{center}
›
lemma deny:
"matches γ m p ⟹ a = Drop ∨ a = Reject ⟹ iptables_bigstep Γ γ p [Rule m a] Undecided (Decision FinalDeny)"
by (auto intro: drop reject)
lemma seq_cons:
assumes "Γ,γ,p⊢ ⟨[r],Undecided⟩ ⇒ t" and "Γ,γ,p⊢ ⟨rs,t⟩ ⇒ t'"
shows "Γ,γ,p⊢ ⟨r#rs, Undecided⟩ ⇒ t'"
proof -
from assms have "Γ,γ,p⊢ ⟨[r] @ rs, Undecided⟩ ⇒ t'" by (rule seq)
thus ?thesis by simp
qed
lemma iptables_bigstep_induct
[case_names Skip Allow Deny Log Nomatch Decision Seq Call_return Call_result,
induct pred: iptables_bigstep]:
"⟦ Γ,γ,p⊢ ⟨rs,s⟩ ⇒ t;
⋀t. P [] t t;
⋀m a. matches γ m p ⟹ a = Accept ⟹ P [Rule m a] Undecided (Decision FinalAllow);
⋀m a. matches γ m p ⟹ a = Drop ∨ a = Reject ⟹ P [Rule m a] Undecided (Decision FinalDeny);
⋀m a. matches γ m p ⟹ a = Log ∨ a = Empty ⟹ P [Rule m a] Undecided Undecided;
⋀m a. ¬ matches γ m p ⟹ P [Rule m a] Undecided Undecided;
⋀rs X. P rs (Decision X) (Decision X);
⋀rs rs⇩1 rs⇩2 t t'. rs = rs⇩1 @ rs⇩2 ⟹ Γ,γ,p⊢ ⟨rs⇩1,Undecided⟩ ⇒ t ⟹ P rs⇩1 Undecided t ⟹ Γ,γ,p⊢ ⟨rs⇩2,t⟩ ⇒ t' ⟹ P rs⇩2 t t' ⟹ P rs Undecided t';
⋀m a chain rs⇩1 m' rs⇩2. matches γ m p ⟹ a = Call chain ⟹ Γ chain = Some (rs⇩1 @ [Rule m' Return] @ rs⇩2) ⟹ matches γ m' p ⟹ Γ,γ,p⊢ ⟨rs⇩1,Undecided⟩ ⇒ Undecided ⟹ P rs⇩1 Undecided Undecided ⟹ P [Rule m a] Undecided Undecided;
⋀m a chain rs t. matches γ m p ⟹ a = Call chain ⟹ Γ chain = Some rs ⟹ Γ,γ,p⊢ ⟨rs,Undecided⟩ ⇒ t ⟹ P rs Undecided t ⟹ P [Rule m a] Undecided t ⟧ ⟹
P rs s t"
by (induction rule: iptables_bigstep.induct) auto
lemma skipD: "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t ⟹ r = [] ⟹ s = t"
by (induction rule: iptables_bigstep.induct) auto
lemma decisionD: "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t ⟹ s = Decision X ⟹ t = Decision X"
by (induction rule: iptables_bigstep_induct) auto
context
notes skipD[dest] list_app_singletonE[elim]
begin
lemma acceptD: "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t ⟹ r = [Rule m Accept] ⟹ matches γ m p ⟹ s = Undecided ⟹ t = Decision FinalAllow"
by (induction rule: iptables_bigstep.induct) auto
lemma dropD: "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t ⟹ r = [Rule m Drop] ⟹ matches γ m p ⟹ s = Undecided ⟹ t = Decision FinalDeny"
by (induction rule: iptables_bigstep.induct) auto
lemma rejectD: "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t ⟹ r = [Rule m Reject] ⟹ matches γ m p ⟹ s = Undecided ⟹ t = Decision FinalDeny"
by (induction rule: iptables_bigstep.induct) auto
lemma logD: "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t ⟹ r = [Rule m Log] ⟹ matches γ m p ⟹ s = Undecided ⟹ t = Undecided"
by (induction rule: iptables_bigstep.induct) auto
lemma emptyD: "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t ⟹ r = [Rule m Empty] ⟹ matches γ m p ⟹ s = Undecided ⟹ t = Undecided"
by (induction rule: iptables_bigstep.induct) auto
lemma nomatchD: "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t ⟹ r = [Rule m a] ⟹ s = Undecided ⟹ ¬ matches γ m p ⟹ t = Undecided"
by (induction rule: iptables_bigstep.induct) auto
lemma callD:
assumes "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t" "r = [Rule m (Call chain)]" "s = Undecided" "matches γ m p" "Γ chain = Some rs"
obtains "Γ,γ,p⊢ ⟨rs,s⟩ ⇒ t"
| rs⇩1 rs⇩2 m' where "rs = rs⇩1 @ Rule m' Return # rs⇩2" "matches γ m' p" "Γ,γ,p⊢ ⟨rs⇩1,s⟩ ⇒ Undecided" "t = Undecided"
using assms
proof (induction r s t arbitrary: rs rule: iptables_bigstep.induct)
case (seq rs⇩1)
thus ?case by (cases rs⇩1) auto
qed auto
end
lemmas iptables_bigstepD = skipD acceptD dropD rejectD logD emptyD nomatchD decisionD callD
lemma seq':
assumes "rs = rs⇩1 @ rs⇩2" "Γ,γ,p⊢ ⟨rs⇩1,s⟩ ⇒ t" "Γ,γ,p⊢ ⟨rs⇩2,t⟩ ⇒ t'"
shows "Γ,γ,p⊢ ⟨rs,s⟩ ⇒ t'"
using assms by (cases s) (auto intro: seq decision dest: decisionD)
lemma seq'_cons: "Γ,γ,p⊢ ⟨[r],s⟩ ⇒ t ⟹ Γ,γ,p⊢ ⟨rs,t⟩ ⇒ t' ⟹ Γ,γ,p⊢ ⟨r#rs, s⟩ ⇒ t'"
by (metis decision decisionD state.exhaust seq_cons)
lemma seq_split:
assumes "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t" "rs = rs⇩1@rs⇩2"
obtains t' where "Γ,γ,p⊢ ⟨rs⇩1,s⟩ ⇒ t'" "Γ,γ,p⊢ ⟨rs⇩2,t'⟩ ⇒ t"
using assms
proof (induction rs s t arbitrary: rs⇩1 rs⇩2 thesis rule: iptables_bigstep_induct)
case Allow thus ?case by (cases rs⇩1) (auto intro: iptables_bigstep.intros)
next
case Deny thus ?case by (cases rs⇩1) (auto intro: iptables_bigstep.intros)
next
case Log thus ?case by (cases rs⇩1) (auto intro: iptables_bigstep.intros)
next
case Nomatch thus ?case by (cases rs⇩1) (auto intro: iptables_bigstep.intros)
next
case (Seq rs rsa rsb t t')
hence rs: "rsa @ rsb = rs⇩1 @ rs⇩2" by simp
note List.append_eq_append_conv_if[simp]
from rs show ?case
proof (cases rule: list_app_eq_cases)
case longer
with Seq have t1: "Γ,γ,p⊢ ⟨take (length rsa) rs⇩1, Undecided⟩ ⇒ t"
by simp
from Seq longer obtain t2
where t2a: "Γ,γ,p⊢ ⟨drop (length rsa) rs⇩1,t⟩ ⇒ t2"
and rs2_t2: "Γ,γ,p⊢ ⟨rs⇩2,t2⟩ ⇒ t'"
by blast
with t1 rs2_t2 have "Γ,γ,p⊢ ⟨take (length rsa) rs⇩1 @ drop (length rsa) rs⇩1,Undecided⟩ ⇒ t2"
by (blast intro: iptables_bigstep.seq)
with Seq rs2_t2 show ?thesis
by simp
next
case shorter
with rs have rsa': "rsa = rs⇩1 @ take (length rsa - length rs⇩1) rs⇩2"
by (metis append_eq_conv_conj length_drop)
from shorter rs have rsb': "rsb = drop (length rsa - length rs⇩1) rs⇩2"
by (metis append_eq_conv_conj length_drop)
from Seq rsa' obtain t1
where t1a: "Γ,γ,p⊢ ⟨rs⇩1,Undecided⟩ ⇒ t1"
and t1b: "Γ,γ,p⊢ ⟨take (length rsa - length rs⇩1) rs⇩2,t1⟩ ⇒ t"
by blast
from rsb' Seq.hyps have t2: "Γ,γ,p⊢ ⟨drop (length rsa - length rs⇩1) rs⇩2,t⟩ ⇒ t'"
by blast
with seq' t1b have "Γ,γ,p⊢ ⟨rs⇩2,t1⟩ ⇒ t'"
by fastforce
with Seq t1a show ?thesis
by fast
qed
next
case Call_return
hence "Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided" "Γ,γ,p⊢ ⟨rs⇩2, Undecided⟩ ⇒ Undecided"
by (case_tac [!] rs⇩1) (auto intro: iptables_bigstep.skip iptables_bigstep.call_return)
thus ?case by fact
next
case (Call_result _ _ _ _ t)
show ?case
proof (cases rs⇩1)
case Nil
with Call_result have "Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided" "Γ,γ,p⊢ ⟨rs⇩2, Undecided⟩ ⇒ t"
by (auto intro: iptables_bigstep.intros)
thus ?thesis by fact
next
case Cons
with Call_result have "Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ t" "Γ,γ,p⊢ ⟨rs⇩2, t⟩ ⇒ t"
by (auto intro: iptables_bigstep.intros)
thus ?thesis by fact
qed
qed (auto intro: iptables_bigstep.intros)
lemma seqE:
assumes "Γ,γ,p⊢ ⟨rs⇩1@rs⇩2, s⟩ ⇒ t"
obtains ti where "Γ,γ,p⊢ ⟨rs⇩1,s⟩ ⇒ ti" "Γ,γ,p⊢ ⟨rs⇩2,ti⟩ ⇒ t"
using assms by (force elim: seq_split)
lemma seqE_cons:
assumes "Γ,γ,p⊢ ⟨r#rs, s⟩ ⇒ t"
obtains ti where "Γ,γ,p⊢ ⟨[r],s⟩ ⇒ ti" "Γ,γ,p⊢ ⟨rs,ti⟩ ⇒ t"
using assms by (metis append_Cons append_Nil seqE)
lemma nomatch':
assumes "⋀r. r ∈ set rs ⟹ ¬ matches γ (get_match r) p"
shows "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ s"
proof(cases s)
case Undecided
have "∀r∈set rs. ¬ matches γ (get_match r) p ⟹ Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
proof(induction rs)
case Nil
thus ?case by (fast intro: skip)
next
case (Cons r rs)
hence "Γ,γ,p⊢ ⟨[r], Undecided⟩ ⇒ Undecided"
by (cases r) (auto intro: nomatch)
with Cons show ?case
by (fastforce intro: seq_cons)
qed
with assms Undecided show ?thesis by simp
qed (blast intro: decision)
text‹there are only two cases when there can be a Return on top-level:
▪ the firewall is in a Decision state
▪ the return does not match
In both cases, it is not applied!
›
lemma no_free_return: assumes "Γ,γ,p⊢ ⟨[Rule m Return], Undecided⟩ ⇒ t" and "matches γ m p" shows "False"
proof -
{ fix a s
have no_free_return_hlp: "Γ,γ,p⊢ ⟨a,s⟩ ⇒ t ⟹ matches γ m p ⟹ s = Undecided ⟹ a = [Rule m Return] ⟹ False"
proof (induction rule: iptables_bigstep.induct)
case (seq rs⇩1)
thus ?case
by (cases rs⇩1) (auto dest: skipD)
qed simp_all
} with assms show ?thesis by blast
qed
lemma seq_progress: "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t ⟹ rs = rs⇩1@rs⇩2 ⟹ Γ,γ,p⊢ ⟨rs⇩1, s⟩ ⇒ t' ⟹ Γ,γ,p⊢ ⟨rs⇩2, t'⟩ ⇒ t"
proof(induction arbitrary: rs⇩1 rs⇩2 t' rule: iptables_bigstep_induct)
case Allow
thus ?case
by (cases "rs⇩1") (auto intro: iptables_bigstep.intros dest: iptables_bigstepD)
next
case Deny
thus ?case
by (cases "rs⇩1") (auto intro: iptables_bigstep.intros dest: iptables_bigstepD)
next
case Log
thus ?case
by (cases "rs⇩1") (auto intro: iptables_bigstep.intros dest: iptables_bigstepD)
next
case Nomatch
thus ?case
by (cases "rs⇩1") (auto intro: iptables_bigstep.intros dest: iptables_bigstepD)
next
case Decision
thus ?case
by (cases "rs⇩1") (auto intro: iptables_bigstep.intros dest: iptables_bigstepD)
next
case(Seq rs rsa rsb t t' rs⇩1 rs⇩2 t'')
hence rs: "rsa @ rsb = rs⇩1 @ rs⇩2" by simp
note List.append_eq_append_conv_if[simp]
from rs show "Γ,γ,p⊢ ⟨rs⇩2,t''⟩ ⇒ t'"
proof(cases rule: list_app_eq_cases)
case longer
have "rs⇩1 = take (length rsa) rs⇩1 @ drop (length rsa) rs⇩1"
by auto
with Seq longer show ?thesis
by (metis append_Nil2 skipD seq_split)
next
case shorter
with Seq(7) Seq.hyps(3) Seq.IH(1) rs show ?thesis
by (metis seq' append_eq_conv_conj)
qed
next
case(Call_return m a chain rsa m' rsb)
have xx: "Γ,γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ t' ⟹ matches γ m p ⟹
Γ chain = Some (rsa @ Rule m' Return # rsb) ⟹
matches γ m' p ⟹
Γ,γ,p⊢ ⟨rsa, Undecided⟩ ⇒ Undecided ⟹
t' = Undecided"
apply(erule callD)
apply(simp_all)
apply(erule seqE)
apply(erule seqE_cons)
by (metis Call_return.IH no_free_return self_append_conv skipD)
show ?case
proof (cases rs⇩1)
case (Cons r rs)
thus ?thesis
using Call_return
apply(case_tac "[Rule m a] = rs⇩2")
apply(simp)
apply(simp)
using xx by blast
next
case Nil
moreover hence "t' = Undecided"
by (metis Call_return.hyps(1) Call_return.prems(2) append.simps(1) decision no_free_return seq state.exhaust)
moreover have "⋀m. Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ Undecided"
by (metis (no_types) Call_return(2) Call_return.hyps(3) Call_return.hyps(4) Call_return.hyps(5) call_return nomatch)
ultimately show ?thesis
using Call_return.prems(1) by auto
qed
next
case(Call_result m a chain rs t)
thus ?case
proof (cases rs⇩1)
case Cons
thus ?thesis
using Call_result
apply(auto simp add: iptables_bigstep.skip iptables_bigstep.call_result dest: skipD)
apply(drule callD, simp_all)
apply blast
by (metis Cons_eq_appendI append_self_conv2 no_free_return seq_split)
qed (fastforce intro: iptables_bigstep.intros dest: skipD)
qed (auto dest: iptables_bigstepD)
theorem iptables_bigstep_deterministic: assumes "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t" and "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t'" shows "t = t'"
proof -
{ fix r1 r2 m t
assume a1: "Γ,γ,p⊢ ⟨r1 @ Rule m Return # r2, Undecided⟩ ⇒ t" and a2: "matches γ m p" and a3: "Γ,γ,p⊢ ⟨r1,Undecided⟩ ⇒ Undecided"
have False
proof -
from a1 a3 have "Γ,γ,p⊢ ⟨Rule m Return # r2, Undecided⟩ ⇒ t"
by (blast intro: seq_progress)
hence "Γ,γ,p⊢ ⟨[Rule m Return] @ r2, Undecided⟩ ⇒ t"
by simp
from seqE[OF this] obtain ti where "Γ,γ,p⊢ ⟨[Rule m Return], Undecided⟩ ⇒ ti" by blast
with no_free_return a2 show False by fast
qed
} note no_free_return_seq=this
from assms show ?thesis
proof (induction arbitrary: t' rule: iptables_bigstep_induct)
case Seq
thus ?case
by (metis seq_progress)
next
case Call_result
thus ?case
by (metis no_free_return_seq callD)
next
case Call_return
thus ?case
by (metis append_Cons callD no_free_return_seq)
qed (auto dest: iptables_bigstepD)
qed
lemma iptables_bigstep_to_undecided: "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ Undecided ⟹ s = Undecided"
by (metis decisionD state.exhaust)
lemma iptables_bigstep_to_decision: "Γ,γ,p⊢ ⟨rs, Decision Y⟩ ⇒ Decision X ⟹ Y = X"
by (metis decisionD state.inject)
lemma Rule_UndecidedE:
assumes "Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ Undecided"
obtains (nomatch) "¬ matches γ m p"
| (log) "a = Log ∨ a = Empty"
| (call) c where "a = Call c" "matches γ m p"
using assms
proof (induction "[Rule m a]" Undecided Undecided rule: iptables_bigstep_induct)
case Seq
thus ?case
by (metis append_eq_Cons_conv append_is_Nil_conv iptables_bigstep_to_undecided)
qed simp_all
lemma Rule_DecisionE:
assumes "Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ Decision X"
obtains (call) chain where "matches γ m p" "a = Call chain"
| (accept_reject) "matches γ m p" "X = FinalAllow ⟹ a = Accept" "X = FinalDeny ⟹ a = Drop ∨ a = Reject"
using assms
proof (induction "[Rule m a]" Undecided "Decision X" rule: iptables_bigstep_induct)
case (Seq rs⇩1)
thus ?case
by (cases rs⇩1) (auto dest: skipD)
qed simp_all
lemma log_remove:
assumes "Γ,γ,p⊢ ⟨rs⇩1 @ [Rule m Log] @ rs⇩2, s⟩ ⇒ t"
shows "Γ,γ,p⊢ ⟨rs⇩1 @ rs⇩2, s⟩ ⇒ t"
proof -
from assms obtain t' where t': "Γ,γ,p⊢ ⟨rs⇩1, s⟩ ⇒ t'" "Γ,γ,p⊢ ⟨[Rule m Log] @ rs⇩2, t'⟩ ⇒ t"
by (blast elim: seqE)
hence "Γ,γ,p⊢ ⟨Rule m Log # rs⇩2, t'⟩ ⇒ t"
by simp
then obtain t'' where "Γ,γ,p⊢ ⟨[Rule m Log], t'⟩ ⇒ t''" "Γ,γ,p⊢ ⟨rs⇩2, t''⟩ ⇒ t"
by (blast elim: seqE_cons)
with t' show ?thesis
by (metis state.exhaust iptables_bigstep_deterministic decision log nomatch seq)
qed
lemma empty_empty:
assumes "Γ,γ,p⊢ ⟨rs⇩1 @ [Rule m Empty] @ rs⇩2, s⟩ ⇒ t"
shows "Γ,γ,p⊢ ⟨rs⇩1 @ rs⇩2, s⟩ ⇒ t"
proof -
from assms obtain t' where t': "Γ,γ,p⊢ ⟨rs⇩1, s⟩ ⇒ t'" "Γ,γ,p⊢ ⟨[Rule m Empty] @ rs⇩2, t'⟩ ⇒ t"
by (blast elim: seqE)
hence "Γ,γ,p⊢ ⟨Rule m Empty # rs⇩2, t'⟩ ⇒ t"
by simp
then obtain t'' where "Γ,γ,p⊢ ⟨[Rule m Empty], t'⟩ ⇒ t''" "Γ,γ,p⊢ ⟨rs⇩2, t''⟩ ⇒ t"
by (blast elim: seqE_cons)
with t' show ?thesis
by (metis state.exhaust iptables_bigstep_deterministic decision empty nomatch seq)
qed
lemma Unknown_actions_False: "Γ,γ,p⊢ ⟨r # rs, Undecided⟩ ⇒ t ⟹ r = Rule m a ⟹ matches γ m p ⟹ a = Unknown ∨ (∃chain. a = Goto chain) ⟹ False"
proof -
have 1: "Γ,γ,p⊢ ⟨[Rule m Unknown], Undecided⟩ ⇒ t ⟹ matches γ m p ⟹ False"
by (induction "[Rule m Unknown]" Undecided t rule: iptables_bigstep.induct)
(auto elim: list_app_singletonE dest: skipD)
{ fix chain
have "Γ,γ,p⊢ ⟨[Rule m (Goto chain)], Undecided⟩ ⇒ t ⟹ matches γ m p ⟹ False"
by (induction "[Rule m (Goto chain)]" Undecided t rule: iptables_bigstep.induct)
(auto elim: list_app_singletonE dest: skipD)
}note 2=this
show "Γ,γ,p⊢ ⟨r # rs, Undecided⟩ ⇒ t ⟹ r = Rule m a ⟹ matches γ m p ⟹ a = Unknown ∨ (∃chain. a = Goto chain) ⟹ False"
apply(erule seqE_cons)
apply(case_tac ti)
apply(simp_all)
using Rule_UndecidedE apply fastforce
by (metis "1" "2" decision iptables_bigstep_deterministic)
qed
text‹
The notation we prefer in the paper. The semantics are defined for fixed ‹Γ› and ‹γ›
›
locale iptables_bigstep_fixedbackground =
fixes Γ::"'a ruleset"
and γ::"('a, 'p) matcher"
begin
inductive iptables_bigstep' :: "'p ⇒ 'a rule list ⇒ state ⇒ state ⇒ bool"
("_⊢'' ⟨_, _⟩ ⇒ _" [60,20,98,98] 89)
for p where
skip: "p⊢' ⟨[], t⟩ ⇒ t" |
accept: "matches γ m p ⟹ p⊢' ⟨[Rule m Accept], Undecided⟩ ⇒ Decision FinalAllow" |
drop: "matches γ m p ⟹ p⊢' ⟨[Rule m Drop], Undecided⟩ ⇒ Decision FinalDeny" |
reject: "matches γ m p ⟹ p⊢' ⟨[Rule m Reject], Undecided⟩ ⇒ Decision FinalDeny" |
log: "matches γ m p ⟹ p⊢' ⟨[Rule m Log], Undecided⟩ ⇒ Undecided" |
empty: "matches γ m p ⟹ p⊢' ⟨[Rule m Empty], Undecided⟩ ⇒ Undecided" |
nomatch: "¬ matches γ m p ⟹ p⊢' ⟨[Rule m a], Undecided⟩ ⇒ Undecided" |
decision: "p⊢' ⟨rs, Decision X⟩ ⇒ Decision X" |
seq: "⟦p⊢' ⟨rs⇩1, Undecided⟩ ⇒ t; p⊢' ⟨rs⇩2, t⟩ ⇒ t'⟧ ⟹ p⊢' ⟨rs⇩1@rs⇩2, Undecided⟩ ⇒ t'" |
call_return: "⟦ matches γ m p; Γ chain = Some (rs⇩1@[Rule m' Return]@rs⇩2);
matches γ m' p; p⊢' ⟨rs⇩1, Undecided⟩ ⇒ Undecided ⟧ ⟹
p⊢' ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided" |
call_result: "⟦ matches γ m p; p⊢' ⟨the (Γ chain), Undecided⟩ ⇒ t ⟧ ⟹
p⊢' ⟨[Rule m (Call chain)], Undecided⟩ ⇒ t"
definition wf_Γ:: "'a rule list ⇒ bool" where
"wf_Γ rs ≡ ∀rsg ∈ ran Γ ∪ {rs}. (∀r ∈ set rsg. ∀ chain. get_action r = Call chain ⟶ Γ chain ≠ None)"
lemma wf_Γ_append: "wf_Γ (rs1@rs2) ⟷ wf_Γ rs1 ∧ wf_Γ rs2"
by(simp add: wf_Γ_def, blast)
lemma wf_Γ_tail: "wf_Γ (r # rs) ⟹ wf_Γ rs" by(simp add: wf_Γ_def)
lemma wf_Γ_Call: "wf_Γ [Rule m (Call chain)] ⟹ wf_Γ (the (Γ chain)) ∧ (∃rs. Γ chain = Some rs)"
apply(simp add: wf_Γ_def)
by (metis option.collapse ranI)
lemma "wf_Γ rs ⟹ p⊢' ⟨rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
apply(rule iffI)
apply(rotate_tac 1)
apply(induction rs s t rule: iptables_bigstep'.induct)
apply(auto intro: iptables_bigstep.intros simp: wf_Γ_append dest!: wf_Γ_Call)[11]
apply(rotate_tac 1)
apply(induction rs s t rule: iptables_bigstep.induct)
apply(auto intro: iptables_bigstep'.intros simp: wf_Γ_append dest!: wf_Γ_Call)[11]
done
end
text‹Showing that semantics are defined.
For rulesets which can be loaded by the Linux kernel. The kernel does not allow loops.›
text‹
We call a ruleset well-formed (wf) iff all @{const Call}s are into actually existing chains.
›
definition wf_chain :: "'a ruleset ⇒ 'a rule list ⇒ bool" where
"wf_chain Γ rs ≡ (∀r ∈ set rs. ∀ chain. get_action r = Call chain ⟶ Γ chain ≠ None)"
lemma wf_chain_append: "wf_chain Γ (rs1@rs2) ⟷ wf_chain Γ rs1 ∧ wf_chain Γ rs2"
by(simp add: wf_chain_def, blast)
lemma wf_chain_fst: "wf_chain Γ (r # rs) ⟹ wf_chain Γ (rs)"
by(simp add: wf_chain_def)
text‹This is what our tool will check at runtime›
definition sanity_wf_ruleset :: "(string × 'a rule list) list ⇒ bool" where
"sanity_wf_ruleset Γ ≡ distinct (map fst Γ) ∧
(∀ rs ∈ ran (map_of Γ). (∀r ∈ set rs. case get_action r of Accept ⇒ True
| Drop ⇒ True
| Reject ⇒ True
| Log ⇒ True
| Empty ⇒ True
| Call chain ⇒ chain ∈ dom (map_of Γ)
| Goto chain ⇒ chain ∈ dom (map_of Γ)
| Return ⇒ True
| _ ⇒ False))"
lemma sanity_wf_ruleset_wf_chain: "sanity_wf_ruleset Γ ⟹ rs ∈ ran (map_of Γ) ⟹ wf_chain (map_of Γ) rs"
apply(simp add: sanity_wf_ruleset_def wf_chain_def)
by fastforce
lemma sanity_wf_ruleset_start: "sanity_wf_ruleset Γ ⟹ chain_name ∈ dom (map_of Γ) ⟹
default_action = Accept ∨ default_action = Drop ⟹
wf_chain (map_of Γ) [Rule MatchAny (Call chain_name), Rule MatchAny default_action]"
apply(simp add: sanity_wf_ruleset_def wf_chain_def)
apply(safe)
apply(simp_all)
apply blast+
done
lemma [code]: "sanity_wf_ruleset Γ =
(let dom = map fst Γ;
ran = map snd Γ
in distinct dom ∧
(∀ rs ∈ set ran. (∀r ∈ set rs. case get_action r of Accept ⇒ True
| Drop ⇒ True
| Reject ⇒ True
| Log ⇒ True
| Empty ⇒ True
| Call chain ⇒ chain ∈ set dom
| Goto chain ⇒ chain ∈ set dom
| Return ⇒ True
| _ ⇒ False)))"
proof -
have set_map_fst: "set (map fst Γ) = dom (map_of Γ)"
by (simp add: dom_map_of_conv_image_fst)
have set_map_snd: "distinct (map fst Γ) ⟹ set (map snd Γ) = ran (map_of Γ)"
by (simp add: ran_distinct)
show ?thesis
unfolding sanity_wf_ruleset_def Let_def
apply(subst set_map_fst)+
apply(rule iffI)
apply(elim conjE)
apply(subst set_map_snd)
apply(simp)
apply(simp)
apply(elim conjE)
apply(subst(asm) set_map_snd)
apply(simp_all)
done
qed
lemma semantics_bigstep_defined1: assumes "∀rsg ∈ ran Γ ∪ {rs}. wf_chain Γ rsg"
and "∀rsg ∈ ran Γ ∪ {rs}. ∀ r ∈ set rsg. (∀chain. get_action r ≠ Goto chain) ∧ get_action r ≠ Unknown"
and "∀ r ∈ set rs. get_action r ≠ Return"
and "(∀name ∈ dom Γ. ∃t. Γ,γ,p⊢ ⟨the (Γ name), Undecided⟩ ⇒ t)"
shows "∃t. Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
using assms proof(induction rs)
case Nil thus ?case
apply(rule_tac x=s in exI)
by(simp add: skip)
next
case (Cons r rs)
from Cons.prems Cons.IH obtain t' where t': "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t'"
apply simp
apply(elim conjE)
apply(simp add: wf_chain_fst)
by blast
obtain m a where r: "r = Rule m a" by(cases r) blast
show ?case
proof(cases "matches γ m p")
case False
hence "Γ,γ,p⊢ ⟨[r], s⟩ ⇒ s"
apply(cases s)
apply(simp add: nomatch r)
by(simp add: decision)
thus ?thesis
apply(rule_tac x=t' in exI)
apply(rule_tac t=s in seq'_cons)
apply assumption
using t' by(simp)
next
case True
show ?thesis
proof(cases s)
case (Decision X) thus ?thesis
apply(rule_tac x="Decision X" in exI)
by(simp add: decision)
next
case Undecided
have "∃t. Γ,γ,p⊢ ⟨Rule m a # rs, Undecided⟩ ⇒ t"
proof(cases a)
case Accept with True show ?thesis
apply(rule_tac x="Decision FinalAllow" in exI)
apply(rule_tac t="Decision FinalAllow" in seq'_cons)
by(auto intro: iptables_bigstep.intros)
next
case Drop with True show ?thesis
apply(rule_tac x="Decision FinalDeny" in exI)
apply(rule_tac t="Decision FinalDeny" in seq'_cons)
by(auto intro: iptables_bigstep.intros)
next
case Log with True t' Undecided show ?thesis
apply(rule_tac x=t' in exI)
apply(rule_tac t=Undecided in seq'_cons)
by(auto intro: iptables_bigstep.intros)
next
case Reject with True show ?thesis
apply(rule_tac x="Decision FinalDeny" in exI)
apply(rule_tac t="Decision FinalDeny" in seq'_cons)
by(auto intro: iptables_bigstep.intros)[2]
next
case Return with Cons.prems(3)[simplified r] show ?thesis by simp
next
case Goto with Cons.prems(2)[simplified r] show ?thesis by auto
next
case (Call chain_name)
from Call Cons.prems(1) obtain rs' where 1: "Γ chain_name = Some rs'" by(simp add: r wf_chain_def) blast
with Cons.prems(4) obtain t'' where 2: "Γ,γ,p⊢ ⟨the (Γ chain_name), Undecided⟩ ⇒ t''" by blast
from 1 2 True have "Γ,γ,p⊢ ⟨[Rule m (Call chain_name)], Undecided⟩ ⇒ t''" by(auto dest: call_result)
with Call t' Undecided show ?thesis
apply(simp add: r)
apply(cases t'')
apply simp
apply(rule_tac x=t' in exI)
apply(rule_tac t=Undecided in seq'_cons)
apply(auto intro: iptables_bigstep.intros)[2]
apply(simp)
apply(rule_tac x=t'' in exI)
apply(rule_tac t=t'' in seq'_cons)
apply(auto intro: iptables_bigstep.intros)
done
next
case Empty with True t' Undecided show ?thesis
apply(rule_tac x=t' in exI)
apply(rule_tac t=Undecided in seq'_cons)
by(auto intro: iptables_bigstep.intros)
next
case Unknown with Cons.prems(2)[simplified r] show ?thesis by(simp)
qed
thus ?thesis
unfolding r Undecided by simp
qed
qed
qed
text‹Showing the main theorem›
context
begin
private lemma iptables_bigstep_defined_if_singleton_rules:
"∀ r ∈ set rs. (∃t. Γ,γ,p⊢ ⟨[r], s⟩ ⇒ t) ⟹ ∃t. Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
proof(induction rs arbitrary: s)
case Nil hence "Γ,γ,p⊢ ⟨[], s⟩ ⇒ s" by(simp add: skip)
thus ?case by blast
next
case(Cons r rs s)
from Cons.prems obtain t where t: "Γ,γ,p⊢ ⟨[r], s⟩ ⇒ t" by simp blast
with Cons show ?case
proof(cases t)
case Decision with t show ?thesis by (meson decision seq'_cons)
next
case Undecided
from Cons obtain t' where t': "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t'" by simp blast
with Undecided t show ?thesis
apply(rule_tac x=t' in exI)
apply(rule seq'_cons)
apply(simp)
using iptables_bigstep_to_undecided by fastforce
qed
qed
text‹well founded relation.›
definition calls_chain :: "'a ruleset ⇒ (string × string) set" where
"calls_chain Γ = {(r, s). case Γ r of Some rs ⇒ ∃m. Rule m (Call s) ∈ set rs | None ⇒ False}"
lemma calls_chain_def2: "calls_chain Γ = {(caller, callee). ∃rs m. Γ caller = Some rs ∧ Rule m (Call callee) ∈ set rs}"
unfolding calls_chain_def
apply(safe)
apply(simp split: option.split_asm)
apply(simp)
by blast
text‹example›
private lemma "calls_chain [
''FORWARD'' ↦ [(Rule m1 Log), (Rule m2 (Call ''foo'')), (Rule m3 Accept), (Rule m' (Call ''baz''))],
''foo'' ↦ [(Rule m4 Log), (Rule m5 Return), (Rule m6 (Call ''bar''))],
''bar'' ↦ [],
''baz'' ↦ []] =
{(''FORWARD'', ''foo''), (''FORWARD'', ''baz''), (''foo'', ''bar'')}"
unfolding calls_chain_def by(auto split: option.split_asm if_split_asm)
private lemma "wf (calls_chain [
''FORWARD'' ↦ [(Rule m1 Log), (Rule m2 (Call ''foo'')), (Rule m3 Accept), (Rule m' (Call ''baz''))],
''foo'' ↦ [(Rule m4 Log), (Rule m5 Return), (Rule m6 (Call ''bar''))],
''bar'' ↦ [],
''baz'' ↦ []])"
proof -
have g: "calls_chain [''FORWARD'' ↦ [(Rule m1 Log), (Rule m2 (Call ''foo'')), (Rule m3 Accept), (Rule m' (Call ''baz''))],
''foo'' ↦ [(Rule m4 Log), (Rule m5 Return), (Rule m6 (Call ''bar''))],
''bar'' ↦ [],
''baz'' ↦ []] = {(''FORWARD'', ''foo''), (''FORWARD'', ''baz''), (''foo'', ''bar'')}"
by(auto simp add: calls_chain_def split: option.split_asm if_split_asm)
show ?thesis
unfolding g
apply(simp)
apply safe
apply(erule rtranclE, simp_all)
apply(erule rtranclE, simp_all)
done
qed
text‹In our proof, we will need the reverse.›
private definition called_by_chain :: "'a ruleset ⇒ (string × string) set" where
"called_by_chain Γ = {(callee, caller). case Γ caller of Some rs ⇒ ∃m. Rule m (Call callee) ∈ set rs | None ⇒ False}"
private lemma called_by_chain_converse: "calls_chain Γ = converse (called_by_chain Γ)"
apply(simp add: calls_chain_def called_by_chain_def)
by blast
private lemma wf_called_by_chain: "finite (calls_chain Γ) ⟹ wf (calls_chain Γ) ⟹ wf (called_by_chain Γ)"
apply(frule Wellfounded.wf_acyclic)
apply(drule(1) Wellfounded.finite_acyclic_wf_converse)
apply(simp add: called_by_chain_converse)
done
private lemma helper_cases_call_subchain_defined_or_return:
"(∀x∈ran Γ. wf_chain Γ x) ⟹
∀rsg∈ran Γ. ∀r∈set rsg. (∀chain. get_action r ≠ Goto chain) ∧ get_action r ≠ Unknown ⟹
∀y m. ∀r∈set rs_called. r = Rule m (Call y) ⟶ (∃t. Γ,γ,p⊢ ⟨[Rule m (Call y)], Undecided⟩ ⇒ t) ⟹
wf_chain Γ rs_called ⟹
∀r∈set rs_called. (∀chain. get_action r ≠ Goto chain) ∧ get_action r ≠ Unknown ⟹
(∃t. Γ,γ,p⊢ ⟨rs_called, Undecided⟩ ⇒ t) ∨
(∃rs_called1 rs_called2 m'.
rs_called = (rs_called1 @ [Rule m' Return] @ rs_called2) ∧
matches γ m' p ∧ Γ,γ,p⊢ ⟨rs_called1, Undecided⟩ ⇒ Undecided)"
proof(induction rs_called arbitrary:)
case Nil hence "∃t. Γ,γ,p⊢ ⟨[], Undecided⟩ ⇒ t"
apply(rule_tac x=Undecided in exI)
by(simp add: skip)
thus ?case by simp
next
case (Cons r rs)
from Cons.prems have "wf_chain Γ [r]" by(simp add: wf_chain_def)
from Cons.prems have IH:"(∃t'. Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ t') ∨
(∃rs_called1 rs_called2 m'.
rs = (rs_called1 @ [Rule m' Return] @ rs_called2) ∧
matches γ m' p ∧ Γ,γ,p⊢ ⟨rs_called1, Undecided⟩ ⇒ Undecided)"
apply -
apply(rule Cons.IH)
apply(auto dest: wf_chain_fst)
done
from Cons.prems have case_call: "r = Rule m (Call y) ⟹ (∃t. Γ,γ,p⊢ ⟨[Rule m (Call y)], Undecided⟩ ⇒ t)" for y m
by(simp)
obtain m a where r: "r = Rule m a" by(cases r) simp
from Cons.prems have a_not: "(∀chain. a ≠ Goto chain) ∧ a ≠ Unknown" by(simp add: r)
have ex_neq_ret: "a ≠ Return ⟹ ∃t. Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ t"
proof(cases "matches γ m p")
case False thus ?thesis by(rule_tac x=Undecided in exI)(simp add: nomatch; fail)
next
case True
assume "a ≠ Return"
show ?thesis
proof(cases a)
case Accept with True show ?thesis
by(rule_tac x="Decision FinalAllow" in exI) (simp add: accept; fail)
next
case Drop with True show ?thesis
by(rule_tac x="Decision FinalDeny" in exI) (simp add: drop; fail)
next
case Log with True show ?thesis
by(rule_tac x="Undecided" in exI)(simp add: log; fail)
next
case Reject with True show ?thesis
by(rule_tac x="Decision FinalDeny" in exI) (simp add: reject; fail)
next
case Call with True show ?thesis
apply(simp)
apply(rule case_call)
apply(simp add: r; fail)
done
next
case Empty with True show ?thesis by(rule_tac x="Undecided" in exI) (simp add: empty; fail)
next
case Return with ‹a ≠ Return› show ?thesis by simp
qed(simp_all add: a_not)
qed
have *: "?case"
if pre: "rs = rs_called1 @ Rule m' Return # rs_called2 ∧ matches γ m' p ∧ Γ,γ,p⊢ ⟨rs_called1, Undecided⟩ ⇒ Undecided"
for rs_called1 m' rs_called2
proof(cases "matches γ m p")
case False thus ?thesis
apply -
apply(rule disjI2)
apply(rule_tac x="r#rs_called1" in exI)
apply(rule_tac x=rs_called2 in exI)
apply(rule_tac x=m' in exI)
apply(simp add: r pre)
apply(rule_tac t=Undecided in seq_cons)
apply(simp add: r nomatch; fail)
apply(simp add: pre; fail)
done
next
case True
from pre have rule_case_dijs1: "∃X. Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ Decision X ⟹ ?thesis"
apply -
apply(rule disjI1)
apply(elim exE conjE, rename_tac X)
apply(simp)
apply(rule_tac x="Decision X" in exI)
apply(rule_tac t="Decision X" in seq_cons)
apply(simp add: r; fail)
apply(simp add: decision; fail)
done
from pre have rule_case_dijs2: "Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ Undecided ⟹ ?thesis"
apply -
apply(rule disjI2)
apply(rule_tac x="r#rs_called1" in exI)
apply(rule_tac x=rs_called2 in exI)
apply(rule_tac x=m' in exI)
apply(simp add: r)
apply(rule_tac t=Undecided in seq_cons)
apply(simp; fail)
apply(simp;fail)
done
show ?thesis
proof(cases a)
case Accept show ?thesis
apply(rule rule_case_dijs1)
apply(rule_tac x="FinalAllow" in exI)
using True pre Accept by(simp add: accept)
next
case Drop show ?thesis
apply(rule rule_case_dijs1)
apply(rule_tac x="FinalDeny" in exI)
using True Drop by(simp add: deny)
next
case Log show ?thesis
apply(rule rule_case_dijs2)
using Log True by(simp add: log)
next
case Reject show ?thesis
apply(rule rule_case_dijs1)
apply(rule_tac x="FinalDeny" in exI)
using Reject True by(simp add: reject)
next
case (Call x5)
have "∃t. Γ,γ,p⊢ ⟨[Rule m (Call x5)], Undecided⟩ ⇒ t" by(rule case_call) (simp add: r Call)
with Call pre True show ?thesis
apply(simp)
apply(elim exE, rename_tac t_called)
apply(case_tac t_called)
apply(simp)
apply(rule disjI2)
apply(rule_tac x="r#rs_called1" in exI)
apply(rule_tac x=rs_called2 in exI)
apply(rule_tac x=m' in exI)
apply(simp add: r)
apply(rule_tac t=Undecided in seq_cons)
apply(simp add: r; fail)
apply(simp; fail)
apply(rule disjI1)
apply(rule_tac x=t_called in exI)
apply(rule_tac t=t_called in seq_cons)
apply(simp add: r; fail)
apply(simp add: decision; fail)
done
next
case Empty show ?thesis
apply(rule rule_case_dijs2)
using Empty True by(simp add: pre empty)
next
case Return show ?thesis
apply(rule disjI2)
apply(rule_tac x="[]" in exI)
apply(rule_tac x="rs_called1 @ Rule m' Return # rs_called2" in exI)
apply(rule_tac x=m in exI)
using Return True pre by(simp add: skip r)
qed(simp_all add: a_not)
qed
from IH have **: "a ≠ Return ⟶ (∃t. Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ t) ⟹ ?case"
proof(elim disjE, goal_cases)
case 2
from this obtain rs_called1 m' rs_called2 where
a1: "rs = rs_called1 @ [Rule m' Return] @ rs_called2" and
a2: "matches γ m' p" and a3: "Γ,γ,p⊢ ⟨rs_called1, Undecided⟩ ⇒ Undecided" by blast
show ?case
apply(rule *)
using a1 a2 a3 by simp
next
case 1 thus ?case
proof(cases "a ≠ Return")
case True
with 1 obtain t1 t2 where t1: "Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ t1"
and t2: "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ t2" by blast
from t1 t2 show ?thesis
apply -
apply(rule disjI1)
apply(simp add: r)
apply(cases t1)
apply(simp_all)
apply(rule_tac x=t2 in exI)
apply(rule_tac seq'_cons)
apply(simp_all)
apply (meson decision seq_cons)
done
next
case False show ?thesis
proof(cases "matches γ m p")
assume "¬ matches γ m p" with 1 show ?thesis
apply -
apply(rule disjI1)
apply(elim exE)
apply(rename_tac t')
apply(rule_tac x=t' in exI)
apply(rule_tac t=Undecided in seq_cons)
apply(simp add: r nomatch; fail)
by(simp)
next
assume "matches γ m p" with False show ?thesis
apply -
apply(rule disjI2)
apply(rule_tac x="[]" in exI)
apply(rule_tac x=rs in exI)
apply(rule_tac x=m in exI)
apply(simp add: r skip; fail)
done
qed
qed
qed
thus ?case using ex_neq_ret by blast
qed
lemma helper_defined_single:
assumes "wf (called_by_chain Γ)"
and "∀rsg ∈ ran Γ ∪ {[Rule m a]}. wf_chain Γ rsg"
and "∀rsg ∈ ran Γ ∪ {[Rule m a]}. ∀ r ∈ set rsg. (¬(∃chain. get_action r = Goto chain)) ∧ get_action r ≠ Unknown"
and "a ≠ Return"
shows "∃t. Γ,γ,p⊢ ⟨[Rule m a], s⟩ ⇒ t"
proof(cases s)
case (Decision decision) thus ?thesis
apply(rule_tac x="Decision decision" in exI)
apply(simp)
using iptables_bigstep.decision by fast
next
case Undecided
have "∃t. Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ t"
proof(cases "matches γ m p")
case False with assms show ?thesis
apply(rule_tac x=Undecided in exI)
apply(rule_tac t=Undecided in seq'_cons)
apply (metis empty_iff empty_set insert_iff list.simps(15) nomatch' rule.sel(1))
apply(simp add: skip; fail)
done
next
case True
show ?thesis
proof(cases a)
case Unknown with assms(3) show ?thesis by simp
next
case Goto with assms(3) show ?thesis by auto
next
case Accept with True show ?thesis by(auto intro: iptables_bigstep.intros)
next
case Drop with True show ?thesis by(auto intro: iptables_bigstep.intros)
next
case Reject with True show ?thesis by(auto intro: iptables_bigstep.intros)
next
case Log with True show ?thesis by(auto intro: iptables_bigstep.intros)
next
case Empty with True show ?thesis by(auto intro: iptables_bigstep.intros)
next
case Return with assms show ?thesis by simp
next
case (Call chain_name)
thm wf_induct_rule[where r="(calls_chain Γ)" and P="λx. ∃t. Γ,γ,p⊢ ⟨[Rule m (Call x)], Undecided⟩ ⇒ t"]
from assms have "wf (called_by_chain Γ)"
"∀rsg∈ran Γ. wf_chain Γ rsg"
"∀rsg∈ran Γ. ∀r∈set rsg. (∀chain. get_action r ≠ Goto chain) ∧ get_action r ≠ Unknown" by auto
hence "matches γ m p ⟹ wf_chain Γ [Rule m (Call chain_name)] ⟹ (∃t. Γ,γ,p⊢ ⟨[Rule m (Call chain_name)], Undecided⟩ ⇒ t)"
proof(induction arbitrary: m rule: wf_induct_rule[where r="called_by_chain Γ"])
case (less chain_name_neu)
from less.prems have "Γ chain_name_neu ≠ None" by(simp add: wf_chain_def)
from this obtain rs_called where rs_called: "Γ chain_name_neu = Some rs_called" by blast
from less rs_called have "wf_chain Γ rs_called" by (simp add: ranI)
from less rs_called have "rs_called ∈ ran Γ" by (simp add: ranI)
from less.prems rs_called have
"∀y m. ∀r ∈ set rs_called. r = Rule m (Call y) ⟶ (y, chain_name_neu) ∈ called_by_chain Γ ∧ wf_chain Γ [Rule m (Call y)]"
apply(simp)
apply(intro impI allI conjI)
apply(simp add: called_by_chain_def)
apply blast
apply(simp add: wf_chain_def)
apply (meson ranI rule.sel(2))
done
with less have "∀y m. ∀r∈set rs_called. r = Rule m (Call y) ⟶ (∃t. Γ,γ,p⊢ ⟨[Rule m (Call y)], Undecided⟩ ⇒ t)"
apply(intro allI, rename_tac y my)
apply(case_tac "matches γ my p")
apply blast
apply(intro ballI impI)
apply(rule_tac x=Undecided in exI)
apply(simp add: nomatch; fail)
done
from less.prems(4) rs_called ‹rs_called ∈ ran Γ›
helper_cases_call_subchain_defined_or_return[OF less.prems(3) less.prems(4) this ‹wf_chain Γ rs_called›] have
"(∃t. Γ,γ,p⊢ ⟨rs_called, Undecided⟩ ⇒ t) ∨
(∃rs_called1 rs_called2 m'.
Γ chain_name_neu = Some (rs_called1@[Rule m' Return]@rs_called2) ∧
matches γ m' p ∧ Γ,γ,p⊢ ⟨rs_called1, Undecided⟩ ⇒ Undecided)" by simp
thus ?case
proof(elim disjE exE conjE)
fix t
assume a: "Γ,γ,p⊢ ⟨rs_called, Undecided⟩ ⇒ t" show ?case
using call_result[OF less.prems(1) rs_called a] by(blast)
next
fix m' rs_called1 rs_called2
assume a1: "Γ chain_name_neu = Some (rs_called1 @ [Rule m' Return] @ rs_called2)"
and a2: "matches γ m' p" and a3: "Γ,γ,p⊢ ⟨rs_called1, Undecided⟩ ⇒ Undecided"
show ?case using call_return[OF less.prems(1) a1 a2 a3 ] by(blast)
qed
qed
with True assms Call show ?thesis by simp
qed
qed
with Undecided show ?thesis by simp
qed
private lemma helper_defined_ruleset_calledby: "wf (called_by_chain Γ) ⟹
∀rsg ∈ ran Γ ∪ {rs}. wf_chain Γ rsg ⟹
∀rsg ∈ ran Γ ∪ {rs}. ∀ r ∈ set rsg. (¬(∃chain. get_action r = Goto chain)) ∧ get_action r ≠ Unknown ⟹
∀ r ∈ set rs. get_action r ≠ Return ⟹
∃t. Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
apply(rule iptables_bigstep_defined_if_singleton_rules)
apply(intro ballI, rename_tac r, case_tac r, rename_tac m a, simp)
apply(rule helper_defined_single)
apply(simp; fail)
apply(simp add: wf_chain_def; fail)
apply fastforce
apply fastforce
done
corollary semantics_bigstep_defined: "finite (calls_chain Γ) ⟹ wf (calls_chain Γ) ⟹
∀rsg ∈ ran Γ ∪ {rs}. wf_chain Γ rsg ⟹
∀rsg ∈ ran Γ ∪ {rs}. ∀ r ∈ set rsg. (∀x. get_action r ≠ Goto x) ∧ get_action r ≠ Unknown ⟹
∀ r ∈ set rs. get_action r ≠ Return ⟹
∃t. Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
apply(drule(1) wf_called_by_chain)
apply(thin_tac "wf (calls_chain Γ)")
apply(rule helper_defined_ruleset_calledby)
apply(simp_all)
done
end
text‹Common Algorithms›
lemma iptables_bigstep_rm_LogEmpty: "Γ,γ,p⊢ ⟨rm_LogEmpty rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
proof(induction rs arbitrary: s)
case Nil thus ?case by(simp)
next
case (Cons r rs)
have step_IH: "(⋀s. Γ,γ,p⊢ ⟨rs1, s⟩ ⇒ t = Γ,γ,p⊢ ⟨rs2, s⟩ ⇒ t) ⟹
Γ,γ,p⊢ ⟨r#rs1, s⟩ ⇒ t = Γ,γ,p⊢ ⟨r#rs2, s⟩ ⇒ t" for rs1 rs2 r
by (meson seq'_cons seqE_cons)
have case_log: "Γ,γ,p⊢ ⟨Rule m Log # rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t" for m
apply(rule iffI)
apply(erule seqE_cons)
apply (metis append_Nil log_remove seq')
apply(rule_tac t=s in seq'_cons)
apply(cases s)
apply(cases "matches γ m p")
apply(simp add: log; fail)
apply(simp add: nomatch; fail)
apply(simp add: decision; fail)
apply simp
done
have case_empty: "Γ,γ,p⊢ ⟨Rule m Empty # rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t" for m
apply(rule iffI)
apply(erule seqE_cons)
apply (metis append_Nil empty_empty seq')
apply(rule_tac t=s in seq'_cons)
apply(cases s)
apply(cases "matches γ m p")
apply(simp add: empty; fail)
apply(simp add: nomatch; fail)
apply(simp add: decision; fail)
apply simp
done
from Cons show ?case
apply(cases r, rename_tac m a)
apply(case_tac a)
apply(simp_all)
apply(simp_all cong: step_IH)
apply(simp_all add: case_log case_empty)
done
qed
lemma iptables_bigstep_rw_Reject: "Γ,γ,p⊢ ⟨rw_Reject rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
proof(induction rs arbitrary: s)
case Nil thus ?case by(simp)
next
case (Cons r rs)
have step_IH: "(⋀s. Γ,γ,p⊢ ⟨rs1, s⟩ ⇒ t = Γ,γ,p⊢ ⟨rs2, s⟩ ⇒ t) ⟹
Γ,γ,p⊢ ⟨r#rs1, s⟩ ⇒ t = Γ,γ,p⊢ ⟨r#rs2, s⟩ ⇒ t" for rs1 rs2 r
by (meson seq'_cons seqE_cons)
have fst_rule: "(⋀t. Γ,γ,p⊢ ⟨[r1], s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[r2], s⟩ ⇒ t) ⟹
Γ,γ,p⊢ ⟨r1 # rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨r2 # rs, s⟩ ⇒ t" for r1 r2 rs s t
by (meson seq'_cons seqE_cons)
have dropreject: "Γ,γ,p⊢ ⟨[Rule m Drop], s⟩ ⇒ t = Γ,γ,p⊢ ⟨[Rule m Reject], s⟩ ⇒ t" for m t
apply(cases s)
apply(cases "matches γ m p")
using drop reject dropD rejectD apply fast
using nomatch nomatchD apply fast
using decision decisionD apply fast
done
from Cons show ?case
apply(cases r, rename_tac m a)
apply simp
apply(case_tac a)
apply(simp_all)
apply(simp_all cong: step_IH)
apply(rule fst_rule)
apply(simp add: dropreject)
done
qed
end