diff -r 0d219ddd6354 -r 9fc384154e84 Dynamic2static.thy --- a/Dynamic2static.thy Mon Oct 21 16:18:19 2013 +0800 +++ b/Dynamic2static.thy Tue Oct 22 10:08:27 2013 +0800 @@ -55,16 +55,10 @@ sorry -lemma tainted_has_sobj: - "\obj \ tainted s; valid s\ \ \ sobj. co2sobj s obj = Some sobj" -apply (frule tainted_in_current, case_tac obj) -apply (auto dest:valid_tainted_obj simp:co2sobj.simps split:option.splits) -oops - lemma t2ts: "obj \ tainted s \ co2sobj s obj = Some sobj \ tainted_s (s2ss s) sobj" apply (frule tainted_in_current, frule tainted_is_valid) -apply (frule d2s_main', simp) +apply (frule s2ss_included_sobj, simp) apply (case_tac sobj, simp_all) apply (case_tac [!] obj, simp_all add:co2sobj.simps split:option.splits if_splits) apply (drule dir_not_tainted, simp) @@ -91,9 +85,12 @@ by (auto simp:taintable_def) hence vs: "valid s" by (simp add:tainted_is_valid) hence static: "s2ss s \ static" using d2s_main by auto - from tainted obtain sobj where sobj: "co2sobj s obj = Some sobj" sorry -(* should constrain undeletable with file/dir/process only, while msg and fd are excluded - using vs tainted_has_sobj by blast *) + from tainted tbl vs obtain sobj where sobj: "co2sobj s obj = Some sobj" + apply (clarsimp simp add:taintable_def) + apply (frule tainted_in_current) + apply (case_tac obj, simp_all add:co2sobj.simps) + apply (frule current_proc_has_sp, simp, auto) + done from undel vs have "\ deleted obj s" and init_alive: "init_alive obj" by (auto simp:undeletable_def) with vs sobj have "init_obj_related sobj obj" @@ -182,6 +179,12 @@ apply auto done +lemma init_related_imp_init_sobj: + "init_obj_related sobj obj \ is_init_sobj sobj" +apply (case_tac sobj, case_tac [!] obj, auto) +apply (rule_tac x = "(Init list, (aa, ab, b), ac, ba)" in bexI, auto) +done + theorem undeletable_s_complete: assumes undel_s: "undeletable_s obj" shows "undeletable obj" @@ -195,7 +198,11 @@ then obtain s where vs: "valid s" and del: "deleted obj s" by auto from vs have vss: "s2ss s \ static" by (rule d2s_main) with alive_s obtain sobj where in_ss: "sobj \ (s2ss s)" - and related: "init_obj_related sobj obj" apply auto + and related: "init_obj_related sobj obj" + apply (simp add:init_ss_in_def init_ss_eq_def) + apply (erule bexE, erule_tac x= ss' in ballE) + apply (auto dest:init_related_imp_init_sobj) + done from init_alive del vs have "deletable_s obj" by (auto elim:deleted_imp_deletable_s) with alive_s @@ -210,14 +217,8 @@ apply (erule swap) by (simp add:static_complete undeletable_s_complete) - - (************** static \ dynamic ***************) -lemma created_can_have_many: - "\valid s; alive s obj; \ init_alive obj\ \ \ s'. valid s' \ alive s' obj \ alive s' obj' \ s2ss s = s2ss s'" -sorry - lemma s2d_main: "ss \ static \ \ s. valid s \ s2ss s = ss" apply (erule static.induct) @@ -227,15 +228,6 @@ sorry -lemma tainted_s_in_ss: - "tainted_s ss sobj \ sobj \ ss" -apply (case_tac sobj, simp_all) -apply (case_tac bool, simp+) -apply (case_tac bool, simp+) -apply (case_tac prod1, case_tac prod2, simp) -thm tainted_s.simps -oops - lemma set_eq_D: "\x \ S; {x. P x} = S\ \ P x" by auto @@ -251,6 +243,8 @@ \ \ m. cm2smsg s q m = Some sm" by (auto simp:cq2smsgq_def split: option.splits intro:cqm2sms_prop1) +declare co2sobj.simps [simp add] + lemma tainted_s_imp_tainted: "\tainted_s ss sobj; ss \ static\ \ \ s obj. valid s \ co2sobj s obj = Some sobj \ obj \ tainted s" apply (drule s2d_main) @@ -264,29 +258,11 @@ apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) apply (rule_tac x = obj in exI, simp) apply (case_tac obj, (simp split:option.splits if_splits)+) - -apply (case_tac prod1, case_tac prod2, simp) -apply ((erule conjE)+, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) -apply (case_tac obj, simp_all split:option.splits if_splits) -apply (drule_tac sm = "(aa, ba, True)" in sq_sm_prop, simp+, erule exE) -apply (rule_tac x = "O_msg nat m" in exI) -apply (rule conjI) -apply simp -apply (simp add -apply (simp add:co2sobj.simps) -apply (simp add:cm2smsg_def split:option.splits if_splits) done -lemma has_inode_tainted_aux: - "O_file f \ tainted s \ \ f'. has_same_inode s f f' \ O_file f' \ tainted s" -apply (erule tainted.induct) -apply (auto intro:tainted.intros simp:has_same_inode_def) -(*?? need simpset for tainted *) -sorry - -lemma has_same_inode_tainted: - "\has_same_inode s f f'; O_file f' \ tainted s\ \ O_file f \ tainted s" -by (drule has_inode_tainted_aux, auto simp:has_same_inode_def) +lemma has_same_inode_prop3: + "has_same_inode s f f' \ has_same_inode s f' f" +by (auto simp:has_same_inode_def) theorem static_sound: assumes tbl_s: "taintable_s obj" @@ -306,19 +282,14 @@ apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_def is_file_def is_dir_def split:option.splits t_inode_tag.splits dest!:cf2sfile_fi) done - with tainted' have tainted: "obj \ tainted s" - by (auto intro:has_same_inode_tainted) - with vs init_alive + with tainted' vs have tainted: "obj \ tainted s" + by (auto dest:has_same_inode_prop3 intro:has_same_inode_tainted) + from sobj related init_alive have "appropriate obj" + by (case_tac obj, case_tac [!] sobj, auto) + with vs init_alive tainted show ?thesis by (auto simp:taintable_def) qed - - -lemma ts2t: - "obj \ tainted_s ss \ \ s. obj \ tainted s" - "obj \ tainted_s ss \ \ so. so True \ ss \ so True \ ss \ \ s. valid s \ s2ss s = ss \ so True \ s2ss s \ tainted s obj. " - - - +end end \ No newline at end of file