Dynamic_static.thy
changeset 68 742bed613245
parent 67 811e3028d169
child 70 002c34a6ff4f
equal deleted inserted replaced
67:811e3028d169 68:742bed613245
    50 fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> t_state"
    50 fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> t_state"
    51 where 
    51 where 
    52   "enrich_proc [] tp dp = []"
    52   "enrich_proc [] tp dp = []"
    53 | "enrich_proc (Execve p f fds # s) tp dp = (
    53 | "enrich_proc (Execve p f fds # s) tp dp = (
    54      if (tp = p) 
    54      if (tp = p) 
    55      then Execve dp f fds # Execve p f fds # (enrich_proc s tp dp)
    55      then Execve dp f (fds \<inter> proc_file_fds s p) # Execve p f fds # (enrich_proc s tp dp)
    56      else Execve p f fds # (enrich_proc s tp dp))"
    56      else Execve p f fds # (enrich_proc s tp dp))"
    57 | "enrich_proc (Clone p p' fds shms # s) tp dp = (
    57 | "enrich_proc (Clone p p' fds shms # s) tp dp = (
    58      if (tp = p') 
    58      if (tp = p') 
    59      then Clone p dp fds shms # Clone p p' fds shms # s
    59      then Clone p dp (fds \<inter> proc_file_fds s p) shms # Clone p p' fds shms # s
    60      else Clone p dp fds shms # (enrich_proc s tp dp))"
    60      else Clone p p' fds shms # (enrich_proc s tp dp))"
    61 | "enrich_proc (Open p f flags fd opt # s) tp dp = (
    61 | "enrich_proc (Open p f flags fd opt # s) tp dp = (
    62      if (tp = p)
    62      if (tp = p)
    63      then Open dp f (remove_create_flag flags) fd opt # Open p f flags fd opt # (enrich_proc s tp dp)
    63      then Open dp f (remove_create_flag flags) fd opt # Open p f flags fd opt # (enrich_proc s tp dp)
    64      else Open p f flags fd opt # (enrich_proc s tp dp))"
    64      else Open p f flags fd opt # (enrich_proc s tp dp))"
    65 | "enrich_proc (CloseFd p fd # s) tp dp = (
    65 | "enrich_proc (CloseFd p fd # s) tp dp = (
    84 
    84 
    85 definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
    85 definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
    86 where
    86 where
    87   "is_created_proc s p \<equiv> p \<in> init_procs \<longrightarrow> deleted (O_proc p) s"
    87   "is_created_proc s p \<equiv> p \<in> init_procs \<longrightarrow> deleted (O_proc p) s"
    88 
    88 
       
    89 lemma enrich_search_check:
       
    90   assumes grant: "search_check s (up, rp, tp) f"
       
    91   and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f"
       
    92   and vd: "valid s" and f_in: "is_file s f"  and f_in': "is_file s' f"
       
    93   and sec: "sectxt_of_obj s' (O_file f) = sectxt_of_obj s (O_file f)"
       
    94   shows "search_check s' (up, rp, tp) f"
       
    95 proof (cases f)
       
    96   case Nil
       
    97   with f_in vd have "False" 
       
    98     by (auto dest:root_is_dir') 
       
    99   thus ?thesis by simp
       
   100 next
       
   101   case (Cons n pf)
       
   102   from vd f_in obtain sf where sf: "cf2sfile s f = Some sf"
       
   103     apply (drule_tac is_file_in_current, drule_tac current_file_has_sfile, simp)
       
   104     apply (erule exE, simp)
       
   105     done
       
   106   then obtain psfs where psfs: "get_parentfs_ctxts s pf = Some psfs" using Cons
       
   107     by (auto simp:cf2sfile_def split:option.splits if_splits)
       
   108   from sf cf2sf f_in have sf': "cf2sfile s' f = Some sf" by (auto dest:is_file_in_current)
       
   109   then obtain psfs' where psfs': "get_parentfs_ctxts s' pf = Some psfs'"using Cons
       
   110     by (auto simp:cf2sfile_def split:option.splits if_splits)
       
   111   with sf sf' psfs have psfs_eq: "set psfs' = set psfs" using Cons f_in f_in'
       
   112     apply (simp add:cf2sfile_def split:option.splits)
       
   113     apply (case_tac sf, simp)
       
   114     done
       
   115   show ?thesis using grant f_in f_in' psfs psfs' psfs_eq sec
       
   116     apply (simp add:Cons split:option.splits)
       
   117     by (case_tac a, simp)
       
   118 qed
       
   119 
       
   120 lemma enrich_inherit_fds_check:
       
   121   assumes grant: "inherit_fds_check s (up, nr, nt) p fds"  and vd: "valid s"
       
   122   and fd2sfd: "\<forall> fd. fd \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p"
       
   123   and p_in: "p \<in> current_procs s" and p_in': "p \<in> current_procs s'"
       
   124   and fd_in: "fds \<subseteq> current_proc_fds s p" and fd_in': "fds \<subseteq> current_proc_fds s' p"
       
   125   shows "inherit_fds_check s' (up, nr, nt) p fds"
       
   126 proof-
       
   127   have "\<And> fd. fd \<in> fds \<Longrightarrow> sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)"
       
   128   proof-
       
   129     fix fd
       
   130     assume fd_in_fds: "fd \<in> fds"
       
   131     hence fd_in_cfds: "fd \<in> current_proc_fds s p" 
       
   132       and fd_in_cfds': "fd \<in> current_proc_fds s' p" 
       
   133       using fd_in fd_in' by auto
       
   134     from p_in vd obtain sp where csp: "cp2sproc s p = Some sp" 
       
   135       by (drule_tac current_proc_has_sp, simp, erule_tac exE, simp)
       
   136     with cp2sp have "cpfd2sfds s p = cpfd2sfds s' p"
       
   137       apply (erule_tac x = p in allE)
       
   138       by (auto simp:cp2sproc_def split:option.splits simp:p_in)
       
   139     hence "cfd2sfd s p fd = cfd2sfd s' p fd"
       
   140       apply (simp add:cpfd2sfds_def)
       
   141       thm inherit_fds_check_def
       
   142       thm sectxts_of_fds_def
       
   143       thm cpfd2sfds_def
       
   144       apply (
       
   145 
       
   146     show "sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)"
       
   147       sorry
       
   148   qed
       
   149   hence "sectxts_of_fds s' p fds = sectxts_of_fds s p fds"
       
   150     by (simp add:sectxts_of_fds_def)
       
   151   thus ?thesis using grant
       
   152     by (simp add:inherit_fds_check_def)
       
   153 qed
       
   154   
       
   155 
    89 lemma enrich_proc_aux1:
   156 lemma enrich_proc_aux1:
    90   assumes vs': "valid s'"
   157   assumes vs': "valid s'"
    91     and os: "os_grant s e" and grant: "grant s e"
   158     and os: "os_grant s e" and grant: "grant s e" and vd: "valid s"
    92     and alive: "\<forall> obj. alive s obj \<longrightarrow> alive s' obj"
   159     and alive: "\<forall> obj. alive s obj \<longrightarrow> alive s' obj"
    93     and cp2sp: "\<forall> p. p \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p"
   160     and cp2sp: "\<forall> p. p \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p"
    94     and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f"
   161     and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f"
    95   shows "valid (e # s')"
   162   shows "valid (e # s')"
    96 proof (cases e)
   163 proof (cases e)
   103     by (auto simp:Execve)
   170     by (auto simp:Execve)
   104   have fd_in: "fds \<subseteq> current_proc_fds s' p" using os alive
   171   have fd_in: "fds \<subseteq> current_proc_fds s' p" using os alive
   105     apply (auto simp:Execve)
   172     apply (auto simp:Execve)
   106     by (erule_tac x = "O_fd p x" in allE, auto)
   173     by (erule_tac x = "O_fd p x" in allE, auto)
   107   have "os_grant s' e" using p_in f_in fd_in by (simp add:Execve)
   174   have "os_grant s' e" using p_in f_in fd_in by (simp add:Execve)
   108   moreover have "grant s' e"
   175   moreover have "grant s' e" apply (simp add:Execve)
   109   proof-
   176   proof-
   110     from grant obtain up rp tp uf rf tf 
   177     from grant obtain up rp tp uf rf tf 
   111       where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"
   178       where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"
   112       and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" 
   179       and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" 
   113       by (simp add:Execve split:option.splits, blast)
   180       by (simp add:Execve split:option.splits, blast)
   115       by (simp add:Execve split:option.splits del:npctxt_execve.simps, blast)
   182       by (simp add:Execve split:option.splits del:npctxt_execve.simps, blast)
   116     from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)"
   183     from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)"
   117       using os cp2sp
   184       using os cp2sp
   118       apply (erule_tac x = p in allE)
   185       apply (erule_tac x = p in allE)
   119       by (auto simp:Execve co2sobj.simps cp2sproc_def split:option.splits)
   186       by (auto simp:Execve co2sobj.simps cp2sproc_def split:option.splits)
   120     from p2 have p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" 
   187     from os have f_in': "is_file s f" by (simp add:Execve)
   121       using os cf2sf
   188     from vd os have "\<exists> sf. cf2sfile s f = Some sf"
   122       apply (erule_tac x = "f" in allE)
   189       by (auto dest!:is_file_in_current current_file_has_sfile simp:Execve)
   123       apply (auto simp:Execve dest:is_file_in_current)
   190     hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using f_in f_in' p2 cf2sf
   124       thm cf2sfile_def
   191       apply (erule_tac x = f in allE)
   125       apply (auto simp:cf2sfile_def split:option.splits)
   192       apply (auto dest:is_file_in_current simp:cf2sfile_def split:option.splits)
   126       apply (auto simp:Execve co2sobj.simps cf2sfile_simps split:option.splits)
   193       apply (case_tac f, simp)
   127       apply (simp add:cf2sfiles_def)
   194       apply (drule_tac s = s in root_is_dir', simp add:vd, simp+)
   128       apply (auto)[1]
   195       done
   129       using os pre
   196   show ?
   130   show ?thesis
       
   131   proof-
   197   proof-
   132     have
   198     have
   133     
   199     
   134 
   200 
   135 
   201 
   136 
   202 
   137 lemma enrich_proc_prop:
   203 lemma enrich_proc_prop:
   138   "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk>
   204   "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk>
   139    \<Longrightarrow> valid (enrich_proc s p p') \<and> 
   205    \<Longrightarrow> valid (enrich_proc s p p') \<and> 
   140        (p \<in> current_procs s \<longrightarrow> co2sobj (enrich_proc s p p') (O_proc p') = co2sobj (enrich_proc s p p') (O_proc p)) \<and>
   206        (p \<in> current_procs s \<longrightarrow> co2sobj (enrich_proc s p p') (O_proc p') = co2sobj (enrich_proc s p p') (O_proc p)) \<and>
   141        (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p')  obj \<and> co2sobj (enrich_proc s p p') obj = co2sobj s obj)"
   207        (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p')  obj) \<and> 
       
   208        (\<forall> p'. p' \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and>
       
   209        (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and>
       
   210        (Tainted (enrich_proc s p p') = (Tainted s \<union> (if (O_proc p \<in> Tainted s) then {O_proc p'} else {})))"
   142 proof (induct s)
   211 proof (induct s)
   143   case Nil
   212   case Nil
   144   thus ?case by (auto simp:is_created_proc_def)
   213   thus ?case by (auto simp:is_created_proc_def)
   145 next
   214 next
   146   case (Cons e s)
   215   case (Cons e s)