info_flow_shm is wrongly defined: p -flow-> p'; p' -flow-> p'' ==> p -flow-> p'', this property cannot be infered by current definition. we should use inductive
--- a/Tainted_prop.thy Sun Jun 09 14:28:58 2013 +0800
+++ b/Tainted_prop.thy Sun Jun 16 08:05:37 2013 +0800
@@ -75,25 +75,76 @@
intro:has_same_inode_prop2 has_same_inode_prop1 dest:info_shm_flow_in_procs)
done
+lemma Tainted_proc_in_current:
+ "\<lbrakk>O_proc p \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
+by (drule Tainted_in_current, simp+)
+
+lemma has_inode_tainted_aux:
+ "O_file f \<in> tainted s \<Longrightarrow> \<forall> f'. has_same_inode s f f' \<longrightarrow> O_file f' \<in> tainted s"
+apply (erule tainted.induct)
+apply (auto intro:tainted.intros simp:has_same_inode_def)
+(*?? need simpset for tainted *)
+
+
+sorry
lemma has_inode_Tainted_aux:
- "\<lbrakk>O_file f \<in> tainted s; has_same_inode s f f'\<rbrakk> \<Longrightarrow> O_file f' \<in> tainted s"
-apply (erule tainted.induct)
+ "\<lbrakk>O_file f \<in> Tainted s; has_same_inode s f f'\<rbrakk> \<Longrightarrow> O_file f' \<in> Tainted s"
+apply (induct s, auto)
apply (auto intro:tainted.intros simp:has_same_inode_def)
(*?? need simpset for tainted *)
sorry
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"
-proof (induct s)
+proof (induct s arbitrary:p p')
case Nil
- thus ?case
- apply simp
-apply (induct s)
+ thus ?case by (simp add:flow_shm_in_seeds)
+next
+ case (Cons e s)
+ hence p1: "O_proc p \<in> Tainted (e # s)" and p2: "info_flow_shm (e # s) p p'" and p3: "valid (e # s)"
+ and p4: "\<And> p p'. \<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s"
+ and p5: "valid s" and p6: "os_grant s e"
+ by (auto dest:vd_cons intro:vd_cons vt_grant_os)
+ 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 simp:info_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'")
+ 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_def split:if_splits option.splits)
+ apply (rule allI|rule impI|rule conjI)+
+ apply (erule disjE, drule_tac p = p and p' = p' in p4', simp+)
+ apply (erule disjE, rule disjI2, rule disjI2, rule_tac x = h in exI, simp, rule_tac x= toflag in exI, simp)
+ apply ((erule exE|erule conjE)+)
+
+
+ apply (auto simp:info_flow_shm_def dest:p4'
+ procs_of_shm_prop2 Tainted_in_current split:if_splits option.splits)[1]
+ apply (drule_tac p = p and p' = p' in p4')
+ apply (erule_tac x = ha in allE, simp)
+ apply (drule_tac p = "nat1" and p' = p' in p4')
+ apply (auto dest:p4'[where p = nat1 and p' = p'])
+
+apply (induct s) (*
apply simp defer
apply (frule vd_cons, frule vt_grant_os, case_tac a)
apply (auto simp:info_flow_shm_def elim!:disjE)
-sorry
+sorry *)
+ sorry
+next
+ case (Cons e s)
+ show ?case
+ sorry
+qed
lemma tainted_imp_Tainted:
"obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s"