--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/no_shm_selinux/Tainted_prop.thy	Tue Dec 17 13:30:21 2013 +0800
@@ -0,0 +1,186 @@
+theory Tainted_prop 
+imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop Alive_prop
+begin
+
+ML {*quick_and_dirty := true*}
+
+context tainting begin
+
+lemma valid_tainted_obj:
+  "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> (\<forall> f. obj \<noteq> O_dir f) \<and> (\<forall> q. obj \<noteq> O_msgq q) \<and> (\<forall> p fd. obj \<noteq> O_fd p fd) \<and> (\<forall> s. obj \<noteq> O_tcp_sock s) \<and> (\<forall> s. obj \<noteq> O_udp_sock s)" (*(\<forall> h. obj \<noteq> O_shm h) \<and>*)
+apply (induct s, simp)
+apply (drule seeds_appropriate, case_tac obj, simp+)
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto split:if_splits option.splits)
+done
+
+lemma dir_not_tainted: "\<lbrakk>O_dir f \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> False"
+by (auto dest!:valid_tainted_obj)
+
+lemma msgq_not_tainted: "\<lbrakk>O_msgq q \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> False"
+by (auto dest:valid_tainted_obj)
+
+lemma tainted_in_current:
+  "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj"
+apply (induct s, simp)
+apply (drule seeds_appropriate, 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:same_inode_files_prop1 (*procs_of_shm_prop2 
+            dest:info_shm_flow_in_procs *))
+apply (auto simp:same_inode_files_def is_file_def split:if_splits)
+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 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 arbitrary:p p')
+  case Nil
+  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 one_flow_shm_def procs_of_shm_prop2 p5)    
+  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 "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)+
+
+
+    apply (auto dest:p4'   procs_of_shm_prop2 tainted_in_current split:if_splits option.splits)[1]
+
+    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
+qed
+qed
+*)
+
+lemma has_same_inode_comm:
+  "has_same_inode s f f' = has_same_inode s f' f"
+by (auto simp add:has_same_inode_def same_inode_files_def is_file_def)
+
+(*
+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"
+by (simp only:tainted_eq_tainted info_flow_shm_tainted)
+*)
+
+lemma same_inode_files_tainted:
+  "\<lbrakk>O_file f \<in> tainted s; f' \<in> same_inode_files s f; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> tainted s"
+apply (induct s arbitrary:f f', simp add:same_inode_in_seeds has_same_inode_def)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+prefer 6
+apply (simp split:if_splits option.splits add:same_inode_files_open current_files_simps)
+prefer 8
+apply (frule tainted_in_current, simp, simp add:alive.simps, drule is_file_in_current)
+apply (auto simp add:same_inode_files_closefd split:option.splits if_splits)[1]
+prefer 8
+apply (frule tainted_in_current, simp, simp add:alive.simps, drule is_file_in_current)
+apply (auto simp add:same_inode_files_unlink split:option.splits if_splits)[1]
+prefer 10
+apply (auto split:if_splits option.splits simp:same_inode_files_linkhard current_files_simps)[1]
+apply (drule tainted_in_current, simp, simp add:alive.simps is_file_in_current)
+apply (drule same_inode_files_prop5, simp)
+apply (drule same_inode_files_prop5, drule_tac f' = list1 and f'' = f' in same_inode_files_prop4, simp, simp)
+
+apply (auto simp:same_inode_files_other split:if_splits)
+apply (drule_tac f'' = f' and f' = f and f = fa in same_inode_files_prop4, simp+)
+apply (drule_tac f'' = f' and f' = f and f = list in same_inode_files_prop4, simp+)
+done
+
+lemma has_same_inode_tainted:
+  "\<lbrakk>O_file f \<in> tainted s; has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> tainted s"
+by (simp add:has_same_inode_def same_inode_files_tainted)
+
+lemma same_inodes_tainted:
+  "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> (O_file f \<in> tainted s) = (O_file f' \<in> tainted s)"
+apply (frule same_inode_files_prop8, frule same_inode_files_prop7)
+apply (auto intro:has_same_inode_tainted)
+done
+
+lemma t_remain: "\<lbrakk>obj \<in> tainted s; valid (e # s); alive (e # s) obj\<rbrakk> 
+             \<Longrightarrow> obj \<in> tainted (e # s)"
+apply (frule vd_cons, frule vt_grant_os, case_tac e)
+apply (auto simp:alive_simps split:option.splits if_splits)
+done
+
+lemma not_exited_cons:
+  "\<not> exited obj (e # s) \<Longrightarrow> \<not> exited obj s"
+apply (case_tac e, case_tac [!] obj)
+by (auto)
+
+lemma t_remain_app:
+  "\<lbrakk>obj \<in> tainted s; \<not> died obj (s' @ s); valid (s' @ s)\<rbrakk> 
+  \<Longrightarrow> obj \<in> tainted (s' @ s)"
+apply (induct s', simp)
+apply (simp (no_asm) only:cons_app_simp_aux, rule t_remain)
+apply (simp_all add:not_died_cons_D vd_cons) 
+apply (frule tainted_in_current)
+apply (simp add:vd_cons)
+apply (drule valid_tainted_obj, simp add:vd_cons) 
+apply (case_tac a, auto simp:alive_simps split:t_object.splits option.splits)
+done
+
+lemma t_remain_app_deleted:
+  "\<lbrakk>obj \<in> tainted s; \<not> deleted obj (s' @ s); appropriate obj; \<not> exited obj (s' @ s); valid (s' @ s)\<rbrakk>
+   \<Longrightarrow> obj \<in> tainted (s' @ s)"
+apply (rule t_remain_app, simp_all add:deleted_died)
+done
+
+end
+
+end
\ No newline at end of file