diff -r 042e1e7fd505 -r b7fd75d104bf no_shm_selinux/Enrich2.thy
--- a/no_shm_selinux/Enrich2.thy	Thu Jan 09 22:53:45 2014 +0800
+++ b/no_shm_selinux/Enrich2.thy	Thu Jan 16 11:04:04 2014 +0800
@@ -1,43 +1,371 @@
 theory Enrich2
 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2
- Temp Enrich Proc_fd_of_file_prop
+ Temp Enrich Proc_fd_of_file_prop New_obj_prop
 begin
 
+fun assoc :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option"
+where
+  "assoc [] a = None"
+| "assoc (e # l) a = (if (fst e = a) then Some (snd e) else assoc l a)"
+
+context flask begin
+
+lemma sock_inum_eq_prop:
+  "\<lbrakk>inum_of_socket s (p, fd) = Some im; inum_of_socket s (p', fd') = Some im; valid s\<rbrakk>
+   \<Longrightarrow> (p' = p \<and> fd' = fd)"
+apply (induct s arbitrary:p p')
+apply (simp) defer
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto split:if_splits option.splits simp:proc_file_fds_def)
+sorry
+
+lemma inums_execve:
+  "valid (Execve p f fds # s) \<Longrightarrow>  
+     current_inode_nums (Execve p f fds # s) = current_inode_nums s - 
+     {inum. \<exists> fd. inum_of_socket s (p, fd) = Some inum}"
+apply (frule vt_grant_os, frule vd_cons)
+apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def
+  dest:filefd_socket_conflict fim_noninter_sim' dest:fim_noninter_sim'' sock_inum_eq_prop)
+apply (drule set_mp, simp, simp, erule exE, drule filefd_socket_conflict, 
+  simp add:current_sockets_def, simp, simp)+
+apply (case_tac "a = p", simp)
+apply (auto)
+done
+
+lemma inums_clone:
+  "valid (Clone p p' fds # s) \<Longrightarrow> 
+     current_inode_nums (Clone p p' fds # s) = current_inode_nums s"
+apply (frule vt_grant_os, frule vd_cons)
+apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def
+  dest:filefd_socket_conflict fim_noninter_sim' dest:fim_noninter_sim'' sock_inum_eq_prop)
+apply (case_tac "a = p'")
+apply (subgoal_tac "(p', b) \<in> current_sockets s")
+apply (drule cn_in_curp, simp, simp, simp add:current_sockets_def)
+apply auto
+done
+
+lemma inums_kill:
+  "valid (Kill p p' # s) \<Longrightarrow> current_inode_nums (Kill p p' # s) = current_inode_nums s - 
+     {inum. \<exists> fd. inum_of_socket s (p', fd) = Some inum}"
+apply (frule vt_grant_os, frule vd_cons)
+apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def
+  dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop)
+done
+
+lemma inums_exit:
+  "valid (Exit p # s) \<Longrightarrow> current_inode_nums (Exit p # s) = current_inode_nums s -
+     {inum. \<exists> fd. inum_of_socket s (p, fd) = Some inum}"
+apply (frule vt_grant_os, frule vd_cons)
+apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def
+  dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop)
+done
+
+lemma inums_ptrace:
+  "current_inode_nums (Ptrace p p' # s) = current_inode_nums s"
+apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def
+  dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop)
+done
+
+lemma inums_open:
+  "valid (Open p f flags fd opt # s) \<Longrightarrow> 
+    current_inode_nums (Open p f flags fd opt # s) = (
+     case opt of
+       None \<Rightarrow> current_inode_nums s
+     | Some i \<Rightarrow> current_inode_nums s \<union> {i})"
+apply (frule vt_grant_os, frule vd_cons)
+apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def
+  dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop split:option.splits)
+apply (case_tac "fa = f", simp add:current_files_def)
+apply (rule_tac x = fa in exI, auto)
+done
+
+lemma inums_readfile:
+  "current_inode_nums (ReadFile p fd # s) = current_inode_nums s"
+apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def)  
+done
+
+lemma inums_writefile:
+  "current_inode_nums (WriteFile p fd # s) = current_inode_nums s"
+apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def)  
+done
+
+lemma inums_mkdir:
+  "valid (Mkdir p f inum # s) \<Longrightarrow> current_inode_nums (Mkdir p f inum # s) = current_inode_nums s \<union> {inum}"
+apply (frule vt_grant_os, frule vd_cons)
+apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def
+  dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop split:option.splits)
+apply (case_tac "fa = f", simp add:current_files_def)
+apply (rule_tac x = fa in exI, auto)
+done
+
+lemma inums_linkhard:
+  "valid (LinkHard p f f' # s) \<Longrightarrow> current_inode_nums (LinkHard p f f' # s) = current_inode_nums s"
+apply (frule vt_grant_os, frule vd_cons)
+apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def
+  dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop split:option.splits)
+apply (case_tac "fa = f'", simp add:current_files_def)
+apply (rule_tac x = fa in exI, auto)
+done 
+
+lemma inums_truncate:
+  "current_inode_nums (Truncate p f len # s) = current_inode_nums s"
+apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def)  
+done
+
+lemma inums_createmsgq:
+  "current_inode_nums (CreateMsgq p q # s) = current_inode_nums s"
+by (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def)  
+
+lemma inums_sendmsg:
+  "current_inode_nums (SendMsg p q m # s) = current_inode_nums s"
+by (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def)  
+
+lemma inums_recvmsg:
+  "current_inode_nums (RecvMsg p q m # s) = current_inode_nums s"
+by (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def)  
+
+lemma inums_removemsgq:
+  "current_inode_nums (RemoveMsgq p q # s) = current_inode_nums s"
+by (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def)  
+
+lemma inums_bind:
+  "valid (Bind p fd addr # s) \<Longrightarrow> current_inode_nums (Bind p fd addr # s) = current_inode_nums s"
+by (auto dest:vt_grant)
+
+lemma inums_connect:
+  "valid (Connect p fd addr # s) \<Longrightarrow> current_inode_nums (Connect p fd addr # s) = current_inode_nums s"
+by (auto dest:vt_grant)
+
+lemma inums_listen:
+  "valid (Listen p fd # s) \<Longrightarrow> current_inode_nums (Listen p fd # s) = current_inode_nums s"
+by (auto dest:vt_grant)
+
+lemma inums_sendsock:
+  "valid (SendSock p fd # s) \<Longrightarrow> current_inode_nums (SendSock p fd # s) = current_inode_nums s"
+by (auto dest:vt_grant)
+
+lemma inums_recvsock:
+  "valid (RecvSock p fd # s) \<Longrightarrow> current_inode_nums (RecvSock p fd # s) = current_inode_nums s"
+by (auto dest:vt_grant)
+
+lemma inums_shutdown:
+  "valid (Shutdown p fd how # s) \<Longrightarrow> current_inode_nums (Shutdown p fd how # s) = current_inode_nums s"
+by (auto dest:vt_grant)
+
+lemma inums_createsock:
+  "valid (CreateSock p af st fd inum # s) \<Longrightarrow> current_inode_nums (CreateSock p af st fd inum # s) = 
+     current_inode_nums s"
+by (auto dest:vt_grant)
+
+lemma inums_accept:
+  "valid (Accept p fd addr port fd inum # s) \<Longrightarrow> current_inode_nums (Accept p fd addr port fd inum # s) = 
+     current_inode_nums s"
+by (auto dest:vt_grant)
+
+lemmas current_inode_nums_simps = inums_execve inums_open inums_mkdir 
+  inums_linkhard inums_createmsgq inums_sendmsg
+  inums_createsock inums_accept inums_clone inums_kill inums_ptrace inums_exit inums_readfile
+  inums_writefile inums_truncate inums_recvmsg inums_removemsgq
+  inums_bind inums_connect inums_listen inums_sendsock
+  inums_recvsock inums_shutdown
+
+end
+
 context tainting_s begin
 
-fun new_cf :: "t_state \<Rightarrow> t_file set \<Rightarrow> t_file \<Rightarrow> t_file"
+fun new_cf :: "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"
+  "new_cf fs []     = []"
+| "new_cf fs (f#pf) = new_childf_general pf fs"
 
-fun enrich_dufs:: "t_state \<Rightarrow> t_file \<Rightarrow> t_state \<Rightarrow> (t_file \<times> t_file) list"
+lemma new_cf_notin_fs:
+  "\<lbrakk>finite fs; f \<noteq> []\<rbrakk> \<Longrightarrow> new_cf fs f \<notin> fs"
+apply (case_tac f, simp)
+apply (auto simp:ncf_notin_curf_general)
+done
+
+fun enrich_dufs:: "t_state \<Rightarrow> t_file set \<Rightarrow> t_file set \<Rightarrow> (t_file \<times> t_file) list"
 where
-  "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'"
+  "enrich_dufs [] sames curfs = []"
+| "enrich_dufs (Open p f flags fd opt # s) sames curfs = 
+    (if (f \<in> sames \<and> opt \<noteq> None) 
+     then (f, new_cf (curfs \<union> set (map snd (enrich_dufs s sames curfs))) f) # enrich_dufs s sames curfs
+     else enrich_dufs s sames curfs)"
+| "enrich_dufs (LinkHard p f f' # s) sames curfs = 
+    (if (f' \<in> sames) 
+     then (f', new_cf (curfs \<union> set (map snd (enrich_dufs s sames curfs))) f') # enrich_dufs s sames curfs
+     else enrich_dufs s sames curfs)"
+| "enrich_dufs (_ # s) sames curfs = enrich_dufs s sames curfs"
+
+lemma enrich_dufs_sameinodes1:
+  "set (map fst (enrich_dufs s sames curfs)) \<subseteq> sames"
+apply (induct s, simp)
+by (case_tac a, auto)
 
 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)
+  "\<lbrakk>valid s; \<forall> f \<in> sames. f \<notin> init_files; no_del_event s\<rbrakk> 
+   \<Longrightarrow> set (map fst (enrich_dufs s sames curfs)) = sames \<inter> {f. is_file s f} "
+apply (induct s)
+apply (auto simp:is_file_nil is_init_file_props current_files_simps)[1]
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto simp:is_file_simps is_file_in_current current_files_simps 
+  same_inode_files_simps split:option.splits if_splits)
+done
+
+lemma finite_enrich_nfs:
+  "finite (snd ` set (enrich_dufs s sames curfs))"
+by (auto)
 
-apply (erule enrich_dufs.induct)
+lemma new_cf_enrich:
+  "\<lbrakk>finite curfs; f \<noteq> []\<rbrakk> \<Longrightarrow> new_cf (curfs \<union> snd ` set (enrich_dufs s sames curfs)) f \<notin> curfs \<union> snd ` set (enrich_dufs s sames curfs)"
+using finite_enrich_nfs[where s = s and sames =sames and curfs = curfs]
+apply (drule_tac F = curfs and G = "snd ` set (enrich_dufs s sames curfs)" in finite_UnI, simp)
+apply (rule new_cf_notin_fs, simp+)
+done
+
+lemma enrich_dufs_nfs:
+  "\<lbrakk>finite curfs; [] \<notin> sames\<rbrakk>
+   \<Longrightarrow> set (map snd (enrich_dufs s sames curfs)) \<inter> curfs = {}"
+apply (induct s)
+apply (simp)
+apply ( case_tac a)
+apply (auto simp:is_file_in_current)
+apply (drule_tac f = list and sames = sames and curfs = curfs and s = s in new_cf_enrich)
+apply (rule notI, simp+)
+apply (drule_tac f = list2 and sames = sames and curfs = curfs and s = s in new_cf_enrich)
+apply (rule notI, simp+)
+done
+
+lemma pair_list_set: "(a, b) \<in> set l \<Longrightarrow> b \<in> snd ` set l"
+by (induct l, auto)
 
-fun enrich_file :: "t_state \<Rightarrow> t_file \<Rightarrow> t_inode_num \<Rightarrow> t_state \<Rightarrow> (t_file set \<times> t_state)"
+lemma enrich_dufs_nfs_distinct:
+  "\<lbrakk>finite curfs; [] \<notin> sames\<rbrakk> \<Longrightarrow> distinct (map snd (enrich_dufs s sames curfs))"
+apply (induct s, simp)
+apply (case_tac a, auto)
+apply (drule pair_list_set)
+apply (drule_tac f = list and s = s and sames = sames and curfs = curfs in new_cf_enrich)
+apply (rule notI, simp, simp)
+apply (drule pair_list_set)
+apply (drule_tac f = list2 and s = s and sames = sames and curfs = curfs in new_cf_enrich)
+apply (rule notI, simp, simp)
+done
+
+fun all_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set"
 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"
+  "all_fds [] = init_fds_of_proc"
+| "all_fds (Open p f flags fd ipt # s) = (all_fds s) (p := all_fds s p \<union> {fd})" (*
+| "all_fds (CreateSock p sf st fd i # s) = (all_fds s) (p := all_fds s p \<union> {fd})"
+| "all_fds (Accept p fd' raddr port fd i # s) = (all_fds s) (p := all_fds s p \<union> {fd})" *)
+| "all_fds (Clone p p' fds # s) = (all_fds s) (p' := fds)"
+| "all_fds (_ # s) = all_fds s"
+
+fun enrich_dufds :: "t_state \<Rightarrow> t_file set \<Rightarrow> (t_process \<Rightarrow> t_fd set) \<Rightarrow> (t_state \<times> t_fd) list"
+where 
+  "enrich_dufds [] sames allpfds = []"
+| "enrich_dufds (Open p f flags fd opt # s) sames allpfds = 
+    (if (f \<in> sames) 
+     then (Open p f flags fd opt # s, next_nat (allpfds p \<union> set (map snd (enrich_dufds s sames allpfds)))) #
+          (enrich_dufds s sames allpfds)
+     else enrich_dufds s sames allpfds)"
+| "enrich_dufds (e # s) sames allpfds = enrich_dufds s sames allpfds"
+
+fun index_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_state"
+where
+  "index_fd [] p fd = []"
+| "index_fd (Open p f flags fd opt # s) p' fd' = 
+    (if (p' = p \<and> fd' = fd) then Open p f flags fd opt # s
+     else index_fd s p' fd')"
+| "index_fd (e # s) p fd = index_fd s p fd"
+
+definition enrich_fdset :: "t_state \<Rightarrow> (t_state \<times> t_fd) list \<Rightarrow> t_process \<Rightarrow> t_fd set \<Rightarrow> t_fd set"
+where
+  "enrich_fdset s dufds p fds \<equiv> 
+    fds \<union> {fd'. \<exists> fd \<in> fds. assoc dufds (index_fd s p fd) = Some fd'}"
 
 
+fun enrich_file :: "t_state \<Rightarrow> t_inode_num \<Rightarrow> (t_file \<times> t_file) list 
+  \<Rightarrow> ((t_file \<times> t_process \<times> t_fd) \<times> t_fd) list \<Rightarrow> t_state"
+where
+  "enrich_file [] inum dufs dufds = []"
+| "enrich_file (Open p f flags fd None # s) inum dufs dufds = 
+    (case (assoc dufds (Open p f flags fd None # s), assoc dufs f) of
+       (Some fd', Some f') \<Rightarrow> Open p f' flags fd' None # Open p f flags fd None # enrich_file s inum dufs dufds
+     | _                   \<Rightarrow> Open p f flags fd None # (enrich_file s inum dufs dufds))"
+| "enrich_file (Open p f flags fd (Some inum) # s) inum' dufs dufds = 
+    (case (assoc dufs f, assoc dufds (f, p, fd)) of
+        (Some f', Some fd') \<Rightarrow> Open p f' flags fd' (Some inum') # Open p f flags fd (Some inum) #
+                               enrich_file s inum dufs dufds
+    | _ \<Rightarrow> Open p f flags fd (Some inum) # enrich_file s inum dufs dufds)"
+| "enrich_file (LinkHard p f f' # s) inum dufs dufds = 
+    (case (assoc dufs f, assoc dufs f') of
+       (Some df, Some df') \<Rightarrow> LinkHard p df df' # LinkHard p f f' # enrich_file s inum dufs dufds
+     | _ \<Rightarrow> LinkHard p f f' # enrich_file s inum dufs dufds)"
+| "enrich_file (Clone p p' fds # s) inum dufs dufds = 
+    Clone p p' (enrich_fdset s dufds p fds) # (enrich_file s inum dufs dufds)" 
+| "enrich_file (Execve p f fds # s) inum dufs dufds = 
+    Execve p f (enrich_fdset s dufds p fds) # (enrich_file s inum dufs dufds)"    
+| "enrich_file (WriteFile p fd # s) inum dufs dufds = 
+    (case (file_of_proc_fd s p fd) of 
+       Some f \<Rightarrow> (case (assoc dufds (f, p, fd)) of
+                    Some fd' \<Rightarrow> WriteFile p fd' # WriteFile p fd # enrich_file s inum dufs dufds
+                  | _        \<Rightarrow> WriteFile p fd # enrich_file s inum dufs dufds)
+    | _       \<Rightarrow> [])"
+| "enrich_file (e # s) inum dufs dufds = e # enrich_file s inum dufs dufds"
+
+definition same_inodes_list :: "t_state \<Rightarrow> t_file list \<Rightarrow> bool"
+where
+  "same_inodes_list s flist \<equiv> flist \<noteq> [] \<and> set flist = same_inode_files s (hd flist)"
+
+lemma assoc_dufs_prop1:
+  "\<lbrakk>\<forall> f \<in> set (map snd dufs). f \<notin> current_files s; assoc dufs f = Some f'\<rbrakk> \<Longrightarrow> f' \<notin> current_files s"
+apply (erule_tac x = "f'" in ballE)
+apply auto
+apply (induct dufs, auto split:if_splits)
+done
+
+
+lemma enrich_file_dufs_inode_aux1:
+  "\<lbrakk>no_del_event s; valid s; f \<in> current_files s; \<And> f f'. assoc dufs f = Some f' \<Longrightarrow> f' \<notin> current_files s\<rbrakk> 
+   \<Longrightarrow> inum_of_file (enrich_file s inum dufs) f = inum_of_file s f"
+apply (induct s arbitrary:f, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto split:option.splits simp:current_files_simps dest:is_file_in_current is_dir_in_current)
+done
+
+lemma enrich_file_dufs_inode1:
+  "\<lbrakk>no_del_event s; valid s; f \<in> current_files s; \<forall> f \<in> set (map snd dufs). f \<notin> current_files s\<rbrakk> 
+   \<Longrightarrow> inum_of_file (enrich_file s inum dufs) f = inum_of_file s f"
+apply (erule enrich_file_dufs_inode_aux1)
+apply (simp, simp)
+apply (erule assoc_dufs_prop1, simp+)
+done
+
+lemma enrich_file_dufs_inode2:
+  "\<lbrakk>no_del_event s; valid s; is_file s f; f \<notin> init_files; assoc dufs f = Some f';
+    \<And> f f'. assoc dufs f = Some f' \<Longrightarrow> f' \<notin> current_files s;    
+    \<And> f f'. assoc dufs f = Some f' \<Longrightarrow> inum_of_file s f' = None\<rbrakk> 
+   \<Longrightarrow> inum_of_file (enrich_file s inum dufs) f' = Some inum"
+apply (induct s arbitrary:f f', simp) defer
+apply(frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto split:option.splits if_splits
+ simp:current_files_simps  current_inode_nums_simps is_file_simps
+dest:is_file_in_current is_dir_in_current)
+
+
+lemma enrich_file_dufs_sameinodes:
+  "\<lbrakk>same_inodes_list s (map fst dufs); \<forall> f \<in> set (map fst dufs). f \<notin> init_files; inum \<notin> current_inode_nums s; 
+    distinct (map snd dufs); \<forall> f \<in> set (map snd dufs). f \<notin> current_files s; valid s\<rbrakk> 
+   \<Longrightarrow> same_inodes_list (enrich_file s inum dufs) (map snd dufs)"
+apply (induct s) apply (simp add:same_inodes_list_def same_inode_files_simps)
+defer
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto simp:same_inodes_list_def same_inode_files_simps)
+
+
+
+lemma enrich_dufs_fst:
+  "\<lbrakk>valid s; "
 
 
 lemma enrich_msgq_s2ss: