diff -r 924ab7a4e7fa -r 271e9818b6f6 simple_selinux/Temp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/simple_selinux/Temp.thy	Mon Dec 02 10:52:40 2013 +0800
@@ -0,0 +1,233 @@
+theory Temp
+imports Static_type OS_type_def Flask_type Flask Static
+begin
+
+context tainting_s
+
+begin
+
+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}"
+
+
+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 (update_ss_shms ss (pi,pctxt,fds,shms) (tagp \<or> tagm)) 
+                 (S_msgq (qi, qctxt, (mi, mctxt, tagm)#sms))
+                 (S_msgq (qi, qctxt, sms))) \<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 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,secm,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"
+
+(* this definition is wrong, cause process can exited from static-world 
+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)"
+*)
+
+fun deleted_s :: "t_sproc \<Rightarrow> t_object \<Rightarrow> bool"
+where
+  "deleted_s (pi, pctxt, fds, shms) (O_proc p) = (pi \<noteq> Init p \<and> permission_check pctxt  "
+
+definition deletable_s :: "t_object \<Rightarrow> bool"
+  "deletable_s obj \<equiv> init_alive obj \<and> (\<exists> ss \<in> static. \<exists> sp tagp. S_proc sp tagp \<in> ss \<and> deleted_s sp 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)"
+
+definition init_ss_eq:: "t_static_state \<Rightarrow> t_static_state \<Rightarrow> bool" (infix "\<doteq>" 100)
+where
+  "ss \<doteq> ss' \<equiv> ss \<subseteq> ss' \<and> {sobj. is_init_sobj sobj \<and> sobj \<in> ss'} \<subseteq> ss"
+
+lemma [simp]: "ss \<doteq> ss"
+by (auto simp:init_ss_eq_def)
+
+definition init_ss_in:: "t_static_state \<Rightarrow> t_static_state set \<Rightarrow> bool" (infix "\<propto>" 101)
+where
+  "ss \<propto> sss \<equiv> \<exists> ss' \<in> sss. ss \<doteq> ss'"
+
+lemma s2ss_included_sobj:
+  "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)"
+by (simp add:s2ss_def, rule_tac x = obj in exI, simp)
+
+lemma init_ss_in_prop:
+  "\<lbrakk>s2ss s \<propto> static; co2sobj s obj = Some sobj; alive s obj; init_obj_related sobj obj\<rbrakk>
+   \<Longrightarrow> \<exists> ss \<in> static. sobj \<in> ss"
+apply (simp add:init_ss_in_def init_ss_eq_def)
+apply (erule bexE, erule conjE)
+apply (rule_tac x = ss' in bexI, auto dest!:s2ss_included_sobj)
+done
+
+
+
+
+end
+
+end
\ No newline at end of file