# HG changeset patch
# User chunhan
# Date 1371341137 -28800
# Node ID 566b0d1c3669002e01901938a4f91c75afc7af00
# Parent  25e55731ed01ef19dd097e916a9eb4a2c5e05c4b
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

diff -r 25e55731ed01 -r 566b0d1c3669 Tainted_prop.thy
--- 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"