1 theory Temp

     2 imports Static_type OS_type_def Flask_type Flask Static

     3 begin

     4 

     5 context tainting_s

     6 

     7 begin

     8 

     9 definition update_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"

    10 where

    11   "update_ss ss so so' \<equiv> if (is_many so) then ss \<union> {so'} else (ss - {so}) \<union> {so'}"

    12 

    13 definition add_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state"

    14 where

    15   "add_ss ss so \<equiv> ss \<union> {so}"

    16 

    17 definition del_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state"

    18 where

    19   "del_ss ss so \<equiv> if (is_many so) then ss else ss - {so}"

    20 

    21 (* all reachable static states(sobjects set) *)

    22 inductive_set static :: "t_static_state set"

    23 where

    24   s_init:    "init_static_state \<in> static"

    25 | s_execve:  "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds) tagp \<in> ss; S_file sfs tagf \<in> ss;

    26                (fi,fsec,pfsec,asecs) \<in> sfs; npctxt_execve pctxt fsec = Some pctxt';

    27                grant_execve pctxt fsec pctxt'; search_check_s pctxt (fi,fsec,pfsec,asecs) True; 

    28                inherit_fds_check_s pctxt' fds'; fds' \<subseteq> fds\<rbrakk>

    29   \<Longrightarrow> (update_ss ss (S_proc (pi, pctxt, fds) tagp) 

    30                     (S_proc (pi, pctxt', fds') (tagp \<or> tagf))) \<in> static"

    31 | s_clone:   "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds) tagp \<in> ss; 

    32                permission_check pctxt pctxt C_process P_fork;

    33                inherit_fds_check_s pctxt fds'; fds' \<subseteq> fds\<rbrakk>

    34   \<Longrightarrow> (add_ss ss (S_proc (Created, pctxt, fds') tagp)) \<in> static"

    35 (*

    36 | s_kill:    "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds) tagp \<in> ss; 

    37                S_proc (pi', pctxt', fds') tagp' \<in> ss; 

    38                permission_check pctxt pctxt' C_process P_sigkill\<rbrakk>

    39   \<Longrightarrow> (del_ss ss (S_proc (pi', pctxt', fds', shms') tagp')) \<in> static"

    40 *)

    41 | s_ptrace:  "\<lbrakk>ss \<in> static; S_proc sp False \<in> ss; S_proc sp' True \<in> ss; 

    42                permission_check (sextxt_of_sproc sp) (sectxt_of_sproc sp') C_process P_ptrace\<rbrakk>

    43   \<Longrightarrow> (update_ss ss (S_proc sp False) (S_proc sp True)) \<in> static"

    44 | s_ptrace': "\<lbrakk>ss \<in> static; S_proc sp True \<in> ss; S_proc sp' False \<in> ss; 

    45                permission_check (sextxt_of_sproc sp) (sectxt_of_sproc sp') C_process P_ptrace\<rbrakk>

    46   \<Longrightarrow> (update_ss ss (S_proc sp' False) (S_proc sp' True)) \<in> static"

    47 (*

    48 | s_exit:    "\<lbrakk>ss \<in> static; S_proc sp tagp \<in> ss\<rbrakk> \<Longrightarrow> (del_ss ss (S_proc sp tagp)) \<in> static"

    49 *)

    50 | s_open:    "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds) tagp \<in> ss; S_file sfs tagf \<in> ss; sf \<in> sfs;

    51               search_check_s pctxt sf True; \<not> is_creat_excl_flag flags; 

    52               oflags_check flags pctxt (sectxt_of_sfile sf); permission_check pctxt pctxt C_fd P_setattr\<rbrakk>

    53   \<Longrightarrow> (update_ss ss (S_proc (pi, pctxt, fds) tagp)

    54                     (S_proc (pi, pctxt, fds \<union> {(pctxt,flags,sf)}) tagp)) \<in> static"

    55 | s_open':   "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds) tagp \<in> ss; is_creat_excl_flag flags;

    56                S_dir (pfi,fsec,pfsec,asecs) \<in> ss; search_check_s pctxt (pfi,fsec,pfsec,asecs) False; 

    57                nfsec = nfctxt_create pctxt fsec C_file; oflags_check flags pctxt nfsec;

    58                permission_check pctxt fsec C_dir P_add_rename; permission_check pctxt pctxt C_fd P_setattr\<rbrakk>

    59   \<Longrightarrow> (update_ss (add_ss ss (S_file {(Created, nfsec, Some fsec, asecs \<union> {fsec})} tagp))

    60          (S_proc (pi, pctxt, fds) tagp)

    61          (S_proc (pi, pctxt, fds \<union> {(pctxt, flags, (Created, nfsec, Some fsec, asecs \<union> {fsec}))}) tagp)

    62       ) \<in> static"

    63 | S_readf:   "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) False \<in> ss; (fdctxt,flags,sf) \<in> fds; 

    64                permission_check pctxt fdctxt C_fd P_setattr; S_file sfs True \<in> ss; sf \<in> sfs;

    65                permission_check pctxt (sectxt_of_sfile sf) C_file P_read; is_read_flag flags\<rbrakk>

    66   \<Longrightarrow> (update_ss ss (S_proc (pi, pctxt,fds) False) (S_proc (pi, pctxt, fds) True)) \<in> static"

    67 | S_writef:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) True \<in> ss; (fdctxt,flags,sf) \<in> fds; 

    68                permission_check pctxt fdctxt C_fd P_setattr; sf \<in> sfs; S_file sfs False \<in> ss; 

    69                permission_check pctxt (sectxt_of_sfile sf) C_file P_write; is_write_flag flags\<rbrakk>

    70   \<Longrightarrow> (update_ss ss (S_file sfs False) (S_file sfs True)) \<in> static"

    71 (*

    72 | S_unlink:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss;  

    73                (Init f,fsec,Some pfsec,asecs) \<in> sfs; 

    74                search_check_s pctxt (Init f,fsec,Some pfsec,asecs) True; 

    75                permission_check pctxt fsec C_file P_unlink; 

    76                permission_check pctxt pfsec C_dir P_remove_name\<rbrakk>

    77   \<Longrightarrow> ((ss - {S_file sfs tagf}) \<union> {S_file (sfs - {(Init f,fsec,Some pfsec,asecs)}) tagf}) \<in> static"

    78 | S_rmdir:   "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; 

    79                S_dir (fi,fsec,Some pfsec,asecs) \<in> ss;  

    80                search_check_s pctxt (fi,fsec,Some pfsec,asecs) False; 

    81                permission_check pctxt fsec C_dir P_rmdir;

    82                permission_check pctxt pfsec C_dir P_remove_name\<rbrakk>

    83   \<Longrightarrow> (del_ss ss (S_dir (fi,fsec,Some pfsec,asecs))) \<in> static"

    84 *)

    85 | S_mkdir:   "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss; S_dir (fi,fsec,pfsec,asecs) \<in> ss;  

    86                search_check_s pctxt (fi,fsec,pfsec,asecs) False; 

    87                permission_check pctxt (nfctxt_create pctxt fsec C_dir) C_dir P_create;

    88                permission_check pctxt fsec C_dir P_add_name\<rbrakk>

    89   \<Longrightarrow> (add_ss ss (S_dir (Created,nfctxt_create pctxt fsec C_dir,Some fsec,asecs \<union> {fsec}))) \<in> static"

    90 | s_link:    "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss; S_dir (pfi,pfsec,ppfsec,asecs) \<in> ss;

    91                S_file sfs tagf \<in> ss; sf \<in> sfs; nfsec = nfctxt_create pctxt pfsec C_file;  

    92                search_check_s pctxt (pfi,pfsec,ppfsec,asecs) False; search_check_s pctxt sf True;

    93                permission_check pctxt (sectxt_of_sfile sf) C_file P_link; 

    94                permission_check pctxt pfsec C_dir P_add_name\<rbrakk>

    95   \<Longrightarrow> (update_ss ss (S_file sfs tagf) 

    96                   (S_file (sfs \<union> {(Created,nfsec,Some pfsec, asecs \<union> {pfsec})}) tagf)) \<in> static"

    97 | s_trunc:   "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) True \<in> ss; S_file sfs False \<in> ss; sf \<in> sfs; 

    98                search_check_s pctxt sf True; permission_check pctxt (sectxt_of_sfile sf) C_file P_setattr\<rbrakk>

    99   \<Longrightarrow> (update_ss ss (S_file sfs False) (S_file sfs True)) \<in> static"

   100 (*

   101 | s_rename:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss; S_file sfs tagf \<in> ss;

   102                (sf#spf') \<in> sfs; S_dir spf tagpf \<in> ss; \<not>((sf#spf') \<preceq> (sf#spf)); 

   103                search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True; 

   104                sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt;  

   105                permission_check pctxt fctxt C_file P_rename;

   106                permission_check pctxt pfctxt C_dir P_add_name;

   107                ss_rename ss (sf#spf') (sf#spf) ss'; 

   108                ss_rename_no_same_fname ss (sf#spf') (sf#spf)\<rbrakk>

   109               \<Longrightarrow> ss' \<in> static"

   110 | s_rename': "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss; S_dir (sf#spf') tagf \<in> ss;

   111                S_dir spf tagpf \<in> ss; \<not>((sf#spf') \<preceq> (sf#spf)); 

   112                search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True; 

   113                sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt;  

   114                permission_check pctxt fctxt C_dir P_reparent;

   115                permission_check pctxt pfctxt C_dir P_add_name;

   116                ss_rename ss (sf#spf') (sf#spf) ss'; 

   117                ss_rename_no_same_fname ss (sf#spf') (sf#spf)\<rbrakk>

   118               \<Longrightarrow> ss' \<in> static"

   119 *)

   120 | s_createq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss; 

   121                permission_check pctxt pctxt C_msgq P_associate;

   122                permission_check pctxt pctxt C_msgq P_create\<rbrakk>

   123   \<Longrightarrow> (add_ss ss (S_msgq (Created,pctxt,[]))) \<in> static" 

   124 | s_sendmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss;

   125                permission_check pctxt qctxt C_msgq P_enqueue;

   126                permission_check pctxt qctxt C_msgq P_write; 

   127                permission_check pctxt pctxt C_msg  P_create\<rbrakk>

   128   \<Longrightarrow> (update_ss ss (S_msgq (qi,qctxt,sms)) 

   129                     (S_msgq (qi,qctxt,sms @ [(Created, pctxt, tagp)]))) \<in> static"

   130 | s_recvmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss; 

   131                S_msgq (qi,qctxt,(mi,mctxt,tagm)#sms) \<in> ss;

   132                permission_check pctxt qctxt C_msgq P_read; 

   133                permission_check pctxt mctxt C_msg  P_receive\<rbrakk>

   134   \<Longrightarrow> (update_ss (update_ss ss (S_proc (pi,pctxt,fds) tagp) (S_proc (pi, pctxt, fds) (tagp \<or> tagm))) 

   135                  (S_msgq (qi, qctxt, (mi, mctxt, tagm)#sms))

   136                  (S_msgq (qi, qctxt, sms))) \<in> static"

   137 (*

   138 | s_removeq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss;

   139                permission_check pctxt qctxt C_msgq P_destroy\<rbrakk>

   140   \<Longrightarrow> (del_ss ss (S_msgq (qi,qctxt,sms))) \<in> static"

   141 | s_createh: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss;

   142                permission_check pctxt pctxt C_shm P_associate; 

   143                permission_check pctxt pctxt C_shm P_create\<rbrakk>

   144    \<Longrightarrow> (add_ss ss (S_shm (Created, pctxt))) \<in> static"

   145 | s_attach:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss; S_shm (hi,hctxt) \<in> ss;

   146                if flag = SHM_RDONLY then permission_check pctxt hctxt C_shm P_read

   147                else (permission_check pctxt hctxt C_shm P_read \<and>

   148                      permission_check pctxt hctxt C_shm P_write)\<rbrakk>

   149    \<Longrightarrow> (update_ss ss (S_proc (pi,pctxt,fds) tagp)

   150                     (S_proc (pi,pctxt,fds,shms \<union> {((hi,hctxt),flag)}) tagp)) \<in> static"

   151 | s_detach:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss; S_shm sh \<in> ss;

   152                (sh,flag) \<in> shms; \<not> is_many_sshm sh\<rbrakk>

   153    \<Longrightarrow> (update_ss ss (S_proc (pi,pctxt,fds) tagp)

   154                     (S_proc (pi,pctxt,fds,shms - {(sh,flag)}) tagp)) \<in> static"

   155 | s_deleteh: "\<lbrakk>ss \<notin> static; S_proc (pi,pctxt,fds) tagp \<in> ss; S_shm (hi,hctxt) \<in> ss;

   156                permission_check pctxt hctxt C_shm P_destroy; \<not> is_many_sshm sh\<rbrakk>

   157    \<Longrightarrow> (remove_sproc_sshm (del_ss ss (S_shm (hi,hctxt))) (hi,hctxt)) \<in> static"

   158 *)

   159 

   160 fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool"

   161 where

   162   "tainted_s ss (S_proc sp  tag) = (S_proc sp tag  \<in> ss \<and> tag = True)"

   163 | "tainted_s ss (S_file sfs tag) = (S_file sfs tag \<in> ss \<and> tag = True)"

   164 (*

   165 | "tainted_s ss (S_msg  (qi, sec, sms)  (mi, secm, tag)) = 

   166      (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,secm,tag) \<in> set sms \<and> tag = True)"

   167 *)

   168 | "tainted_s ss _ = False"

   169 

   170 (*

   171 fun tainted_s :: "t_object \<Rightarrow> t_static_state \<Rightarrow> bool"

   172 where 

   173   "tainted_s (O_proc p)  ss = (\<exists> sp. S_proc sp True \<in> ss \<and> sproc_related p sp)"

   174 | "tainted_s (O_file f)  ss = (\<exists> sfs sf. S_file sfs True \<in> ss \<and> sf \<in> sfs \<and> sfile_related f sf)"

   175 | "tainted_s (O_msg q m) ss = (\<exists> sq. S_msgq sq \<in> ss \<and> smsgq_smsg_relatainted q m sq)"

   176 | "tainted_s _           ss = False"

   177 *)

   178 

   179 definition taintable_s :: "t_object \<Rightarrow> bool"

   180 where

   181   "taintable_s obj \<equiv> \<exists> ss \<in> static. \<exists> sobj. tainted_s ss sobj \<and> init_obj_related sobj obj"

   182 

   183 (* this definition is wrong, cause process can exited from static-world 

   184 definition deletable_s :: "t_object \<Rightarrow> bool"

   185 where

   186   "deletable_s obj \<equiv> init_alive obj \<and> (\<exists> ss \<in> static. \<forall> sobj \<in> ss. \<not> init_obj_related sobj obj)"

   187 *)

   188 

   189 lemma ss_init_sp_unique_initstate:

   190   "\<lbrakk>S_proc (Init p, pctxt, fds) tagp \<in> init_static_state;

   191     S_proc (Init p, pctxt', fds') tagp' \<in> init_static_state\<rbrakk>

   192    \<Longrightarrow> pctxt' = pctxt \<and> fds' = fds \<and> tagp' = tagp"

   193 apply (simp add:init_static_state_def)

   194 apply (erule exE|erule conjE)+

   195 apply (case_tac obj, case_tac [!] obja)

   196 apply (auto simp:init_cp2sproc_def split:option.splits)

   197 done

   198 

   199 (*

   200 lemma ss_init_sp_unique:

   201   "ss \<in> static \<Longrightarrow> \<forall> p pctxt fds tagp pctxt' fds' tagp'. S_proc (Init p, pctxt, fds) tagp \<in> ss 

   202       \<and> S_proc (Init p, pctxt', fds') tagp' \<in> ss \<longrightarrow> pctxt' = pctxt \<and> fds' = fds \<and> tagp' = tagp"

   203 apply (erule static.induct)

   204 apply (rule allI|rule impI|erule conjE)+

   205 apply (erule ss_init_sp_unique_initstate, simp)

   206 sorry

   207 

   208 lemma taintable_s_imp_init_alive_aux[rule_format]:

   209   "ss \<in> static \<Longrightarrow> \<forall> sobj obj. sobj \<in> ss \<and> init_obj_related sobj obj \<longrightarrow> init_alive obj"

   210 apply (erule static.induct)

   211 apply (clarsimp simp:init_static_state_def)

   212 apply (case_tac obj, simp)

   213 sorry

   214 

   215 lemma taintable_s_imp_init_alive:

   216   "taintable_s obj \<Longrightarrow> init_alive obj"

   217 apply (clarsimp simp add:taintable_s_def)

   218 thm taintable_s_imp_init_alive_aux

   219 apply (erule_tac sobj = sobj in taintable_s_imp_init_alive_aux)

   220 apply (case_tac sobj)

   221 apply simp_all

   222 apply (case_tac [!] obj)

   223 apply ( simp_all)

   224 apply (case_tac bool, simp, simp)

   225 apply (case_tac bool, simp+)

   226 done

   227 *)

   228 

   229 fun deleted_s :: "t_static_state \<Rightarrow> t_object \<Rightarrow> bool"

   230 where

   231   "deleted_s ss (O_proc p) = (\<exists> pi pctxt fds tagp pctxt' fds' tagp'. S_proc (pi, pctxt, fds) tagp \<in> ss \<and>

   232      S_proc (Init p, pctxt', fds') tagp' \<in> ss \<and> pi \<noteq> Init p \<and> permission_check pctxt pctxt' C_process P_sigkill)"

   233 | "deleted_s ss (O_file f) = (\<exists> pi pctxt fds tagp sfs tagf fsec pfsec asecs. S_proc (pi, pctxt, fds) tagp \<in> ss \<and>

   234      S_file sfs tagf \<in> ss \<and> (Init f, fsec, Some pfsec, asecs) \<in> sfs \<and> 

   235      search_check_s pctxt (Init f, fsec, Some pfsec, asecs) True \<and>

   236      permission_check pctxt fsec C_file P_unlink \<and>

   237      permission_check pctxt pfsec C_dir P_remove_name)"

   238 | "deleted_s ss (O_dir f) = (\<exists> pi pctxt fds tagp fsec pfsec asecs. S_proc (pi, pctxt, fds) tagp \<in> ss \<and>

   239      S_dir (Init f, fsec, Some pfsec, asecs) \<in> ss \<and> search_check_s pctxt (Init f, fsec, Some pfsec, asecs) False \<and>

   240      permission_check pctxt fsec C_dir P_rmdir \<and> permission_check pctxt pfsec C_dir P_remove_name)"

   241 | "deleted_s ss (O_msgq q) = (\<exists> pi pctxt fds tagp qctxt sms. S_proc (pi, pctxt, fds) tagp \<in> ss \<and>

   242      S_msgq (Init q, qctxt, sms) \<in> ss \<and> permission_check pctxt qctxt C_msgq P_destroy)"

   243 

   244 definition deletable_s :: "t_object \<Rightarrow> bool"

   245 where

   246   "deletable_s obj \<equiv> init_alive obj \<and> (\<exists> ss \<in> static. deleted_s ss obj)"

   247 

   248 definition undeletable_s :: "t_object \<Rightarrow> bool"

   249 where

   250   "undeletable_s obj \<equiv> init_alive obj \<and> (\<forall> ss \<in> static. \<not> deleted_s ss obj)"

   251 

   252 definition init_ss_eq:: "t_static_state \<Rightarrow> t_static_state \<Rightarrow> bool" (infix "\<doteq>" 100)

   253 where

   254   "ss \<doteq> ss' \<equiv> ss \<subseteq> ss' \<and> {sobj. is_init_sobj sobj \<and> sobj \<in> ss'} \<subseteq> ss"

   255 

   256 lemma [simp]: "ss \<doteq> ss"

   257 by (auto simp:init_ss_eq_def)

   258 

   259 definition init_ss_in:: "t_static_state \<Rightarrow> t_static_state set \<Rightarrow> bool" (infix "\<propto>" 101)

   260 where

   261   "ss \<propto> sss \<equiv> \<exists> ss' \<in> sss. ss \<doteq> ss'"

   262 

   263 lemma s2ss_included_sobj:

   264   "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)"

   265 by (simp add:s2ss_def, rule_tac x = obj in exI, simp)

   266 

   267 lemma init_ss_in_prop:

   268   "\<lbrakk>s2ss s \<propto> static; co2sobj s obj = Some sobj; alive s obj; init_obj_related sobj obj\<rbrakk>

   269    \<Longrightarrow> \<exists> ss \<in> static. sobj \<in> ss"

   270 apply (simp add:init_ss_in_def init_ss_eq_def)

   271 apply (erule bexE, erule conjE)

   272 apply (rule_tac x = ss' in bexI, auto dest!:s2ss_included_sobj)

   273 done

   274 

   275 

   276 end

   277 

   278 end