
diff -r 34d01e9a772e -r 7d9c0ed02b56 Static.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Static.thy	Fri May 03 08:20:21 2013 +0100
@@ -0,0 +1,871 @@
+theory Static
+imports Static_type OS_type_def Flask_type Flask
+begin
+
+locale tainting_s = tainting 
+
+begin
+
+fun init_role_of_obj :: "t_object \<Rightarrow> role_t option"
+where
+  "init_role_of_obj (O_proc p) = init_role_of_proc p"
+| "init_role_of_obj _          = Some R_object"
+
+definition init_sectxt_of_obj :: "t_object \<Rightarrow> security_context_t option"
+where
+  "init_sectxt_of_obj obj \<equiv>
+     (case (init_user_of_obj obj, init_role_of_obj obj, init_type_of_obj obj) of
+        (Some u, Some r, Some t) \<Rightarrow> Some (u,r,t)
+      | _ \<Rightarrow> None)"
+
+(*
+definition init_sectxt_of_file:: "t_file \<Rightarrow> security_context_t option"
+where
+  "init_sectxt_of_file f \<equiv> 
+     if (is_init_file f) then init_sectxt_of_obj (O_file f)
+     else if (is_init_dir f) then init_sectxt_of_obj (O_dir f)
+     else None"
+*)
+
+definition sec_of_root :: "security_context_t"
+where
+  "sec_of_root \<equiv> (case (init_user_of_obj (O_dir []), init_type_of_obj (O_dir [])) of
+     (Some u, Some t) \<Rightarrow> (u, R_object, t))"
+
+definition sroot :: "t_sfile"
+where
+  "sroot \<equiv> (Init [], sec_of_root, None, {})"
+
+definition init_cf2sfile :: "t_file \<Rightarrow> t_sfile option"
+where
+  "init_cf2sfile f \<equiv> 
+     case (parent f) of 
+       None \<Rightarrow> Some sroot
+     | Some pf \<Rightarrow> if (is_init_file f) then 
+ (case (init_sectxt_of_obj (O_file f), init_sectxt_of_obj (O_dir pf), get_parentfs_ctxts [] pf) of
+    (Some sec, Some psec, Some aseclist) \<Rightarrow> Some (Init f, sec, Some psec, set aseclist)
+  | _ \<Rightarrow> None)    else 
+ (case (init_sectxt_of_obj (O_dir f), init_sectxt_of_obj (O_dir pf), get_parentfs_ctxts [] pf) of
+    (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"
+where
+  "init_cfs2sfiles fs \<equiv> {sf. \<exists>f \<in> fs. 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
+  "init_cfd2sfd p fd = 
+     (case (init_file_of_proc_fd p fd, init_oflags_of_proc_fd p fd, init_sectxt_of_obj (O_fd p fd)) of
+        (Some f, Some flags, Some sec) \<Rightarrow> (case (init_cf2sfile f) of 
+                                             Some sf \<Rightarrow> Some (sec, flags, sf)
+                                           | _ \<Rightarrow> None)
+      | _ \<Rightarrow> None)"
+
+definition init_cfds2sfds :: "t_process \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) set"
+where
+  "init_cfds2sfds p \<equiv> { sfd. \<exists> fd sfd f. init_file_of_proc_fd p fd = Some f \<and> init_cfd2sfd p fd = Some sfd}"
+
+definition init_ch2sshm :: "t_shm \<Rightarrow> t_sshm option"
+where
+  "init_ch2sshm h \<equiv> (case (init_sectxt_of_obj (O_shm h)) of
+                       Some sec \<Rightarrow> Some (Init h, sec)
+                     | _        \<Rightarrow> None)"
+
+definition init_cph2spshs 
+  :: "t_process \<Rightarrow> (t_sshm \<times> t_shm_attach_flag) set"
+where
+  "init_cph2spshs p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> init_procs_of_shm h \<and> 
+                                             init_ch2sshm h = Some sh}"
+
+definition init_cp2sproc :: "t_process \<Rightarrow> t_sproc option"
+where
+  "init_cp2sproc p \<equiv> (case (init_sectxt_of_obj (O_proc p)) of 
+       Some sec \<Rightarrow> Some (Init p, sec, (init_cfds2sfds p), (init_cph2spshs p))
+     | None     \<Rightarrow> None)"
+
+(* acient files of init-file 
+definition init_o2s_afs :: "t_file \<Rightarrow> security_context_t set"
+where
+  "init_o2s_afs f \<equiv> {sec. \<exists> f'. f' \<preceq> f \<and> init_sectxt_of_obj (O_dir f') = Some sec}" *)
+
+definition init_cm2smsg :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
+where
+  "init_cm2smsg q m \<equiv> (case (init_sectxt_of_obj (O_msg q m)) of 
+                         Some sec \<Rightarrow> Some (Init m, sec, (O_msg q m) \<in> seeds)
+                       | _ \<Rightarrow> None)"
+
+fun init_cqm2sms :: "t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option"
+where
+  "init_cqm2sms q []     = Some []"
+| "init_cqm2sms q (m#ms) = 
+     (case (init_cqm2sms q ms, init_cm2smsg q m) of 
+        (Some sms, Some sm) \<Rightarrow> Some (sm # sms)
+      | _        \<Rightarrow> None)"
+
+definition init_cq2smsgq :: "t_msgq \<Rightarrow> t_smsgq option"
+where
+  "init_cq2smsgq q \<equiv> (case (init_sectxt_of_obj (O_msgq q), init_cqm2sms q (init_msgs_of_queue q)) of 
+       (Some sec, Some sms) \<Rightarrow> Some (Init q, sec, sms)
+     | _ \<Rightarrow> None)"
+
+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'}"
+
+fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject option"
+where
+  "init_obj2sobj (O_proc p) = 
+     (case (init_cp2sproc p) of 
+       Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds))
+     | _ \<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)) 
+                        (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))
+      else None)"
+| "init_obj2sobj (O_dir f) = 
+     (if (is_init_dir f) then 
+        (case (init_cf2sfile f) of
+           Some sf \<Rightarrow> Some (S_dir sf) 
+         | _ \<Rightarrow> None)
+      else None)"
+| "init_obj2sobj (O_msgq q) = 
+     (case (init_cq2smsgq q) of
+       Some sq \<Rightarrow> Some (S_msgq sq)
+     | _ \<Rightarrow> None)"
+| "init_obj2sobj (O_shm h) = 
+     (case (init_ch2sshm h) of 
+       Some sh \<Rightarrow> Some (S_shm sh)
+     | _       \<Rightarrow> None)"
+| "init_obj2sobj (O_msg q m) = 
+     (case (init_cq2smsgq q, init_cm2smsg q m) of 
+        (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
+      | _                  \<Rightarrow> None)"
+| "init_obj2sobj _ = None"
+
+definition  
+  "init_static_state \<equiv> {sobj. \<exists> obj. init_alive obj \<and> init_obj2sobj obj = Some sobj}"
+
+fun is_init_sfile :: "t_sfile \<Rightarrow> bool"
+where
+  "is_init_sfile (Init _, sec, psec,asec) = True"
+| "is_init_sfile _ = False"
+
+fun is_many_sfile :: "t_sfile \<Rightarrow> bool"
+where
+  "is_many_sfile (Created, sec, psec, asec) = True"
+| "is_many_sfile _ = False"
+
+fun is_init_sproc :: "t_sproc \<Rightarrow> bool"
+where
+  "is_init_sproc (Init p, sec, fds, shms) = True"
+| "is_init_sproc _                        = False"
+
+fun is_many_sproc :: "t_sproc \<Rightarrow> bool"
+where
+  "is_many_sproc (Created, sec,fds,shms) = True"
+| "is_many_sproc _                       = False"
+
+fun is_many_smsg :: "t_smsg \<Rightarrow> bool"
+where
+  "is_many_smsg (Created,sec,tag) = True"
+| "is_many_smsg _                 = False"
+
+fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool"
+where
+  "is_many_smsgq (Created,sec,sms) = (True \<and> (\<forall> sm \<in> (set sms). is_many_smsg sm))"
+| "is_many_smsgq _                 = False"
+
+fun is_many_sshm :: "t_sshm \<Rightarrow> bool"
+where
+  "is_many_sshm (Created, sec) = True"
+| "is_many_sshm _              = False"
+
+(*
+fun is_init_sobj :: "t_sobject \<Rightarrow> bool"
+where
+  "is_init_sobj (S_proc (popt, sec, fds, shms) tag) = (popt \<noteq> None)"
+| "is_init_sobj (S_file sf tag) = (is_init_sfile sf)"
+| "is_init_sobj (S_dir  sf tag) = (is_init_sfile sf)"
+| "is_init_sobj (S_msg" *)
+
+fun is_many :: "t_sobject \<Rightarrow> bool"
+where
+  "is_many (S_proc (Many, sec, fds, shms) tag) = True"
+| "is_many (S_file sfs                    tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)"
+| "is_many (S_dir  sf                        ) = is_many_sfile sf"
+| "is_many (S_msgq sq                        ) = is_many_smsgq sq"
+| "is_many (S_shm  sh                        ) = is_many_sshm  sh"
+
+(*
+fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
+where
+  "update_ss_sp ss (S_proc sp tag) (S_proc sp' tag') = 
+     (if (is_many_sproc sp) then ss \<union> {S_proc sp' tag'} 
+      else (ss - {S_proc sp tag}) \<union> {S_proc sp' tag'})"
+
+fun update_ss_sd:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
+where
+  "update_ss_sd ss (S_dir sf tag) (S_dir sf' tag') = 
+     (if (is_many_sfile sf) then ss \<union> {S_dir sf' tag'} 
+      else (ss - {S_dir sf tag}) \<union> {S_dir sf' tag'})"
+*)
+
+definition update_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
+where
+  "update_ss ss so so' \<equiv> if (is_many so) then ss \<union> {so'} else (ss - {so}) \<union> {so'}"
+
+definition add_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
+where
+  "add_ss ss so \<equiv> ss \<union> {so}"
+
+definition del_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
+where
+  "del_ss ss so \<equiv> if (is_many so) then ss else ss - {so}"
+
+(*
+fun sparent :: "t_sfile \<Rightarrow> t_sfile option"
+where
+  "sparent (Sroot si sec) = None"
+| "sparent (Sfile si sec spf) = Some spf"
+
+inductive is_ancesf :: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool" 
+where
+  "is_ancesf sf sf"
+| "sparent sf = Some spf \<Longrightarrow> is_ancesf spf sf"
+| "\<lbrakk>sparent sf = Some spf; is_ancesf saf spf\<rbrakk> \<Longrightarrow> is_ancesf saf sf"
+
+definition sfile_reparent :: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile"
+where
+  "sfile_reparent (Sroot)"
+*)
+
+(*
+(* sfds rename aux definitions *)
+definition sfds_rename_notrelated 
+  :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
+where
+  "sfds_rename_notrelated sfds from to sfds' \<equiv> 
+     (\<forall> sec flag sf. (sec,flag,sf) \<in> sfds \<and> (\<not> from \<preceq> sf) \<longrightarrow> (sec,flag,sf) \<in> sfds')"
+
+definition sfds_rename_renamed
+  :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
+where
+  "sfds_rename_renamed sfds sf from to sfds' \<equiv> 
+     (\<forall> sec flag sf'. (sec,flag,sf) \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow>
+         (sec, flag, file_after_rename sf' from to) \<in> sfds' \<and> (sec,flag,sf) \<notin> sfds')"
+
+definition sfds_rename_remain
+  :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
+where
+  "sfds_rename_remain sfds sf from to sfds' \<equiv> 
+     (\<forall> sec flag sf'. (sec,flag,sf') \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow> 
+         (sec, flag, sf') \<in> sfds' \<and> (sec,flag, file_after_rename sf' from to) \<notin> sfds')"
+
+(* for not many, choose on renamed or not *)
+definition sfds_rename_choices
+  :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
+where
+  "sfds_rename_choices sfds sf from to sfds' \<equiv> 
+     sfds_rename_remain sfds sf from to sfds' \<or> sfds_rename_renamed sfds sf from to sfds'"
+
+(* for many, merge renamed with not renamed *)
+definition sfds_rename_both
+  :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
+where
+  "sfds_rename_both sfds sf from to sfds' \<equiv> 
+     (\<forall> sec flag sf'. (sec,flag,sf') \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow> 
+         (sec, flag, sf') \<in> sfds' \<or> (sec,flag, file_after_rename sf' from to) \<in> sfds')"
+  
+(* added to the new sfds, are those only under the new sfile *)
+definition sfds_rename_added
+  :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
+where
+  "sfds_rename_added sfds from to sfds' \<equiv> 
+     (\<forall> sec' flag' sf' sec flag. (sec',flag',sf') \<in> sfds' \<and> (sec,flag,sf') \<notin> sfds \<longrightarrow> 
+        (\<exists> sf. (sec,flag,sf) \<in> sfds \<and> sf' = file_after_rename from to sf))"
+
+definition sproc_sfds_renamed
+  :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
+where
+  "sproc_sfds_renamed ss sf from to ss' \<equiv>
+     (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> 
+       (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_renamed sfds sf from to sfds'))"
+
+definition sproc_sfds_remain
+  :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
+where
+  "sproc_sfds_remain ss sf from to ss' \<equiv>
+     (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> 
+       (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_remain sfds sf from to sfds'))"
+
+(* for not many, choose on renamed or not *)
+definition sproc_sfds_choices
+  :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
+where
+  "sproc_sfds_choices ss sf from to ss' \<equiv>
+     (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> 
+       (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_choices sfds sf from to sfds'))"
+  
+(* for many, merge renamed with not renamed *)
+definition sproc_sfds_both
+  :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
+where
+  "sproc_sfds_both ss sf from to ss' \<equiv>
+     (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> 
+       (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_both sfds sf from to sfds'))"
+
+(* remove (\<forall> sp tag. S_proc sp tag \<in> ss \<longrightarrow> S_proc sp tag \<in> ss'),
+ * cause sfds contains sfs informations *)
+definition ss_rename_notrelated 
+  :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
+where
+  "ss_rename_notrelated ss sf sf' ss' \<equiv> 
+     (\<forall> sq. S_msgq sq \<in> ss \<longrightarrow> S_msgq sq \<in> ss') \<and> 
+     (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> (\<exists> sfds'.  
+         S_proc (pi,sec,sfds',sshms) tagp \<in> ss'\<and> sfds_rename_notrelated sfds sf sf' sfds'))  \<and>
+     (\<forall> sfs sf'' tag. S_file sfs tag \<in> ss \<and> sf'' \<in> sfs \<and> (\<not> sf \<preceq> sf'') \<longrightarrow> (\<exists> sfs'. 
+         S_file sfs tag \<in> ss' \<and> sf'' \<in> sfs')) \<and>
+     (\<forall> sf'' tag. S_dir sf'' tag \<in> ss \<and> (\<not> sf \<preceq> sf'') \<longrightarrow> S_dir sf'' tag \<in> ss')" 
+
+(* rename from to, from should definited renamed if not many *)
+definition all_descendant_sf_renamed 
+  :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
+where
+  "all_descendant_sf_renamed ss sf from to ss' \<equiv>
+     (\<forall> sfs sf' tagf. sf \<preceq> sf' \<and> S_file sfs tagf \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. 
+       S_file sfs' tagf \<in> ss' \<and> file_after_rename from to sf' \<in> sfs' \<and> sf' \<notin> sfs')) \<and> 
+     (\<forall> sf' tagf. sf \<preceq> sf' \<and> S_dir sf' tagf \<in> ss \<longrightarrow> S_dir (file_after_rename from to sf') tagf \<in> ss' \<and> S_dir sf' tagf \<notin> ss') \<and>
+     sproc_sfds_renamed ss sf from to ss'"
+
+(* not renamed *)
+definition all_descendant_sf_remain
+  :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
+where
+  "all_descendant_sf_remain ss sf from to ss' \<equiv>
+     (\<forall> sfs sf' tag'. sf \<preceq> sf' \<and> S_file sfs tag' \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. 
+       S_file sfs' tag' \<in> ss \<and> file_after_rename from to sf' \<notin> sfs' \<and> sf' \<in> sfs')) \<and> 
+     (\<forall> sf' tag'. sf \<preceq> sf' \<and> S_dir sf' tag' \<in> ss \<longrightarrow> S_dir (file_after_rename from to sf') tag' \<notin> ss' \<and> S_dir sf' tag' \<in> ss') \<and>
+     sproc_sfds_remain ss sf from to ss'"
+
+definition all_descendant_sf_choices
+  :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
+where
+  "all_descendant_sf_choices ss sf from to ss' \<equiv>
+     all_descendant_sf_renamed ss sf from to ss' \<or> all_descendant_sf_remain ss sf from to ss'"
+
+definition all_descendant_sf_both
+  :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
+where
+  "all_descendant_sf_both ss sf from to ss' \<equiv>
+     (\<forall> sfs sf' tag'. sf \<preceq> sf' \<and> S_file sfs tag' \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. 
+        S_file sfs' tag' \<in> ss \<and> file_after_rename from to sf' \<in> sfs' \<or> sf' \<in> sfs')) \<and> 
+     (\<forall> sf' tag'. sf \<preceq> sf' \<and> S_dir sf' tag' \<in> ss \<longrightarrow> 
+        S_dir (file_after_rename from to sf') tag' \<in> ss' \<or> S_dir sf' tag' \<in> ss') \<and>
+     sproc_sfds_both ss sf from to ss'"
+
+definition ss_renamed_file 
+  :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
+where
+  "ss_renamed_file ss sf sf' ss' \<equiv> 
+     (if (is_many_sfile sf) 
+        then all_descendant_sf_choices ss sf sf sf' ss'
+        else all_descendant_sf_renamed ss sf sf sf' ss')"
+
+(* added to the new sfs, are those only under the new sfile *)
+definition sfs_rename_added
+  :: "t_sfile set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile set \<Rightarrow> bool"
+where
+  "sfs_rename_added sfs from to sfs' \<equiv> 
+     (\<forall> sf'. sf' \<in> sfs' \<and> sf' \<notin> sfs \<longrightarrow> (\<exists> sf. sf \<in> sfs \<and> sf' = file_after_rename from to sf))"
+
+(* added to the new sfile, are those only under the new sfile *)
+definition ss_rename_added
+  :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
+where
+  "ss_rename_added ss from to ss' \<equiv> 
+     (\<forall> pi sec fds fds' shms tagp. S_proc (pi, sec, fds,shms) tagp \<in> ss \<and> 
+        S_proc (pi,sec,fds',shms) tagp \<in> ss' \<longrightarrow> sfds_rename_added fds from to fds') \<and>
+     (\<forall> sq. S_msgq sq \<in> ss' \<longrightarrow> S_msgq sq \<in> ss) \<and>
+     (\<forall> sfs sfs' tagf. S_file sfs' tagf \<in> ss' \<and> S_file sfs tagf \<in> ss \<longrightarrow> 
+        sfs_rename_added sfs from to sfs') \<and>
+     (\<forall> sf' tagf. S_dir sf' tagf \<in> ss' \<and> S_dir sf' tagf \<notin> ss \<longrightarrow> 
+        (\<exists> sf. S_dir sf tagf \<in> ss \<and> sf' = file_after_rename from to sf))" 
+
+definition sfile_alive :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> bool"
+where
+  "sfile_alive ss sf \<equiv> (\<exists> sfs tagf. sf \<in> sfs \<and> S_file sfs tagf \<in> ss)"
+
+definition sf_alive :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> bool"
+where
+  "sf_alive ss sf \<equiv> (\<exists> tagd. S_dir sf tagd \<in> ss) \<or> sfile_alive ss sf"
+
+(* constrains that the new static state should satisfy *)
+definition ss_rename:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
+where
+  "ss_rename ss sf sf' ss' \<equiv> 
+     ss_rename_notrelated ss sf sf' ss' \<and>
+     ss_renamed_file ss sf sf' ss' \<and> ss_rename_added ss sf sf' ss' \<and>
+     (\<forall> sf''. sf_alive ss sf'' \<and> sf \<prec> sf'' \<longrightarrow> 
+       (if (is_many_sfile sf'') 
+        then all_descendant_sf_choices ss sf'' sf sf' ss'
+        else all_descendant_sf_both ss sf'' sf sf' ss'))"
+
+(* two sfile, the last fname should not be equal *)
+fun sfile_same_fname:: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool"
+where
+  "sfile_same_fname ((Init n, sec)#spf) ((Init n', sec')#spf') = (n = n')"
+| "sfile_same_fname _                   _                      = False"
+
+(* no same init sfile/only sfile in the target-to spf, should be in static_state addmissble check *)
+definition ss_rename_no_same_fname:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool"
+where
+  "ss_rename_no_same_fname ss from spf \<equiv>
+    \<not> (\<exists> to. sfile_same_fname from to \<and> parent to = Some spf \<and> sf_alive ss to)" 
+
+(* is not a function, is a relation (one 2 many)
+definition update_ss_rename :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
+where
+  "update_ss_rename ss sf sf' \<equiv> if (is_many_sfile sf) 
+     then (ss \<union> {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss}
+              \<union> {S_dir  (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss})
+     else (ss - {S_file sf'' tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss}
+              - {S_dir  sf'' tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss})
+              \<union> {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss}
+              \<union> {S_dir  (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss}" 
+*)
+*)
+
+fun sectxt_of_sproc :: "t_sproc \<Rightarrow> security_context_t"
+where
+  "sectxt_of_sproc (pi,sec,fds,shms) = sec"
+
+fun sectxt_of_sfile :: "t_sfile \<Rightarrow> security_context_t"
+where
+  "sectxt_of_sfile (fi,sec,psec,asecs) = sec"
+
+fun asecs_of_sfile :: "t_sfile \<Rightarrow> security_context_t set"
+where
+  "asecs_of_sfile (fi,sec,psec,asecs) = asecs"
+
+definition search_check_s :: "security_context_t \<Rightarrow> t_sfile \<Rightarrow> bool \<Rightarrow> bool"
+where
+  "search_check_s pctxt sf if_file = 
+    (if if_file 
+      then search_check_file pctxt (sectxt_of_sfile sf) \<and> search_check_allp pctxt (asecs_of_sfile sf)
+      else search_check_dir  pctxt (sectxt_of_sfile sf) \<and> search_check_allp pctxt (asecs_of_sfile sf))"
+
+definition sectxts_of_sfds :: "t_sfd set \<Rightarrow> security_context_t set"
+where
+  "sectxts_of_sfds sfds \<equiv> {ctxt. \<exists> flag sf. (ctxt, flag, sf) \<in> sfds}"
+
+definition inherit_fds_check_s :: "security_context_t \<Rightarrow> t_sfd set \<Rightarrow> bool"
+where
+  "inherit_fds_check_s pctxt sfds \<equiv> 
+     (\<forall> ctxt \<in> sectxts_of_sfds sfds. permission_check pctxt ctxt C_fd P_inherit)"
+
+definition sectxts_of_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> security_context_t set"
+where
+  "sectxts_of_sproc_sshms sshms \<equiv> {ctxt. \<exists> hi flag. ((hi, ctxt),flag) \<in> sshms}"
+
+definition inherit_shms_check_s :: "security_context_t \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool"
+where
+  "inherit_shms_check_s pctxt sshms \<equiv> 
+     (\<forall> ctxt \<in> sectxts_of_sproc_sshms sshms. permission_check pctxt ctxt C_shm P_inherit)"
+
+(*
+fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool"
+where
+  "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = 
+     (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')" 
+*)
+definition info_flow_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool"
+where
+  "info_flow_sproc_sshms shms shms' \<equiv> (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')" 
+
+fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool"
+where
+  "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = info_flow_sproc_sshms shms shms'"
+
+definition update_ss_shms :: "t_static_state \<Rightarrow> t_sproc \<Rightarrow> bool \<Rightarrow> t_static_state"
+where
+  "update_ss_shms ss spfrom tag \<equiv> {sobj. \<exists> sobj' \<in> ss. 
+     (case sobj' of 
+        S_proc sp tagp \<Rightarrow> if (info_flow_sshm spfrom sp) 
+                          then if (is_many_sproc sp)
+                               then (sobj = S_proc sp tagp \<or> sobj = S_proc sp (tagp \<or> tag))
+                               else (sobj = S_proc sp (tagp \<or> tag))
+                          else (sobj = S_proc sp tag)
+     | _ \<Rightarrow> sobj = sobj')}"
+
+
+
+(* all reachable static states(sobjects set) *)
+inductive_set static :: "t_static_state set"
+where
+  s_init:    "init_static_state \<in> static"
+| s_execve:  "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss;
+               (fi,fsec,pfsec,asecs) \<in> sfs; npctxt_execve pctxt fsec = Some pctxt';
+               grant_execve pctxt fsec pctxt'; search_check_s pctxt (fi,fsec,pfsec,asecs) True; 
+               inherit_fds_check_s pctxt' fds'; fds' \<subseteq> fds\<rbrakk>
+  \<Longrightarrow> (update_ss ss (S_proc (pi, pctxt, fds, shms) tagp) 
+                    (S_proc (pi, pctxt', fds', {}) (tagp \<or> tagf))) \<in> static"
+| s_clone:   "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; 
+               permission_check pctxt pctxt C_process P_fork;
+               inherit_fds_check_s pctxt fds'; fds' \<subseteq> fds; 
+               inherit_shms_check_s pctxt shms'; shms' \<subseteq> shms\<rbrakk>
+  \<Longrightarrow> (add_ss ss (S_proc (Created, pctxt, fds', shms') tagp)) \<in> static"
+| s_kill:    "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; 
+               S_proc (pi', pctxt', fds', shms') tagp' \<in> ss; 
+               permission_check pctxt pctxt' C_process P_sigkill\<rbrakk>
+  \<Longrightarrow> (del_ss ss (S_proc (pi', pctxt', fds', shms') tagp')) \<in> static"
+| s_ptrace:  "\<lbrakk>ss \<in> static; S_proc sp tagp \<in> ss; S_proc sp' tagp' \<in> ss; 
+               permission_check (sextxt_of_sproc sp) (sectxt_of_sproc sp') C_process P_ptrace\<rbrakk>
+  \<Longrightarrow> (update_ss_shms (update_ss_shms ss sp tagp) sp' tagp') \<in> static"
+| s_exit:    "\<lbrakk>ss \<in> static; S_proc sp tagp \<in> ss\<rbrakk> \<Longrightarrow> (del_ss ss (S_proc sp tagp)) \<in> static"
+| s_open:    "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss; sf \<in> sfs;
+              search_check_s pctxt sf True; \<not> is_creat_excl_flag flags; 
+              oflags_check flags pctxt (sectxt_of_sfile sf); permission_check pctxt pctxt C_fd P_setattr\<rbrakk>
+  \<Longrightarrow> (update_ss ss (S_proc (pi, pctxt, fds, shms) tagp)
+                    (S_proc (pi, pctxt, fds \<union> {(pctxt,flags,sf)}, shms) tagp)) \<in> static"
+| s_open':   "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; is_creat_excl_flag flags;
+               S_dir (pfi,fsec,pfsec,asecs) \<in> ss; search_check_s pctxt (pfi,fsec,pfsec,asecs) False; 
+               nfsec = nfctxt_create pctxt fsec C_file; oflags_check flags pctxt nfsec;
+               permission_check pctxt fsec C_dir P_add_rename; permission_check pctxt pctxt C_fd P_setattr\<rbrakk>
+  \<Longrightarrow> (update_ss (add_ss ss (S_file {(Created, nfsec, Some fsec, asecs \<union> {fsec})} tagp))
+         (S_proc (pi, pctxt, fds, shms) tagp)
+         (S_proc (pi, pctxt, fds \<union> {(pctxt, flags, (Created, nfsec, Some fsec, asecs \<union> {fsec}))}, shms) tagp)
+      ) \<in> static"
+| S_readf:   "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds; 
+               permission_check pctxt fdctxt C_fd P_setattr; S_file sfs tagf \<in> ss; sf \<in> sfs;
+               permission_check pctxt (sectxt_of_sfile sf) C_file P_read; is_read_flag flags\<rbrakk>
+  \<Longrightarrow> (update_ss_shms ss (pi, pctxt,fds,shms) (tagp \<or> tagf)) \<in> static"
+| S_writef:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds; 
+               permission_check pctxt fdctxt C_fd P_setattr; sf \<in> sfs; S_file sfs tagf \<in> ss; 
+               permission_check pctxt (sectxt_of_sfile sf) C_file P_write; is_write_flag flags\<rbrakk>
+  \<Longrightarrow> (update_ss ss (S_file sfs tagf) (S_file sfs (tagp \<or> tagf))) \<in> static"
+| S_unlink:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss;  
+               (Init f,fsec,Some pfsec,asecs) \<in> sfs; 
+               search_check_s pctxt (Init f,fsec,Some pfsec,asecs) True; 
+               permission_check pctxt fsec C_file P_unlink; 
+               permission_check pctxt pfsec C_dir P_remove_name\<rbrakk>
+  \<Longrightarrow> ((ss - {S_file sfs tagf}) \<union> {S_file (sfs - {(Init f,fsec,Some pfsec,asecs)}) tagf}) \<in> static"
+| S_rmdir:   "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; 
+               S_dir (fi,fsec,Some pfsec,asecs) \<in> ss;  
+               search_check_s pctxt (fi,fsec,Some pfsec,asecs) False; 
+               permission_check pctxt fsec C_dir P_rmdir;
+               permission_check pctxt pfsec C_dir P_remove_name\<rbrakk>
+  \<Longrightarrow> (del_ss ss (S_dir (fi,fsec,Some pfsec,asecs))) \<in> static"
+| S_mkdir:   "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (fi,fsec,pfsec,asecs) \<in> ss;  
+               search_check_s pctxt (fi,fsec,pfsec,asecs) False; 
+               permission_check pctxt (nfctxt_create pctxt fsec C_dir) C_dir P_create;
+               permission_check pctxt fsec C_dir P_add_name\<rbrakk>
+  \<Longrightarrow> (add_ss ss (S_dir (Created,nfctxt_create pctxt fsec C_dir,Some fsec,asecs \<union> {fsec}))) \<in> static"
+| s_link:    "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (pfi,pfsec,ppfsec,asecs) \<in> ss;
+               S_file sfs tagf \<in> ss; sf \<in> sfs; nfsec = nfctxt_create pctxt pfsec C_file;  
+               search_check_s pctxt (pfi,pfsec,ppfsec,asecs) False; search_check_s pctxt sf True;
+               permission_check pctxt (sectxt_of_sfile sf) C_file P_link; 
+               permission_check pctxt pfsec C_dir P_add_name\<rbrakk>
+  \<Longrightarrow> (update_ss ss (S_file sfs tagf) 
+                  (S_file (sfs \<union> {(Created,nfsec,Some pfsec, asecs \<union> {pfsec})}) tagf)) \<in> static"
+| s_trunc:   "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss; sf \<in> sfs; 
+               search_check_s pctxt sf True; permission_check pctxt (sectxt_of_sfile sf) C_file P_setattr\<rbrakk>
+  \<Longrightarrow> (update_ss ss (S_file sfs tagf) (S_file sfs (tagf \<or> tagp))) \<in> static"
+(*
+| s_rename:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss;
+               (sf#spf') \<in> sfs; S_dir spf tagpf \<in> ss; \<not>((sf#spf') \<preceq> (sf#spf)); 
+               search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True; 
+               sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt;  
+               permission_check pctxt fctxt C_file P_rename;
+               permission_check pctxt pfctxt C_dir P_add_name;
+               ss_rename ss (sf#spf') (sf#spf) ss'; 
+               ss_rename_no_same_fname ss (sf#spf') (sf#spf)\<rbrakk>
+              \<Longrightarrow> ss' \<in> static"
+| s_rename': "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (sf#spf') tagf \<in> ss;
+               S_dir spf tagpf \<in> ss; \<not>((sf#spf') \<preceq> (sf#spf)); 
+               search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True; 
+               sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt;  
+               permission_check pctxt fctxt C_dir P_reparent;
+               permission_check pctxt pfctxt C_dir P_add_name;
+               ss_rename ss (sf#spf') (sf#spf) ss'; 
+               ss_rename_no_same_fname ss (sf#spf') (sf#spf)\<rbrakk>
+              \<Longrightarrow> ss' \<in> static"
+*)
+| s_createq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; 
+               permission_check pctxt pctxt C_msgq P_associate;
+               permission_check pctxt pctxt C_msgq P_create\<rbrakk>
+  \<Longrightarrow> (add_ss ss (S_msgq (Created,pctxt,[]))) \<in> static" 
+| s_sendmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss;
+               permission_check pctxt qctxt C_msgq P_enqueue;
+               permission_check pctxt qctxt C_msgq P_write; 
+               permission_check pctxt pctxt C_msg  P_create\<rbrakk>
+  \<Longrightarrow> (update_ss ss (S_msgq (qi,qctxt,sms)) 
+                    (S_msgq (qi,qctxt,sms @ [(Created, pctxt, tagp)]))) \<in> static"
+| s_recvmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; 
+               S_msgq (qi,qctxt,(mi,mctxt,tagm)#sms) \<in> ss;
+               permission_check pctxt qctxt C_msgq P_read; 
+               permission_check pctxt mctxt C_msg  P_receive\<rbrakk>
+  \<Longrightarrow> (update_ss_shms ss (pi,pctxt,fds,shms) (tagp \<or> tagm)) \<in> static"
+| s_removeq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss;
+               permission_check pctxt qctxt C_msgq P_destroy\<rbrakk>
+  \<Longrightarrow> (del_ss ss (S_msgq (qi,qctxt,sms))) \<in> static"
+| s_createh: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss;
+               permission_check pctxt pctxt C_shm P_associate; 
+               permission_check pctxt pctxt C_shm P_create\<rbrakk>
+   \<Longrightarrow> (add_ss ss (S_shm (Created, pctxt))) \<in> static"
+| s_attach:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm (hi,hctxt) \<in> ss;
+               if flag = SHM_RDONLY then permission_check pctxt hctxt C_shm P_read
+               else (permission_check pctxt hctxt C_shm P_read \<and>
+                     permission_check pctxt hctxt C_shm P_write)\<rbrakk>
+   \<Longrightarrow> (update_ss ss (S_proc (pi,pctxt,fds,shms) tagp)
+                    (S_proc (pi,pctxt,fds,shms \<union> {((hi,hctxt),flag)}) tagp)) \<in> static"
+| s_detach:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm sh \<in> ss;
+               (sh,flag) \<in> shms; \<not> is_many_sshm sh\<rbrakk>
+   \<Longrightarrow> (update_ss ss (S_proc (pi,pctxt,fds,shms) tagp)
+                    (S_proc (pi,pctxt,fds,shms - {(sh,flag)}) tagp)) \<in> static"
+| s_deleteh: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm (hi,hctxt) \<in> ss;
+               permission_check pctxt hctxt C_shm P_destroy; \<not> is_many_sshm sh\<rbrakk>
+   \<Longrightarrow> (remove_sproc_sshm (del_ss ss (S_shm (hi,hctxt))) (hi,hctxt)) \<in> static"
+
+(*
+fun smsg_related :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool" 
+where
+  "smsg_related m []                   = False" 
+| "smsg_related m ((mi, sec, tag)#sms) =  
+    (if (mi = Init m) then True else smsg_related m sms)" 
+
+fun smsgq_smsg_related :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsgq \<Rightarrow> bool"
+where
+  "smsgq_smsg_related q m (qi, sec, smsgslist) = ((qi = Init q) \<and> (smsg_related m smsgslist))"
+
+fun smsg_relatainted :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool"
+where
+  "smsg_relatainted m []                     = False"
+| "smsg_relatainted m ((mi, sec, tag)#sms) = 
+    (if (mi = Init m \<and> tag = True) then True else smsg_relatainted m sms)"
+
+fun smsgq_smsg_relatainted :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsgq \<Rightarrow> bool"
+where
+  "smsgq_smsg_relatainted q m (qi, sec, smsgslist) = 
+     ((qi = Init q) \<and> (smsg_relatainted m smsgslist))"
+*)
+
+fun sfile_related :: "t_sfile \<Rightarrow> t_file \<Rightarrow> bool"
+where
+  "sfile_related (fi,sec,psec,asecs) f = (fi = Init f)"
+(*
+fun sproc_related :: "t_process \<Rightarrow> t_sproc \<Rightarrow> bool"
+where
+  "sproc_related p (pi, sec, fds, shms) = (pi = Init p)"
+*)
+fun init_obj_related :: "t_sobject \<Rightarrow> t_object \<Rightarrow> bool"
+where
+  "init_obj_related (S_proc (Init p, sec, fds, shms) tag) (O_proc p') = (p = p')"
+| "init_obj_related (S_file sfs tag) (O_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)"
+| "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)"
+| "init_obj_related (S_msgq (Init q, sec, sms)) (O_msgq q') = (q = q')"
+| "init_obj_related (S_shm (Init h, sec)) (O_shm h') = (h = h')"
+| "init_obj_related (S_msg (Init q, sec, sms) (Init m, secm, tagm)) (O_msg q' m') = (q = q' \<and> m = m')"
+| "init_obj_related _ _ = False"
+
+fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool"
+where
+  "tainted_s ss (S_proc sp  tag) = (S_proc sp tag  \<in> ss \<and> tag = True)"
+| "tainted_s ss (S_file sfs tag) = (S_file sfs tag \<in> ss \<and> tag = True)"
+| "tainted_s ss (S_msg  (qi, sec, sms)  (mi, secm, tag)) = 
+     (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,sec,tag) \<in> set sms \<and> tag = True)"
+| "tainted_s ss _ = False"
+
+(*
+fun tainted_s :: "t_object \<Rightarrow> t_static_state \<Rightarrow> bool"
+where 
+  "tainted_s (O_proc p)  ss = (\<exists> sp. S_proc sp True \<in> ss \<and> sproc_related p sp)"
+| "tainted_s (O_file f)  ss = (\<exists> sfs sf. S_file sfs True \<in> ss \<and> sf \<in> sfs \<and> sfile_related f sf)"
+| "tainted_s (O_msg q m) ss = (\<exists> sq. S_msgq sq \<in> ss \<and> smsgq_smsg_relatainted q m sq)"
+| "tainted_s _           ss = False"
+*)
+
+definition taintable_s :: "t_object \<Rightarrow> bool"
+where
+  "taintable_s obj \<equiv> \<exists> ss \<in> static. \<exists> sobj. tainted_s ss sobj \<and> init_obj_related sobj obj \<and> init_alive obj"
+
+definition deletable_s :: "t_object \<Rightarrow> bool"
+where
+  "deletable_s obj \<equiv> init_alive obj \<and> (\<exists> ss \<in> static. \<forall> sobj \<in> ss. \<not> init_obj_related sobj obj)"
+
+definition undeletable_s :: "t_object \<Rightarrow> bool"
+where
+  "undeletable_s obj \<equiv> init_alive obj \<and> (\<forall> ss \<in> static. \<exists> sobj \<in> ss. init_obj_related sobj obj)"
+
+
+(**************** translation from dynamic to static *******************)
+
+definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> bool \<Rightarrow> t_sfile option"
+where
+  "cf2sfile s f Is_file \<equiv>
+     case (parent f) of 
+       None \<Rightarrow> if Is_file then None else Some sroot
+     | Some pf \<Rightarrow> if Is_file 
+     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)
+          | _ \<Rightarrow> None) 
+     else (case (sectxt_of_obj 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 (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"
+where
+  "cfs2sfiles s fs \<equiv> {sf. \<exists> f \<in> fs. cf2sfile s f True = Some sf}"
+
+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'}"
+
+(* 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 sf \<Rightarrow> Some (sec, flags, sf)
+                                        | _       \<Rightarrow> None)
+    | _ \<Rightarrow> None)"
+
+
+definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set"
+where
+  "cpfd2sfds s p \<equiv> {sfd. \<exists> fd sfd f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}"
+
+definition ch2sshm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_sshm option"
+where
+  "ch2sshm s h \<equiv> (case (sectxt_of_obj s (O_shm h)) of
+                    Some sec \<Rightarrow> 
+ Some (if (\<not> deleted (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec)
+                  | _ \<Rightarrow> None)"
+
+definition cph2spshs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set"
+where
+  "cph2spshs s p \<equiv> {(sh, flag) | sh flag h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}"
+
+definition cp2sproc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc option"
+where
+  "cp2sproc s p \<equiv> (case (sectxt_of_obj s (O_proc p)) of 
+                     Some sec \<Rightarrow> 
+ Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) then Init p else Created, sec, 
+       cpfd2sfds s p, cph2spshs s p)
+                   | _ \<Rightarrow> None)"
+
+definition cm2smsg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
+where
+  "cm2smsg s q m \<equiv> (case (sectxt_of_obj s (O_msg q m)) of 
+                      Some sec \<Rightarrow>
+ Some (if (\<not> deleted (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q)) then Init m else Created,
+       sec, O_msg q m \<in> tainted s)
+                    | _ \<Rightarrow> None)"
+
+fun cqm2sms:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option"
+where 
+  "cqm2sms s q [] = Some []"
+| "cqm2sms s q (m#ms) = 
+     (case (cqm2sms s q ms, cm2smsg s q m) of 
+       (Some sms, Some sm) \<Rightarrow> Some (sm#sms) 
+     | _ \<Rightarrow> None)"
+
+definition cq2smsgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_smsgq option"
+where
+  "cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of 
+                     (Some sec, Some sms) \<Rightarrow> 
+ Some (if (\<not> deleted (O_msgq q) s \<and> q \<in> init_msgqs) then Init q else Created,
+       sec, sms)
+                   | _ \<Rightarrow> None)"
+
+fun co2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject option"
+where
+  "co2sobj s (O_proc p) = 
+     (case (cp2sproc s p) of 
+        Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
+      | _       \<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))
+      else None)"
+| "co2sobj s (O_dir f) = 
+     (case (cf2sfile s f False) of
+        Some sf  \<Rightarrow> Some (S_dir sf)
+      | _ \<Rightarrow> None)"
+| "co2sobj s (O_msgq q) = 
+     (case (cq2smsgq s q) of
+        Some sq \<Rightarrow> Some (S_msgq sq)
+      | _ \<Rightarrow> None)"
+| "co2sobj s (O_shm h) = 
+     (case (ch2sshm s h) of 
+        Some sh \<Rightarrow> Some (S_shm sh)
+      | _ \<Rightarrow> None)"
+| "co2sobj s (O_msg q m) = 
+     (case (cq2smsgq s q, cm2smsg s q m) of 
+       (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
+     | _ \<Rightarrow> None)"
+| "co2sobj s _ = None"
+
+
+(***************** for backward proof when Instancing static objects ******************)
+
+definition next_nat :: "nat set \<Rightarrow> nat"
+where
+  "next_nat nset = (Max nset) + 1"
+
+definition new_proc :: "t_state \<Rightarrow> t_process"
+where 
+  "new_proc \<tau> = next_nat (current_procs \<tau>)"
+
+definition new_inode_num :: "t_state \<Rightarrow> nat"
+where
+  "new_inode_num \<tau> = next_nat (current_inode_nums \<tau>)"
+
+definition new_msgq :: "t_state \<Rightarrow> t_msgq"
+where
+  "new_msgq s = next_nat (current_msgqs s)"
+
+definition new_msg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> nat"
+where
+  "new_msg s q = next_nat (set (msgs_of_queue s q))"
+
+definition new_shm :: "t_state \<Rightarrow> nat"
+where
+  "new_shm \<tau> = next_nat (current_shms \<tau>)"
+
+definition new_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd"
+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_fname set"
+where
+  "all_fname_under_dir d \<tau> = {fn. \<exists> f. fn # d = f \<and> f \<in> current_files \<tau>}"
+
+fun fname_all_a:: "nat \<Rightarrow> t_fname"
+where
+  "fname_all_a 0 = []" |
+  "fname_all_a (Suc n) = ''a''@(fname_all_a n)"
+
+definition fname_length_set :: "t_fname set \<Rightarrow> nat set"
+where
+  "fname_length_set fns = length`fns"
+
+definition next_fname:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname"
+where
+  "next_fname pf \<tau> = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf \<tau>))) + 1)"
+
+definition new_childf:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file"
+where
+  "new_childf pf \<tau> = next_fname pf \<tau> # pf"
+
+definition s2ss :: "t_state \<Rightarrow> t_static_state"
+where
+  "s2ss s \<equiv> {sobj. \<exists> obj. alive s obj \<and> co2sobj s obj = Some sobj}"
+
+end
+
+end
\ No newline at end of file




