1 (*<*)

     1 (*<*)

     2 theory S2ss_prop

     2 theory S2ss_prop

     4 begin

     4 begin

     5 (*>*)

     5 (*>*)

     6 

     6 

     7 context tainting_s begin

     7 context tainting_s begin

     8 

     8 

     9 (* simpset for s2ss*)

     9 (* simpset for s2ss*)

    10 

    10 

    24 lemma s2ss_execve':

    11 lemma s2ss_execve':

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

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

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

    14      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)}

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

    29            | _ \<Rightarrow> {} )

    16            | _ \<Rightarrow> {} )

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

    17      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)}

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

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

    26 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)

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

    41 apply (erule exE, simp)

    28 apply (erule exE, simp)

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

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

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

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

    45 apply (simp add:co2sobj_execve split:if_splits)

    32 apply (simp add:co2sobj_execve split:if_splits)

    46 apply (simp add:co2sobj_execve, rule disjI2)

    33 apply (simp add:co2sobj_execve, rule disjI2)

    48 apply (simp, erule disjE)

    35 apply (simp, erule disjE)

    50 apply (erule exE| erule conjE)+

    37 apply (erule exE| erule conjE)+

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

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

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

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

    58 

    44 

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

    45 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)") 

    46 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)

    47 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)

    48 apply (erule exE, erule conjE, simp)

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

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

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

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

    66 apply (rule disjI1, simp split:if_splits)

    52 apply (rule disjI1, simp split:if_splits)

    67 apply (simp add:co2sobj_execve, rule disjI2)

    53 apply (simp add:co2sobj_execve, rule disjI2)

    69 apply (rule notI, simp, case_tac obj)

    55 apply (rule notI, simp, case_tac obj)

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

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

    71 apply (erule disjE, simp)

    57 apply (erule disjE, simp)

    73 apply (erule exE|erule conjE)+

    59 apply (erule exE|erule conjE)+

    77 apply (rule impI, simp, simp)

    62 apply (rule impI, simp, simp)

    78 done

    63 done

    84 

    64 

    85 lemma s2ss_clone:

    65 lemma s2ss_clone:

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

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

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

    67      case (cp2sproc (Clone p p' fds # s) p') of

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

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

    89      | _       \<Rightarrow> {})"

    69      | _       \<Rightarrow> {})"

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

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

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

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

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

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

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

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

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

    75 apply (case_tac "O_proc p' \<in> tainted s", drule tainted_in_current, simp+)

    96 apply (rule disjI1, simp split:if_splits)

    76 apply (rule disjI1, simp split:if_splits)

    97 apply (simp, rule disjI2)

    77 apply (simp, rule disjI2)

    98 apply (frule co2sobj_clone, simp)

    78 apply (frule co2sobj_clone, simp)

   100 

    81 

   101 apply (simp, erule disjE, simp)

    82 apply (simp, erule disjE, simp)

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

    84 apply (rule impI, rule notI, drule tainted_in_current, simp+)

   104 apply (erule exE| erule conjE)+

    85 apply (erule exE| erule conjE)+

   109 done

    91 done

   110 

    92 

   111 (*

    93 (*

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

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

   113 where

    95 where

   165       else if (O_proc p' \<in> tainted s \<and> O_proc p \<notin> tainted s)

   147       else if (O_proc p' \<in> tainted s \<and> O_proc p \<notin> tainted s)

   166            then tainted s \<union> {O_proc p}

   148            then tainted s \<union> {O_proc p}

   167                 else tainted s)"

   149                 else tainted s)"

   168 by auto

   150 by auto

   169 

   151 

   170 lemma co2sobj_some_caseD:

   153 lemma co2sobj_some_caseD:

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

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

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

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

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

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

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

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

   175    \<Longrightarrow> P obj"

   158    \<Longrightarrow> P obj"

   176 by (case_tac obj, auto)

   159 by (case_tac obj, auto)

   179 where

   163 where

   180   "update_s2ss_obj s ss obj sobj sobj' = 

   164   "update_s2ss_obj s ss obj sobj sobj' = 

   182       then ss \<union> {sobj'}

   166       then ss \<union> {sobj'}

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

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

   184 

   168 

   185 ML {*

   169 ML {*

   186 fun my_setiff_tac i = 

   170 fun my_setiff_tac i = 

   216    ORELSE' etac @{thm bexE}

   200    ORELSE' etac @{thm bexE}

   217    ORELSE' etac @{thm disjE}) i)

   201    ORELSE' etac @{thm disjE}) i)

   218 *}

   202 *}

   219 

   203 

   220 lemma co2sobj_sproc_imp:

   204 lemma co2sobj_sproc_imp:

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

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

   223 

   207 

   224 lemma co2sobj_sfile_imp:

   208 lemma co2sobj_sfile_imp:

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

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

   227 

   211 

   228 lemma co2sobj_sdir_imp:

   212 lemma co2sobj_sdir_imp:

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

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

   231 

   215 

   232 lemma co2sobj_smsgq_imp:

   216 lemma co2sobj_smsgq_imp:

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

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

   235 

   219 

   236 lemma s2ss_execve:

   220 lemma s2ss_execve:

   237   "valid (Execve p f fds # s) \<Longrightarrow> 

   221   "valid (Execve p f fds # s) \<Longrightarrow> 

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

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

   239         (Some sp, Some sp') \<Rightarrow> s2ss (Execve p f fds # s) = 

   223         (Some sp, Some sp') \<Rightarrow> s2ss (Execve p f fds # s) = 

   241                           (S_proc sp' (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s))

   225                           (S_proc sp' (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s))

   242       | _ \<Rightarrow> s2ss (Execve p f fds # s) = {})"

   226       | _ \<Rightarrow> s2ss (Execve p f fds # s) = {})"

   243 apply (frule vd_cons, frule vt_grant_os)

   227 apply (frule vd_cons, frule vt_grant_os)

   244 apply (clarsimp simp only:os_grant.simps)

   228 apply (clarsimp simp only:os_grant.simps)

   245 apply (case_tac "cp2sproc s p")

   229 apply (case_tac "cp2sproc s p")

   255 apply (rule impI)

   239 apply (rule impI)

   256 apply (simp add:s2ss_execve')

   240 apply (simp add:s2ss_execve')

   257 apply (rule impI)

   241 apply (rule impI)

   258 apply (tactic {*my_clarify_tac 1*})

   242 apply (tactic {*my_clarify_tac 1*})

   259 apply (simp split:option.splits)

   243 apply (simp split:option.splits)

   261 done

   245 done

   262 

   246 

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

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

   264 

   248 

   265 lemma s2ss_ptrace1:

   249 lemma s2ss_ptrace1:

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

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

   267    \<Longrightarrow> (case (cp2sproc s p') of 

   251    \<Longrightarrow> (case (cp2sproc s p') of 

   268           Some sp' \<Rightarrow> s2ss (Ptrace p p' # s) = 

   252           Some sp' \<Rightarrow> s2ss (Ptrace p p' # s) = 

   270         | _        \<Rightarrow> s2ss (Ptrace p p' # s) = {})"

   254         | _        \<Rightarrow> s2ss (Ptrace p p' # s) = {})"

   271 apply (frule vd_cons, frule vt_grant_os)

   255 apply (frule vd_cons, frule vt_grant_os)

   272 apply (clarsimp simp only:os_grant.simps)

   256 apply (clarsimp simp only:os_grant.simps)

   273 apply (case_tac "cp2sproc s p'")

   257 apply (case_tac "cp2sproc s p'")

   274 apply (drule current_proc_has_sp', simp+)

   258 apply (drule current_proc_has_sp', simp+)

   277 

   261 

   278 apply (simp add:update_s2ss_obj_def)

   262 apply (simp add:update_s2ss_obj_def)

   279 apply (tactic {*my_clarify_tac 1*})

   263 apply (tactic {*my_clarify_tac 1*})

   280 apply (simp add:s2ss_def)

   264 apply (simp add:s2ss_def)

   281 apply (tactic {*my_seteq_tac 1*})

   265 apply (tactic {*my_seteq_tac 1*})

   283 apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)

   267 apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)

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

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

   290 apply (rule_tac x = obj' in exI)

   274 apply (rule_tac x = obj' in exI)

   292 apply (auto simp:co2sobj.simps)[1]

   276 apply (auto simp:co2sobj.simps)[1]

   294 apply (auto simp:co2sobj.simps)[1]

   278 apply (auto simp:co2sobj.simps)[1]

   295 

   279 

   296 apply (rule impI)

   280 apply (rule impI)

   297 apply (simp add:s2ss_def)

   281 apply (simp add:s2ss_def)

   298 apply (tactic {*my_seteq_tac 1*})

   282 apply (tactic {*my_seteq_tac 1*})

   300 apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)

   284 apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)

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

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

   303 apply (rule notI, simp)

   287 apply (rule notI, simp)

   304 apply (frule_tac obj = obj in co2sobj_sproc_imp, erule exE, simp)

   288 apply (frule_tac obj = obj in co2sobj_sproc_imp, erule exE, simp)

   305 apply (erule_tac x = obj in allE, simp add:co2sobj_ptrace cp2sproc_other split:option.splits)

   289 apply (erule_tac x = obj in allE, simp add:co2sobj_ptrace cp2sproc_other split:option.splits)

   306 apply (tactic {*my_setiff_tac 1*})

   290 apply (tactic {*my_setiff_tac 1*})

   310 apply (simp add:co2sobj.simps cp2sproc_other)

   294 apply (simp add:co2sobj.simps cp2sproc_other)

   312 apply (auto simp:co2sobj.simps)[1]

   296 apply (auto simp:co2sobj.simps)[1]

   313 done

   297 done

   314 

   298 

   315 lemma s2ss_ptrace2:

   299 lemma s2ss_ptrace2:

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

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

   317    \<Longrightarrow> (case (cp2sproc s p) of 

   301    \<Longrightarrow> (case (cp2sproc s p) of 

   318           Some sp \<Rightarrow> s2ss (Ptrace p p' # s) = 

   302           Some sp \<Rightarrow> s2ss (Ptrace p p' # s) = 

   320         | _       \<Rightarrow> s2ss (Ptrace p p' # s) = {})"

   304         | _       \<Rightarrow> s2ss (Ptrace p p' # s) = {})"

   321 apply (frule vd_cons, frule vt_grant_os)

   305 apply (frule vd_cons, frule vt_grant_os)

   322 apply (clarsimp simp only:os_grant.simps)

   306 apply (clarsimp simp only:os_grant.simps)

   323 apply (case_tac "cp2sproc s p'")

   307 apply (case_tac "cp2sproc s p'")

   324 apply (drule current_proc_has_sp', simp+)

   308 apply (drule current_proc_has_sp', simp+)

   327 

   311 

   328 apply (simp add:update_s2ss_obj_def)

   312 apply (simp add:update_s2ss_obj_def)

   329 apply (tactic {*my_clarify_tac 1*})

   313 apply (tactic {*my_clarify_tac 1*})

   330 apply (simp add:s2ss_def)

   314 apply (simp add:s2ss_def)

   331 apply (tactic {*my_seteq_tac 1*})

   315 apply (tactic {*my_seteq_tac 1*})

   333 apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)

   317 apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)

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

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

   340 apply (rule_tac x = obj' in exI)

   324 apply (rule_tac x = obj' in exI)

   342 apply (auto simp:co2sobj.simps)[1]

   326 apply (auto simp:co2sobj.simps)[1]

   344 apply (auto simp:co2sobj.simps)[1]

   328 apply (auto simp:co2sobj.simps)[1]

   345 

   329 

   346 apply (rule impI)

   330 apply (rule impI)

   347 apply (simp add:s2ss_def)

   331 apply (simp add:s2ss_def)

   348 apply (tactic {*my_seteq_tac 1*})

   332 apply (tactic {*my_seteq_tac 1*})

   350 apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)

   334 apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)

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

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

   353 apply (rule notI, simp)

   337 apply (rule notI, simp)

   354 apply (frule_tac obj = obj in co2sobj_sproc_imp, erule exE, simp)

   338 apply (frule_tac obj = obj in co2sobj_sproc_imp, erule exE, simp)

   355 apply (erule_tac x = obj in allE, simp add:co2sobj_ptrace cp2sproc_other split:option.splits)

   339 apply (erule_tac x = obj in allE, simp add:co2sobj_ptrace cp2sproc_other split:option.splits)

   356 apply (tactic {*my_setiff_tac 1*})

   340 apply (tactic {*my_setiff_tac 1*})

   360 apply (simp add:co2sobj.simps cp2sproc_other)

   344 apply (simp add:co2sobj.simps cp2sproc_other)

   362 apply (auto simp:co2sobj.simps)[1]

   346 apply (auto simp:co2sobj.simps)[1]

   363 done

   347 done

   364 

   348 

   365 lemma s2ss_ptrace3:

   349 lemma s2ss_ptrace3:

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

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

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

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

   368 unfolding s2ss_def

   352 unfolding s2ss_def

   369 apply (frule vd_cons, frule vt_grant_os, rule set_eqI, rule iffI)

   353 apply (frule vd_cons, frule vt_grant_os, rule set_eqI, rule iffI)

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

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

   371 apply (rule_tac x = obj in exI)

   355 apply (rule_tac x = obj in exI)

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

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

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

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

   380 apply (case_tac "cp2sproc s p'")

   364 apply (case_tac "cp2sproc s p'")

   381 apply (drule current_proc_has_sp', simp, simp)

   365 apply (drule current_proc_has_sp', simp, simp)

   382 apply (case_tac "cp2sproc s p")

   366 apply (case_tac "cp2sproc s p")

   383 apply (drule current_proc_has_sp', simp, simp)

   367 apply (drule current_proc_has_sp', simp, simp)

   384 apply (case_tac "O_proc p' \<in> tainted s")

   368 apply (case_tac "O_proc p' \<in> tainted s")

   386 done

   370 done

   387 

   371 

   388 lemma s2ss_ptrace:

   372 lemma s2ss_ptrace:

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

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

   390      if (O_proc p \<in> tainted s \<and> O_proc p' \<notin> tainted s) 

   374      if (O_proc p \<in> tainted s \<and> O_proc p' \<notin> tainted s) 

   391      then (case (cp2sproc s p') of 

   375      then (case (cp2sproc s p') of 

   393            | _       \<Rightarrow> {})

   377            | _       \<Rightarrow> {})

   394      else if (O_proc p' \<in> tainted s \<and> O_proc p \<notin> tainted s)

   378      else if (O_proc p' \<in> tainted s \<and> O_proc p \<notin> tainted s)

   395           then (case (cp2sproc s p) of 

   379           then (case (cp2sproc s p) of 

   397                 | _       \<Rightarrow> {})

   381                 | _       \<Rightarrow> {})

   398           else s2ss s                                   )"

   382           else s2ss s                                   )"

   399 apply (case_tac "O_proc p \<in> tainted s \<and> O_proc p' \<notin> tainted s")

   383 apply (case_tac "O_proc p \<in> tainted s \<and> O_proc p' \<notin> tainted s")

   400 apply (drule s2ss_ptrace1, simp, simp, simp split:option.splits)

   384 apply (drule s2ss_ptrace1, simp, simp, simp split:option.splits)

   401 apply (case_tac "O_proc p' \<in> tainted s \<and> O_proc p \<notin> tainted s")

   385 apply (case_tac "O_proc p' \<in> tainted s \<and> O_proc p \<notin> tainted s")

   403 apply (drule s2ss_ptrace3, auto)

   387 apply (drule s2ss_ptrace3, auto)

   404 done

   388 done

   405 

   389 

   406 lemma s2ss_kill':

   390 lemma s2ss_kill':

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

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

   409      then s2ss s 

   393      then s2ss s 

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

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

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

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

   413 apply (frule vt_grant_os, frule vd_cons)

   397 apply (frule vt_grant_os, frule vd_cons)

   414 unfolding s2ss_def

   398 unfolding s2ss_def

   415 apply (simp split:if_splits, rule conjI)

   399 apply (simp split:if_splits, rule conjI)

   417 apply (split option.splits)

   401 apply (split option.splits)

   418 apply (drule current_proc_has_sp', simp, simp)

   402 apply (drule current_proc_has_sp', simp, simp)

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

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

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

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

   421 apply (rule_tac x = obj in exI)

   405 apply (rule_tac x = obj in exI)

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

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

   433 

   417 

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

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

   435 apply (rule set_eqI, rule iffI)

   419 apply (rule set_eqI, rule iffI)

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

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

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

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

   439 apply (rule notI, simp, case_tac obj)

   423 apply (rule notI, simp, case_tac obj)

   440 apply (erule_tac x = nat in allE)

   424 apply (erule_tac x = nat in allE)

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

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

   442 apply (simp split:option.splits)+

   426 apply (simp split:option.splits)+

   455 where

   439 where

   456   "del_s2ss_obj s ss obj sobj \<equiv> 

   440   "del_s2ss_obj s ss obj sobj \<equiv> 

   458      then ss

   442      then ss

   459      else ss - {sobj}"

   443      else ss - {sobj}"

   460 

   444 

   461 lemma del_update_s2ss_obj:

   445 lemma del_update_s2ss_obj:

   462   "update_s2ss_obj s ss obj sobj sobj' = del_s2ss_obj s ss obj sobj \<union> {sobj'}"

   446   "update_s2ss_obj s ss obj sobj sobj' = del_s2ss_obj s ss obj sobj \<union> {sobj'}"

   463 by (auto simp:update_s2ss_obj_def del_s2ss_obj_def split:if_splits)

   447 by (auto simp:update_s2ss_obj_def del_s2ss_obj_def split:if_splits)

   464 

   448 

   465 lemma s2ss_kill:

   449 lemma s2ss_kill:

   466   "valid (Kill p p' # s) \<Longrightarrow> (

   450   "valid (Kill p p' # s) \<Longrightarrow> (

   467       case (cp2sproc s p') of 

   451       case (cp2sproc s p') of 

   469       | _       \<Rightarrow> s2ss (Kill p p' # s) = {})"

   453       | _       \<Rightarrow> s2ss (Kill p p' # s) = {})"

   470 apply (frule vd_cons, frule vt_grant_os)

   454 apply (frule vd_cons, frule vt_grant_os)

   471 apply (clarsimp simp only:os_grant.simps)

   455 apply (clarsimp simp only:os_grant.simps)

   472 apply (split option.splits, rule conjI, rule impI)

   456 apply (split option.splits, rule conjI, rule impI)

   473 apply (drule current_proc_has_sp', simp, simp)

   457 apply (drule current_proc_has_sp', simp, simp)

   481 apply (rule impI)

   465 apply (rule impI)

   482 apply (simp add:s2ss_kill')

   466 apply (simp add:s2ss_kill')

   483 apply (rule impI)

   467 apply (rule impI)

   484 apply (tactic {*my_clarify_tac 1*})

   468 apply (tactic {*my_clarify_tac 1*})

   485 apply (simp split:option.splits)

   469 apply (simp split:option.splits)

   487 done

   471 done

   488 

   472 

   489 lemma s2ss_exit':

   473 lemma s2ss_exit':

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

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

   492      then s2ss s 

   476      then s2ss s 

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

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

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

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

   496 apply (frule vt_grant_os, frule vd_cons)

   480 apply (frule vt_grant_os, frule vd_cons)

   497 unfolding s2ss_def

   481 unfolding s2ss_def

   498 apply (simp split:if_splits, rule conjI)

   482 apply (simp split:if_splits, rule conjI)

   500 apply (split option.splits)

   484 apply (split option.splits)

   501 apply (drule current_proc_has_sp', simp, simp)

   485 apply (drule current_proc_has_sp', simp, simp)

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

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

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

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

   504 apply (rule_tac x = obj in exI)

   488 apply (rule_tac x = obj in exI)

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

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

   516 

   500 

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

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

   518 apply (rule set_eqI, rule iffI)

   502 apply (rule set_eqI, rule iffI)

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

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

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

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

   522 apply (rule notI, simp, case_tac obj)

   506 apply (rule notI, simp, case_tac obj)

   523 apply (erule_tac x = nat in allE)

   507 apply (erule_tac x = nat in allE)

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

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

   525 apply (simp split:option.splits)+

   509 apply (simp split:option.splits)+

   535 done

   519 done

   536 

   520 

   537 lemma s2ss_exit:

   521 lemma s2ss_exit:

   538   "valid (Exit p # s) \<Longrightarrow> (

   522   "valid (Exit p # s) \<Longrightarrow> (

   539       case (cp2sproc s p) of 

   523       case (cp2sproc s p) of 

   541       | _       \<Rightarrow> s2ss (Exit p # s) = {})"

   525       | _       \<Rightarrow> s2ss (Exit p # s) = {})"

   542 apply (frule vd_cons, frule vt_grant_os)

   526 apply (frule vd_cons, frule vt_grant_os)

   543 apply (clarsimp simp only:os_grant.simps)

   527 apply (clarsimp simp only:os_grant.simps)

   544 apply (split option.splits, rule conjI, rule impI)

   528 apply (split option.splits, rule conjI, rule impI)

   545 apply (drule current_proc_has_sp', simp, simp)

   529 apply (drule current_proc_has_sp', simp, simp)

   553 apply (rule impI)

   537 apply (rule impI)

   554 apply (simp add:s2ss_exit')

   538 apply (simp add:s2ss_exit')

   555 apply (rule impI)

   539 apply (rule impI)

   556 apply (tactic {*my_clarify_tac 1*})

   540 apply (tactic {*my_clarify_tac 1*})

   557 apply (simp split:option.splits)

   541 apply (simp split:option.splits)

   563 apply (case_tac obj)

   547 apply (case_tac obj)

   564 apply (auto split:option.splits)

   548 apply (auto split:option.splits)

   565 oops

   549 oops

   566 

   550 

   567 declare co2sobj.simps [simp del]

   551 declare co2sobj.simps [simp del]

   568 

   552 

   569 lemma co2sobj_open_none:

   553 lemma co2sobj_open_none:

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

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

   573               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))

   557               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))

   574            | _       \<Rightarrow> None)

   558            | _       \<Rightarrow> None)

   575       else co2sobj s obj)"

   559       else co2sobj s obj)"

   576 apply (frule vt_grant_os, frule vd_cons)

   560 apply (frule vt_grant_os, frule vd_cons)

   579 done

   563 done

   580 

   564 

   581 lemma co2sobj_open_some:

   565 lemma co2sobj_open_some:

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

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

   585               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))

   569               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))

   586            | _       \<Rightarrow> None)

   570            | _       \<Rightarrow> None)

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

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

   589                    Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> tainted s))

   573                    Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> tainted s))

   590                  | _       \<Rightarrow> None)

   574                  | _       \<Rightarrow> None)

   591            else co2sobj s obj)"

   575            else co2sobj s obj)"

   592 apply (frule vt_grant_os, frule vd_cons)

   576 apply (frule vt_grant_os, frule vd_cons)

   606 

   580 

   607 lemma co2sobj_proc_obj:

   581 lemma co2sobj_proc_obj:

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

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

   611 

   585 

   612 lemma s2ss_open_none:

   586 lemma s2ss_open_none:

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

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

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

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

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

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

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

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

   619       | _                   \<Rightarrow> {} )"

   593       | _                   \<Rightarrow> {} )"

   620 unfolding s2ss_def

   594 unfolding s2ss_def

   621 apply (frule vt_grant_os, frule vd_cons)

   595 apply (frule vt_grant_os, frule vd_cons)

   623 apply (drule current_proc_has_sp', simp, simp)

   597 apply (drule current_proc_has_sp', simp, simp)

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

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

   626 apply (drule current_proc_has_sp', simp, simp)

   600 apply (drule current_proc_has_sp', simp, simp)

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

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

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

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

   632 apply (rule impI)

   606 apply (rule impI)

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

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

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

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

   640 

   614 

   641 apply (simp split:if_splits)

   615 apply (simp split:if_splits)

   661 

   625 

   662 lemma s2ss_open_some:

   626 lemma s2ss_open_some:

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

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

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

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

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

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

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

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

   670       | _                   \<Rightarrow> {} )"

   634       | _                   \<Rightarrow> {} )"

   671 unfolding s2ss_def

   635 unfolding s2ss_def

   672 apply (frule vt_grant_os, frule vd_cons)

   636 apply (frule vt_grant_os, frule vd_cons)

   674 apply (drule current_proc_has_sp', simp, simp)

   638 apply (drule current_proc_has_sp', simp, simp)

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

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

   677 apply (drule current_proc_has_sp', simp, simp)

   641 apply (drule current_proc_has_sp', simp, simp)

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

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

   680 apply (clarsimp split del:if_splits)

   644 apply (clarsimp split del:if_splits)

   681 

   645 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   697 

   659 

   698 apply (simp split:if_splits, erule disjE)

   660 apply (simp split:if_splits, erule disjE)

   701 apply (erule exE, erule conjE)

   663 apply (erule exE, erule conjE)

   708 apply (erule conjE, erule exE, erule conjE)

   670 apply (erule conjE, erule exE, erule conjE)

   712 done

   674 done

   713 

   675 

   714 lemma s2ss_open':

   676 lemma s2ss_open':

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

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

   716      if opt = None

   678      if opt = None

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

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

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

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

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

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

   722       | _                   \<Rightarrow> {} )

   684       | _                   \<Rightarrow> {} )

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

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

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

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

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

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

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

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

   730 apply (case_tac opt)

   692 apply (case_tac opt)

   731 apply (simp add:s2ss_open_some s2ss_open_none)+

   693 apply (simp add:s2ss_open_some s2ss_open_none)+

   732 done

   694 done

   733 

   695 

   734 lemma co2sobj_proc_eq_some:

   696 lemma co2sobj_proc_eq_some:

   737 apply (case_tac obj, case_tac[!] sp)

   699 apply (case_tac obj, case_tac[!] sp)

   738 by (auto simp:co2sobj.simps split:option.splits)

   700 by (auto simp:co2sobj.simps split:option.splits)

   739 

   701 

   740 lemma s2ss_open:

   702 lemma s2ss_open:

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

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

   744        (Some sp, Some sp', Some sf) \<Rightarrow> s2ss (Open p f flag fd opt # s) = (

   706        (Some sp, Some sp', Some sf) \<Rightarrow> s2ss (Open p f flag fd opt # s) = (

   745        if opt = None

   707        if opt = None

   748      | _ \<Rightarrow> s2ss (Open p f flag fd opt # s) = {})"

   710      | _ \<Rightarrow> s2ss (Open p f flag fd opt # s) = {})"

   749 apply (frule vt_grant_os, frule vd_cons, clarsimp simp only:os_grant.simps)

   711 apply (frule vt_grant_os, frule vd_cons, clarsimp simp only:os_grant.simps)

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

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

   752 apply (drule current_proc_has_sp', simp, simp)

   714 apply (drule current_proc_has_sp', simp, simp)

   753 apply (drule current_proc_has_sp', simp, simp)

   715 apply (drule current_proc_has_sp', simp, simp)

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

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

   756 apply (drule current_proc_has_sp', simp, simp)

   718 apply (drule current_proc_has_sp', simp, simp)

   757 apply (drule current_proc_has_sp', simp, simp)

   719 apply (drule current_proc_has_sp', simp, simp)

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

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

   760 apply (simp split:option.splits add:s2ss_open' update_s2ss_obj_def)

   722 apply (simp split:option.splits add:s2ss_open' update_s2ss_obj_def)

   761 apply (auto)

   723 apply (auto)

   763 apply (frule_tac obj = obj' in co2sobj_proc_eq_some, simp, erule exE, simp)

   725 apply (frule_tac obj = obj' in co2sobj_proc_eq_some, simp, erule exE, simp)

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

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

   766 apply (frule_tac obj = obj' in co2sobj_proc_eq_some, simp, erule exE, simp)

   728 apply (frule_tac obj = obj' in co2sobj_proc_eq_some, simp, erule exE, simp)

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

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

   769 apply (frule_tac obj = obj' in co2sobj_proc_eq_some, simp, erule exE, simp)

   731 apply (frule_tac obj = obj' in co2sobj_proc_eq_some, simp, erule exE, simp)

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

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

   771 done

   733 done

   772 

   734 

   773 lemma s2ss_readfile:

   735 lemma s2ss_readfile:

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

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

   775      case (file_of_proc_fd s p fd) of 

   737      case (file_of_proc_fd s p fd) of 

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

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

   777                  then (case (cp2sproc s p) of 

   739                  then (case (cp2sproc s p) of 

   779                        | _       \<Rightarrow> {})

   741                        | _       \<Rightarrow> {})

   780                  else s2ss s

   742                  else s2ss s

   781      | _      \<Rightarrow> {})"

   743      | _      \<Rightarrow> {})"

   782 apply (frule vt_grant_os, frule vd_cons, clarsimp simp only:os_grant.simps)

   744 apply (frule vt_grant_os, frule vd_cons, clarsimp simp only:os_grant.simps)

   783 apply (case_tac "cp2sproc s p")

   745 apply (case_tac "cp2sproc s p")

   787 apply (simp add:update_s2ss_obj_def)

   749 apply (simp add:update_s2ss_obj_def)

   788 apply (tactic {*my_clarify_tac 1*})

   750 apply (tactic {*my_clarify_tac 1*})

   789 apply (frule co2sobj_sproc_imp, erule exE, simp split:option.splits)

   751 apply (frule co2sobj_sproc_imp, erule exE, simp split:option.splits)

   790 apply (simp add:s2ss_def)

   752 apply (simp add:s2ss_def)

   791 apply (tactic {*my_seteq_tac 1*})

   753 apply (tactic {*my_seteq_tac 1*})

   793 apply (rule disjI1, simp add:co2sobj_readfile)

   755 apply (rule disjI1, simp add:co2sobj_readfile)

   794 apply (rule disjI2, simp)

   756 apply (rule disjI2, simp)

   795 apply (rule_tac x = obj in exI)

   757 apply (rule_tac x = obj in exI)

   805 apply (tactic {*my_clarify_tac 1*})

   767 apply (tactic {*my_clarify_tac 1*})

   806 apply (simp add:s2ss_def)

   768 apply (simp add:s2ss_def)

   807 apply (tactic {*my_seteq_tac 1*})

   769 apply (tactic {*my_seteq_tac 1*})

   809 apply (rule disjI1, simp add:co2sobj_readfile)

   771 apply (rule disjI1, simp add:co2sobj_readfile)

   810 apply (rule disjI2, rule DiffI)

   772 apply (rule disjI2, rule DiffI)

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

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

   813 apply (rule notI, erule_tac x = obj in allE)

   775 apply (rule notI, erule_tac x = obj in allE)

   820 apply (simp add:co2sobj.simps)

   782 apply (simp add:co2sobj.simps)

   821 

   783 

   822 apply (simp add:s2ss_def, rule impI)

   784 apply (simp add:s2ss_def, rule impI)

   823 apply (tactic {*my_seteq_tac 1*})

   785 apply (tactic {*my_seteq_tac 1*})

   824 apply (rule_tac x = obj in exI)

   786 apply (rule_tac x = obj in exI)

   830 apply (simp add:co2sobj.simps)

   792 apply (simp add:co2sobj.simps)

   831 done

   793 done

   832 

   794 

   833 lemma same_inode_files_prop9:

   795 lemma same_inode_files_prop9:

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

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

   843 apply (drule same_inode_files_prop5)

   805 apply (drule same_inode_files_prop5)

   844 apply (erule same_inode_files_prop4, simp)

   806 apply (erule same_inode_files_prop4, simp)

   845 done

   807 done

   846 

   808 

   847 lemma co2sobj_writefile_unchange:

   809 lemma co2sobj_writefile_unchange:

   849     O_proc p \<in> tainted s \<longrightarrow> O_file f \<in> tainted s\<rbrakk> 

   811     O_proc p \<in> tainted s \<longrightarrow> O_file f \<in> tainted s\<rbrakk> 

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

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

   852 apply (simp add:co2sobj.simps)

   814 apply (simp add:co2sobj.simps)

   853 apply (case_tac "O_proc p \<in> tainted s")

   815 apply (case_tac "O_proc p \<in> tainted s")

   854 apply (simp add:same_inodes_tainted)+

   816 apply (simp add:same_inodes_tainted)+

   855 done

   817 done

   856 

   818 

   857 lemma s2ss_writefile':

   819 lemma s2ss_writefile':

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

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

   859      case (file_of_proc_fd s p fd) of

   821      case (file_of_proc_fd s p fd) of

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

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

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

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

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

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

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

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

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

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

   866                  else s2ss s

   828                  else s2ss s

   867      | _      \<Rightarrow> {})"

   829      | _      \<Rightarrow> {})"

   868 apply (frule vd_cons, frule vt_grant_os)

   830 apply (frule vd_cons, frule vt_grant_os)

   869 apply (clarsimp split:option.splits)

   831 apply (clarsimp split:option.splits)

   870 unfolding s2ss_def

   832 unfolding s2ss_def

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

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

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

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

   876 apply (rule disjI1, simp add:cf2sfiles_prop)

   838 apply (rule disjI1, simp add:cf2sfiles_prop)

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

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

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

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

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

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

   885 apply (simp add:co2sobj.simps)

   842 apply (simp add:co2sobj.simps)

   886 

   843 

   887 apply (erule disjE)

   844 apply (erule disjE)

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

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

   891 apply (erule exE, erule conjE, erule conjE)

   848 apply (erule exE, erule conjE, erule conjE)

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

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

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

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

   898 apply (rule impI, simp add:co2sobj.simps same_inodes_tainted)

   855 apply (rule impI, simp add:co2sobj.simps same_inodes_tainted)

   900 apply (rule impI, simp add:same_inode_files_prop5)

   857 apply (rule impI, simp add:same_inode_files_prop5)

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

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

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

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

   903 

   860 

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

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

   907 apply (simp add:co2sobj.simps same_inodes_tainted)

   864 apply (simp add:co2sobj.simps same_inodes_tainted)

   908 apply (case_tac "O_proc p \<in> tainted s", simp, simp)

   865 apply (case_tac "O_proc p \<in> tainted s", simp, simp)

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

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

   910 apply (rule_tac x = obj in exI)

   867 apply (rule_tac x = obj in exI)

   912 

   869 

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

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

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

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

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

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

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

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

   918 apply (simp split:if_splits)

   875 apply (simp split:if_splits)

   919 apply (rule disjI1, simp add:cf2sfiles_prop)

   876 apply (rule disjI1, simp add:cf2sfiles_prop)

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

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

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

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

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

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

   923 apply (simp add:co2sobj.simps)

   880 apply (simp add:co2sobj.simps)

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

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

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

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

   926 apply (simp add:co2sobj.simps)

   885 apply (simp add:co2sobj.simps)

   934 apply (erule disjE)

   886 apply (erule disjE)

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

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

   937 apply (erule exE|erule conjE)+

   890 apply (erule exE|erule conjE)+

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

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

   941 apply (frule cf2sfiles_prop, simp, simp add:co2sobj.simps same_inodes_tainted)

   894 apply (frule cf2sfiles_prop, simp, simp add:co2sobj.simps same_inodes_tainted)

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

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

   943 apply (rule impI, simp add:same_inode_files_prop5)

   896 apply (rule impI, simp add:same_inode_files_prop5)

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

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

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

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

   946 apply (rule impI, rule impI)

   900 apply (rule impI, rule impI)

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

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

   949 apply (rule_tac x = obj in exI)

   902 apply (rule_tac x = obj in exI)

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

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

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

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

   954 done

   907 done

   955 

   908 

   956 definition update_s2ss_sfile_tainted:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> bool \<Rightarrow> t_static_state"

   909 definition update_s2ss_sfile_tainted:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> bool \<Rightarrow> t_static_state"

   957 where

   910 where

   958  "update_s2ss_sfile_tainted s ss f tag \<equiv>

   911  "update_s2ss_sfile_tainted s ss f tag \<equiv>

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

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

   961        then ss \<union> {S_file (cf2sfiles s f) True}

   914        then ss \<union> {S_file (cf2sfiles s f) True}

   962        else ss - {S_file (cf2sfiles s f) False} 

   915        else ss - {S_file (cf2sfiles s f) False} 

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

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

   964 

   917 

   965 lemma s2ss_writefile:

   918 lemma s2ss_writefile:

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

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

   988 where

   941 where

   989   "del_s2ss_file s ss f sf = 

   942   "del_s2ss_file s ss f sf = 

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

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

   991       then ss

   944       then ss

   993            then update_s2ss_sfile_del s ss f sf

   946            then update_s2ss_sfile_del s ss f sf

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

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

   995 

   948 

   996 

   949 

   999     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>

   952     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>

  1006     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>

   959     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>

  1024 

   975 

  1025 lemma same_inode_files_prop10:

   976 lemma same_inode_files_prop10:

  1026   "\<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"

   977   "\<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"

  1027 by (auto simp:same_inode_files_def split:if_splits)

   978 by (auto simp:same_inode_files_def split:if_splits)

  1028 

   979 

  1039      case (file_of_proc_fd s p fd) of

   990      case (file_of_proc_fd s p fd) of

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

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

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

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

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

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

  1043                             (del_s2ss_file s (

   994                             (del_s2ss_file s (

  1045                                  (S_proc sp (O_proc p \<in> tainted s))

   996                                  (S_proc sp (O_proc p \<in> tainted s))

  1046                                  (S_proc sp' (O_proc p \<in> tainted s))) f sf)

   997                                  (S_proc sp' (O_proc p \<in> tainted s))) f sf)

  1047                       | _ \<Rightarrow> {})

   998                       | _ \<Rightarrow> {})

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

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

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

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

  1051                                (S_proc sp (O_proc p \<in> tainted s))

  1002                                (S_proc sp (O_proc p \<in> tainted s))

  1052                                (S_proc sp' (O_proc p \<in> tainted s)))

  1003                                (S_proc sp' (O_proc p \<in> tainted s)))

  1053                       | _ \<Rightarrow> {})

  1004                       | _ \<Rightarrow> {})

  1054       | _     \<Rightarrow> s2ss s)"

  1005       | _     \<Rightarrow> s2ss s)"

  1055 apply (frule vd_cons, frule vt_grant_os)

  1006 apply (frule vd_cons, frule vt_grant_os)

  1057 apply (frule current_proc_has_sp, simp, erule exE)

  1008 apply (frule current_proc_has_sp, simp, erule exE)

  1058 apply (case_tac "file_of_proc_fd s p fd")

  1009 apply (case_tac "file_of_proc_fd s p fd")

  1059 

  1010 

  1060 apply (simp add:s2ss_def)

  1011 apply (simp add:s2ss_def)

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

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

  1063 apply (frule co2sobj_closefd, simp)

  1014 apply (frule co2sobj_closefd, simp)

  1064 apply (frule cp2sproc_closefd, simp)

  1015 apply (frule cp2sproc_closefd, simp)

  1066 apply (simp split:if_splits add:co2sobj.simps)

  1017 apply (simp split:if_splits add:co2sobj.simps)

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

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

  1070 apply (frule cp2sproc_closefd, simp)

  1021 apply (frule cp2sproc_closefd, simp)

  1071 apply (auto simp add:proc_file_fds_def co2sobj.simps 

  1022 apply (auto simp add:proc_file_fds_def co2sobj.simps 

  1073 

  1024 

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

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

  1075 apply (drule current_proc_has_sp', simp, simp)

  1026 apply (drule current_proc_has_sp', simp, simp)

  1076 apply (case_tac "cf2sfile s a")

  1027 apply (case_tac "cf2sfile s a")

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

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

  1083 

  1034 

  1084 apply (simp add:update_s2ss_obj_def)

  1035 apply (simp add:update_s2ss_obj_def)

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

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

  1086 apply (tactic {*my_seteq_tac 1*})

  1037 apply (tactic {*my_seteq_tac 1*})

  1087 apply simp

  1038 apply simp

  1089 apply (simp add:co2sobj.simps)

  1040 apply (simp add:co2sobj.simps)

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

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

  1098 apply (rule_tac x = obj' in exI)

  1049 apply (rule_tac x = obj' in exI)

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

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

  1100 apply (simp add:co2sobj.simps)

  1051 apply (simp add:co2sobj.simps)

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

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

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

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

  1110 

  1061 

  1111 apply (rule impI)+

  1062 apply (rule impI)+

  1112 apply (tactic {*my_seteq_tac 1*})

  1063 apply (tactic {*my_seteq_tac 1*})

  1114 apply (rule disjI2)

  1065 apply (rule disjI2)

  1116 apply (rule DiffI, simp)

  1067 apply (rule DiffI, simp)

  1117 apply (rule_tac x = obj in exI)

  1068 apply (rule_tac x = obj in exI)

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

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

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

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

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

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

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

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

  1135 

  1086 

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

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

  1137 apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def)

  1088 apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  1159 apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)

  1110 apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)

  1160 apply (erule bexE, erule conjE)

  1111 apply (erule bexE, erule conjE)

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

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

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

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

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

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

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

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

  1168 apply (rule impI, rule conjI, rule impI)

  1119 apply (rule impI, rule conjI, rule impI)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  1184 apply (rule impI)

  1135 apply (rule impI)

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

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

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

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

  1190 apply (rule notI, simp add:co2sobj_closefd)

  1141 apply (rule notI, simp add:co2sobj_closefd)

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

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

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

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

  1195 apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)

  1146 apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)

  1196 apply (erule bexE, erule conjE)

  1147 apply (erule bexE, erule conjE)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  1207 

  1158 

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

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

  1210 apply (erule exE, erule conjE)

  1161 apply (erule exE, erule conjE)

  1212 apply (rule_tac x = obj' in exI)

  1163 apply (rule_tac x = obj' in exI)

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

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

  1214 apply (simp add:co2sobj.simps)

  1165 apply (simp add:co2sobj.simps)

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

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

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

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

  1225 apply (erule conjE, erule exE, erule conjE)

  1176 apply (erule conjE, erule exE, erule conjE)

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

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

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

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

  1237 apply (erule disjE)

  1188 apply (erule disjE)

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

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

  1240 apply (frule same_inode_files_prop11)

  1191 apply (frule same_inode_files_prop11)

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

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

  1244 apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted split:if_splits)

  1195 apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted split:if_splits)

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

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

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

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

  1247 apply (erule disjE)

  1198 apply (erule disjE)

  1249 apply (erule exE, erule conjE)

  1200 apply (erule exE, erule conjE)

  1251 apply (rule_tac x = obj' in exI)

  1202 apply (rule_tac x = obj' in exI)

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

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

  1253 apply (simp add:co2sobj.simps)

  1204 apply (simp add:co2sobj.simps)

  1255 apply (rule_tac x = obj in exI)

  1206 apply (rule_tac x = obj in exI)

  1256 apply (simp add:co2sobj_closefd)

  1207 apply (simp add:co2sobj_closefd)

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

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

  1260 apply (rule conjI, rule notI, simp add:same_inode_files_prop9)

  1211 apply (rule conjI, rule notI, simp add:same_inode_files_prop9)

  1261 apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)

  1212 apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)

  1262 apply (rule_tac x = obj in exI)

  1213 apply (rule_tac x = obj in exI)

  1263 apply (simp add:co2sobj_closefd is_file_simps)

  1214 apply (simp add:co2sobj_closefd is_file_simps)

  1265 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_dir_simps)

  1216 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_dir_simps)

  1266 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)

  1217 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)

  1267 

  1218 

  1268 apply (erule disjE)

  1219 apply (erule disjE)

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

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

  1271 apply (frule same_inode_files_prop11)

  1222 apply (frule same_inode_files_prop11)

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

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

  1275 apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted split:if_splits)

  1226 apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted split:if_splits)

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

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

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

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

  1278 apply (erule disjE)

  1229 apply (erule disjE)

  1280 apply (simp add:co2sobj.simps)

  1231 apply (simp add:co2sobj.simps)

  1281 apply (erule conjE, erule exE, erule conjE)

  1232 apply (erule conjE, erule exE, erule conjE)

  1285 apply (rule_tac x = obj in exI)

  1236 apply (rule_tac x = obj in exI)

  1286 apply (simp add:co2sobj_closefd)

  1237 apply (simp add:co2sobj_closefd)

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

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

  1290 apply (rule conjI, rule notI, simp add:same_inode_files_prop9)