theory Type_System
imports Language_Composition
begin
locale Type_System =
WWP: WHATWHERE_Secure_Programs "E" "BMap" "DA" "lH"
for E :: "('exp, 'id, 'val) Evalfunction"
and BMap :: "'val => bool"
and DA :: "('id, 'd::order) DomainAssignment"
and lH :: "('d, 'exp) lHatches"
+
fixes
AssignSideCondition :: "'id => 'exp => nat => bool"
and WhileSideCondition :: "'exp => bool"
and IfSideCondition ::
"'exp => ('exp,'id) MWLsCom => ('exp,'id) MWLsCom => bool"
assumes semAssignSC: "AssignSideCondition x e ι ==>
e ≡⇘DA x,(htchLoc ι)⇙ e ∧ (∀m m' d ι'. (m ∼⇘d,(htchLoc ι')⇙ m' ∧
[|x :=⇘ι⇙ e|](m) =⇘d⇙ [|x :=⇘ι⇙ e|](m'))
--> [|x :=⇘ι⇙ e|](m) ∼⇘d,(htchLoc ι')⇙ [|x :=⇘ι⇙ e|](m'))"
and semWhileSC: "WhileSideCondition e ==> ∀d. e ≡⇘d⇙ e"
and semIfSC: "IfSideCondition e c1 c2 ==> ∀d. e ≡⇘d⇙ e"
begin
-- "Security typing rules for the language commands"
inductive
ComSecTyping :: "('exp, 'id) MWLsCom => bool"
("\<turnstile>⇘\<C>⇙ _")
and ComSecTypingL :: "('exp,'id) MWLsCom list => bool"
("\<turnstile>⇘\<V>⇙ _")
where
Skip: "\<turnstile>⇘\<C>⇙ skip⇘ι⇙" |
Assign: "[| AssignSideCondition x e ι |] ==> \<turnstile>⇘\<C>⇙ x :=⇘ι⇙ e" |
Spawn: "[| \<turnstile>⇘\<V>⇙ V |] ==> \<turnstile>⇘\<C>⇙ spawn⇘ι⇙ V" |
Seq: "[| \<turnstile>⇘\<C>⇙ c1; \<turnstile>⇘\<C>⇙ c2 |] ==> \<turnstile>⇘\<C>⇙ c1;c2" |
While: "[| \<turnstile>⇘\<C>⇙ c; WhileSideCondition b |]
==> \<turnstile>⇘\<C>⇙ while⇘ι⇙ b do c od" |
If: "[| \<turnstile>⇘\<C>⇙ c1; \<turnstile>⇘\<C>⇙ c2; IfSideCondition b c1 c2 |]
==> \<turnstile>⇘\<C>⇙ if⇘ι⇙ b then c1 else c2 fi" |
Parallel: "[| ∀i < length V. \<turnstile>⇘\<C>⇙ V!i |] ==> \<turnstile>⇘\<V>⇙ V"
inductive_cases parallel_cases:
"\<turnstile>⇘\<V>⇙ V"
definition auxiliary_predicate
where
"auxiliary_predicate V ≡ unique_PPV V --> WHATWHERE_Secure V"
--"soundness proof of abstract type system"
theorem ComSecTyping_single_is_sound:
"[| \<turnstile>⇘\<C>⇙ c; unique_PPc c |]
==> WHATWHERE_Secure [c]"
proof (induct rule: ComSecTyping_ComSecTypingL.inducts(1)
[of _ _ "auxiliary_predicate"], simp_all add: auxiliary_predicate_def)
fix ι
show "WHATWHERE_Secure [skip⇘ι⇙]"
by (metis WHATWHERE_Secure_Skip)
next
fix x e ι
assume "AssignSideCondition x e ι"
thus "WHATWHERE_Secure [x :=⇘ι⇙ e]"
by (metis WHATWHERE_Secure_Assign semAssignSC)
next
fix V ι
assume IH: "unique_PPV V --> WHATWHERE_Secure V"
assume uniPPspawn: "unique_PPc (spawn⇘ι⇙ V)"
hence "unique_PPV V"
by (simp add: unique_PPV_def unique_PPc_def)
with IH have "WHATWHERE_Secure V"
..
with uniPPspawn show "WHATWHERE_Secure [spawn⇘ι⇙ V]"
by (metis Compositionality_Spawn)
next
fix c1 c2
assume IH1: "unique_PPc c1 ==> WHATWHERE_Secure [c1]"
assume IH2: "unique_PPc c2 ==> WHATWHERE_Secure [c2]"
assume uniPPc1c2: "unique_PPc (c1;c2)"
from uniPPc1c2 have uniPPc1: "unique_PPc c1"
by (simp add: unique_PPc_def)
with IH1 have IS1: "WHATWHERE_Secure [c1]"
.
from uniPPc1c2 have uniPPc2: "unique_PPc c2"
by (simp add: unique_PPc_def)
with IH2 have IS2: "WHATWHERE_Secure [c2]"
.
from IS1 IS2 uniPPc1c2 show "WHATWHERE_Secure [c1;c2]"
by (metis Compositionality_Seq)
next
fix c b ι
assume SC: "WhileSideCondition b"
assume IH: "unique_PPc c ==> WHATWHERE_Secure [c]"
assume uniPPwhile: "unique_PPc (while⇘ι⇙ b do c od)"
hence "unique_PPc c"
by (simp add: unique_PPc_def)
with IH have "WHATWHERE_Secure [c]"
.
with uniPPwhile SC show "WHATWHERE_Secure [while⇘ι⇙ b do c od]"
by (metis Compositionality_While semWhileSC)
next
fix c1 c2 b ι
assume SC: "IfSideCondition b c1 c2"
assume IH1: "unique_PPc c1 ==> WHATWHERE_Secure [c1]"
assume IH2: "unique_PPc c2 ==> WHATWHERE_Secure [c2]"
assume uniPPif: "unique_PPc (if⇘ι⇙ b then c1 else c2 fi)"
from uniPPif have "unique_PPc c1"
by (simp add: unique_PPc_def)
with IH1 have IS1: "WHATWHERE_Secure [c1]"
.
from uniPPif have "unique_PPc c2"
by (simp add: unique_PPc_def)
with IH2 have IS2: "WHATWHERE_Secure [c2]"
.
from IS1 IS2 SC uniPPif show
"WHATWHERE_Secure [if⇘ι⇙ b then c1 else c2 fi]"
by (metis Compositionality_If semIfSC)
next
fix V
assume IH: "∀i < length V. \<turnstile>⇘\<C>⇙ V ! i ∧
(unique_PPc (V!i) --> WHATWHERE_Secure [V!i])"
have "unique_PPV V --> (∀i < length V. unique_PPc (V!i))"
by (metis uniPPV_uniPPc)
with IH have "unique_PPV V --> (∀i < length V. WHATWHERE_Secure [V!i])"
by auto
thus uniPPV: "unique_PPV V --> WHATWHERE_Secure V"
by (metis parallel_composition)
qed
theorem ComSecTyping_list_is_sound:
"[| \<turnstile>⇘\<V>⇙ V; unique_PPV V |] ==> WHATWHERE_Secure V"
by (metis ComSecTyping_single_is_sound parallel_cases
parallel_composition uniPPV_uniPPc)
end
end