# HG changeset patch
# User chunhan
# Date 1370332262 -28800
# Node ID 9b42765ce554b6844a379fdb4b6db666620ca9c2
# Parent  570f90f175eec2ef94d5caa1124c42c6976e8ef7
info_flow did NOT guarantee in current_procs

diff -r 570f90f175ee -r 9b42765ce554 Co2sobj_prop.thy
--- a/Co2sobj_prop.thy	Tue Jun 04 15:37:49 2013 +0800
+++ b/Co2sobj_prop.thy	Tue Jun 04 15:51:02 2013 +0800
@@ -852,39 +852,6 @@
 
 (********** cph2spshs simpset **********)
 
-  (*???*) lemma procs_of_shm_prop1: "\<lbrakk> p_flag \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> h \<in> current_shms s"
-apply (induct s arbitrary:p_flag)
-apply (case_tac p_flag, simp, drule init_procs_has_shm, simp)
-apply (frule vd_cons, frule vt_grant_os)
-apply (case_tac a, auto split:if_splits option.splits)
-done
-
-lemma procs_of_shm_prop2: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
-apply (induct s arbitrary:p flag)
-apply (simp, drule init_procs_has_shm, simp)
-apply (frule vd_cons, frule vt_grant_os)
-apply (case_tac a, auto split:if_splits option.splits)
-done
-
-lemma procs_of_shm_prop3: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; (p, flag') \<in> procs_of_shm s h; valid s\<rbrakk>
-  \<Longrightarrow> flag = flag'"
-apply (induct s arbitrary:p flag flag')
-apply (simp, drule_tac flag = flag in init_procs_has_shm, drule_tac flag = flag' in init_procs_has_shm, 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
-
-lemma procs_of_shm_prop4: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> flag_of_proc_shm s p h = Some flag"
-apply (induct s arbitrary:p flag)
-apply (simp, drule init_procs_has_shm, 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
-
-lemma procs_of_shm_prop4':
-  "\<lbrakk>flag_of_proc_shm s p h = None; valid s\<rbrakk> \<Longrightarrow> \<forall> flag. (p, flag) \<notin> procs_of_shm s h"
-by (auto dest:procs_of_shm_prop4)
-
 lemma cph2spshs_attach:
   "valid (Attach p h flag # s) \<Longrightarrow> 
    cph2spshs (Attach p h flag # s) = (cph2spshs s) (p := 
@@ -1102,14 +1069,6 @@
 
 (******** cp2sproc simpset *********)
 
-lemma not_init_intro_proc: (*???*)
-  "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> deleted (O_proc p) s \<or> p \<notin> init_procs"
-using not_deleted_init_proc by auto
-
-lemma not_init_intro_proc': (*???*)
-  "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"
-using not_deleted_init_proc by auto
-
 lemma cp2sproc_clone:
   "valid (Clone p p' fds shms # s) \<Longrightarrow> cp2sproc (Clone p p' fds shms # s) = (cp2sproc s) (p' := 
      case (sectxt_of_obj s (O_proc p)) of 
diff -r 570f90f175ee -r 9b42765ce554 Current_prop.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Current_prop.thy	Tue Jun 04 15:51:02 2013 +0800
@@ -0,0 +1,51 @@
+theory Current_prop
+imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop Delete_prop
+begin
+(*<*)
+
+context flask begin
+
+lemma procs_of_shm_prop1: "\<lbrakk> p_flag \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> h \<in> current_shms s"
+apply (induct s arbitrary:p_flag)
+apply (case_tac p_flag, simp, drule init_procs_has_shm, simp)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a, auto split:if_splits option.splits)
+done
+
+lemma procs_of_shm_prop2: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
+apply (induct s arbitrary:p flag)
+apply (simp, drule init_procs_has_shm, simp)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a, auto split:if_splits option.splits)
+done
+
+lemma procs_of_shm_prop3: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; (p, flag') \<in> procs_of_shm s h; valid s\<rbrakk>
+  \<Longrightarrow> flag = flag'"
+apply (induct s arbitrary:p flag flag')
+apply (simp, drule_tac flag = flag in init_procs_has_shm, drule_tac flag = flag' in init_procs_has_shm, 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
+
+lemma procs_of_shm_prop4: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> flag_of_proc_shm s p h = Some flag"
+apply (induct s arbitrary:p flag)
+apply (simp, drule init_procs_has_shm, 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
+
+lemma procs_of_shm_prop4':
+  "\<lbrakk>flag_of_proc_shm s p h = None; valid s\<rbrakk> \<Longrightarrow> \<forall> flag. (p, flag) \<notin> procs_of_shm s h"
+by (auto dest:procs_of_shm_prop4)
+
+lemma not_init_intro_proc:
+  "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> deleted (O_proc p) s \<or> p \<notin> init_procs"
+using not_deleted_init_proc by auto
+
+lemma not_init_intro_proc':
+  "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"
+using not_deleted_init_proc by auto
+
+end
+
+end
\ No newline at end of file
diff -r 570f90f175ee -r 9b42765ce554 Flask.thy
--- a/Flask.thy	Tue Jun 04 15:37:49 2013 +0800
+++ b/Flask.thy	Tue Jun 04 15:51:02 2013 +0800
@@ -476,7 +476,7 @@
 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
 where
   "info_flow_shm \<tau> from to \<equiv> (from = to) \<or> (\<exists> h \<in> current_shms \<tau>. \<exists> toflag. 
-    (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))"
+    (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))" 
 
 fun current_msgqs :: "t_state \<Rightarrow> t_msg set"
 where
@@ -1428,14 +1428,14 @@
              \<Longrightarrow> O_proc p' \<in> tainted (Clone p p' fds shms # s)"
 | t_execve: "\<lbrakk>O_file f \<in> tainted s; valid (Execve p f fds # s)\<rbrakk> 
              \<Longrightarrow> O_proc p \<in> tainted (Execve p f fds # s)"
-| t_ptrace: "\<lbrakk>O_proc p \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p' p''\<rbrakk>
+| t_ptrace: "\<lbrakk>O_proc p \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p' p''; p'' \<in> current_procs s\<rbrakk>
              \<Longrightarrow> O_proc p'' \<in> tainted (Ptrace p p' # s)"
-| t_ptrace':"\<lbrakk>O_proc p' \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p p''\<rbrakk>
+| t_ptrace':"\<lbrakk>O_proc p' \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p p''; p'' \<in> current_procs s\<rbrakk>
              \<Longrightarrow> O_proc p'' \<in> tainted (Ptrace p p' # s)"
 | t_cfile:  "\<lbrakk>O_proc p \<in> tainted s; valid (Open p f flags fd (Some inum) # s)\<rbrakk>
              \<Longrightarrow> O_file f \<in> tainted (Open p f flags fd (Some inum) # s)"
 | t_read:   "\<lbrakk>O_file f \<in> tainted s; valid (ReadFile p fd # s); 
-              file_of_proc_fd s p fd = Some f; info_flow_shm s p p'\<rbrakk> 
+              file_of_proc_fd s p fd = Some f; info_flow_shm s p p'; p' \<in> current_procs s\<rbrakk> 
              \<Longrightarrow> O_proc p' \<in> tainted (ReadFile p fd # s)"
 | t_write:  "\<lbrakk>O_proc p \<in> tainted s; valid (WriteFile p fd # s);
               file_of_proc_fd s p fd = Some f; has_same_inode s f f'\<rbrakk> 
@@ -1456,7 +1456,7 @@
 *)
 | t_sendmsg:"\<lbrakk>O_proc p \<in> tainted s; valid (SendMsg p q m # s)\<rbrakk>
              \<Longrightarrow> O_msg q m \<in> tainted (SendMsg p q m # s)"
-| t_recvmsg:"\<lbrakk>O_msg q m \<in> tainted s; valid (RecvMsg p q m # s); info_flow_shm s p p'\<rbrakk>
+| t_recvmsg:"\<lbrakk>O_msg q m \<in> tainted s; valid (RecvMsg p q m # s); info_flow_shm s p p'; p' \<in> current_procs s\<rbrakk>
              \<Longrightarrow> O_proc p' \<in> tainted (RecvMsg p q m # s)"
 | t_remain: "\<lbrakk>obj \<in> tainted s; valid (e # s); alive (e # s) obj\<rbrakk> 
              \<Longrightarrow> obj \<in> tainted (e # s)"
diff -r 570f90f175ee -r 9b42765ce554 Tainted_prop.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Tainted_prop.thy	Tue Jun 04 15:51:02 2013 +0800
@@ -0,0 +1,20 @@
+theory Tainted_prop 
+imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop
+begin
+
+context tainting begin
+
+lemma tainted_in_current:
+  "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj"
+apply (erule tainted.induct, auto dest:vt_grant_os simp:is_file_simps)
+
+
+
+
+end
+
+end
+
+
+
+