--- a/Current_prop.thy Mon Jun 24 15:22:37 2013 +0800
+++ b/Current_prop.thy Tue Jul 09 14:43:51 2013 +0800
@@ -55,15 +55,332 @@
"\<lbrakk>info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s \<and> p' \<in> current_procs s"
by (auto intro:procs_of_shm_prop2 simp:info_flow_shm_def one_flow_shm_def)
-(*********** simpset for info_flow_shm **************)
+lemma flag_of_proc_shm_prop1:
+ "\<lbrakk>flag_of_proc_shm s p h = Some flag; valid s\<rbrakk> \<Longrightarrow> (p, flag) \<in> procs_of_shm s h"
+apply (induct s arbitrary:p flag)
+apply (simp, drule init_shmflag_has_proc, simp)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)
+done
+
+(*********** simpset for one_flow_shm **************)
+
+lemma one_flow_not_self:
+ "one_flow_shm s h p p \<Longrightarrow> False"
+by (simp add:one_flow_shm_def)
+
+lemma one_flow_shm_attach:
+ "valid (Attach p h flag # s) \<Longrightarrow> one_flow_shm (Attach p h flag # s) = (\<lambda> h' pa pb.
+ if (h' = h)
+ then (pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pb, flagb) \<in> procs_of_shm s h)) \<or>
+ (pb = p \<and> pa \<noteq> p \<and> (pa, SHM_RDWR) \<in> procs_of_shm s h) \<or>
+ (one_flow_shm s h pa pb)
+ else one_flow_shm s h' pa pb )"
+apply (rule ext, rule ext, rule ext, frule vd_cons, frule vt_grant_os)
+by (auto simp add: one_flow_shm_def)
+
+lemma one_flow_shm_detach:
+ "valid (Detach p h # s) \<Longrightarrow> one_flow_shm (Detach p h # s) = (\<lambda> h' pa pb.
+ if (h' = h)
+ then (pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h' pa pb)
+ else one_flow_shm s h' pa pb)"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os)
+by (auto simp:one_flow_shm_def)
+
+lemma one_flow_shm_deleteshm:
+ "valid (DeleteShM p h # s) \<Longrightarrow> one_flow_shm (DeleteShM p h # s) = (\<lambda> h' pa pb.
+ if (h' = h)
+ then False
+ else one_flow_shm s h' pa pb)"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os)
+by (auto simp: one_flow_shm_def)
+
+lemma one_flow_shm_clone:
+ "valid (Clone p p' fds shms # s) \<Longrightarrow> one_flow_shm (Clone p p' fds shms # s) = (\<lambda> h pa pb.
+ if (pa = p' \<and> pb \<noteq> p' \<and> h \<in> shms)
+ then (if (pb = p) then (flag_of_proc_shm s p h = Some SHM_RDWR) else one_flow_shm s h p pb)
+ else if (pb = p' \<and> pa \<noteq> p' \<and> h \<in> shms)
+ then (if (pa = p) then (flag_of_proc_shm s p h = Some SHM_RDWR) else one_flow_shm s h pa p)
+ else one_flow_shm s h pa pb)"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons, clarsimp)
+apply (frule_tac p = p' in procs_of_shm_prop2', simp)
+apply (auto simp:one_flow_shm_def intro:procs_of_shm_prop4 flag_of_proc_shm_prop1)
+done
+
+lemma one_flow_shm_execve:
+ "valid (Execve p f fds # s) \<Longrightarrow> one_flow_shm (Execve p f fds # s) = (\<lambda> h pa pb.
+ pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h pa pb )"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+by (auto simp:one_flow_shm_def)
+
+lemma one_flow_shm_kill:
+ "valid (Kill p p' # s) \<Longrightarrow> one_flow_shm (Kill p p' # s) = (\<lambda> h pa pb.
+ pa \<noteq> p' \<and> pb \<noteq> p' \<and> one_flow_shm s h pa pb )"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+by (auto simp:one_flow_shm_def)
+
+lemma one_flow_shm_exit:
+ "valid (Exit p # s) \<Longrightarrow> one_flow_shm (Exit p # s) = (\<lambda> h pa pb.
+ pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h pa pb )"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+by (auto simp:one_flow_shm_def)
+
+lemma one_flow_shm_other:
+ "\<lbrakk>valid (e # s);
+ \<forall> p h flag. e \<noteq> Attach p h flag;
+ \<forall> p h. e \<noteq> Detach p h;
+ \<forall> p h. e \<noteq> DeleteShM p h;
+ \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
+ \<forall> p f fds. e \<noteq> Execve p f fds;
+ \<forall> p p'. e \<noteq> Kill p p';
+ \<forall> p. e \<noteq> Exit p
+ \<rbrakk> \<Longrightarrow> one_flow_shm (e # s) = one_flow_shm s"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+apply (case_tac e, auto simp:one_flow_shm_def dest:procs_of_shm_prop2)
+apply (drule procs_of_shm_prop1, auto)
+done
+
+lemmas one_flow_shm_simps = one_flow_shm_other one_flow_shm_attach one_flow_shm_detach one_flow_shm_deleteshm
+ one_flow_shm_clone one_flow_shm_execve one_flow_shm_kill one_flow_shm_exit
+
+
+inductive Info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
+where
+ ifs_self: "p \<in> current_procs s \<Longrightarrow> Info_flow_shm s p p"
+| ifs_flow:"\<lbrakk>Info_flow_shm s p p'; one_flow_shm s h p' p''\<rbrakk> \<Longrightarrow> Info_flow_shm s p p''"
+
+lemma Info_flow_trans_aux:
+ "Info_flow_shm s p' p'' \<Longrightarrow> \<forall>p. Info_flow_shm s p p' \<longrightarrow> Info_flow_shm s p p''"
+apply (erule Info_flow_shm.induct)
+by (auto intro:Info_flow_shm.intros)
+
+lemma Info_flow_trans:
+ "\<lbrakk>Info_flow_shm s p p'; Info_flow_shm s p' p''\<rbrakk> \<Longrightarrow> Info_flow_shm s p p''"
+by (auto dest:Info_flow_trans_aux)
+
+lemma one_flow_flows:
+ "\<lbrakk>one_flow_shm s h p p'; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p'"
+apply (rule Info_flow_shm.intros(2), simp_all)
+apply (rule Info_flow_shm.intros(1))
+apply (auto intro:procs_of_shm_prop2 simp:one_flow_shm_def)
+done
+
+lemma ifs_flow': "\<lbrakk>one_flow_shm s h p p'; Info_flow_shm s p' p''; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p''"
+apply (drule one_flow_flows, simp+)
+apply (erule Info_flow_trans, simp+)
+done
+
+lemma Info_flow_shm_cases1:
+ "\<lbrakk>Info_flow_shm s pa pb;
+ \<And>p \<tau>. \<lbrakk>\<tau> = s; pa = p; pb = p; p \<in> current_procs \<tau>\<rbrakk> \<Longrightarrow> P;
+ \<And>\<tau> p p' h p''. \<lbrakk>\<tau> = s; pa = p; pb = p''; Info_flow_shm \<tau> p p'; one_flow_shm \<tau> h p' p''\<rbrakk> \<Longrightarrow> P\<rbrakk>
+ \<Longrightarrow> P"
+by (erule Info_flow_shm.cases, auto)
+
+
+lemma Info_flow_shm_prop1:
+ "\<not> Info_flow_shm s p p \<Longrightarrow> p \<notin> current_procs s"
+by (rule notI, drule Info_flow_shm.intros(1), simp)
+
+lemma Info_flow_shm_intro4:
+ "\<lbrakk>(p, flagb) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p"
+by (drule procs_of_shm_prop2, simp, simp add:Info_flow_shm.intros)
+
+(********* simpset for inductive Info_flow_shm **********)
-lemma info_flow_shm_attach:
- "valid (Attach p h flag # s) \<Longrightarrow> info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb.
- (pa = p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pb, flagb) \<in> procs_of_shm s h)) \<or>
- (pb = p \<and> (pa, SHM_RDWR) \<in> procs_of_shm s h) \<or>
- (info_flow_shm s pa pb) )"
-apply (rule ext, rule ext, frule vt_grant_os)
-by (auto simp add:info_flow_shm_def one_flow_shm_def)
+lemma Info_flow_shm_attach1:
+ "Info_flow_shm s' pa pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow>
+ ((Info_flow_shm s pa pb) \<or>
+ (\<not> Info_flow_shm s pa pb \<and> pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and>
+ (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>
+ (\<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and>
+ (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')))"
+proof (induct rule:Info_flow_shm.induct)
+ case (ifs_self proc \<tau>)
+ show ?case
+ proof (rule impI)
+ assume pre: "valid \<tau> \<and> \<tau> = Attach p h flag # s"
+ hence p1: "p \<in> current_procs s" and p2: "valid s" by (auto intro:vd_cons dest:vt_grant_os)
+ hence p3: "Info_flow_shm s p p" by (auto intro:Info_flow_shm.intros)
+ from ifs_self pre have "proc \<in> current_procs s" by simp
+ hence p4: "Info_flow_shm s proc proc" by (auto intro:Info_flow_shm.intros)
+ show "Info_flow_shm s proc proc \<or>
+ (\<not> Info_flow_shm s proc proc \<and> proc = p \<and> proc \<noteq> p \<and> flag = SHM_RDWR \<and>
+ (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc)) \<or>
+ (\<not> Info_flow_shm s proc proc \<and> proc = p \<and> proc \<noteq> p \<and>
+ (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s proc p'))"
+ using p4 p3 by auto
+ qed
+next
+ case (ifs_flow \<tau> pa pb h' pc)
+ thus ?case
+ proof (rule_tac impI)
+ assume p1:"Info_flow_shm \<tau> pa pb" and p2: "valid \<tau> \<and> (\<tau> = Attach p h flag # s) \<longrightarrow> Info_flow_shm s pa pb \<or>
+ \<not> Info_flow_shm s pa pb \<and> pa = p \<and>
+ pb \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or>
+ \<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and> (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')"
+ and p3: "one_flow_shm \<tau> h' pb pc" and p4: "valid \<tau> \<and> \<tau> = Attach p h flag # s"
+ from p2 and p4 have p2': "Info_flow_shm s pa pb \<or>
+ (\<not> Info_flow_shm s pa pb \<and> pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and>
+ (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>
+ (\<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and>
+ (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'))"
+ by (erule_tac impE, simp)
+ from p4 have p5: "valid s" and p6: "os_grant s (Attach p h flag)" by (auto intro:vd_cons dest:vt_grant_os)
+ from p6 have "p \<in> current_procs s" by simp hence p7:"Info_flow_shm s p p" by (erule_tac Info_flow_shm.intros)
+ from p3 p4 have p8: "if (h' = h)
+ then (pb = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pc, flagb) \<in> procs_of_shm s h)) \<or>
+ (pc = p \<and> pb \<noteq> p \<and> (pb, SHM_RDWR) \<in> procs_of_shm s h) \<or>
+ (one_flow_shm s h pb pc)
+ else one_flow_shm s h' pb pc " by (auto simp add:one_flow_shm_attach)
+
+ have "\<lbrakk>pa = p; pc = p\<rbrakk> \<Longrightarrow> Info_flow_shm s pa pc " using p7 by simp
+ moreover have "\<lbrakk>pa = p; pc \<noteq> p; flag = SHM_RDWR; \<not> Info_flow_shm s pa pc\<rbrakk>
+ \<Longrightarrow> \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc"
+ sorry
+ moreover have "\<lbrakk>pa = p; pc \<noteq> p; flag \<noteq> SHM_RDWR; \<not> Info_flow_shm s pa pc\<rbrakk>
+ \<Longrightarrow> Info_flow_shm s pa pc"
+ sorry
+ moreover have "\<lbrakk>pc = p; pa \<noteq> p; \<not> Info_flow_shm s pa pc\<rbrakk>
+ \<Longrightarrow> \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'"
+ sorry
+ ultimately
+
+
+
+ show "Info_flow_shm s pa pc \<or>
+ (\<not> Info_flow_shm s pa pc \<and> pa = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and>
+ (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc)) \<or>
+ (\<not> Info_flow_shm s pa pc \<and> pc = p \<and> pa \<noteq> p \<and>
+ (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'))"
+ apply auto
+ sorry
+ qed
+qed
+
+lemma Info_flow_shm_intro3:
+ "\<lbrakk>Info_flow_shm s p from; (from, SHM_RDWR) \<in> procs_of_shm s h; (to, flag) \<in> procs_of_shm s h\<rbrakk>
+ \<Longrightarrow> Info_flow_shm s p to"
+apply (case_tac "from = to", simp)
+apply (erule_tac h = h in Info_flow_shm.intros(2), simp add:one_flow_shm_def)
+by (rule_tac x = flag in exI, simp)
+
+lemma Info_flow_shm_attach1:
+ "Info_flow_shm s' pa pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow>
+ (if Info_flow_shm s pa pb then True else
+ (if (pa = p \<and> flag = SHM_RDWR)
+ then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)
+ else if (pb = p)
+ then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')
+ else (\<exists> p' flag'. Info_flow_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and>
+ Info_flow_shm s p' pb) \<or>
+ (\<exists> p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb)
+ ) )"
+proof (induct rule:Info_flow_shm.induct)
+ case (ifs_self proc \<tau>)
+ show ?case
+ proof (rule impI)
+ assume pre: "valid \<tau> \<and> \<tau> = Attach p h flag # s"
+ hence p1: "p \<in> current_procs s" and p2: "valid s" by (auto intro:vd_cons dest:vt_grant_os)
+ hence p3: "Info_flow_shm s p p" by (auto intro:Info_flow_shm.intros)
+ from ifs_self pre have "proc \<in> current_procs s" by simp
+ hence p4: "Info_flow_shm s proc proc" by (auto intro:Info_flow_shm.intros)
+ show "if Info_flow_shm s proc proc then True
+ else if proc = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc
+ else if proc = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s proc p'
+ else (\<exists>p' flag'. Info_flow_shm s proc p \<and>
+ flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc) \<or>
+ (\<exists>p'. Info_flow_shm s proc p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p proc)" using p4 p3 by auto
+ qed
+next
+ case (ifs_flow \<tau> pa pb h' pc)
+ thus ?case
+ proof (rule_tac impI)
+ assume p1:"Info_flow_shm \<tau> pa pb" and p2: "valid \<tau> \<and> \<tau> = Attach p h flag # s \<longrightarrow>
+ (if Info_flow_shm s pa pb then True
+ else if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb
+ else if pb = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'
+ else (\<exists>p' flag'. Info_flow_shm s pa p \<and>
+ flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or>
+ (\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb))"
+ and p3: "one_flow_shm \<tau> h' pb pc" and p4: "valid \<tau> \<and> \<tau> = Attach p h flag # s"
+
+ from p2 and p4 have p2': "(if Info_flow_shm s pa pb then True
+ else if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb
+ else if pb = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'
+ else (\<exists>p' flag'. Info_flow_shm s pa p \<and>
+ flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or>
+ (\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb))"
+ by (erule_tac impE, simp)
+ from p4 have p5: "valid s" and p6: "os_grant s (Attach p h flag)" by (auto intro:vd_cons dest:vt_grant_os)
+ from p6 have "p \<in> current_procs s" by simp hence p7:"Info_flow_shm s p p" by (erule_tac Info_flow_shm.intros)
+ from p3 p4 have p8: "if (h' = h)
+ then (pb = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pc, flagb) \<in> procs_of_shm s h)) \<or>
+ (pc = p \<and> pb \<noteq> p \<and> (pb, SHM_RDWR) \<in> procs_of_shm s h) \<or>
+ (one_flow_shm s h pb pc)
+ else one_flow_shm s h' pb pc " by (auto simp add:one_flow_shm_attach)
+
+ have "\<And> flagb. (pc, flagb) \<in> procs_of_shm s h
+ \<Longrightarrow> \<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc"
+ apply (rule_tac x= pc in exI, rule_tac x = flagb in exI, frule procs_of_shm_prop2)
+ by (simp add:p5, simp add:Info_flow_shm.intros(1))
+ hence p10: "\<not> Info_flow_shm s p pc \<Longrightarrow> (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc) \<or>
+ Info_flow_shm s pa pc"
+ using p2' p7 p8 p5
+ by (auto split:if_splits dest:Info_flow_shm.intros(2))
+ (* apply (rule_tac x = pb in exI, simp add:one_flow_flows, rule_tac x = flagb in exI, simp)+ *)
+ moreover have "pc = p \<Longrightarrow> (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')
+ \<or> Info_flow_shm s pa pc"
+ using p2' p7 p8 p5
+ by (auto split:if_splits intro:Info_flow_shm_intro3 simp:one_flow_shm_def)
+ moreover have "\<lbrakk>pc \<noteq> p; pa \<noteq> p \<or> flag \<noteq> SHM_RDWR\<rbrakk> \<Longrightarrow> (\<exists>p' flag'. Info_flow_shm s pa p \<and>
+ flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc) \<or>
+ (\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pc) \<or>
+ Info_flow_shm s pa pc"
+ using p2' p7 p8 p5
+ apply (auto split:if_splits intro:Info_flow_shm_intro3 simp:one_flow_shm_def)
+ apply (rule_tac x = pc in exI, simp add:Info_flow_shm_intro4)
+ apply (rule_tac x = flagb in exI, simp)
+ done
+ ultimately show "if Info_flow_shm s pa pc then True
+ else if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc
+ else if pc = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'
+ else (\<exists>p' flag'. Info_flow_shm s pa p \<and>
+ flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc) \<or>
+ (\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pc)"
+ using p7 by auto
+ qed
+qed
+
+
+
+
+
+
+
+
+
+
+lemma Info_flow_shm_attach:
+ "valid (Attach p h flag # s) \<Longrightarrow> Info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb.
+ (Info_flow_shm s pa pb) \<or>
+ (pa = p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>
+ (pb = p \<and> (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pa)) )"
+apply (rule ext, rule ext, rule iffI)
+apply (case_tac "Info_flow_shm s pa pb", simp)
+apply (case_tac "pa = p \<and> flag = SHM_RDWR \<and> (\<exists>flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)", simp)
+
+apply (erule Info_flow_shm_cases1, simp, drule_tac p = pc in Info_flow_shm.intros(1), simp)
+apply (simp add:one_flow_shm_simps split:if_splits, erule disjE, simp)
+
+
+
+apply (simp split:if_splits, (rule impI|rule allI|rule conjI|erule conjE|erule exE)+, simp)
+apply (simp)
+apply (simp, erule Info_flow_shm_cases', simp, simp)
+apply (rule_tac x =
+apply (auto dest:Info_flow_shm.cases)
+apply (auto simp add:one_flow_shm_simps)
lemma info_flow_shm_detach:
"valid (Detach p h # s) \<Longrightarrow> info_flow_shm (Detach p h # s) = (\<lambda> pa pb.
--- a/Tainted_prop.thy Mon Jun 24 15:22:37 2013 +0800
+++ b/Tainted_prop.thy Tue Jul 09 14:43:51 2013 +0800
@@ -50,6 +50,12 @@
(if (len > 0 \<and> O_proc p \<in> Tainted s)
then Tainted s \<union> {O_file f' | f'. has_same_inode s f f'}
else Tainted s)"
+| "Tainted (Attach p h flag # s) =
+ (if (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR)
+ then Tainted s \<union> {O_proc p' | p' flag'. (p', flag') \<in> procs_of_shm s h}
+ else if (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h)
+ then Tainted s \<union> {O_proc p}
+ else Tainted s)"
| "Tainted (SendMsg p q m # s) =
(if (O_proc p \<in> Tainted s) then Tainted s \<union> {O_msg q m} else Tainted s)"
| "Tainted (RecvMsg p q m # s) =
@@ -72,7 +78,8 @@
apply (drule seeds_in_init, case_tac obj, simp_all add:is_file_nil)
apply (frule vd_cons, frule valid_Tainted_obj, simp, frule vt_grant_os, case_tac a)
apply (auto simp:alive_simps split:if_splits option.splits t_object.splits
- intro:has_same_inode_prop2 has_same_inode_prop1 dest:info_shm_flow_in_procs)
+ intro:has_same_inode_prop2 has_same_inode_prop1 procs_of_shm_prop2
+ dest:info_shm_flow_in_procs)
done
lemma Tainted_proc_in_current:
@@ -95,12 +102,6 @@
(*?? need simpset for tainted *)
sorry
-lemma info_flow_shm_intro:
- "\<lbrakk>(p, SHM_RDWR) \<in> procs_of_shm s h; (p', flag) \<in> procs_of_shm s h; valid s\<rbrakk>
- \<Longrightarrow> info_flow_shm s p p'"
-apply (rule_tac p = p and p' = p in info_flow_shm.intros(2))
-apply (auto intro!:info_flow_shm.intros(1) procs_of_shm_prop2)
-done
lemma info_flow_shm_Tainted:
"\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s"
@@ -116,17 +117,40 @@
have p4':
"\<And> p p' h flag. \<lbrakk>O_proc p \<in> Tainted s; (p, SHM_RDWR) \<in> procs_of_shm s h; (p', flag) \<in> procs_of_shm s h\<rbrakk>
\<Longrightarrow> O_proc p' \<in> Tainted s"
- by (rule p4, auto intro!:info_flow_shm_intro p5)
+ by (rule p4, auto simp:info_flow_shm_def one_flow_shm_def)
from p2 p3 have p7: "p \<in> current_procs (e # s)" and p8: "p' \<in> current_procs (e # s)"
by (auto dest:info_shm_flow_in_procs)
show ?case
- proof (cases "p = p'")
+ proof (cases "self_shm s p p'")
case True with p1 show ?thesis by simp
next
case False
with p1 p2 p5 p6 p7 p8 p3 show ?thesis
apply (case_tac e)
prefer 7
+ apply (simp add:info_flow_shm_simps split:if_splits option.splits)
+ apply (rule allI|rule impI|rule conjI)+
+ apply simp
+ apply (case_tac "O_proc p \<in> Tainted s", drule_tac p'=p' in p4, simp+)
+ apply simp
+
+
+
+
+ apply (auto simp:info_flow_shm_simps one_flow_shm_def dest:Tainted_in_current
+ intro:p4 p4' split:if_splits option.splits)
+ apply (auto simp:info_flow_shm_def one_flow_shm_def)
+
+
+
+ apply (auto simp:one_flow_shm_def intro:p4 p4' split:if_splits option.splits)
+
+
+
+
+
+
+ prefer 7
apply (simp split:if_splits option.splits)
apply (rule allI|rule impI|rule conjI)+