(*<*) theory ex07 imports "HOL-IMP.Small_Step" "HOL-IMP.Def_Init" "HOL-IMP.Sec_Typing" begin (*>*) text \\ExerciseSheet{07}{02.12.2019} \ text \ \Exercise{Available Expressions} \ text \ Regard the following function @{text "AA"}, which computes the {\em available assignments} of a command. An available assignment is a pair of a variable and an expression such that the variable holds the value of the expression in the current state. The function @{text "AA c A"} computes the available assignments after executing command @{text "c"}, assuming that @{text "A"} is the set of available assignments for the initial state. Note that available assignments can be used for program optimization, by avoiding recomputation of expressions whose value is already available in some variable. \ fun AA :: "com \ (vname \ aexp) set \ (vname \ aexp) set" where "AA SKIP A = A" | "AA (x ::= a) A = (if x \ vars a then {} else {(x, a)}) \ {(x', a'). (x', a') \ A \ x \ {x'} \ vars a'}" | "AA (c\<^sub>1;; c\<^sub>2) A = (AA c\<^sub>2 \ AA c\<^sub>1) A" | "AA (IF b THEN c\<^sub>1 ELSE c\<^sub>2) A = AA c\<^sub>1 A \ AA c\<^sub>2 A" | "AA (WHILE b DO c) A = A \ AA c A" text \ Show that available assignment analysis is a gen/kill analysis, i.e., define two functions @{text "gen"} and @{text "kill"} such that @{text [display] "AA c A = (A \ gen c) - kill c."} Note that the above characterization differs from the one that you have seen on the slides, which is @{text "(A - kill c) \ gen c"}. However, the same properties (monotonicity, etc.) can be derived using either version. \ fun gen :: "com \ (vname \ aexp) set" and kill :: "com \ (vname \ aexp) set" (*<*) where "gen SKIP = {}" | "gen (x ::= a) = (if x \ vars a then {} else {(x,a)})" | "gen (c1;; c2) = gen c2 \ (gen c1 - kill c2)" | "gen (IF b THEN c1 ELSE c2) = gen c1 \ gen c2" | "gen (WHILE b DO c) = {}" | "kill SKIP = {}" | "kill (x ::= a) = {(x',a'). x=x' \ a\a' | x \ vars a'}" | "kill (c1;; c2) = (kill c1 - gen c2) \ kill c2" | "kill (IF b THEN c1 ELSE c2) = kill c1 \ kill c2" | "kill (WHILE b DO c) = kill c" (*>*) lemma AA_gen_kill: "AA c A = (A \ gen c) - kill c" (*<*)by (induction c arbitrary:A) auto(*>*) text \ \emph{Hint:} Defining @{text "gen"} and @{text "kill"} functions for available assignments will require \emph{mutual recursion}, i.e., @{text "gen"} must make recursive calls to @{text "kill"}, and @{text "kill"} must also make recursive calls to @{text "gen"}. The \textbf{and}-syntax in the function declaration allows you to define both functions simultaneously with mutual recursion. After the \textbf{where} keyword, list all the equations for both functions, separated by @{text "|"} as usual. \ (*<*) lemma AA_mono: "A1 \ A2 \ AA c A1 \ AA c A2" by(auto simp add: AA_gen_kill) lemma AA_distr: "AA c (A1 \ A2) = AA c A1 \ AA c A2" by(auto simp add: AA_gen_kill) lemma AA_idemp: "AA c (AA c A) = AA c A" by(auto simp add: AA_gen_kill) (*>*) text \Now show that the analysis is sound:\ theorem AA_sound: "(c, s) \ s' \ \(x, a) \ AA c {}. s' x = aval a s'" (*<*)oops(*>*) text \\emph{Hint:} You will have to generalize the theorem for the induction to go through.\ (*<*) lemma AA_sound_aux: "(c,s) \ s' \ \ (x,a) \ A. s x = aval a s \ \ (x,a) \ AA c A. s' x = aval a s'" proof (induct arbitrary: A rule: big_step_induct) case (WhileTrue b s\<^sub>1 c s\<^sub>2 s\<^sub>3) from WhileTrue(6) have "\(x, a)\AA c A. s\<^sub>2 x = aval a s\<^sub>2" by (rule WhileTrue(3)) then have "\(x, a)\AA (WHILE b DO c) (AA c A). s\<^sub>3 x = aval a s\<^sub>3" by (rule WhileTrue(5)) then show ?case by (simp add: AA_idemp) qed (fastforce split: if_split_asm)+ theorem AA_sound: "(c,s) \ s' \ \ (x,a) \ AA c {}. s' x = aval a s'" using AA_sound_aux[where A="{}"] by auto (*>*) text \\Exercise{Security type system: bottom-up with subsumption} Recall security type systems for information flow control from the lecture. Such a type systems can either be defined in a top-down or in a bottom-up manner. Independently of this choice, the type system may or may not contain a subsumption rule (also called anti-monotonicity in the lecture). The lecture discussed already all but one combination: a bottom-up type system with subsumption. \begin{enumerate} \item Define a bottom-up security type system for information flow control with subsumption rule (see below, add the subsumption rule). \item Prove the equivalence of the newly introduced bottom-up type system with the bottom-up type system without subsumption rule from the lecture. \end{enumerate} \ 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"(*<*) proof (induction rule: sec_type2.induct) case Seq2 thus ?case by (metis Semi2' Subsumption2' min_absorb1 min.cobounded2 nat_le_linear) next case If2 thus ?case by (metis If2' Subsumption2' min.bounded_iff nat_le_linear) qed (auto intro: sec_type2'.intros)(*>*) lemma "\' c : l \ \l' \ l. \ c : l'"(*<*) proof (induct rule: sec_type2'.induct) case Skip2' then show ?case by (metis Skip2 less_or_eq_imp_le) next case Assign2' then show ?case by (metis Assign2 less_or_eq_imp_le) next case Semi2' then show ?case by (metis Seq2 min.bounded_iff) next case If2' then show ?case by (metis If' anti_mono' sec_type'_sec_type2 sec_type2_sec_type') next case While2' then show ?case by (metis While2 le_trans) next case Subsumption2' then show ?case by (metis le_trans) qed (*>*) (*<*) end (*>*)