# HG changeset patch
# User chunhan
# Date 1368588099 -28800
# Node ID 8779d321cc2e9a21d59dc71f6bc04887c7a99d2a
# Parent  0c209a3e2647804ed2aeb5d5088f4b7e4cfb0ae2
remove duplicated pre-condition of current_files in OS_grant, since it is property if is_file/is_dir.

diff -r 0c209a3e2647 -r 8779d321cc2e Co2sobj_prop.thy
--- a/Co2sobj_prop.thy	Fri May 10 10:23:34 2013 +0800
+++ b/Co2sobj_prop.thy	Wed May 15 11:21:39 2013 +0800
@@ -1,6 +1,6 @@
 (*<*)
 theory Co2sobj_prop
-imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop
+imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop
 begin
 (*<*)
 
@@ -10,6 +10,98 @@
 
 declare get_parentfs_ctxts.simps [simp del]
 
+lemma sroot_only:
+  "cf2sfile s [] = Some sroot"
+by (simp add:cf2sfile_def)
+
+lemma not_file_is_dir:
+  "\<lbrakk>\<not> is_file s f; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_dir s f"
+by (auto simp:is_file_def current_files_def is_dir_def 
+         dest:finum_has_itag finum_has_ftag' split:t_inode_tag.splits option.splits)
+
+lemma not_dir_is_file:
+  "\<lbrakk>\<not> is_dir s f; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_file s f"
+by (auto simp:is_file_def current_files_def is_dir_def 
+         dest:finum_has_itag finum_has_ftag' split:t_inode_tag.splits option.splits)
+
+lemma is_file_or_dir:
+  "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_file s f \<or> is_dir s f"
+by (auto dest:not_dir_is_file)
+
+lemma current_file_has_sfile:
+  "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"
+apply (induct f)
+apply (rule_tac x = "sroot" in exI, simp add:sroot_only)
+apply (frule parentf_in_current', simp, clarsimp)
+apply (frule parentf_is_dir'', simp)
+apply (frule is_file_or_dir, simp)
+apply (auto dest!:current_has_sec'
+            simp:cf2sfile_def split:option.splits if_splits dest!:get_pfs_secs_prop)
+done
+
+definition sectxt_of_pf :: "t_state \<Rightarrow> t_file \<Rightarrow> security_context_t option"
+where
+  "sectxt_of_pf s f = (case f of [] \<Rightarrow> None | (a # pf) \<Rightarrow> sectxt_of_obj s (O_dir pf))"
+
+definition get_parentfs_ctxts' :: "t_state \<Rightarrow> t_file \<Rightarrow> (security_context_t list) option"
+where
+  "get_parentfs_ctxts' s f = (case f of [] \<Rightarrow> None | (a # pf) \<Rightarrow> get_parentfs_ctxts s pf)"
+
+lemma is_file_has_sfile:
+  "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sec psec asecs. cf2sfile s f = Some 
+      (if (\<not> deleted (O_file f) s \<and> is_init_file f) then Init f else Created,
+       sec, Some psec, set asecs) \<and> (sectxt_of_obj s (O_file f) = Some sec) \<and>
+       (sectxt_of_pf s f = Some psec) \<and> (get_parentfs_ctxts' s f = Some asecs)"
+apply (case_tac f, simp, drule root_is_dir', simp, simp)
+apply (frule is_file_in_current)
+apply (drule current_file_has_sfile, simp)
+apply (auto simp:cf2sfile_def sectxt_of_pf_def get_parentfs_ctxts'_def split:if_splits option.splits)
+done
+
+lemma is_dir_has_sfile:
+  "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> (case f of
+      [] \<Rightarrow> cf2sfile s f = Some sroot
+    | a # pf \<Rightarrow> (\<exists> sec psec asecs. cf2sfile s f = Some 
+      (if (\<not> deleted (O_dir f) s \<and> is_init_dir f) then Init f else Created,
+       sec, Some psec, set asecs) \<and> (sectxt_of_obj s (O_dir f) = Some sec) \<and>
+       (sectxt_of_obj s (O_dir pf) = Some psec) \<and> (get_parentfs_ctxts s pf = Some asecs)))"
+apply (case_tac f, simp add:sroot_only)
+apply (frule is_dir_in_current, frule is_dir_not_file)
+apply (drule current_file_has_sfile, simp)
+apply (auto simp:cf2sfile_def split:if_splits option.splits)
+done
+
+lemma cf2sfile_path:
+  "\<lbrakk>f # pf \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = (
+     case (cf2sfile s pf) of
+       Some (pfi, pfsec, psec, asecs) \<Rightarrow> (if (is_file s (f # pf))
+         then (case (sectxt_of_obj s (O_file (f # pf))) of
+                 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)
+                                   else Created, fsec, Some pfsec, asecs \<union> {pfsec})
+               | None \<Rightarrow> None)
+         else (case (sectxt_of_obj s (O_dir (f # pf))) of
+                 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)
+                                   else Created, fsec, Some pfsec, asecs \<union> {pfsec})
+               | None \<Rightarrow> None)           )
+     | None \<Rightarrow> None)"
+apply (frule parentf_is_dir'', simp)
+apply (frule parentf_in_current', simp)
+apply (frule is_file_or_dir, simp)
+apply (frule_tac f = pf in current_file_has_sfile, simp, erule exE)
+apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop
+            simp:cf2sfile_def split:option.splits if_splits)
+apply (case_tac "is_file s (f # pf)")
+apply (frule is_file_has_sec, simp)
+apply (frule is_dir_has_sec, simp)
+apply (frule is_dir_not_file)
+apply (erule exE)+
+apply (auto split:option.splits)[1]
+apply simp
+
+apply (rule ext)
+apply (subst (1) cf2sfile_def)
+apply (auto simp del:deleted.simps get_parentfs_ctxts.simps split:option.splits if_splits)
+
 lemma cf2sfile_open_none1:
   "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f b = cf2sfile s f b"
 apply (frule vd_cons, frule vt_grant_os)
@@ -33,10 +125,6 @@
 apply (simp add:cf2sfile_open_none1 cf2sfile_open_none2)
 done
 
-lemma sroot_only:
-  "cf2sfile s [] = (\<lambda> b. if b then None else Some sroot)"
-by (rule ext, simp add:cf2sfile_def)
-
 lemma cf2sfile_open_some1:
   "\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk>
    \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"
@@ -60,7 +148,7 @@
 apply (frule vd_cons, drule is_dir_in_current)
 by (simp add:cf2sfile_open_some1)
 
-lemma cf2sfile_open_some:
+lemma cf2sfile_open_some4:
   "valid (Open p f flag fd (Some inum) # s) \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f True = (
      case (parent f) of
        Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd (Some inum) # s) (O_file f), sectxt_of_obj s (O_dir pf), 
@@ -72,30 +160,87 @@
 apply (case_tac f, simp)
 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
                get_parentfs_ctxts_simps)
-apply (rule impI)
-thm not_deleted_imp_exists
-apply (auto split:if_splits option.splits    dest!:current_has_sec'
-          simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
-               get_parentfs_ctxts_simps)
+apply (rule impI, (erule conjE)+)
+apply (drule not_deleted_init_file, simp+)
+apply (simp add:is_file_in_current)
+done
+
+lemma cf2sfile_open_some5:
+  "valid (Open p f flag fd (Some inum) # s) \<Longrightarrow> 
+   cf2sfile (Open p f flag fd (Some inum) # s) f False = cf2sfile s f False"
+apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
+apply (case_tac f, simp)
+apply (auto simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
+               get_parentfs_ctxts_simps split:option.splits)
+done
+
+lemma cf2sfile_open:
+  "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk>
+   \<Longrightarrow> cf2sfile (Open p f flag fd opt # s) f' b = (
+     if (opt = None) then cf2sfile s f' b
+     else if (f' = f \<and> b) 
+     then (case (parent f) of
+             Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd opt # s) (O_file f), sectxt_of_obj s (O_dir pf), 
+                 get_parentfs_ctxts s pf) of
+                          (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)
+                        | _ \<Rightarrow> None)
+           | None \<Rightarrow> None)
+     else cf2sfile s f' b)"
+apply (case_tac opt)
+apply (simp add:cf2sfile_open_none)
+apply (case_tac "f = f'")
+apply (auto simp:cf2sfile_open_some1 cf2sfile_open_some4 cf2sfile_open_some5 current_files_simps)
+done
+
+lemma cf2sfile_mkdir1:
+  "\<lbrakk>valid (Mkdir p f i # s); f' \<in> current_files s\<rbrakk>
+   \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"
+apply (frule vd_cons, frule vt_grant_os, frule noroot_events, rule ext)
+apply (case_tac "f = f'", simp)
+apply (induct f', simp add:sroot_only, simp)
+apply (frule parentf_in_current', simp+)
+apply clarsimp
+apply (case_tac "f = f'", simp+)
+apply (simp (no_asm_simp) add:cf2sfile_def)
+apply (auto simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
+               get_parentfs_ctxts_simps split:if_splits option.splits)
+done
+
+lemma cf2sfile_mkdir2:
+  "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_file s f'\<rbrakk>
+   \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' True = cf2sfile s f' True"
+apply (frule vd_cons, drule is_file_in_current)
+by (simp add:cf2sfile_open_some1)
+
+lemma cf2sfile_mkdir3:
+  "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_dir s f'\<rbrakk>
+   \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' False = cf2sfile s f' False"
+apply (frule vd_cons, drule is_dir_in_current)
+by (simp add:cf2sfile_open_some1)
+
+
+lemma cf2sfile_mkdir:
+  "valid (Mkdir p f i # s)
+  \<Longrightarrow> cf2sfile (Mkdir p f i # s) = (\<lambda> f' b. 
+    if (f' = f \<and> \<not> b) 
+    then (case (parent f) of
+             Some pf \<Rightarrow> (case (sectxt_of_obj (Mkdir p f i # s) (O_dir f), sectxt_of_obj s (O_dir pf), 
+                 get_parentfs_ctxts s pf) of
+                          (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)
+                        | _ \<Rightarrow> None)
+           | None \<Rightarrow> None)
+     else cf2sfile s f' b)"
+apply (frule vd_cons, frule vt_grant_os)
+apply (rule ext, rule ext)
+
+apply (auto simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
+               get_parentfs_ctxts_simps  split:if_splits option.splits)
 
 
 
-lemma cf2sfile_open:
-  "valid (Open p f flag fd opt # s) \<Longrightarrow> cf2sfile (Open p f flag fd opt # s) = (\<lambda> f' b. 
-     if (opt = None) then cf2sfile s f' b
-     else if (f' = f \<and> b = True) 
-     then (case (parent f) of
-             Some pf \<Rightarrow> (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), 
-                 get_parentfs_ctxts s pf) of
-                          (Some sec, Some psec, Some asecs) \<Rightarrow>
-                              Some (if (\<not> deleted (O_file f) s \<and> f \<in> init_files) 
-                                    then Init f else Created, sec, Some psec, set asecs)
-                        | _ \<Rightarrow> None)
-           | None \<Rightarrow> None)
-     else cf2sfile s f' b)"
-apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext)
-apply (auto split:if_splits option.splits 
-             simp:sectxt_of_obj_simps)
+
+
+
 
 
 
diff -r 0c209a3e2647 -r 8779d321cc2e Current_files_prop.thy
--- a/Current_files_prop.thy	Fri May 10 10:23:34 2013 +0800
+++ b/Current_files_prop.thy	Wed May 15 11:21:39 2013 +0800
@@ -432,6 +432,9 @@
 lemma parentf_is_dir: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf"
 by (clarsimp simp:current_files_def parentf_is_dir')
 
+lemma parentf_is_dir'': "\<lbrakk>f # pf \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf"
+by (auto intro!:parentf_is_dir)
+
 lemma ancenf_is_dir_aux: "\<forall> f. f \<preceq> f' \<and> f \<noteq> f' \<and> f' \<in> current_files \<tau> \<and> valid \<tau> \<longrightarrow> is_dir \<tau> f"
 proof (induct f')
   case Nil show ?case
diff -r 0c209a3e2647 -r 8779d321cc2e Delete_prop.thy
--- a/Delete_prop.thy	Fri May 10 10:23:34 2013 +0800
+++ b/Delete_prop.thy	Wed May 15 11:21:39 2013 +0800
@@ -1,4 +1,4 @@
-theory Deleted_prop
+theory Delete_prop
 imports Main Flask Flask_type Init_prop Alive_prop Current_files_prop
 begin
 
diff -r 0c209a3e2647 -r 8779d321cc2e Flask.thy
--- a/Flask.thy	Fri May 10 10:23:34 2013 +0800
+++ b/Flask.thy	Wed May 15 11:21:39 2013 +0800
@@ -207,7 +207,7 @@
 
 definition init_same_inode_files :: "t_file \<Rightarrow> t_file set"
 where
-  "init_same_inode_files f \<equiv> {f'. init_inum_of_file f = init_inum_of_file f'}"
+  "init_same_inode_files f \<equiv> if is_init_file f then {f'. init_inum_of_file f = init_inum_of_file f'} else {}"
 
 fun init_alive :: "t_object \<Rightarrow> bool"
 where
@@ -357,7 +357,7 @@
       | DGRAM  \<Rightarrow> (itag_of_inum \<tau>) (ino := Some Tag_UDP_SOCK) )"
 | "itag_of_inum (Accept p fd addr lport' fd' ino # \<tau>) = 
      (itag_of_inum \<tau>) (ino := Some Tag_TCP_SOCK)"
-| "itag_of_inum (_ # \<tau>) = itag_of_inum \<tau>"  (* may be sth wrong with nettemp representing addr \<times> netdev in statical analysis ??? *)
+| "itag_of_inum (_ # \<tau>) = itag_of_inum \<tau>"  
 
 definition is_file:: "t_state \<Rightarrow> t_file \<Rightarrow> bool"
 where
@@ -482,7 +482,7 @@
 
 definition same_inode_files :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file set"
 where
-  "same_inode_files s f \<equiv> {f'. inum_of_file s f = inum_of_file s f'}"
+  "same_inode_files s f \<equiv> if is_file s f then {f'. inum_of_file s f = inum_of_file s f'} else {}"
 
 fun flags_of_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_open_flags option"
 where
@@ -614,29 +614,28 @@
      case inumopt of
        Some ino \<Rightarrow>
     (p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and> 
-     (\<exists> pf. parent f = Some pf \<and> pf \<in> current_files \<tau> \<and> is_dir \<tau> pf \<and> pf \<notin> files_hung_by_del \<tau>) \<and>
+     (\<exists> pf. parent f = Some pf \<and> is_dir \<tau> pf \<and> pf \<notin> files_hung_by_del \<tau>) \<and>
      is_creat_flag flags \<and> fd \<notin> (current_proc_fds \<tau> p) \<and> ino \<notin> (current_inode_nums \<tau>))
    |   None     \<Rightarrow>
-    (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> \<not> is_creat_excl_flag flags \<and> is_file \<tau> f \<and>
+    (p \<in> current_procs \<tau> \<and> \<not> is_creat_excl_flag flags \<and> is_file \<tau> f \<and>
      fd \<notin> (current_proc_fds \<tau> p))           )"
 (*(if (is_dir \<tau> f) then (is_dir_flag flags \<and> \<not> is_write_flag flags) else (\<not> is_dir_flag flags)),
   here open is not applied to directories, readdir is for that, but it is not security-related *)
 | "os_grant \<tau> (CloseFd p fd)                  = 
     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p)"
 | "os_grant \<tau> (UnLink p f)                    = 
-    (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> is_file \<tau> f \<and> f \<notin> files_hung_by_del \<tau>)"
+    (p \<in> current_procs \<tau> \<and> is_file \<tau> f \<and> f \<notin> files_hung_by_del \<tau>)"
 | "os_grant \<tau> (Rmdir p f)                     = 
-    (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> dir_is_empty \<tau> f \<and> f \<notin> files_hung_by_del \<tau> \<and> f \<noteq> [])" (* root file cannot be deleted *)
+    (p \<in> current_procs \<tau> \<and> dir_is_empty \<tau> f \<and> f \<notin> files_hung_by_del \<tau> \<and> f \<noteq> [])" (* root file cannot be deleted *)
 | "os_grant \<tau> (Mkdir p f ino)                 = 
     (p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and> 
-     (\<exists> pf. parent f = Some pf \<and> pf \<in> current_files \<tau> \<and> is_dir \<tau> pf \<and> pf \<notin> files_hung_by_del \<tau>) \<and>
+     (\<exists> pf. parent f = Some pf \<and> is_dir \<tau> pf \<and> pf \<notin> files_hung_by_del \<tau>) \<and>
      ino \<notin> (current_inode_nums \<tau>))"
 | "os_grant \<tau> (LinkHard p f\<^isub>1 f\<^isub>2)              = 
-    (p \<in> current_procs \<tau> \<and> f\<^isub>1 \<in> current_files \<tau> \<and> f\<^isub>2 \<notin> current_files \<tau> \<and> 
-     (\<exists> pf\<^isub>2. parent f\<^isub>2 = Some pf\<^isub>2 \<and> pf\<^isub>2 \<in> current_files \<tau> \<and> is_dir \<tau> pf\<^isub>2 \<and> 
-             pf\<^isub>2 \<notin> files_hung_by_del \<tau>) \<and> is_file \<tau> f\<^isub>1)"
+    (p \<in> current_procs \<tau> \<and> is_file \<tau> f\<^isub>1 \<and> f\<^isub>2 \<notin> current_files \<tau> \<and> 
+     (\<exists> pf\<^isub>2. parent f\<^isub>2 = Some pf\<^isub>2 \<and> is_dir \<tau> pf\<^isub>2 \<and> pf\<^isub>2 \<notin> files_hung_by_del \<tau>))"
 | "os_grant \<tau> (Truncate p f len)              = 
-    (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> is_file \<tau> f)"
+    (p \<in> current_procs \<tau> \<and> is_file \<tau> f)"
 (*
 | "os_grant \<tau> (FTruncate p fd len)            = 
     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> 
@@ -652,7 +651,7 @@
      (\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau>) \<and> 
      (\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_write_flag flags))"
 | "os_grant \<tau> (Execve p f fds)                = 
-    (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> is_file \<tau> f \<and> fds \<subseteq> current_proc_fds \<tau> p)" (* file_at_writing_by \<tau> f = {} *)
+    (p \<in> current_procs \<tau> \<and> is_file \<tau> f \<and> fds \<subseteq> current_proc_fds \<tau> p)" (* file_at_writing_by \<tau> f = {} *)
 (*
 | "os_grant \<tau> (Rename p f\<^isub>2 f\<^isub>3)                = 
     (p \<in> current_procs \<tau> \<and> f\<^isub>2 \<in> current_files \<tau> \<and> \<not>(f\<^isub>2 \<preceq> f\<^isub>3) \<and> f\<^isub>3 \<notin> current_files \<tau> \<and>
@@ -689,8 +688,8 @@
     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and> 
      socket_state \<tau> (p, fd) = Some SS_bind)"
 | "os_grant \<tau> (Listen p fd)                   = 
-    (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and> 
-     socket_state \<tau> (p, fd) = Some SS_bind \<and> is_tcp_sock \<tau> (p, fd))" (* Listen and Accept should only be used for TCP sever side *)
+    (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> is_tcp_sock \<tau> (p, fd) \<and>
+     socket_state \<tau> (p, fd) = Some SS_bind)" (* Listen and Accept should only be used for TCP sever side *)
 | "os_grant \<tau> (SendSock p fd)                 = 
     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and> 
      socket_in_sending \<tau> (p, fd))"
@@ -716,12 +715,12 @@
 fun alive :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"
 where
   "alive s (O_proc p)     = (p \<in> current_procs s)"
-| "alive s (O_file f)     = (f \<in> current_files s \<and> is_file s f)"
-| "alive s (O_dir  f)     = (f \<in> current_files s \<and> is_dir s f)"
+| "alive s (O_file f)     = (is_file s f)"
+| "alive s (O_dir  f)     = (is_dir s f)"
 | "alive s (O_fd p fd)    = (fd \<in> current_proc_fds s p)"
 | "alive s (O_node n)     = (n \<in> init_nodes)"
-| "alive s (O_tcp_sock k) = (k \<in> current_sockets s \<and> is_tcp_sock s k)"
-| "alive s (O_udp_sock k) = (k \<in> current_sockets s \<and> is_udp_sock s k)"
+| "alive s (O_tcp_sock k) = (is_tcp_sock s k)"
+| "alive s (O_udp_sock k) = (is_udp_sock s k)"
 | "alive s (O_shm  h)     = (h \<in> current_shms s)"
 | "alive s (O_msgq q)     = (q \<in> current_msgqs s)"
 | "alive s (O_msg q m)    = (m \<in> set (msgs_of_queue s q) \<and> q \<in> current_msgqs s)"
diff -r 0c209a3e2647 -r 8779d321cc2e Init_prop.thy
--- a/Init_prop.thy	Fri May 10 10:23:34 2013 +0800
+++ b/Init_prop.thy	Wed May 15 11:21:39 2013 +0800
@@ -273,7 +273,7 @@
 
 lemma same_inode_nil_prop:
   "same_inode_files [] f = init_same_inode_files f"
-by (simp add:same_inode_files_def init_same_inode_files_def)
+by (simp add:same_inode_files_def init_same_inode_files_def is_file_nil)
 
 lemma init_same_inode_prop1:
   "f \<in> init_files \<Longrightarrow> \<forall> f' \<in> init_same_inode_files f. f' \<in> init_files"
@@ -282,6 +282,19 @@
 apply (auto simp:init_files_prop1)
 done
 
+lemma init_same_inode_prop2:
+  "\<lbrakk>f' \<in> init_same_inode_files f; f \<in> init_files\<rbrakk> \<Longrightarrow> f' \<in> init_files"
+by (drule init_same_inode_prop1, simp)
+
+lemma init_same_inode_prop3:
+  "f' \<in> init_same_inode_files f \<Longrightarrow> f \<in> init_same_inode_files f'"
+by (auto simp add:init_same_inode_files_def is_init_file_def split:if_splits)
+
+lemma init_same_inode_prop4:
+  "\<lbrakk>f' \<in> init_same_inode_files f; f' \<in> init_files\<rbrakk> \<Longrightarrow> f \<in> init_files"
+apply (drule init_same_inode_prop3)
+by (simp add:init_same_inode_prop2)
+
 end
 
 context flask begin
@@ -558,7 +571,7 @@
 by (simp add:init_cf2sfile_def)
 
 lemma sroot_valid':
-  "cf2sfile s [] False = Some sroot"
+  "cf2sfile s [] = Some sroot"
 by (simp add:cf2sfile_def)  
 
 lemma init_sectxt_prop:
@@ -646,51 +659,42 @@
 apply (simp add:init_cq2smsgq_def)
 by (case_tac sec, simp+)
 
-lemma cf2sfile_nil_prop1:
-  "f \<in> init_files \<Longrightarrow> cf2sfile [] f (is_init_file f) = init_cf2sfile f"
+lemma cf2sfile_nil_prop:
+  "f \<in> init_files \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"
 apply (case_tac f)
 apply (simp add:init_sectxt_prop cf2sfile_def init_cf2sfile_def)
-apply (rule notI, drule root_is_init_dir', simp)
 apply (auto simp:init_sectxt_prop cf2sfile_def init_cf2sfile_def split:option.splits dest!:init_has_ctxt')
-apply (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits
+apply (auto simp:is_init_file_def is_init_dir_def is_file_nil split:option.splits t_inode_tag.splits 
             dest:init_file_has_inum inof_has_file_tag)
 done
 
-
 lemma init_sec_file_dir:
   "\<lbrakk>init_sectxt_of_obj (O_file f) = Some x; init_sectxt_of_obj (O_dir f) = Some y\<rbrakk> \<Longrightarrow> False"
 apply (drule init_sectxt_prop2)+
 apply (auto intro:init_file_dir_conflict)
 done
 
-lemma cf2sfile_nil_prop2:
-  "f \<in> init_files \<Longrightarrow> cf2sfile [] f (\<not> is_init_file f) = None"
-apply (case_tac f)
-apply (simp add:init_sectxt_prop cf2sfile_def init_cf2sfile_def)
-apply (rule notI, drule root_is_init_dir', simp)
-apply (auto simp:init_sectxt_prop cf2sfile_def init_cf2sfile_def split:option.splits dest!:init_has_ctxt')
-apply (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits
-            dest:init_file_has_inum inof_has_file_tag init_sec_file_dir)
-done
-
-lemma cf2sfile_nil_prop:
-  "f \<in> init_files \<Longrightarrow> cf2sfile [] f = (\<lambda> b. if (b = is_init_file f) then init_cf2sfile f else None)"
-apply (frule cf2sfile_nil_prop1, frule cf2sfile_nil_prop2)
-by (rule ext, auto split:if_splits)
-
 lemma cf2sfile_nil_prop3:
-  "is_init_file f \<Longrightarrow> cf2sfile [] f True = init_cf2sfile f"
+  "is_init_file f \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"
 by (simp add:is_init_file_prop1 cf2sfile_nil_prop)
 
 lemma cf2sfile_nil_prop4:
-  "is_init_dir f \<Longrightarrow> cf2sfile [] f False = init_cf2sfile f"
+  "is_init_dir f \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"
 apply (frule init_file_dir_conflict2)
 by (simp add:is_init_file_prop1 is_init_dir_prop1 cf2sfile_nil_prop)
 
 lemma cfs2sfiles_nil_prop:
-  "\<forall> f \<in> fs. f \<in> init_files \<Longrightarrow> cfs2sfiles [] fs = init_cfs2sfiles fs"
-apply (simp add:cfs2sfiles_def init_cfs2sfiles_def)
-apply (rule set_eqI, rule iffI, auto simp:cf2sfile_nil_prop split:if_splits)
+  "f \<in> init_files \<Longrightarrow> cf2sfiles [] f = init_cf2sfiles f"
+apply (simp add:cf2sfiles_def init_cf2sfiles_def)
+apply (rule set_eqI, rule iffI, auto split:if_splits)
+apply (rule_tac x = f' in bexI, simp add:same_inode_nil_prop cf2sfile_nil_prop)
+apply (drule init_same_inode_prop2, simp)
+apply (simp add:cf2sfile_nil_prop)
+apply (simp add:same_inode_nil_prop)
+apply (rule_tac x = f' in bexI)
+apply (drule init_same_inode_prop2, simp)
+apply ( simp add:same_inode_nil_prop cf2sfile_nil_prop)
+apply (simp add:same_inode_nil_prop)
 done
 
 lemma cfd2sfd_nil_prop:
@@ -762,7 +766,7 @@
                split:option.splits)
 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def)
 apply (simp add:init_files_props)
-apply (auto simp:is_dir_nil is_file_nil dest:init_file_dir_conflict)
+apply (auto simp:is_dir_nil is_file_nil init_files_prop4 dest:init_file_dir_conflict)
 done
 
 lemma s2ss_nil_prop:
diff -r 0c209a3e2647 -r 8779d321cc2e Static.thy
--- a/Static.thy	Fri May 10 10:23:34 2013 +0800
+++ b/Static.thy	Wed May 15 11:21:39 2013 +0800
@@ -49,9 +49,9 @@
     (Some sec, Some psec, Some aseclist) \<Rightarrow> Some (Init f, sec, Some psec, set aseclist)
   | _ \<Rightarrow> None)"
 
-definition init_cfs2sfiles :: "t_file set \<Rightarrow> t_sfile set"
+definition init_cf2sfiles :: "t_file \<Rightarrow> t_sfile set"
 where
-  "init_cfs2sfiles fs \<equiv> {sf. \<exists>f \<in> fs. init_cf2sfile f = Some sf \<and> is_init_file f}"
+  "init_cf2sfiles f \<equiv> {sf. \<exists>f' \<in> init_same_inode_files f. init_cf2sfile f' = Some sf}"
 
 definition init_cfd2sfd :: "t_process \<Rightarrow> t_fd \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) option"
 where
@@ -117,7 +117,7 @@
      | _ \<Rightarrow> None)"
 | "init_obj2sobj (O_file f) = 
      (if (f \<in> init_files \<and> is_init_file f) 
-      then Some (S_file (init_cfs2sfiles (init_same_inode_files f)) 
+      then Some (S_file (init_cf2sfiles f) 
                         (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))
       else None)"
 | "init_obj2sobj (O_dir f) = 
@@ -697,12 +697,12 @@
 
 (**************** translation from dynamic to static *******************)
 
-definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> bool \<Rightarrow> t_sfile option"
+definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option"
 where
-  "cf2sfile s f Is_file \<equiv>
+  "cf2sfile s f \<equiv>
      case (parent f) of 
-       None \<Rightarrow> if Is_file then None else Some sroot
-     | Some pf \<Rightarrow> if Is_file 
+       None \<Rightarrow> Some sroot
+     | Some pf \<Rightarrow> if (is_file s f) 
      then (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of
             (Some sec, Some psec, Some asecs) \<Rightarrow>
  Some (if (\<not> deleted (O_file f) s \<and> is_init_file f) then Init f else Created, sec, Some psec, set asecs)
@@ -712,16 +712,16 @@
  Some (if (\<not> deleted (O_dir f) s \<and> is_init_dir f) then Init f else Created, sec, Some psec, set asecs)
           | _ \<Rightarrow> None)"
 
-definition cfs2sfiles :: "t_state \<Rightarrow> t_file set \<Rightarrow> t_sfile set"
+definition cf2sfiles :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile set"
 where
-  "cfs2sfiles s fs \<equiv> {sf. \<exists> f \<in> fs. cf2sfile s f True = Some sf}"
+  "cf2sfiles s f \<equiv> {sf. \<exists> f' \<in> (same_inode_files s f). cf2sfile s f' = Some sf}"
 
 (* here cf2sfile is passed with True, because, process' fds are only for files not dirs *)
 definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option" 
 where
   "cfd2sfd s p fd \<equiv> 
     (case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of
-      (Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f True) of 
+      (Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f) of 
                                           Some sf \<Rightarrow> Some (sec, flags, sf)
                                         | _       \<Rightarrow> None)
     | _ \<Rightarrow> None)"
@@ -782,10 +782,10 @@
       | _       \<Rightarrow> None)"
 | "co2sobj s (O_file f) = 
      (if (f \<in> current_files s) then 
-        Some (S_file (cfs2sfiles s (same_inode_files s f)) (O_file f \<in> tainted s))
+        Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))
       else None)"
 | "co2sobj s (O_dir f) = 
-     (case (cf2sfile s f False) of
+     (case (cf2sfile s f) of
         Some sf  \<Rightarrow> Some (S_dir sf)
       | _ \<Rightarrow> None)"
 | "co2sobj s (O_msgq q) =