# HG changeset patch
# User chunhan
# Date 1388418118 -28800
# Node ID 690636b7b6f1f82212a90ba1a17f4a53a0c9048b
# Parent  1d1aa5bdd37d3af193768687da6e8a16c3c73f28
find bug: a created proc can be tainted by a message, which cannot remain and maynot be duplicated

diff -r 1d1aa5bdd37d -r 690636b7b6f1 no_shm_selinux/Enrich2.thy
--- a/no_shm_selinux/Enrich2.thy	Mon Dec 30 14:04:23 2013 +0800
+++ b/no_shm_selinux/Enrich2.thy	Mon Dec 30 23:41:58 2013 +0800
@@ -256,22 +256,23 @@
      (cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and>
      (\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd)"
     using vd all_procs nodel by auto
+  
+  from pre have pre_vd: "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p')" by simp
+  have vd_enrich:"is_created_proc s p \<Longrightarrow> valid (e # enrich_proc s p p')" 
+    apply (frule pre_vd)
+    apply (erule_tac s = s and obj' = "E_proc p'" in enrich_valid_intro_cons)
+    apply (simp_all add: pre nodel_cons all_procs_cons vd_cons')
+    apply (clarsimp simp:enrich_proc_alive nodel all_procs vd)
+    apply (rule allI, rule impI, erule enrich_proc_not_alive)
+    apply (simp_all add:nodel all_procs vd enrich_proc_hungs enrich_proc_cur_msgs)
+    apply ((rule allI| rule impI)+, erule enrich_proc_filefd)
+    apply (simp_all add:nodel all_procs vd)
+    apply ((rule allI| rule impI)+, erule enrich_proc_flagfd)
+    apply (simp_all add:nodel all_procs vd)
+    done  
   have vd_enrich_cons: "valid (enrich_proc (e # s) p p')"
   proof-
-    from pre have pre': "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p')" by simp
-    have "is_created_proc s p \<Longrightarrow> valid (e # enrich_proc s p p')" 
-      apply (frule pre')
-      apply (erule_tac s = s and obj' = "E_proc p'" in enrich_valid_intro_cons)
-      apply (simp_all add: pre nodel_cons all_procs_cons vd_cons')
-      apply (clarsimp simp:enrich_proc_alive nodel all_procs vd)
-      apply (rule allI, rule impI, erule enrich_proc_not_alive)
-      apply (simp_all add:nodel all_procs vd enrich_proc_hungs enrich_proc_cur_msgs)
-      apply ((rule allI| rule impI)+, erule enrich_proc_filefd)
-      apply (simp_all add:nodel all_procs vd)
-      apply ((rule allI| rule impI)+, erule enrich_proc_flagfd)
-      apply (simp_all add:nodel all_procs vd)
-      done
-    moreover have "\<And>f fds. \<lbrakk>valid (Execve p f fds # enrich_proc s p p'); is_created_proc s p; 
+    have "\<And>f fds. \<lbrakk>valid (Execve p f fds # enrich_proc s p p'); is_created_proc s p; 
       valid (Execve p f fds # s); p' \<notin> all_procs s\<rbrakk>
       \<Longrightarrow> valid (Execve p' f (fds \<inter> proc_file_fds s p) # Execve p f fds # enrich_proc s p p')"
     proof-
@@ -517,6 +518,7 @@
             apply (erule_tac search_check_leveling_f)
             apply (simp_all)
             apply (simp add:search_check_file_def)
+            (* create new file, grant only check pf's SEARCH permission, not newfile itself, so we make assumptions of this case in the locale *)
             apply (simp add:permission_check.simps)
             sorry
         qed
@@ -543,7 +545,7 @@
         using a2 a3 vd
         by (auto intro:enrich_proc_dup_in)
       moreover have "fd \<in> current_proc_fds (enrich_proc s p p') p'"      
-        using a5 a2 a3 vd pre' nodel
+        using a5 a2 a3 vd pre_vd nodel
         apply (simp)
         apply (drule_tac s = "enrich_proc s p p'" and p = p' in file_fds_subset_pfds)
         apply (erule set_mp)
@@ -551,7 +553,7 @@
         done
       ultimately show "valid (CloseFd p' fd # CloseFd p fd # enrich_proc s p p')"
         apply (rule_tac valid.intros(2))
-        apply (simp_all add:a1 a0 a2 pre')
+        apply (simp_all add:a1 a0 a2 pre_vd)
         done
     qed
     moreover have "\<And> fd. \<lbrakk>valid (ReadFile p fd # enrich_proc s p p');
@@ -643,11 +645,18 @@
       qed
     qed
     ultimately show ?thesis 
-      using created_cons vd_cons' all_procs_cons
+      using vd_enrich created_cons vd_cons' all_procs_cons
       apply (case_tac e)
       apply (auto simp:is_created_proc_simps split:if_splits)
       done
   qed
+  have sec_proc:
+    "\<And> tp. \<lbrakk>tp \<in> current_procs s; is_created_proc s p\<rbrakk> 
+    \<Longrightarrow> sectxt_of_obj (enrich_proc s p p') (O_proc tp) = sectxt_of_obj s (O_proc tp)"
+    using pre 
+    apply (clarsimp)
+    apply (erule_tac x = tp in allE, auto simp:cp2sproc_def split:option.splits)
+    done
   have sf_cons:
     "\<forall>f. f \<in> current_files (e # s) \<longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
   proof clarify
@@ -659,18 +668,251 @@
     from a1 have a1': "f \<in> current_files (enrich_proc (e # s) p p')"
       using vd_cons' nodel_cons
       by (simp add:enrich_proc_cur_files)
+    from a1 have a1'': "f \<in> current_files (e # enrich_proc s p p')"
+      using vd_cons' nodel_cons os vd vd_enrich created_cons
+      apply (case_tac e)
+      apply (auto simp:enrich_proc_cur_files current_files_simps is_created_proc_simps
+        dest:is_file_in_current is_dir_in_current split:option.splits)
+      done
+    
+    have sec_dir:
+      "\<And> tf. \<lbrakk>is_dir s tf; is_created_proc s p\<rbrakk>
+      \<Longrightarrow> sectxt_of_obj (enrich_proc s p p') (O_dir tf) = sectxt_of_obj s (O_dir tf)"
+    proof-
+      fix tf 
+      assume a1: "is_dir s tf" and a2: "is_created_proc s p"
+      from a2 pre
+      have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f"
+        and vd_enrich: "valid (enrich_proc s p p')"
+        by auto
+      hence csf: "cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
+        using a1 by (auto simp:is_dir_in_current)
+      from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf"
+        apply (case_tac "cf2sfile s tf")
+        apply (drule current_file_has_sfile')
+        apply (simp add:vd, simp add:is_dir_in_current, simp)
+        done      
+      from a1 have a1': "is_dir (enrich_proc s p p') tf"
+        using enrich_proc_is_dir vd nodel all_procs by simp
+      from a1 have a3: "\<not> is_file s tf" using vd by (simp add:is_dir_not_file)
+      from a1' vd have a3': "\<not> is_file (enrich_proc s p p') tf" by (simp add:is_dir_not_file)  
+      show "sectxt_of_obj (enrich_proc s p p') (O_dir tf) = sectxt_of_obj s (O_dir tf)"
+        using csf csf_some a3 a3' vd_enrich vd
+        apply (auto simp:cf2sfile_def split:option.splits)
+        apply (case_tac tf)
+        apply (simp add:root_sec_remains, simp)
+        done
+    qed
+    have sec_file:
+      "\<And> tf. \<lbrakk>is_file s tf; is_created_proc s p\<rbrakk>
+      \<Longrightarrow> sectxt_of_obj (enrich_proc s p p') (O_file tf) = sectxt_of_obj s (O_file tf)"
+    proof-
+      fix tf 
+      assume a1: "is_file s tf" and a2: "is_created_proc s p"
+      from a2 pre
+      have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f"
+        and vd_enrich: "valid (enrich_proc s p p')"
+        by auto
+      hence csf: "cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
+        using a1 by (auto simp:is_file_in_current)
+      from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf"
+        apply (case_tac "cf2sfile s tf")
+        apply (drule current_file_has_sfile')
+        apply (simp add:vd, simp add:is_file_in_current, simp)
+        done
+      from a1 have a1': "is_file (enrich_proc s p p') tf"
+        using vd nodel all_procs by (simp add:enrich_proc_is_file)
+      show "sectxt_of_obj (enrich_proc s p p') (O_file tf) = sectxt_of_obj s (O_file tf)"
+        using csf csf_some vd_enrich vd a1 a1'
+        apply (auto simp:cf2sfile_def split:option.splits if_splits)
+        apply (case_tac tf, simp_all)
+        apply (drule root_is_dir', simp+)
+        done
+    qed
+    have secs_dir:
+      "\<And> tf ctxts'. \<lbrakk>is_dir s tf; is_created_proc s p; get_parentfs_ctxts s tf = Some ctxts'\<rbrakk>
+       \<Longrightarrow> \<exists> ctxts. get_parentfs_ctxts (enrich_proc s p p') tf = Some ctxts \<and> set ctxts = set ctxts'"
+    proof-
+      fix tf ctxts'
+      assume a1: "is_dir s tf" and a2: "is_created_proc s p" 
+        and a4: "get_parentfs_ctxts s tf = Some ctxts'"
+      from a2 pre
+      have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f"
+        and vd_enrich': "valid (enrich_proc s p p')"
+        by auto
+      hence csf: "cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
+        using a1 by (auto simp:is_dir_in_current)
+      from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf"
+        apply (case_tac "cf2sfile s tf")
+        apply (drule current_file_has_sfile')
+        apply (simp add:vd, simp add:is_dir_in_current, simp)
+        done      
+      from a1 have a1': "is_dir (enrich_proc s p p') tf"
+        using enrich_proc_is_dir vd nodel all_procs by simp
+      from a1 have a5: "\<not> is_file s tf" using vd by (simp add:is_dir_not_file)
+      from a1' vd have a5': "\<not> is_file (enrich_proc s p p') tf" by (simp add:is_dir_not_file) 
       
+      from a1' pre_vd a2 obtain ctxts 
+        where a3: "get_parentfs_ctxts (enrich_proc s p p') tf = Some ctxts"
+        apply (case_tac "get_parentfs_ctxts (enrich_proc s p p') tf")
+        apply (drule get_pfs_secs_prop', simp+)
+        done
+      moreover have "set ctxts = set ctxts'"
+      proof (cases tf)
+        case Nil          
+        with a3 a4 vd vd_enrich'
+        show ?thesis
+          by (simp add:get_parentfs_ctxts.simps root_sec_remains split:option.splits)
+      next
+        case (Cons a ff)
+        with csf csf_some a5 a5' vd_enrich' vd a3 a4
+        show ?thesis
+          apply (auto simp:cf2sfile_def split:option.splits if_splits)
+          done
+      qed
+      ultimately 
+      show "\<exists> ctxts. get_parentfs_ctxts (enrich_proc s p p') tf = Some ctxts \<and> set ctxts = set ctxts'"
+        by auto        
+    qed
+    have b1: "\<And> proc f' flags fd' opt. e = Open proc f' flags fd' opt 
+      \<Longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
+    proof-
+      fix proc f' flags fd' opt
+      assume ev: "e = Open proc f' flags fd' opt"
+      have b1': "cf2sfile (e # enrich_proc s p p') f = cf2sfile (e # s) f"
+      proof (cases opt)
+        case None
+        thus ?thesis
+          using vd_cons' vd_enrich a1 created_cons 
+          by (simp add:cf2sfile_open_none ev pre_sf 
+            is_created_proc_simps current_files_simps)
+      next
+        case (Some inum)
+        show ?thesis
+        proof (cases "f' = f")
+          case True
+          from a1 obtain sf where csf: "cf2sfile (e # s) f = Some sf"
+            apply (case_tac "cf2sfile (e # s) f")
+            apply (drule current_file_has_sfile')
+            apply (simp add:vd_cons', simp, simp)
+            done
+          from a1 ev os Some True obtain pf where parent: "parent f = Some pf"
+            and pdir: "is_dir s pf" and proc_in: "proc \<in> current_procs s" by auto
+          have f_in: "f \<in> current_files (e # enrich_proc s p p')"
+            using ev True Some
+            by (simp add:current_files_open)
+          thus ?thesis using ev Some csf vd_enrich True created_cons vd_cons' a1 parent pdir proc_in
+            apply (simp add:is_created_proc_simps cf2sfile_open)
+            apply (simp add:sectxt_of_obj_simps sec_dir sec_proc split:option.splits)
+            apply (drule_tac tf = pf in secs_dir, simp+) 
+            apply (erule exE, erule conjE, simp)
+            apply (case_tac aa, simp)
+            done
+        next
+          case False
+          have f_in: "f \<in> current_files (e # enrich_proc s p p')"
+            using ev False Some vd_enrich a1 created_cons nodel vd
+            by (simp add:current_files_open is_created_proc_simps enrich_proc_cur_files)
+          with ev Some a1 vd_enrich vd_cons' created_cons False
+          show ?thesis
+            apply (simp add:is_created_proc_simps cf2sfile_open)
+            apply (simp add:current_files_simps pre_sf)
+            done
+        qed
+      qed
+      show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f" 
+        using ev vd_enrich_cons
+        apply simp
+        apply (rule conjI, rule impI)
+        apply (simp add:cf2sfile_open_none)
+        using b1' apply (auto dest:vd_cons)
+        done
+    qed
+    have b2: "\<And> proc f' inum. e = Mkdir proc f' inum
+      \<Longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
+    proof-
+      fix proc f' inum
+      assume ev: "e = Mkdir proc f' inum"
+      
+      show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
+      proof (cases "f' = f")
+        case True
+        from a1 obtain sf where csf: "cf2sfile (e # s) f = Some sf"
+          apply (case_tac "cf2sfile (e # s) f")
+          apply (drule current_file_has_sfile')
+          apply (simp add:vd_cons', simp, simp)
+          done
+        from a1 ev os True obtain pf where parent: "parent f = Some pf"
+          and pdir: "is_dir s pf" and proc_in: "proc \<in> current_procs s" by auto
+        have f_in: "f \<in> current_files (e # enrich_proc s p p')"
+          using ev True
+          by (simp add:current_files_mkdir)
+        thus ?thesis using ev csf vd_enrich True created_cons vd_cons' a1 parent pdir proc_in
+          apply (simp add:is_created_proc_simps cf2sfile_mkdir)
+          apply (simp add:sectxt_of_obj_simps sec_dir sec_proc split:option.splits)
+          apply (drule_tac tf = pf in secs_dir, simp+) 
+          apply (erule exE, erule conjE, simp)
+          apply (case_tac aa, simp)
+          done
+      next
+        case False
+        have f_in: "f \<in> current_files (e # enrich_proc s p p')"
+          using ev False vd_enrich a1 created_cons nodel vd
+          by (simp add:current_files_mkdir is_created_proc_simps enrich_proc_cur_files)
+        with ev a1 vd_enrich vd_cons' created_cons False
+        show ?thesis
+          apply (simp add:is_created_proc_simps cf2sfile_mkdir)
+          apply (simp add:current_files_simps pre_sf)
+          done
+      qed
+    qed
+    have b3: "\<And> proc f' f''. e = LinkHard proc f' f''
+      \<Longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
+    proof-
+      fix proc f' f'' 
+      assume ev: "e = LinkHard proc f' f''"      
+      show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
+      proof (cases "f'' = f")
+        case True
+        from a1 obtain sf where csf: "cf2sfile (e # s) f = Some sf"
+          apply (case_tac "cf2sfile (e # s) f")
+          apply (drule current_file_has_sfile')
+          apply (simp add:vd_cons', simp, simp)
+          done
+        from a1 ev os True obtain pf where parent: "parent f'' = Some pf"
+          and pdir: "is_dir s pf" and proc_in: "proc \<in> current_procs s" by auto
+        have f_in: "f \<in> current_files (e # enrich_proc s p p')"
+          using ev True vd_enrich created_cons
+          by (simp add:current_files_simps is_created_proc_simps)
+        thus ?thesis using ev csf vd_enrich True created_cons vd_cons' a1 parent pdir proc_in
+          apply (simp add:is_created_proc_simps cf2sfile_linkhard)
+          apply (simp add:sectxt_of_obj_simps sec_dir sec_proc split:option.splits)
+          apply (drule_tac tf = pf in secs_dir, simp+) 
+          apply (erule exE, erule conjE, simp)
+          apply (case_tac aa, simp)
+          done
+      next
+        case False
+        have f_in: "f \<in> current_files (e # enrich_proc s p p')"
+          using ev False vd_enrich a1 created_cons nodel vd vd_cons'
+          by (simp add:current_files_linkhard is_created_proc_simps enrich_proc_cur_files)
+        with ev a1 vd_enrich vd_cons' created_cons False
+        show ?thesis
+          apply (simp add:is_created_proc_simps cf2sfile_linkhard)
+          apply (simp add:current_files_simps pre_sf)
+          done
+      qed      
+    qed
     show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
-        apply (case_tac e)
-        using vd created_cons nodel_cons vd_enrich_cons vd_cons' a1 a1'
-        apply (auto intro!:pre_sf simp:cf2sfile_simps is_created_proc_simps 
-          split:if_splits dest:vd_cons)
-        thm cf2sfile_other
-        apply (simp_all)
-        done
-      
-    
-    sorry
+      apply (case_tac e) 
+      prefer 6 apply (erule b1)
+      prefer 11 apply (erule b2)
+      prefer 11 apply (erule b3)
+      using vd created_cons nodel_cons vd_enrich_cons vd_cons' a1 a1'
+      apply (auto intro!:pre_sf simp:cf2sfile_simps is_created_proc_simps current_files_simps
+        split:if_splits dest:vd_cons cf2sfile_other')
+      done
+  qed
   moreover have "\<forall>tp fd. fd \<in> proc_file_fds (e # s) tp \<longrightarrow> 
     cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
   proof clarify
@@ -799,9 +1041,26 @@
         done
     qed
   qed
-  moreover have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_proc (e # s) p p') tp = cp2sproc (e # s) tp"
+  moreover have "\<forall>q. q \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q"
+  proof clarify
+    fix q
+    assume a1: "q \<in> current_msgqs (e # s)"
+    from pre have pre_smsgq: "\<And> q. \<lbrakk>q \<in> current_msgqs s; is_created_proc s p\<rbrakk>
+      \<Longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q"
+      by auto 
+    show "cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q"
+      using vd_enrich_cons a1 created_cons nodel_cons vd_cons' os
+      apply (case_tac e) 
+      apply (auto simp:cq2smsgq_simps cq2smsg_createmsgq is_created_proc_simps sec_proc 
+        dest:cq2smsgq_other intro!:pre_smsgq split:if_splits dest:vd_cons)
+      
+      apply (simp add:sectxt_of_obj_simps split:option.splits)
+      
+      thm sec_proc
+      thm cq2smsgq_simps
+      thm cq2smsg_createmsgq
     sorry
-  moreover have "\<forall>q. q \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q"
+  moreover have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_proc (e # s) p p') tp = cp2sproc (e # s) tp"
     sorry
   moreover have "cp2sproc (enrich_proc (e # s) p p') p' = cp2sproc (e # s) p"
   proof-