--- a/no_shm_selinux/Enrich.thy	Thu Jan 09 19:09:09 2014 +0800
+++ b/no_shm_selinux/Enrich.thy	Thu Jan 09 22:53:45 2014 +0800
@@ -7,6 +7,7 @@
 datatype t_enrich_obj = 
   E_proc "t_process" "t_msgq" "t_msgq"
 | E_file "t_file" "nat" 
+| E_file_link "t_file"
 | E_msgq "t_msgq"
 
 (* objects that need dynamic indexing, all nature-numbers *)

--- a/no_shm_selinux/Enrich2.thy	Thu Jan 09 19:09:09 2014 +0800
+++ b/no_shm_selinux/Enrich2.thy	Thu Jan 09 22:53:45 2014 +0800
@@ -5,12 +5,37 @@
 
 context tainting_s begin
 
-fun enrich_file :: "t_state \<Rightarrow> t_file \<Rightarrow> t_state \<Rightarrow> (t_file set \<times> t_state)"
+fun new_cf :: "t_state \<Rightarrow> t_file set \<Rightarrow> t_file \<Rightarrow> t_file"
+where
+  "new_cf s fs []     = []"
+| "new_cf s fs (f#pf) = new_childf_general pf s fs"
+
+fun enrich_dufs:: "t_state \<Rightarrow> t_file \<Rightarrow> t_state \<Rightarrow> (t_file \<times> t_file) list"
 where
-  "enrich_file [] tf s = ({}, [])"
-| "enrich_file (Open p f flags fd (Some inum) # s) tf s =
-  "
-    
+  "enrich_dufs [] tf s = []"
+| "enrich_dufs (Open p f flags fd (Some inum) # s) tf s' = 
+    (if (f \<in> same_inode_files s' tf) 
+     then [(f, new_cf s' {} f)]
+     else enrich_dufs s tf s')"
+| "enrich_dufs (LinkHard p f f' # s) tf s' = 
+    (if (f' \<in> same_inode_files s' tf) 
+     then (f', new_cf s' (set (map snd (enrich_dufs s tf s'))) f') # enrich_dufs s tf s'
+     else enrich_dufs s tf s')"
+| "enrich_dufs (_ # s) tf s' = enrich_dufs s tf s'"
+
+lemma enrich_dufs_sameinodes:
+  "valid s \<Longrightarrow> set (map snd (enrich_dufs s f s)) = same_inode_files s f"
+thm enrich_dufs.induct
+apply (induct rule:enrich_dufs.induct)
+
+apply (erule enrich_dufs.induct)
+
+fun enrich_file :: "t_state \<Rightarrow> t_file \<Rightarrow> t_inode_num \<Rightarrow> t_state \<Rightarrow> (t_file set \<times> t_state)"
+where
+  "enrich_file [] tf ninum s = ({}, [])"
+| "enrich_file (Open p f flags fd (Some inum) # s) tf ninum s = 
+     if (f \<in> same_inode_fies s tf)
+     then Open p f flags fd (Some"
 
 
 

--- a/no_shm_selinux/New_obj_prop.thy	Thu Jan 09 19:09:09 2014 +0800
+++ b/no_shm_selinux/New_obj_prop.thy	Thu Jan 09 22:53:45 2014 +0800
@@ -83,13 +83,12 @@
 done
 
 lemma ncf_notin_curf_general:
-  assumes vd: "valid \<tau>" and fin_fs: "finite fs"
-  shows "new_childf_general f \<tau> fs \<notin> (current_files \<tau> \<union> fs)"
+  assumes fin_fs: "finite fs"
+  shows "new_childf_general f fs \<notin> fs"
 proof-
-  from vd fin_fs have "finite (current_files \<tau> \<union> fs)"
-    by (auto dest:finite_cf)
-  hence a1: "Suc (Max (fname_length_set {fn. fn # f \<in> (current_files \<tau> \<union> fs)})) \<notin> 
-    fname_length_set {fn. fn # f \<in> (current_files \<tau> \<union> fs)}"
+  have a1: "Suc (Max (fname_length_set {fn. fn # f \<in> fs})) \<notin> 
+    fname_length_set {fn. fn # f \<in> fs}"
+    using fin_fs
     by (erule_tac ncf_notin_curf_aux)
   have a2: "\<And> f pf fs. f # pf \<in> fs \<Longrightarrow> f \<in> {fn. fn # pf \<in> fs}" by auto
   have a3: "\<And> f pf fs. f \<in> {fn. fn # pf \<in> fs} \<Longrightarrow> length f \<in> fname_length_set {fn. fn # pf \<in> fs}"
@@ -104,12 +103,12 @@
   
 lemma ncf_notin_curf:
  "valid \<tau> \<Longrightarrow> new_childf f \<tau> \<notin> (current_files \<tau>)"
-apply (drule_tac fs = "{}" in ncf_notin_curf_general)
-apply (simp)
+apply (drule finite_cf)
+apply (drule_tac fs = "current_files \<tau>" in ncf_notin_curf_general)
 apply (simp add:new_childf_def)
 done
 
-lemma ncf_parent_general: "valid \<tau> \<Longrightarrow> parent (new_childf_general f \<tau> fs) = Some f"
+lemma ncf_parent_general: "valid \<tau> \<Longrightarrow> parent (new_childf_general f fs) = Some f"
 by (simp add:new_childf_general_def)
 
 lemma ncf_parent: "valid \<tau> \<Longrightarrow> parent (new_childf f \<tau>) = Some f"

--- a/no_shm_selinux/Static.thy	Thu Jan 09 19:09:09 2014 +0800
+++ b/no_shm_selinux/Static.thy	Thu Jan 09 22:53:45 2014 +0800
@@ -702,9 +702,9 @@
 where
   "new_proc_fd \<tau> p = next_nat (current_proc_fds \<tau> p)"
 
-definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file set \<Rightarrow> t_fname set"
+definition all_fname_under_dir:: "t_file \<Rightarrow> t_file set \<Rightarrow> t_fname set"
 where
-  "all_fname_under_dir d \<tau> fs = {fn. \<exists> f. fn # d = f \<and> f \<in> (current_files \<tau> \<union> fs)}"
+  "all_fname_under_dir d fs = {fn. fn # d \<in> fs}"
 
 fun fname_all_a:: "nat \<Rightarrow> t_fname"
 where
@@ -715,17 +715,17 @@
 where
   "fname_length_set fns = length`fns"
 
-definition next_fname:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file set \<Rightarrow> t_fname"
+definition next_fname:: "t_file \<Rightarrow> t_file set \<Rightarrow> t_fname"
 where
-  "next_fname pf \<tau> fs = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf \<tau> fs))) + 1)"
+  "next_fname pf fs = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf fs))) + 1)"
 
-definition new_childf_general:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file set \<Rightarrow> t_file"
+definition new_childf_general:: "t_file \<Rightarrow> t_file set \<Rightarrow> t_file"
 where
-  "new_childf_general pf \<tau> fs = next_fname pf \<tau> fs # pf"
+  "new_childf_general pf fs = next_fname pf fs # pf"
 
 definition new_childf:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file"
 where
-  "new_childf pf \<tau> = new_childf_general pf \<tau> {}"
+  "new_childf pf \<tau> = new_childf_general pf (current_files \<tau>)"
 
 end