theory tut08 imports "~~/src/HOL/IMP/Sec_Typing" "~~/src/HOL/IMP/Com" "~~/src/HOL/IMP/Def_Init_Exp" "~~/src/HOL/IMP/Def_Init" "~~/src/HOL/IMP/Vars" begin subsection {* Ex 08.1: Security type system: bottom-up with subsumption *} inductive sec_type2' :: "com \ level \ bool" ("(\' _ : _)" [0,0] 50) where Skip2': "\' SKIP : l" | Assign2': "sec x \ sec a \ \' x ::= a : sec x" | Semi2': "\ \' c\<^sub>1 : l; \' c\<^sub>2 : l \ \ \' c\<^sub>1 ;; c\<^sub>2 : l" | If2': "\ sec b \ l; \' c\<^sub>1 : l; \' c\<^sub>2 : l \ \ \' IF b THEN c\<^sub>1 ELSE c\<^sub>2 : l" | While2': "\ sec b \ l; \' c : l \ \ \' WHILE b DO c : l" | Subsumption2': "\ \' c : l; l' \ l \ \ \' c : l'" lemma "\ c : l \ \' c : l" apply (induction rule: sec_type2.induct) apply (auto intro: sec_type2'.intros) oops lemma assumes "\ c : l" shows "\' c : l" using assms apply (induction) apply (auto intro: sec_type2'.intros) apply (metis Semi2' Subsumption2' min.cobounded1 min.cobounded2) by (metis If2' Subsumption2' min.cobounded2 min.commute min_def) lemma "\' c : l \ \l' \ l. \ c : l'" apply (induction rule: sec_type2'.induct) apply (auto intro: sec_type2.intros) apply (metis Seq2 min.boundedI) apply (metis If2 le_trans min.bounded_iff) apply (metis While2 le_trans) by (metis le_trans) section {* Ex 08.2: Initialization-Sensitive Small Step Semantics *} inductive small_step :: "(com \ state) \ (com \ state) \ bool" (infix "\" 55) where Assign: "aval a s = Some i \ (x ::= a, s) \ (SKIP, s(x := Some i))" | Seq1: "(SKIP;;c,s) \ (c,s)" | Seq2: "(c\<^sub>1,s) \ (c\<^sub>1',s') \ (c\<^sub>1;;c\<^sub>2,s) \ (c\<^sub>1';;c\<^sub>2,s')" | IfTrue: "bval b s = Some True \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \ (c\<^sub>1,s)" | IfFalse: "bval b s = Some False \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \ (c\<^sub>2,s)" | While: "(WHILE b DO c,s) \ (IF b THEN c;; WHILE b DO c ELSE SKIP,s)" lemmas small_step_induct = small_step.induct[split_format(complete)] inductive small_steps :: "com * state \ com * state \ bool" (infix "\*" 55) where refl: "cs \* cs" | step: "cs \ cs' \ cs' \* cs'' \ cs \* cs''" lemmas small_steps_induct = small_steps.induct[split_format(complete)] subsection "Definite Initialization Analysis" fun AA :: "com \ vname set" where "AA SKIP = {}" | "AA (x::=a) = {x}" | "AA (c1;;c2) = AA c1 \ AA c2" | "AA (IF _ THEN c1 ELSE c2) = AA c1 \ AA c2" | "AA (WHILE b DO c) = {}" fun D :: "vname set \ com \ bool" where "D A SKIP = True" | "D A (x::=a) \ vars a \ A" | "D A (c1;;c2) \ D A c1 \ D (A \ AA c1) c2" | "D A (IF b THEN c1 ELSE c2) \ vars b \ A \ D A c1 \ D A c2 " | "D A (WHILE b DO c) \ vars b \ A \ D A c" subsection "Soundness wrt Small Steps" theorem progress: "D (dom s) c \ c \ SKIP \ \ cs'. (c,s) \ cs'" apply (induction c arbitrary: s) apply (auto intro: small_step.intros) apply (metis aval_Some small_step.Assign) apply (force intro: small_step.intros) by (metis (poly_guards_query) bval_Some small_step.IfFalse small_step.IfTrue) lemma D_incr: "(c,s) \ (c',s') \ dom s \ AA c \ dom s' \ AA c'" by (induction rule: small_step_induct) auto lemma D_mono: "A \ A' \ D A c \ D A' c" apply (induction c arbitrary: A A') apply (auto) by (metis inf_sup_aci(6) sup.absorb2 sup.left_commute sup_ge2) theorem D_preservation: "(c,s) \ (c',s') \ D (dom s) c \ D (dom s') c'" apply (induction rule: small_step_induct) apply (auto intro: D_mono dest: D_mono tut08.D_incr) done theorem D_sound: "(c,s) \* (c',s') \ D (dom s) c \ c' \ SKIP \ \cs''. (c',s') \ cs''" apply (induction rule: small_steps_induct) apply auto apply (metis (poly_guards_query) PairE progress) by (metis D_preservation) end