1 (*<*)

     2 theory S2ss_prop

     3 imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop

     4 begin

     5 (*>*)

     6 

     7 context tainting_s begin

     8 

     9 (* simpset for s2ss*)

    10 

    11 lemma co2sobj_some_case:

    12   "\<lbrakk>co2sobj s obj = Some sobj; \<And> p. obj = O_proc p \<Longrightarrow> P (O_proc p);

    13     \<And> f. obj = O_file f \<Longrightarrow> P (O_file f); \<And> h. obj = O_shm h \<Longrightarrow> P (O_shm h);

    14     \<And> f. obj = O_dir f \<Longrightarrow> P (O_dir f); \<And> q. obj = O_msgq q \<Longrightarrow> P (O_msgq q)\<rbrakk>

    15    \<Longrightarrow> P obj"

    16 by (case_tac obj, auto)

    17 

    18 lemma co2sobj_execve_alive:

    19   "\<lbrakk>alive s obj; co2sobj s obj = Some x; valid (Execve p f fds # s)\<rbrakk>

    20    \<Longrightarrow> alive (Execve p f fds # s) obj"

    21 apply (erule co2sobj_some_case)

    22 by (auto simp:alive_simps simp del:alive.simps)

    23 

    24 lemma s2ss_execve:

    25   "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = (

    26      if (\<exists> p'. p' \<noteq> p \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p))

    27      then (case (cp2sproc (Execve p f fds # s) p) of

    28              Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)}

    29            | _ \<Rightarrow> {} )

    30      else (case (cp2sproc (Execve p f fds # s) p, cp2sproc s p) of

    31              (Some sp, Some sp') \<Rightarrow> s2ss s - {S_proc sp' (O_proc p \<in> Tainted s)}

    32                                     \<union> {S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)}

    33            | _ \<Rightarrow> {} ) )"

    34 apply (frule vd_cons, frule vt_grant_os, simp split:if_splits)

    35 

    36 apply (rule conjI, rule impI, (erule exE|erule conjE)+)

    37 apply (frule_tac p = p in current_proc_has_sp, simp, erule exE)

    38 apply (frule_tac p = p' in current_proc_has_sp, simp, erule exE, simp)

    39 apply (subgoal_tac "p \<in> current_procs (Execve p f fds # s)")

    40 apply (drule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp, simp)

    41 apply (erule exE, simp)

    42 apply (simp add:s2ss_def, rule set_eqI, rule iffI)

    43 apply (drule CollectD, (erule exE|erule conjE)+)

    44 apply (case_tac "obj = O_proc p")

    45 apply (simp add:co2sobj_execve tainted_eq_Tainted split:if_splits)

    46 apply (simp add:co2sobj_execve, rule disjI2)

    47 apply (rule_tac x = obj in exI, case_tac obj, (simp add:alive_simps)+)[1]

    48 apply (simp, erule disjE)

    49 apply (rule_tac x = "O_proc p" in exI, simp add:tainted_eq_Tainted)

    50 apply (erule exE| erule conjE)+

    51 apply (case_tac "x = S_proc sp (O_proc p \<in> tainted s)")

    52 apply (rule_tac x = "O_proc p'" in exI)

    53 apply (simp add:alive_execve co2sobj_execve tainted_eq_Tainted cp2sproc_execve)

    54 apply (case_tac "obj = O_proc p", simp)

    55 apply (frule co2sobj_execve_alive, simp, simp)

    56 apply (frule_tac obj = obj in co2sobj_execve, simp)

    57 apply (rule_tac x = obj in exI, simp, simp)

    58 

    59 apply (erule conjE, frule current_proc_has_sp, simp, erule exE, rule impI, simp)

    60 apply (subgoal_tac "p \<in> current_procs (Execve p f fds # s)") 

    61 apply (drule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp, simp)

    62 apply (erule exE, erule conjE, simp)

    63 apply (simp add:s2ss_def, rule set_eqI, rule iffI)

    64 apply (drule CollectD, (erule exE|erule conjE)+)

    65 apply (case_tac "obj = O_proc p", simp add:tainted_eq_Tainted)

    66 apply (rule disjI1, simp split:if_splits)

    67 apply (simp add:co2sobj_execve, rule disjI2)

    68 apply (rule conjI,rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits)

    69 apply (rule notI, simp, case_tac obj)

    70 apply (erule_tac x = nat in allE, simp add:tainted_eq_Tainted, (simp split:option.splits)+)

    71 apply (erule disjE, simp)

    72 apply (rule_tac x = "O_proc p" in exI, simp add:tainted_eq_Tainted)

    73 apply (erule exE|erule conjE)+

    74 apply (rule_tac x = obj in exI)

    75 apply (drule_tac obj = obj in co2sobj_execve_alive, simp+)

    76 apply (frule_tac obj = obj in co2sobj_execve, simp, simp)

    77 apply (rule impI, simp add:tainted_eq_Tainted, simp)

    78 done

    79 

    80 lemma s2ss_clone_alive:

    81   "\<lbrakk>co2sobj s obj = Some x; alive s obj; obj \<noteq> O_proc p'; valid (Clone p p' fds shms # s)\<rbrakk>

    82    \<Longrightarrow> alive (Clone p p' fds shms # s) obj"

    83 by (erule co2sobj_some_case, auto simp:alive_clone)

    84 

    85 lemma s2ss_clone:

    86   "valid (Clone p p' fds shms # s) \<Longrightarrow> s2ss (Clone p p' fds shms # s) = (

    87      case (cp2sproc (Clone p p' fds shms # s) p') of

    88        Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> Tainted s)}

    89      | _       \<Rightarrow> {})"

    90 apply (frule vd_cons, frule vt_grant_os, split option.splits)

    91 apply (rule conjI, rule impI, drule current_proc_has_sp', simp, simp)

    92 apply (rule allI, rule impI, simp add:s2ss_def)

    93 apply (rule set_eqI, rule iffI, drule CollectD, (erule exE|erule conjE)+)

    94 apply (case_tac "obj = O_proc p'", simp add:tainted_eq_Tainted)

    95 apply (case_tac "O_proc p' \<in> Tainted s", drule Tainted_in_current, simp+)

    96 apply (rule disjI1, simp split:if_splits)

    97 apply (simp add:tainted_eq_Tainted, rule disjI2)

    98 apply (frule co2sobj_clone, simp)

    99 apply (rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits)

   100 

   101 apply (simp, erule disjE, simp)

   102 apply (rule_tac x = "O_proc p'" in exI, simp add:tainted_eq_Tainted)

   103 apply (rule impI, rule notI, drule Tainted_in_current, simp+)

   104 apply (erule exE| erule conjE)+

   105 apply (case_tac "obj = O_proc p'", simp)

   106 apply (rule_tac x = obj in exI)

   107 apply (frule s2ss_clone_alive, simp+)

   108 apply (auto simp:co2sobj_clone alive_simps)

   109 done

   110 

   111 definition s2ss_shm_no_backup:: "t_state \<Rightarrow> t_process \<Rightarrow> t_static_state"

   112 where

   113   "s2ss_shm_no_backup s pfrom \<equiv> {S_proc sp False | sp p. info_flow_shm s pfrom p \<and> cp2sproc s p = Some sp \<and>

   114      (\<not> (\<exists> p'. \<not> info_flow_shm s pfrom p' \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = Some (S_proc sp False)))}"

   115 

   116 definition update_s2ss_shm:: "t_state \<Rightarrow> t_process \<Rightarrow> t_static_state" 

   117 where

   118   "update_s2ss_shm s pfrom \<equiv> s2ss s 

   119      \<union> {S_proc sp True| sp p. info_flow_shm s pfrom p \<and> cp2sproc s p = Some sp}

   120      - (s2ss_shm_no_backup s pfrom)"

   121 

   122 lemma s2ss_shm_no_bk_elim:

   123   "\<lbrakk>S_proc sp False \<notin> s2ss_shm_no_backup s pfrom; co2sobj s (O_proc p) = Some (S_proc sp False); 

   124     valid s; info_flow_shm s pfrom p\<rbrakk>

   125    \<Longrightarrow> \<exists> p'. \<not> info_flow_shm s pfrom p' \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = Some (S_proc sp False)"

   126 apply (auto simp:s2ss_shm_no_backup_def co2sobj.simps tainted_eq_Tainted split:option.splits)

   127 apply (erule_tac x = p in allE, auto)

   128 apply (rule_tac x = p' in exI, auto)

   129 done

   130 

   131 lemma s2ss_shm_no_bk_intro1:

   132   "\<lbrakk>co2sobj s' obj = Some x; \<forall> p. obj \<noteq> O_proc p\<rbrakk> \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"

   133 apply (case_tac obj)

   134 apply (auto simp:co2sobj.simps s2ss_shm_no_backup_def split:option.splits)

   135 done

   136 

   137 lemma s2ss_shm_no_bk_intro2:

   138   "\<lbrakk>co2sobj s' obj = Some x; obj \<in> Tainted s'; valid s'\<rbrakk> \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"

   139 apply (case_tac obj)

   140 

   141 apply (auto simp:co2sobj.simps s2ss_shm_no_backup_def tainted_eq_Tainted split:option.splits)

   142 done

   143 

   144 lemma s2ss_shm_no_bk_intro3:

   145   "\<lbrakk>co2sobj s (O_proc p) = Some x; \<not> info_flow_shm s pfrom p; p \<in> current_procs s

   146    \<rbrakk> \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"

   147 apply (auto simp add:s2ss_shm_no_backup_def split:option.splits)

   148 apply (rule_tac x = p in exI, simp)

   149 done

   150 

   151 lemma s2ss_shm_no_bk_intro4:

   152   "\<lbrakk>co2sobj s (O_proc p) = Some x; info_flow_shm s pfrom p; 

   153     \<not> info_flow_shm s pfrom p'; p' \<in> current_procs s; co2sobj s (O_proc p') = Some x\<rbrakk>

   154    \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"

   155 apply (rule notI)

   156 apply (auto simp add:s2ss_shm_no_backup_def co2sobj.simps split:option.splits)

   157 done  

   158 

   159 lemma Tainted_ptrace':

   160   "valid s \<Longrightarrow> Tainted (Ptrace p p' # s) = 

   161      (if (O_proc p \<in> Tainted s \<and> O_proc p' \<notin> Tainted s)

   162       then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p' p''}

   163       else if (O_proc p' \<in> Tainted s \<and> O_proc p \<notin> Tainted s)

   164            then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p p''}

   165                 else Tainted s)"

   166 using info_flow_shm_Tainted by auto

   167 

   168 lemma co2sobj_some_caseD:

   169   "\<lbrakk>co2sobj s obj = Some sobj; \<And> p. \<lbrakk>co2sobj s obj = Some sobj; obj = O_proc p\<rbrakk> \<Longrightarrow> P (O_proc p);

   170     \<And> f. \<lbrakk>co2sobj s obj = Some sobj; obj = O_file f\<rbrakk> \<Longrightarrow> P (O_file f); 

   171     \<And> h. \<lbrakk>co2sobj s obj = Some sobj; obj = O_shm h\<rbrakk> \<Longrightarrow> P (O_shm h);

   172     \<And> f. \<lbrakk>co2sobj s obj = Some sobj; obj = O_dir f\<rbrakk> \<Longrightarrow> P (O_dir f); 

   173     \<And> q. \<lbrakk>co2sobj s obj = Some sobj; obj = O_msgq q\<rbrakk> \<Longrightarrow> P (O_msgq q)\<rbrakk>

   174    \<Longrightarrow> P obj"

   175 by (case_tac obj, auto)

   176 

   177 lemma s2ss_ptrace1_aux: "x \<notin> {x. P x} \<Longrightarrow> \<not> P x" by simp

   178 

   179 lemma s2ss_ptrace1:

   180   "\<lbrakk>valid (Ptrace p p' # s); O_proc p \<in> Tainted s; O_proc p' \<notin> Tainted s\<rbrakk>

   181    \<Longrightarrow> s2ss (Ptrace p p' # s) = update_s2ss_shm s p'"

   182 unfolding update_s2ss_shm_def s2ss_def s2ss_shm_no_backup_def 

   183 apply (frule vd_cons, rule set_eqI, rule iffI)

   184 apply (drule CollectD, (erule exE|erule conjE)+)

   185 apply (erule co2sobj_some_caseD)

   186 apply (rule DiffI)

   187 apply (case_tac "O_proc pa \<in> Tainted s")

   188 apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI)

   189 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)

   190 apply (case_tac "info_flow_shm s p' pa")

   191 apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits)

   192 apply (drule current_proc_has_sp', simp, simp)

   193 apply (rule_tac x = a in exI, rule_tac x = pa in exI)

   194 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)

   195 apply (rule UnI1, simp)

   196 apply (rule_tac x = "O_proc pa" in exI)

   197 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)

   198 apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits)

   199 apply (erule_tac x = pa in allE, simp)

   200 

   201 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,

   202        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

   203 apply (simp)

   204 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,

   205        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

   206 apply (simp split:option.splits)

   207 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,

   208        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

   209 apply (simp split:option.splits)

   210 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,

   211        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

   212 apply (simp split:option.splits)

   213 

   214 apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE)

   215 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)

   216 apply (erule co2sobj_some_caseD)

   217 apply (case_tac "O_proc pa \<in> Tainted s")

   218 apply (rule_tac x = "O_proc pa" in exI)

   219 apply (clarsimp simp add:tainted_eq_Tainted cp2sproc_other split:option.splits)

   220 apply (case_tac "info_flow_shm s p' pa", simp only:co2sobj.simps split:option.splits)

   221 apply (drule current_proc_has_sp', simp, simp)

   222 apply (drule Meson.not_exD, erule_tac x = a in allE, drule Meson.not_exD, erule_tac x = pa in allE)

   223 apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+)

   224 apply (rule_tac x = "O_proc p'a" in exI)

   225 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)

   226 apply (rule_tac x = "O_proc pa" in exI)

   227 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)

   228 

   229 apply (rule_tac x = obj in exI,

   230        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

   231 apply (rule_tac x = obj in exI,

   232        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

   233 apply (rule_tac x = obj in exI,

   234        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

   235 apply (rule_tac x = obj in exI,

   236        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

   237 

   238 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)

   239 apply (rule_tac x = "O_proc pa" in exI)

   240 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs)

   241 done

   242 

   243 lemma s2ss_ptrace2:

   244   "\<lbrakk>valid (Ptrace p p' # s); O_proc p' \<in> Tainted s; O_proc p \<notin> Tainted s\<rbrakk>

   245    \<Longrightarrow> s2ss (Ptrace p p' # s) = update_s2ss_shm s p"

   246 unfolding update_s2ss_shm_def s2ss_def s2ss_shm_no_backup_def

   247 apply (frule vd_cons, rule set_eqI, rule iffI)

   248 apply (drule CollectD, (erule exE|erule conjE)+)

   249 apply (erule co2sobj_some_caseD)

   250 apply (rule DiffI)

   251 apply (case_tac "O_proc pa \<in> Tainted s")

   252 apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI)

   253 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)

   254 apply (case_tac "info_flow_shm s p pa")

   255 apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits)

   256 apply (drule current_proc_has_sp', simp, simp)

   257 apply (rule_tac x = a in exI, rule_tac x = pa in exI)

   258 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)

   259 apply (rule UnI1, simp)

   260 apply (rule_tac x = "O_proc pa" in exI)

   261 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)

   262 apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits)

   263 apply (erule_tac x = pa in allE, simp)

   264 

   265 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,

   266        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

   267 apply (simp)

   268 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,

   269        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

   270 apply (simp split:option.splits)

   271 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,

   272        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

   273 apply (simp split:option.splits)

   274 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,

   275        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

   276 apply (simp split:option.splits)

   277 

   278 apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE)

   279 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)

   280 apply (erule co2sobj_some_caseD)

   281 apply (case_tac "O_proc pa \<in> Tainted s")

   282 apply (rule_tac x = "O_proc pa" in exI)

   283 apply (clarsimp simp add:tainted_eq_Tainted cp2sproc_other split:option.splits)

   284 apply (case_tac "info_flow_shm s p pa", simp only:co2sobj.simps split:option.splits)

   285 apply (drule current_proc_has_sp', simp, simp)

   286 apply (drule Meson.not_exD, erule_tac x = a in allE, drule Meson.not_exD, erule_tac x = pa in allE)

   287 apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+)

   288 apply (rule_tac x = "O_proc p'a" in exI)

   289 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)

   290 apply (rule_tac x = "O_proc pa" in exI)

   291 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)

   292 

   293 apply (rule_tac x = obj in exI,

   294        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

   295 apply (rule_tac x = obj in exI,

   296        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

   297 apply (rule_tac x = obj in exI,

   298        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

   299 apply (rule_tac x = obj in exI,

   300        auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

   301 

   302 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)

   303 apply (rule_tac x = "O_proc pa" in exI)

   304 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs)

   305 done

   306 

   307 lemma s2ss_ptrace3:

   308   "\<lbrakk>valid (Ptrace p p' # s); (O_proc p' \<in> Tainted s) = (O_proc p \<in> Tainted s)\<rbrakk>

   309    \<Longrightarrow> s2ss (Ptrace p p' # s) = s2ss s"

   310 unfolding s2ss_def

   311 apply (frule vd_cons, rule set_eqI, rule iffI)

   312 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)

   313 apply (rule_tac x = obj in exI)

   314 apply (frule alive_other, simp+)

   315 apply (frule_tac obj = obj in co2sobj_ptrace, simp)

   316 apply (auto simp add:tainted_eq_Tainted split:t_object.splits option.splits if_splits

   317   intro:info_flow_shm_Tainted)[1]

   318 

   319 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)

   320 apply (rule_tac x = obj in exI)

   321 apply (frule alive_other, simp+)

   322 apply (frule_tac obj = obj in co2sobj_ptrace, simp)

   323 apply (auto simp add:tainted_eq_Tainted split:t_object.splits option.splits if_splits 

   324   intro:info_flow_shm_Tainted)

   325 done

   326 

   327 lemma s2ss_ptrace:

   328   "valid (Ptrace p p' # s) \<Longrightarrow> s2ss (Ptrace p p' # s) = (

   329      if (O_proc p \<in> Tainted s \<and> O_proc p' \<notin> Tainted s) 

   330      then update_s2ss_shm s p'

   331      else if (O_proc p' \<in> Tainted s \<and> O_proc p \<notin> Tainted s)

   332           then update_s2ss_shm s p

   333           else s2ss s                                   )"

   334 apply (frule vt_grant_os, frule vd_cons)

   335 apply (simp add:s2ss_ptrace2 s2ss_ptrace1 split:if_splits)

   336 by (auto dest:s2ss_ptrace3)

   337 

   338 lemma s2ss_kill:

   339   "valid (Kill p p' # s) \<Longrightarrow> s2ss (Kill p p' # s) = (

   340      if (\<exists> p''. p'' \<in> current_procs s \<and> p'' \<noteq> p' \<and> co2sobj s (O_proc p'') = co2sobj s (O_proc p'))

   341      then s2ss s 

   342      else (case (co2sobj s (O_proc p')) of

   343              Some sp \<Rightarrow> s2ss s - {sp}

   344            | _       \<Rightarrow> {}))"

   345 apply (frule vt_grant_os, frule vd_cons)

   346 unfolding s2ss_def

   347 apply (simp split:if_splits, rule conjI)

   348 apply (rule impI, (erule exE|erule conjE)+)

   349 apply (split option.splits)

   350 apply (drule current_proc_has_sp', simp, simp)

   351 apply (simp split: option.splits, (erule conjE)+)

   352 apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI)

   353 apply (rule_tac x = obj in exI)

   354 apply (simp add:co2sobj_kill tainted_eq_Tainted alive_kill split:t_object.splits if_splits)

   355 apply (erule CollectE, erule exE, erule conjE, rule CollectI)

   356 apply (erule co2sobj_some_caseD)

   357 apply (case_tac "pa = p'")

   358 apply (rule_tac x = "O_proc p''" in exI)

   359 apply (simp add:cp2sproc_kill tainted_eq_Tainted alive_kill

   360   split:t_object.splits if_splits option.splits)

   361 apply (rule_tac x = "O_proc pa" in exI)

   362 apply (clarsimp simp add:cp2sproc_kill tainted_eq_Tainted alive_kill

   363   split:t_object.splits if_splits option.splits)

   364 apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+

   365 

   366 apply (rule impI, erule conjE, frule current_proc_has_sp, simp, erule exE, simp)

   367 apply (rule set_eqI, rule iffI)

   368 apply (erule CollectE, erule exE, erule conjE, rule DiffI)

   369 apply (rule CollectI, rule_tac x = obj in exI)

   370 apply (simp add:co2sobj_kill tainted_eq_Tainted alive_kill split:t_object.splits if_splits)

   371 apply (rule notI, simp, case_tac obj)

   372 apply (erule_tac x = nat in allE)

   373 apply (simp add:co2sobj_kill cp2sproc_kill tainted_eq_Tainted split:option.splits)

   374 apply (simp split:option.splits)+

   375 apply (erule co2sobj_some_caseD)

   376 apply (case_tac "pa = p'")

   377 apply (rule_tac x = "O_proc p''" in exI)

   378 apply (simp add:cp2sproc_kill tainted_eq_Tainted alive_kill

   379   split:t_object.splits if_splits option.splits)

   380 apply (rule_tac x = "O_proc pa" in exI)

   381 apply (clarsimp simp add:cp2sproc_kill tainted_eq_Tainted alive_kill

   382   split:t_object.splits if_splits option.splits)

   383 apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+

   384 done

   385 

   386 lemma s2ss_exit:

   387   "valid (Exit p # s) \<Longrightarrow> s2ss (Exit p # s) = (

   388      if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p))

   389      then s2ss s 

   390      else (case (co2sobj s (O_proc p)) of

   391              Some sp \<Rightarrow> s2ss s - {sp}

   392            | _       \<Rightarrow> {}))"

   393 apply (frule vt_grant_os, frule vd_cons)

   394 unfolding s2ss_def

   395 apply (simp split:if_splits, rule conjI)

   396 apply (rule impI, (erule exE|erule conjE)+)

   397 apply (split option.splits)

   398 apply (drule current_proc_has_sp', simp, simp)

   399 apply (simp split: option.splits, (erule conjE)+)

   400 apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI)

   401 apply (rule_tac x = obj in exI)

   402 apply (simp add:co2sobj_exit tainted_eq_Tainted alive_exit split:t_object.splits if_splits)

   403 apply (erule CollectE, erule exE, erule conjE, rule CollectI)

   404 apply (erule co2sobj_some_caseD)

   405 apply (case_tac "pa = p")

   406 apply (rule_tac x = "O_proc p'" in exI)

   407 apply (simp add:cp2sproc_exit tainted_eq_Tainted alive_exit

   408   split:t_object.splits if_splits option.splits)

   409 apply (rule_tac x = "O_proc pa" in exI)

   410 apply (clarsimp simp add:cp2sproc_exit tainted_eq_Tainted alive_exit

   411   split:t_object.splits if_splits option.splits)

   412 apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+

   413 

   414 apply (rule impI, frule current_proc_has_sp, simp, erule exE, simp)

   415 apply (rule set_eqI, rule iffI)

   416 apply (erule CollectE, erule exE, erule conjE, rule DiffI)

   417 apply (rule CollectI, rule_tac x = obj in exI)

   418 apply (simp add:co2sobj_exit tainted_eq_Tainted alive_exit split:t_object.splits if_splits)

   419 apply (rule notI, simp, case_tac obj)

   420 apply (erule_tac x = nat in allE)

   421 apply (simp add:co2sobj_exit cp2sproc_exit tainted_eq_Tainted split:option.splits)

   422 apply (simp split:option.splits)+

   423 apply (erule co2sobj_some_caseD)

   424 apply (case_tac "pa = p")

   425 apply (rule_tac x = "O_proc p'" in exI)

   426 apply (simp add:cp2sproc_exit tainted_eq_Tainted alive_exit

   427   split:t_object.splits if_splits option.splits)

   428 apply (rule_tac x = "O_proc pa" in exI)

   429 apply (clarsimp simp add:cp2sproc_exit tainted_eq_Tainted alive_exit

   430   split:t_object.splits if_splits option.splits)

   431 apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+

   432 done

   433 

   434 lemma alive_has_sobj':

   435   "\<lbrakk>co2sobj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj"

   436 apply (case_tac obj)

   437 apply (auto split:option.splits)

   438 oops

   439 

   440 declare co2sobj.simps [simp del]

   441 

   442 lemma co2sobj_open_none:

   443   "\<lbrakk>valid (Open p f flag fd None # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Open p f flag fd None # s) obj = (

   444       if (obj = O_proc p) 

   445       then (case (cp2sproc (Open p f flag fd None # s) p) of

   446               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))

   447            | _       \<Rightarrow> None)

   448       else co2sobj s obj)"

   449 apply (frule vt_grant_os, frule vd_cons)

   450 apply (frule_tac obj = obj in co2sobj_open, simp add:alive_open)

   451 apply (auto split:t_object.splits option.splits dest!:current_proc_has_sp')

   452 done

   453 

   454 lemma co2sobj_open_some:

   455   "\<lbrakk>valid (Open p f flag fd (Some i) # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Open p f flag fd (Some i) # s) obj = (

   456       if (obj = O_proc p) 

   457       then (case (cp2sproc (Open p f flag fd (Some i) # s) p) of

   458               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))

   459            | _       \<Rightarrow> None)

   460       else if (obj = O_file f) 

   461            then (case (cf2sfile (Open p f flag fd (Some i) # s) f) of

   462                    Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> Tainted s))

   463                  | _       \<Rightarrow> None)

   464            else co2sobj s obj)"

   465 apply (frule vt_grant_os, frule vd_cons)

   466 apply (frule_tac obj = obj in co2sobj_open, simp add:alive_open)

   467 apply (auto split:t_object.splits option.splits dest!:current_proc_has_sp')

   468 done

   469 

   470 lemma alive_co2sobj_some_open_none:

   471   "\<lbrakk>co2sobj s obj = Some sobj; alive s obj; valid (Open p f flag fd None # s)\<rbrakk>

   472    \<Longrightarrow> alive (Open p f flag fd None # s) obj"

   473 by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)

   474 

   475 lemma alive_co2sobj_some_open_none':

   476   "\<lbrakk>co2sobj (Open p f flag fd None # s) obj = Some sobj; alive (Open p f flag fd None # s) obj; 

   477     valid (Open p f flag fd None # s)\<rbrakk> \<Longrightarrow> alive s obj"

   478 by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)

   479 

   480 lemma co2sobj_proc_obj:

   481   "\<lbrakk>co2sobj s obj = Some x; co2sobj s (O_proc p) = Some x\<rbrakk>

   482    \<Longrightarrow> \<exists> p'. obj = O_proc p'"

   483 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)

   484 

   485 lemma s2ss_open_none:

   486   "valid (Open p f flag fd None # s) \<Longrightarrow> s2ss (Open p f flag fd None # s) = (

   487       case (co2sobj s (O_proc p), co2sobj (Open p f flag fd None # s) (O_proc p)) of

   488         (Some sp, Some sp') \<Rightarrow> 

   489            if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)

   490            then s2ss s \<union> {sp'}

   491            else s2ss s - {sp} \<union> {sp'} 

   492       | _                   \<Rightarrow> {} )"

   493 unfolding s2ss_def

   494 apply (frule vt_grant_os, frule vd_cons)

   495 apply (case_tac "co2sobj s (O_proc p)", simp add:co2sobj.simps split:option.splits)

   496 apply (drule current_proc_has_sp', simp, simp)

   497 apply (case_tac "co2sobj (Open p f flag fd None # s) (O_proc p)")

   498 apply (simp add:co2sobj.simps split:option.splits)

   499 apply (drule current_proc_has_sp', simp, simp)

   500 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, simp)

   501 apply (frule_tac obj = obj in alive_co2sobj_some_open_none', simp, simp)

   502 apply (rule conjI, rule impI, erule exE, (erule conjE)+)

   503 apply (rule Meson.disj_comm, rule disjCI, case_tac "obj = O_proc p", simp)

   504 apply (rule_tac x = obj in exI, simp add:co2sobj_open_none)

   505 apply (rule impI)

   506 apply (case_tac "obj = O_proc p", simp)

   507 apply (rule Meson.disj_comm, rule disjCI, rule conjI)

   508 apply (rule_tac x = obj in exI, simp add:co2sobj_open_none)

   509 apply (simp add:co2sobj_open_none split:option.splits)

   510 apply (rule notI)

   511 apply (frule co2sobj_proc_obj, simp, erule exE)

   512 apply (erule_tac x = p' in allE, simp)

   513 

   514 apply (simp split:if_splits)

   515 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)

   516 apply (erule exE, erule conjE, case_tac "obj = O_proc p")

   517 apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_none)

   518 apply (rule_tac x = obj in exI, simp add:co2sobj_open_none alive_co2sobj_some_open_none)

   519 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)

   520 apply (erule conjE, erule exE, erule conjE, case_tac "obj = O_proc p")

   521 apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_none)

   522 apply (rule_tac x = obj in exI, simp add:co2sobj_open_none alive_co2sobj_some_open_none)

   523 done

   524 

   525 lemma alive_co2sobj_some_open_some:

   526   "\<lbrakk>alive s obj; valid (Open p f flag fd (Some i) # s)\<rbrakk>

   527    \<Longrightarrow> alive (Open p f flag fd (Some i) # s) obj"

   528 by (case_tac obj, auto simp:alive_simps is_file_simps is_dir_simps)

   529 

   530 lemma alive_co2sobj_some_open_some':

   531   "\<lbrakk>co2sobj (Open p f flag fd (Some i) # s) obj = Some sobj; alive (Open p f flag fd (Some i) # s) obj; 

   532     valid (Open p f flag fd (Some i) # s); obj \<noteq> O_file f\<rbrakk> \<Longrightarrow> alive s obj"

   533 by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)

   534 

   535 lemma s2ss_open_some:

   536   "valid (Open p f flag fd (Some i) # s) \<Longrightarrow> s2ss (Open p f flag fd (Some i) # s) = (

   537       case (co2sobj s (O_proc p), co2sobj (Open p f flag fd (Some i) # s) (O_proc p),

   538             co2sobj (Open p f flag fd (Some i) # s) (O_file f)) of

   539         (Some sp, Some sp', Some sf) \<Rightarrow> 

   540            if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)

   541            then s2ss s \<union> {sp', sf} 

   542            else s2ss s - {sp} \<union> {sp', sf} 

   543       | _                   \<Rightarrow> {} )"

   544 unfolding s2ss_def

   545 apply (frule vt_grant_os, frule vd_cons)

   546 apply (case_tac "co2sobj s (O_proc p)", simp add:co2sobj.simps split:option.splits)

   547 apply (drule current_proc_has_sp', simp, simp)

   548 apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (O_proc p)")

   549 apply (simp add:co2sobj.simps split:option.splits)

   550 apply (drule current_proc_has_sp', simp, simp)

   551 apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (O_file f)")

   552 apply (simp add:co2sobj.simps split:option.splits)

   553 apply (clarsimp split del:if_splits)

   554 

   555 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)

   556 apply (split if_splits, rule conjI, rule impI, erule exE, erule conjE, erule conjE)

   557 apply (case_tac "obj = O_proc p", simp, case_tac "obj = O_file f", simp)

   558 apply (rule UnI1, rule CollectI, rule_tac x = obj in exI)

   559 apply (frule_tac obj = obj in alive_co2sobj_some_open_some', simp+)

   560 apply (simp add:co2sobj_open split:t_object.splits)

   561 apply (rule impI, case_tac "obj = O_proc p", simp, case_tac "obj = O_file f", simp)

   562 apply (rule UnI1, rule DiffI, rule CollectI, rule_tac x = obj in exI)

   563 apply (frule_tac obj = obj in alive_co2sobj_some_open_some', simp+)

   564 apply (simp add:co2sobj_open split:t_object.splits)

   565 apply (frule_tac obj = obj in co2sobj_open_some, simp+)

   566 apply (simp add:alive_co2sobj_some_open_some', simp)

   567 apply (rule notI)

   568 apply (frule_tac obj = obj and p = p in co2sobj_proc_obj, simp+, erule exE)

   569 apply (erule_tac x = p' in allE, simp)

   570 

   571 apply (simp split:if_splits, erule disjE)

   572 apply (rule_tac x = "O_proc p" in exI, simp)

   573 apply (erule disjE, rule_tac x = "O_file f" in exI, simp add:is_file_simps)

   574 apply (erule exE, erule conjE)

   575 apply (case_tac "obj = O_proc p", simp)

   576 apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_some)

   577 apply (case_tac "obj = O_file f", simp add:is_file_in_current)

   578 apply (rule_tac x = obj in exI, simp add:co2sobj_open_some alive_co2sobj_some_open_some)

   579 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)

   580 apply (erule disjE, rule_tac x = "O_file f" in exI, simp add:is_file_simps)

   581 apply (erule conjE, erule exE, erule conjE)

   582 apply (case_tac "obj = O_proc p", simp)

   583 apply (case_tac "obj = O_file f", simp add:is_file_in_current)

   584 apply (rule_tac x = obj in exI, simp add:co2sobj_open_some alive_co2sobj_some_open_some)

   585 done

   586 

   587 lemma s2ss_open:

   588   "valid (Open p f flag fd opt # s) \<Longrightarrow> s2ss (Open p f flag fd opt # s) = (

   589      if opt = None

   590      then (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p)) of

   591         (Some sp, Some sp') \<Rightarrow> 

   592            if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)

   593            then s2ss s \<union> {sp'}

   594            else s2ss s - {sp} \<union> {sp'} 

   595       | _                   \<Rightarrow> {} )

   596      else (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p),

   597             co2sobj (Open p f flag fd opt # s) (O_file f)) of

   598         (Some sp, Some sp', Some sf) \<Rightarrow> 

   599            if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)

   600            then s2ss s \<union> {sp', sf} 

   601            else s2ss s - {sp} \<union> {sp', sf} 

   602       | _                   \<Rightarrow> {} ) )"

   603 apply (case_tac opt)

   604 apply (simp add:s2ss_open_some s2ss_open_none)+

   605 done

   606 

   607 lemma s2ss_readfile:

   608   "valid (ReadFile p fd # s) \<Longrightarrow> s2ss (ReadFile p fd # s) = (

   609      case (file_of_proc_fd s p fd) of 

   610        Some f \<Rightarrow> if (O_file f \<in> Tainted s)

   611                  then update_s2ss_shm s p

   612                  else s2ss s

   613      | _      \<Rightarrow> {})"

   614 apply (frule vt_grant_os, frule vd_cons, clarsimp split:option.splits)

   615 apply (rule conjI, rule impI, rule impI, simp)

   616 unfolding update_s2ss_shm_def s2ss_def s2ss_shm_no_backup_def

   617 apply (rule set_eqI, rule iffI)

   618 apply (drule CollectD, (erule exE|erule conjE)+)

   619 apply (erule co2sobj_some_caseD)

   620 apply (rule DiffI)

   621 apply (case_tac "O_proc pa \<in> Tainted s")

   622 apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI)

   623 apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)

   624 apply (case_tac "info_flow_shm s p pa")

   625 apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits)

   626 apply (drule current_proc_has_sp', simp, simp)

   627 apply (rule_tac x = ab in exI, rule_tac x = pa in exI)

   628 apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits)

   629 apply (rule UnI1, simp)

   630 apply (rule_tac x = "O_proc pa" in exI)

   631 apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)

   632 apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)

   633 apply (erule_tac x = pa in allE, simp)

   634 

   635 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI)

   636 apply (simp add:alive_simps co2sobj_readfile, rule notI, clarsimp simp:co2sobj.simps)

   637 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI)

   638 apply (simp add:alive_simps co2sobj_readfile, rule notI, clarsimp simp:co2sobj.simps split:option.splits)

   639 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI)

   640 apply (simp add:alive_simps co2sobj_readfile, rule notI, clarsimp simp:co2sobj.simps split:option.splits)

   641 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI)

   642 apply (simp add:alive_simps co2sobj_readfile, rule notI, clarsimp simp:co2sobj.simps split:option.splits)

   643 

   644 apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE)

   645 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)

   646 apply (erule co2sobj_some_caseD)

   647 apply (case_tac "O_proc pa \<in> Tainted s")

   648 apply (rule_tac x = "O_proc pa" in exI)

   649 apply (clarsimp simp:tainted_eq_Tainted cp2sproc_other co2sobj.simps split:option.splits)

   650 apply (case_tac "info_flow_shm s p pa", simp only:co2sobj.simps split:option.splits)

   651 apply (drule current_proc_has_sp', simp, simp)

   652 apply (drule Meson.not_exD, erule_tac x = ab in allE, drule Meson.not_exD, erule_tac x = pa in allE)

   653 apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+)

   654 apply (rule_tac x = "O_proc p'" in exI)

   655 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)

   656 apply (rule_tac x = "O_proc pa" in exI)

   657 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)

   658 

   659 apply (rule_tac x = obj in exI,

   660        auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1]

   661 apply (rule_tac x = obj in exI,

   662        auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1]

   663 apply (rule_tac x = obj in exI,

   664        auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1]

   665 apply (rule_tac x = obj in exI,

   666        auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1]

   667 

   668 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)

   669 apply (rule_tac x = "O_proc pa" in exI)

   670 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs co2sobj.simps)

   671 

   672 

   673 apply (rule impI, rule impI)

   674 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, rule CollectI)

   675 apply (rule_tac x = obj in exI, simp add:alive_simps co2sobj_readfile split:t_object.splits)

   676 apply (erule CollectE, erule exE, erule conjE, rule CollectI)

   677 apply (rule_tac x = obj in exI, simp add:alive_simps)

   678 apply (drule_tac obj = obj in co2sobj_readfile, simp)

   679 apply (simp split:t_object.splits)

   680 done

   681 

   682 lemma same_inode_files_prop9:

   683   "is_file s f \<Longrightarrow> f \<in> same_inode_files s f"

   684 by (simp add:same_inode_files_def)

   685 

   686 lemma cf2sfiles_prop:

   687   "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> cf2sfiles s f = cf2sfiles s f'"

   688 apply (auto simp:cf2sfiles_def)

   689 apply (rule_tac x = f'a in bexI, simp)

   690 apply (erule same_inode_files_prop4, simp)

   691 apply (rule_tac x = f'a in bexI, simp)

   692 apply (drule same_inode_files_prop5)

   693 apply (erule same_inode_files_prop4, simp)

   694 done

   695 

   696 lemma co2sobj_writefile_unchange:

   697   "\<lbrakk>valid (WriteFile p fd # s); alive s obj; file_of_proc_fd s p fd = Some f;

   698     O_proc p \<in> Tainted s \<longrightarrow> O_file f \<in> Tainted s\<rbrakk> 

   699    \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = co2sobj s obj"

   700 apply (frule vd_cons, frule co2sobj_writefile, simp, simp split:t_object.splits if_splits)

   701 apply (simp add:co2sobj.simps)

   702 apply (case_tac "O_proc p \<in> Tainted s")

   703 apply (simp add:tainted_eq_Tainted same_inodes_Tainted)+

   704 done

   705 

   706 lemma s2ss_writefile:

   707   "valid (WriteFile p fd # s) \<Longrightarrow> s2ss (WriteFile p fd # s) = (

   708      case (file_of_proc_fd s p fd) of

   709        Some f \<Rightarrow> if (O_proc p \<in> Tainted s \<and> O_file f \<notin> Tainted s)

   710                  then (if (\<exists> f'. f' \<notin> same_inode_files s f \<and> is_file s f' \<and>

   711                                  co2sobj s (O_file f') = co2sobj s (O_file f))

   712                        then s2ss s \<union> {S_file (cf2sfiles s f) True}

   713                        else s2ss s - {S_file (cf2sfiles s f) False} 

   714                                    \<union> {S_file (cf2sfiles s f) True})

   715                  else s2ss s

   716      | _      \<Rightarrow> {})"

   717 apply (frule vd_cons, frule vt_grant_os)

   718 apply (clarsimp split:option.splits)

   719 unfolding s2ss_def

   720 apply (rule conjI|rule impI|erule exE|erule conjE)+

   721 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)

   722 apply (frule_tac obj =  obj in co2sobj_writefile, simp add:alive_other)

   723 apply (simp split:t_object.splits if_splits)

   724 apply (rule disjI2, rule_tac x= "O_proc nat" in exI, simp)

   725 apply (rule disjI1, simp add:cf2sfiles_prop)

   726 apply (rule disjI2, rule_tac x = obj in exI, simp add:is_file_simps)

   727 apply (simp add:co2sobj.simps)

   728 apply (rule disjI2, rule_tac x = obj in exI, simp add:is_dir_simps)

   729 apply (simp add:co2sobj.simps)

   730 apply (simp add:co2sobj.simps)

   731 apply (simp add:co2sobj.simps)

   732 apply (rule disjI2, rule_tac x = obj in exI, simp)

   733 apply (rule disjI2, rule_tac x = obj in exI, simp)

   734 apply (simp add:co2sobj.simps)

   735 

   736 apply (simp, erule disjE)

   737 apply (rule_tac x = "O_file aa" in exI, simp add:is_file_simps file_of_pfd_is_file)

   738 apply (frule_tac obj = "O_file aa" in co2sobj_writefile, simp add:file_of_pfd_is_file)

   739 apply (simp split:if_splits add:same_inode_files_def file_of_pfd_is_file)

   740 apply (erule exE, erule conjE)

   741 apply (erule_tac obj = obj in co2sobj_some_caseD)

   742 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)

   743 apply (case_tac "fa \<in> same_inode_files s aa")

   744 apply (frule_tac f = fa and f' = aa in cf2sfiles_prop, simp)

   745 apply (rule_tac x = "O_file f'" in exI, simp add:co2sobj_writefile is_file_simps)

   746 apply (rule conjI, rule impI, simp add:same_inode_files_prop5)

   747 apply (rule impI, simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)

   748 apply (rule_tac x = "O_file fa" in exI, simp add:co2sobj_writefile is_file_simps)

   749 apply (rule impI, simp add:same_inode_files_prop5)

   750 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)

   751 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_dir_simps)

   752 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)

   753 

   754 apply (rule impI, rule impI, simp, rule set_eqI, rule iffI, erule CollectE, (erule conjE|erule exE)+)

   755 apply (rule CollectI, rule_tac x = obj in exI, simp add:alive_simps)

   756 apply (simp add:co2sobj_writefile split:t_object.splits if_splits)

   757 apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)

   758 apply (case_tac "O_proc p \<in> Tainted s", simp, simp)

   759 apply (erule CollectE, (erule conjE|erule exE)+, rule CollectI)

   760 apply (rule_tac x = obj in exI)

   761 apply (simp add:co2sobj_writefile_unchange alive_simps)

   762 

   763 apply (rule impI| rule conjI|erule conjE)+

   764 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)

   765 apply (simp add:alive_simps co2sobj_writefile split:t_object.splits)

   766 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,

   767   rule notI, simp add:co2sobj.simps split:option.splits)

   768 apply (simp split:if_splits)

   769 apply (rule disjI1, simp add:cf2sfiles_prop)

   770 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp)

   771 apply (rule notI, simp add:co2sobj.simps split:option.splits)

   772 apply (erule_tac x = list in allE, simp add:tainted_eq_Tainted same_inode_files_prop5)

   773 apply (simp add:co2sobj.simps)

   774 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,

   775   rule notI, simp add:co2sobj.simps split:option.splits)

   776 apply (simp add:co2sobj.simps)

   777 apply (simp add:co2sobj.simps)

   778 apply (simp add:co2sobj.simps)

   779 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,

   780   rule notI, simp add:co2sobj.simps split:option.splits)

   781 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,

   782   rule notI, simp add:co2sobj.simps split:option.splits)

   783 apply (simp add:co2sobj.simps)

   784 apply (simp)

   785 apply (erule disjE)

   786 apply (rule_tac x= "O_file aa" in exI, simp add:co2sobj_writefile alive_simps file_of_pfd_is_file)

   787 apply (rule impI, simp add:same_inode_files_def file_of_pfd_is_file)

   788 apply (erule exE|erule conjE)+

   789 apply (erule co2sobj_some_caseD)

   790 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)

   791 apply (case_tac "fa \<in> same_inode_files s aa")

   792 apply (frule cf2sfiles_prop, simp, simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)

   793 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_file_simps)

   794 apply (rule impI, simp add:same_inode_files_prop5)

   795 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)

   796 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_dir_simps)

   797 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)

   798 apply (rule impI, rule impI)

   799 

   800 apply (rule set_eqI, rule iffI, erule CollectE,erule exE,erule conjE,rule CollectI)

   801 apply (rule_tac x = obj in exI)

   802 apply (simp add:co2sobj_writefile_unchange alive_simps)

   803 apply (erule CollectE, erule exE, erule conjE)

   804 apply (rule CollectI, rule_tac x = obj in exI)

   805 apply (simp add:co2sobj_writefile_unchange alive_simps)

   806 done

   807 

   808 

   809 definition update_s2ss_obj :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_object \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"

   810 where

   811   "update_s2ss_obj s ss obj sobj sobj' = 

   812      (if (\<exists> obj'. alive s obj' \<and> obj' \<noteq> obj \<and> co2sobj s obj' = Some sobj)

   813       then ss \<union> {sobj'}

   814       else ss - {sobj} \<union> {sobj'})"

   815 

   816 definition update_s2ss_sfile_del :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"

   817 where 

   818   "update_s2ss_sfile_del s ss f sf \<equiv> 

   819      if (same_inode_files s f = {f})

   820      then ss

   821      else ss \<union> {S_file (cf2sfiles s f - {sf}) (O_file f \<in> Tainted s)}"

   822 

   823 definition del_s2ss_file:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"

   824 where

   825   "del_s2ss_file s ss f sf = 

   826      (if (\<exists> f' \<in> same_inode_files s f. f' \<noteq> f \<and> cf2sfile s f' = Some sf)

   827       then ss

   828       else if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (O_file f') = co2sobj s (O_file f))

   829            then update_s2ss_sfile_del s ss f sf

   830            else update_s2ss_sfile_del s (ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)}) f sf)"

   831 

   832 lemma alive_co2sobj_closefd1:

   833   "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; 

   834     file_of_proc_fd s p fd = Some f; \<not> (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})\<rbrakk>

   835    \<Longrightarrow> alive (CloseFd p fd # s) obj"

   836 apply (erule co2sobj_some_caseD)

   837 by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)

   838 

   839 lemma alive_co2sobj_closefd3:

   840   "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; obj \<noteq> O_file f;

   841     file_of_proc_fd s p fd = Some f; f \<in> files_hung_by_del s; proc_fd_of_file s f = {(p, fd)}\<rbrakk>

   842    \<Longrightarrow> alive (CloseFd p fd # s) obj"

   843 apply (erule co2sobj_some_caseD)

   844 by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)

   845 

   846 lemma alive_co2sobj_closefd2:

   847   "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; file_of_proc_fd s p fd = None\<rbrakk>

   848    \<Longrightarrow> alive (CloseFd p fd # s) obj"

   849 apply (erule co2sobj_some_caseD)

   850 by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)

   851 

   852 lemma alive_co2sobj_closefd':

   853   "\<lbrakk>co2sobj (CloseFd p fd # s) obj = Some sobj; alive (CloseFd p fd # s) obj; 

   854     valid (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> alive s obj"

   855 apply (erule co2sobj_some_caseD)

   856 by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits if_splits)

   857 

   858 ML {*asm_full_simp_tac*}

   859 

   860 ML {*

   861 fun my_setiff_tac i = 

   862      (etac @{thm CollectE} i 

   863       ORELSE (     asm_full_simp_tac (HOL_ss addsimps @{thms Set.insert_iff}) i

   864               THEN etac @{thm disjE} i)

   865       ORELSE (     asm_full_simp_tac (HOL_ss addsimps @{thms Set.Diff_iff}) i

   866               THEN etac @{thm conjE} i 

   867               THEN (REPEAT (etac @{thm CollectE} i))))

   868 THEN (REPEAT ((        etac @{thm exE} 

   869                ORELSE' etac @{thm conjE}

   870                ORELSE' etac @{thm bexE}) i))

   871 THEN (rtac @{thm CollectI} i

   872       ORELSE (     asm_full_simp_tac (HOL_ss addsimps @{thms Set.insert_iff}) i))

   873 

   874 *}

   875 

   876 ML {*

   877 fun my_seteq_tac i = 

   878      (simp_tac (HOL_ss addsimps @{thms s2ss_def}) 1)

   879 THEN (rtac @{thm set_eqI} i)

   880 THEN (rtac @{thm iffI} i)

   881 THEN my_setiff_tac i

   882 *}

   883 

   884 lemma co2sobj_sproc_imp:

   885   "co2sobj s obj = Some (S_proc sp tag) \<Longrightarrow> \<exists> p. obj = O_proc p"

   886 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)

   887 

   888 lemma co2sobj_sfile_imp:

   889   "co2sobj s obj = Some (S_file sfs tag) \<Longrightarrow> \<exists> f. obj = O_file f"

   890 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)

   891 

   892 lemma co2sobj_sdir_imp:

   893   "co2sobj s obj = Some (S_dir sf) \<Longrightarrow> \<exists> f. obj = O_dir f"

   894 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)

   895 

   896 lemma co2sobj_sshm_imp:

   897   "co2sobj s obj = Some (S_shm sh) \<Longrightarrow> \<exists> h. obj = O_shm h"

   898 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)

   899 

   900 lemma co2sobj_smsgq_imp:

   901   "co2sobj s obj = Some (S_msgq sq) \<Longrightarrow> \<exists> q. obj = O_msgq q"

   902 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)

   903 

   904 lemma same_inode_files_prop10:

   905   "\<lbrakk>same_inode_files s f \<noteq> {f}; is_file s f\<rbrakk> \<Longrightarrow> \<exists> f'. f' \<in> same_inode_files s f \<and> f' \<noteq> f"

   906 by (auto simp:same_inode_files_def split:if_splits)

   907 

   908 lemma same_inode_files_prop11:

   909   "f \<in> same_inode_files s f' \<Longrightarrow> is_file s f"

   910 by (auto simp:same_inode_files_def is_file_def split:if_splits)

   911 

   912 lemma same_inode_files_prop11':

   913   "f \<in> same_inode_files s f' \<Longrightarrow> is_file s f'"

   914 by (auto simp:same_inode_files_def is_file_def split:if_splits)

   915 

   916 lemma s2ss_closefd:

   917   "valid (CloseFd p fd # s) \<Longrightarrow> s2ss (CloseFd p fd # s) = (

   918      case (file_of_proc_fd s p fd) of

   919        Some f \<Rightarrow> if (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})

   920                  then (case (cf2sfile s f, cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of

   921                          (Some sf, Some sp, Some sp') \<Rightarrow> 

   922                             (del_s2ss_file s (

   923                                update_s2ss_obj s (s2ss s) (O_proc p) 

   924                                  (S_proc sp (O_proc p \<in> Tainted s))

   925                                  (S_proc sp' (O_proc p \<in> Tainted s))) f sf)

   926                       | _ \<Rightarrow> {})

   927                  else (case (cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of 

   928                          (Some sp, Some sp') \<Rightarrow> 

   929                             (update_s2ss_obj s (s2ss s) (O_proc p)

   930                                (S_proc sp (O_proc p \<in> Tainted s))

   931                                (S_proc sp' (O_proc p \<in> Tainted s)))

   932                       | _ \<Rightarrow> {})

   933       | _     \<Rightarrow> s2ss s)"

   934 apply (frule vd_cons, frule vt_grant_os)

   935 apply (clarsimp simp only:os_grant.simps)

   936 apply (frule current_proc_has_sp, simp, erule exE)

   937 apply (case_tac "file_of_proc_fd s p fd")

   938 

   939 apply (simp add:s2ss_def)

   940 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, rule CollectI)

   941 apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd')

   942 apply (frule co2sobj_closefd, simp)

   943 apply (frule cp2sproc_closefd, simp)

   944 apply (simp add:proc_file_fds_def split:t_object.splits)

   945 apply (simp split:if_splits add:co2sobj.simps tainted_eq_Tainted)

   946 apply (erule CollectE, erule exE, erule conjE, rule CollectI)

   947 apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd2)

   948 apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd2)

   949 apply (frule cp2sproc_closefd, simp)

   950 apply (auto simp add:proc_file_fds_def co2sobj.simps tainted_eq_Tainted 

   951             split:t_object.splits option.splits if_splits)[1]

   952 

   953 apply (case_tac "cp2sproc (CloseFd p fd # s) p")

   954 apply (drule current_proc_has_sp', simp, simp)

   955 apply (case_tac "cf2sfile s a")

   956 apply (drule current_file_has_sfile', simp, simp add:file_of_pfd_in_current)

   957 apply (simp)

   958 

   959 apply (rule conjI, rule impI, erule conjE)

   960 apply (simp add:del_s2ss_file_def)

   961 apply (rule conjI|rule impI|erule exE|erule conjE|erule bexE)+

   962 

   963 apply (simp add:update_s2ss_obj_def)

   964 apply (rule conjI|rule impI|erule exE|erule conjE|erule bexE)+

   965 apply (tactic {*my_seteq_tac 1*})

   966 apply simp

   967 apply (case_tac "obj = O_proc p")

   968 apply (simp add:co2sobj.simps tainted_eq_Tainted)

   969 apply (rule disjI2, rule_tac x = obj in exI)

   970 apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_simps)

   971 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)

   972 apply (tactic {*my_setiff_tac 1*})

   973 apply (rule_tac x = "O_proc p" in exI)

   974 apply (simp add:co2sobj.simps tainted_eq_Tainted)

   975 apply (tactic {*my_setiff_tac 1*})

   976 apply (case_tac "obj = O_proc p")

   977 apply (rule_tac x = obj' in exI)

   978 apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)

   979 apply (simp add:co2sobj.simps tainted_eq_Tainted)

   980 apply (case_tac "obj = O_file a")

   981 apply (rule_tac x = "O_file f'" in exI)

   982 apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)

   983 apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)

   984 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)

   985 apply (rule_tac x = obj in exI)

   986 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)

   987 apply (frule_tac obj = obj in co2sobj_closefd, simp)

   988 apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]

   989 

   990 apply (rule impI)+

   991 apply (tactic {*my_seteq_tac 1*})

   992 apply (case_tac "obj = O_proc p", rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted)

   993 apply (rule disjI2)

   994 apply (case_tac "obj = O_file a", simp add:alive_simps)

   995 apply (rule DiffI, simp)

   996 apply (rule_tac x = obj in exI)

   997 apply (frule_tac obj = obj in alive_co2sobj_closefd', simp+)

   998 apply (frule_tac obj = obj in co2sobj_closefd, simp)

   999 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)

  1000 apply (simp, rule notI, simp, frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)

  1001 apply (erule_tac x = "O_proc pa" in allE, simp)

  1002 apply (tactic {*my_setiff_tac 1*})

  1003 apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)

  1004 apply (tactic {*my_setiff_tac 1*})

  1005 apply (case_tac "obj = O_proc p", simp add:co2sobj.simps tainted_eq_Tainted)

  1006 apply (case_tac "obj = O_file a", rule_tac x = "O_file f'" in exI)

  1007 apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)

  1008 apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)

  1009 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)

  1010 apply (rule_tac x = obj in exI)

  1011 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)

  1012 apply (frule_tac obj = obj in co2sobj_closefd, simp)

  1013 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]

  1014 

  1015 apply (rule impI, tactic {*my_seteq_tac 1*})

  1016 apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def)

  1017 apply (rule conjI| rule impI|erule exE|erule conjE)+

  1018 apply (erule_tac obj = obj in co2sobj_some_caseD)

  1019 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)

  1020 apply (rule disjI2, rule_tac x = obj in exI)

  1021 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1022 apply (case_tac "f = a", simp add:alive_simps)

  1023 apply (rule disjI2, rule_tac x = obj in exI)

  1024 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1025 apply (rule disjI2, rule_tac x = obj in exI)

  1026 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1027 apply (rule disjI2, rule_tac x = obj in exI)

  1028 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1029 apply (rule disjI2, rule_tac x = obj in exI)

  1030 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1031 apply (rule conjI| rule impI|erule exE|erule conjE)+

  1032 apply (erule_tac obj = obj in co2sobj_some_caseD)

  1033 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)

  1034 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)

  1035 apply (frule_tac obj = obj in co2sobj_closefd, simp)

  1036 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]

  1037 apply (case_tac "f = a", simp add:alive_simps)

  1038 apply (case_tac "f \<in> same_inode_files s a", rule disjI1)

  1039 apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)

  1040 apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)

  1041 apply (erule bexE, erule conjE)

  1042 apply (erule_tac x = f'' in ballE, simp, simp)

  1043 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)

  1044 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1045 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)

  1046 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1047 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)

  1048 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1049 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)

  1050 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1051 apply (rule impI, rule conjI, rule impI)

  1052 apply (erule_tac obj = obj in co2sobj_some_caseD)

  1053 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)

  1054 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)

  1055 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1056 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_file_simps)

  1057 apply (case_tac "f = a", simp add:alive_simps)

  1058 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)

  1059 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1060 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_file_simps)

  1061 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)

  1062 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1063 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)

  1064 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)

  1065 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1066 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_dir_simps)

  1067 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)

  1068 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1069 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)

  1070 apply (rule impI)

  1071 apply (erule_tac obj = obj in co2sobj_some_caseD)

  1072 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)

  1073 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)

  1074 apply (frule_tac obj = obj in co2sobj_closefd, simp)

  1075 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]

  1076 apply (rule notI, simp add:co2sobj_closefd)

  1077 apply (erule_tac x = obj in allE, simp)

  1078 apply (case_tac "f = a", simp add:alive_simps)

  1079 apply (case_tac "f \<in> same_inode_files s a", rule disjI1)

  1080 apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)

  1081 apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)

  1082 apply (erule bexE, erule conjE)

  1083 apply (erule_tac x = f'' in ballE, simp, simp)

  1084 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)

  1085 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1086 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_file_simps)

  1087 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)

  1088 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1089 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)

  1090 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)

  1091 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1092 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_dir_simps)

  1093 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)

  1094 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)

  1095 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)

  1096 

  1097 apply (simp add:update_s2ss_sfile_del_def update_s2ss_obj_def split:if_splits)

  1098 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)

  1099 apply (erule exE, erule conjE)

  1100 apply (case_tac "obj = O_proc p")

  1101 apply (rule_tac x = obj' in exI)

  1102 apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)

  1103 apply (simp add:co2sobj.simps tainted_eq_Tainted)

  1104 apply (case_tac "obj = O_file a")

  1105 apply (rule_tac x = "O_file f'" in exI)

  1106 apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)

  1107 apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)

  1108 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)

  1109 apply (rule_tac x = obj in exI)

  1110 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)

  1111 apply (frule_tac obj = obj in co2sobj_closefd, simp)

  1112 apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]

  1113 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)

  1114 apply (erule conjE, erule exE, erule conjE)

  1115 apply (case_tac "obj = O_proc p")

  1116 apply (simp add:co2sobj.simps tainted_eq_Tainted)

  1117 apply (case_tac "obj = O_file a")

  1118 apply (rule_tac x = "O_file f'" in exI)

  1119 apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)

  1120 apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)

  1121 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)

  1122 apply (rule_tac x = obj in exI)

  1123 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)

  1124 apply (frule_tac obj = obj in co2sobj_closefd, simp)

  1125 apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]

  1126 apply (erule disjE)

  1127 apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE)

  1128 apply (rule_tac x = "O_file f'a" in exI)

  1129 apply (frule same_inode_files_prop11)

  1130 apply (frule_tac obj = "O_file f'a" in co2sobj_closefd)

  1131 apply (simp add:alive_simps)+

  1132 apply (frule_tac f = "f'a" in is_file_has_sfile', simp, erule exE)

  1133 apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits)

  1134 apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)

  1135 apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)