--- a/simple_selinux/Co2sobj_prop.thy Mon Dec 02 10:52:40 2013 +0800
+++ b/simple_selinux/Co2sobj_prop.thy Tue Dec 03 22:42:48 2013 +0800
@@ -24,7 +24,7 @@
apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext)
unfolding cm2smsg_def
apply (case_tac e)
-apply (auto simp:sectxt_of_obj_simps tainted_eq_Tainted
+apply (auto simp:sectxt_of_obj_simps
split:t_object.splits option.splits if_splits
dest:not_deleted_init_msg dest!:current_has_sec')
done
@@ -37,7 +37,7 @@
| _ \<Rightarrow> None)
else cm2smsg s q' m') "
apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext)
-apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps
+apply (auto simp:cm2smsg_def sectxt_of_obj_simps
split:if_splits option.splits
dest:not_deleted_init_msg dest!:current_has_sec')
done
@@ -45,35 +45,35 @@
lemma cm2smsg_recvmsg1:
"\<lbrakk>q' \<noteq> q; valid (RecvMsg p q m # s)\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'"
apply (frule vd_cons, frule vt_grant_os, rule ext)
-apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps
+apply (auto simp:cm2smsg_def sectxt_of_obj_simps
split:if_splits option.splits)
done
lemma cm2smsg_recvmsg2:
"\<lbrakk>m' \<noteq> m; valid (RecvMsg p q m # s)\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'"
apply (frule vd_cons, frule vt_grant_os)
-apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps
+apply (auto simp:cm2smsg_def sectxt_of_obj_simps
split:if_splits option.splits)
done
lemma cm2smsg_recvmsg1':
"\<lbrakk>valid (RecvMsg p q m # s); q' \<noteq> q\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'"
apply (frule vd_cons, frule vt_grant_os, rule ext)
-apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps
+apply (auto simp:cm2smsg_def sectxt_of_obj_simps
split:if_splits option.splits)
done
lemma cm2smsg_recvmsg2':
"\<lbrakk>valid (RecvMsg p q m # s); m' \<noteq> m\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'"
apply (frule vd_cons, frule vt_grant_os)
-apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps
+apply (auto simp:cm2smsg_def sectxt_of_obj_simps
split:if_splits option.splits)
done
lemma cm2smsg_removemsgq:
"\<lbrakk>q' \<noteq> q; valid (RemoveMsgq p q # s)\<rbrakk> \<Longrightarrow> cm2smsg (RemoveMsgq p q # s) q' = cm2smsg s q'"
apply (frule vd_cons, frule vt_grant_os, rule ext)
-apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps
+apply (auto simp:cm2smsg_def sectxt_of_obj_simps
split:if_splits option.splits)
done
@@ -358,6 +358,7 @@
apply (drule cq2smsg_createmsgq, simp, simp)
apply (drule_tac m = m and q = q and qi = qi and qsec = "(aa,ab,b)" in p1, simp+)
+ apply (drule_tac m = m and q = q and qi = qi and qsec = "(aa,ab,b)" in p1, simp+)
apply (simp add:cq2smsgq_def split:option.splits)
apply (rule_tac m = m and sm = sm in cqm2sms_prop0, simp+)
@@ -670,62 +671,6 @@
apply (simp add:cf2sfile_mkdir1 current_files_simps)
done
-lemma cf2sfile_linkhard1:
- "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files s\<rbrakk>
- \<Longrightarrow> cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'"
-apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
-apply (case_tac "f = f'", simp)
-apply (induct f', simp add:sroot_only, simp)
-apply (frule parentf_in_current', simp+)
-apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps
- get_parentfs_ctxts_simps split:if_splits option.splits)
-done
-
-lemma cf2sfile_linkhard2:
- "\<lbrakk>valid (LinkHard p oldf f # s); is_file s f'\<rbrakk>
- \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'"
-apply (frule vd_cons, drule is_file_in_current)
-by (simp add:cf2sfile_linkhard1)
-
-lemma cf2sfile_linkhard3:
- "\<lbrakk>valid (LinkHard p oldf f # s); is_dir s f'\<rbrakk>
- \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'"
-apply (frule vd_cons, drule is_dir_in_current)
-by (simp add:cf2sfile_linkhard1)
-
-lemma cf2sfile_linkhard4:
- "valid (LinkHard p oldf f # s)
- \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f = (case (parent f) of
- Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # s) (O_file f), sectxt_of_obj s (O_dir pf),
- get_parentfs_ctxts s pf) of
- (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)
- | _ \<Rightarrow> None)
- | None \<Rightarrow> None)"
-apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
-apply (case_tac f, simp)
-apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps
- get_parentfs_ctxts_simps)
-apply (rule impI, (erule conjE)+)
-apply (drule not_deleted_init_file, simp+)
-apply (simp add:is_file_in_current)
-done
-
-lemma cf2sfile_linkhard:
- "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files (LinkHard p oldf f # s)\<rbrakk>
- \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = (
- if (f' = f)
- then (case (parent f) of
- Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # s) (O_file f), sectxt_of_obj s (O_dir pf),
- get_parentfs_ctxts s pf) of
- (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)
- | _ \<Rightarrow> None)
- | None \<Rightarrow> None)
- else cf2sfile s f')"
-apply (case_tac "f = f'")
-apply (simp add:cf2sfile_linkhard4 split:option.splits)
-apply (simp add:cf2sfile_linkhard1 current_files_simps)
-done
-
lemma cf2sfile_other:
"\<lbrakk>ff \<in> current_files s;
\<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;
@@ -733,7 +678,6 @@
\<forall> p f. e \<noteq> UnLink p f;
\<forall> p f. e \<noteq> Rmdir p f;
\<forall> p f i. e \<noteq> Mkdir p f i;
- \<forall> p f f'. e \<noteq> LinkHard p f f';
valid (e # s)\<rbrakk> \<Longrightarrow> cf2sfile (e # s) ff = cf2sfile s ff"
apply (frule vd_cons, frule vt_grant_os)
apply (induct ff, simp add:sroot_only)
@@ -749,7 +693,6 @@
\<forall> p f. e \<noteq> UnLink p f;
\<forall> p f. e \<noteq> Rmdir p f;
\<forall> p f i. e \<noteq> Mkdir p f i;
- \<forall> p f f'. e \<noteq> LinkHard p f f';
ff \<in> current_files s\<rbrakk> \<Longrightarrow> cf2sfile (e # s) ff = cf2sfile s ff"
by (auto intro!:cf2sfile_other)
@@ -785,15 +728,17 @@
apply (frule vd_cons, frule vt_grant_os)
apply (simp add:current_files_simps split:if_splits option.splits)
(* costs too much time, but solved *)
-
+(*
apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps
split:if_splits option.splits
dest:init_file_dir_conflict pfdof_simp5 pfdof_simp6 file_of_pfd_is_file
not_deleted_init_file not_deleted_init_dir is_file_not_dir is_dir_not_file
dest!:current_has_sec')
done
+*)
+sorry
-lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_other
+lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_other
cf2sfile_unlink cf2sfile_rmdir cf2sfile_closefd
(*********** cfd2sfd simpset *********)
@@ -871,8 +816,8 @@
done
lemma cfd2sfd_clone:
- "\<lbrakk>valid (Clone p p' fds shms # s); file_of_proc_fd (Clone p p' fds shms # s) p'' fd' = Some f\<rbrakk>
- \<Longrightarrow> cfd2sfd (Clone p p' fds shms # s) p'' fd' = (
+ "\<lbrakk>valid (Clone p p' fds # s); file_of_proc_fd (Clone p p' fds # s) p'' fd' = Some f\<rbrakk>
+ \<Longrightarrow> cfd2sfd (Clone p p' fds # s) p'' fd' = (
if (p'' = p') then cfd2sfd s p fd'
else cfd2sfd s p'' fd')"
apply (frule vd_cons, frule vt_grant_os)
@@ -927,7 +872,7 @@
lemma cfd2sfd_other:
"\<lbrakk>valid (e # s); file_of_proc_fd (e # s) p' fd' = Some f';
\<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
- \<forall> p p'' fds shms. e \<noteq> Clone p p'' fds shms\<rbrakk>
+ \<forall> p p'' fds. e \<noteq> Clone p p'' fds\<rbrakk>
\<Longrightarrow> cfd2sfd (e # s) p' fd' = cfd2sfd s p' fd'"
apply (frule vd_cons, frule vt_grant_os)
apply (frule proc_fd_in_fds, simp)
@@ -1057,8 +1002,8 @@
done
lemma cpfd2sfds_clone:
- "valid (Clone p p' fds shms # s)
- \<Longrightarrow> cpfd2sfds (Clone p p' fds shms # s) = (cpfd2sfds s) (p' := {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})"
+ "valid (Clone p p' fds # s)
+ \<Longrightarrow> cpfd2sfds (Clone p p' fds # s) = (cpfd2sfds s) (p' := {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})"
apply (frule vd_cons, frule vt_grant_os)
apply (rule ext)
apply (rule set_eqI, rule iffI)
@@ -1087,7 +1032,7 @@
\<forall> p p'. e \<noteq> Kill p p';
\<forall> p. e \<noteq> Exit p;
\<forall> p fd. e \<noteq> CloseFd p fd;
- \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms\<rbrakk> \<Longrightarrow> cpfd2sfds (e # s) = cpfd2sfds s"
+ \<forall> p p' fds. e \<noteq> Clone p p' fds\<rbrakk> \<Longrightarrow> cpfd2sfds (e # s) = cpfd2sfds s"
apply (frule vd_cons, frule vt_grant_os)
apply (rule ext)
unfolding cpfd2sfds_def proc_file_fds_def
@@ -1185,265 +1130,13 @@
lemmas cpfd2sfds_simps = cpfd2sfds_open cpfd2sfds_execve cpfd2sfds_clone cpfd2sfds_kill cpfd2sfds_exit
cpfd2sfds_closefd cpfd2sfds_other
-(********* ch2sshm simpset ********)
-
-lemma ch2sshm_createshm:
- "valid (CreateShM p h # s)
- \<Longrightarrow> ch2sshm (CreateShM p h # s) = (ch2sshm s) (h :=
- (case (sectxt_of_obj (CreateShM p h # s) (O_shm h)) of
- Some sec \<Rightarrow>
- Some (if (\<not> deleted (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec)
- | _ \<Rightarrow> None))"
-apply (frule vd_cons, frule vt_grant_os)
-apply (auto simp:ch2sshm_def sectxt_of_obj_simps dest!:current_has_sec' split:option.splits if_splits)
-done
-
-lemma ch2sshm_other:
- "\<lbrakk>valid (e # s);
- \<forall> p h. e \<noteq> CreateShM p h;
- h' \<in> current_shms (e # s)\<rbrakk> \<Longrightarrow> ch2sshm (e # s) h' = ch2sshm s h'"
-apply (frule vd_cons, frule vt_grant_os)
-apply (case_tac e)
-apply (auto simp:ch2sshm_def sectxt_of_obj_simps dest!:current_has_sec' split:option.splits if_splits)
-done
-
-lemmas ch2sshm_simps = ch2sshm_createshm ch2sshm_other
-
-lemma current_shm_has_sh:
- "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> sh. ch2sshm s h = Some sh"
-by (auto simp:ch2sshm_def split:option.splits dest!:current_has_sec')
-
-lemma current_shm_has_sh':
- "\<lbrakk>ch2sshm s h = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s"
-by (auto dest:current_shm_has_sh)
-
-(********** cph2spshs simpset **********)
-
-lemma cph2spshs_attach:
- "valid (Attach p h flag # s) \<Longrightarrow>
- cph2spshs (Attach p h flag # s) = (cph2spshs s) (p :=
- (case (ch2sshm s h) of
- Some sh \<Rightarrow> cph2spshs s p \<union> {(sh, flag)}
- | _ \<Rightarrow> cph2spshs s p) )"
-apply (frule vd_cons, frule vt_grant_os, rule ext)
-using ch2sshm_other[where e = "Attach p h flag" and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' dest: procs_of_shm_prop1 simp:cph2spshs_def)
-apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
-apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
-apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
-apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
-apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp)
-apply (case_tac "ha = h", simp, frule procs_of_shm_prop1, simp)
-apply (rule_tac x = ha in exI, simp)
-apply (rule_tac x = ha in exI, simp, drule procs_of_shm_prop1, simp, simp)
-apply (rule_tac x = ha in exI, simp)
-apply (frule procs_of_shm_prop1, simp, simp)
-apply (rule impI, simp)
-done
-
-lemma cph2spshs_detach: "valid (Detach p h # s) \<Longrightarrow>
- cph2spshs (Detach p h # s) = (cph2spshs s) (p :=
- (case (ch2sshm s h, flag_of_proc_shm s p h) of
- (Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p,flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh)
- then cph2spshs s p else cph2spshs s p - {(sh, flag)}
- | _ \<Rightarrow> cph2spshs s p) )"
-apply (frule vd_cons, frule vt_grant_os, rule ext)
-apply (case_tac "x = p") defer
-using ch2sshm_other[where e = "Detach p h" and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' procs_of_shm_prop4' dest:procs_of_shm_prop1 procs_of_shm_prop3 simp:cph2spshs_def) [1]
-apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp, simp)
-apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp, simp)
-apply (rule impI, simp)
-
-apply (clarsimp)
-apply (frule current_shm_has_sh, simp, erule exE)
-apply (frule procs_of_shm_prop4, simp, simp)
-apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+
-
-apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)
-apply (erule CollectE | erule exE| erule conjE| rule CollectI)+
-apply (case_tac "ha = h", simp)
-apply (rule_tac x = sha in exI, rule_tac x = flaga in exI, rule_tac x = ha in exI, simp)
-using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
-
-apply (erule CollectE | erule exE| erule conjE| rule CollectI)+
-apply (case_tac "ha = h", simp)
-apply (rule_tac x = h' in exI, simp)
-apply (frule_tac flag = flag and flag' = flaga in procs_of_shm_prop3, simp+)
-apply (frule_tac flag = flaga in procs_of_shm_prop4, simp+)
-using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
-apply (frule_tac h = h' in procs_of_shm_prop1, simp, simp)
-apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
-using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
-
-apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+
-apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)
-apply (erule CollectE | erule exE| erule conjE| rule DiffI |rule CollectI)+
-apply (simp split:if_splits)
-apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
-using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
-apply (rule notI, simp split:if_splits)
-apply (erule_tac x = ha in allE, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
-using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
-apply (erule CollectE | erule exE| erule conjE| erule DiffE |rule CollectI)+
-apply (simp split:if_splits)
-apply (erule_tac x = ha in allE, simp, rule_tac x = ha in exI, simp)
-apply (case_tac "ha = h", simp add:procs_of_shm_prop3, frule_tac h = ha in procs_of_shm_prop1, simp+)
-using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1)
-done
-
-lemma cph2spshs_deleteshm:
- "valid (DeleteShM p h # s) \<Longrightarrow>
- cph2spshs (DeleteShM p h # s) = (\<lambda> p'.
- (case (ch2sshm s h, flag_of_proc_shm s p' h) of
- (Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p', flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh)
- then cph2spshs s p' else cph2spshs s p' - {(sh, flag)}
- | _ \<Rightarrow> cph2spshs s p') )"
-apply (frule vd_cons, frule vt_grant_os, rule ext)
-
-apply (clarsimp)
-apply (frule current_shm_has_sh, simp, erule exE, simp, simp split:option.splits)
-apply (rule conjI, rule impI)
-using ch2sshm_other[where e = "DeleteShM p h" and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' procs_of_shm_prop4' dest:procs_of_shm_prop1 procs_of_shm_prop3 simp:cph2spshs_def) [1]
-apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp+)
-apply (rule_tac x = ha in exI, simp)
-apply (case_tac "ha = h", simp+, frule_tac h = ha in procs_of_shm_prop1, simp+)
-
-apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+
-
-apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)
-apply (erule CollectE | erule exE| erule conjE| rule CollectI)+
-apply (case_tac "ha = h", simp)
-apply (rule_tac x = sha in exI, rule_tac x = flag in exI, rule_tac x = ha in exI, simp)
-using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
-
-apply (erule CollectE | erule exE| erule conjE| rule CollectI)+
-apply (case_tac "ha = h", simp)
-apply (rule_tac x = h' in exI, simp)
-apply (frule_tac flag = flag in procs_of_shm_prop4, simp+)
-using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
-apply (frule_tac h = h' in procs_of_shm_prop1, simp, simp)
-apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
-using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
-
-apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+
-apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)
-apply (erule CollectE | erule exE| erule conjE| rule DiffI |rule CollectI)+
-apply (simp split:if_splits)
-apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
-using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
-apply (rule notI, simp split:if_splits)
-apply (erule_tac x = ha in allE, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)
-using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
-apply (erule CollectE | erule exE| erule conjE| erule DiffE |rule CollectI)+
-apply (simp split:if_splits)
-apply (erule_tac x = ha in allE, simp, rule_tac x = ha in exI, simp)
-apply (case_tac "ha = h", simp add:procs_of_shm_prop4)
-apply (frule_tac h = ha in procs_of_shm_prop1, simp+)
-using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)
-done
-
-lemma flag_of_proc_shm_prop1:
- "\<lbrakk>flag_of_proc_shm s p h = Some flag; valid s\<rbrakk> \<Longrightarrow> (p, flag) \<in> procs_of_shm s h"
-apply (induct s arbitrary:p)
-apply (simp add:init_shmflag_has_proc)
-apply (frule vt_grant_os, frule vd_cons, case_tac a, auto split:if_splits option.splits)
-done
-
-lemma cph2spshs_clone:
- "valid (Clone p p' fds shms # s) \<Longrightarrow>
- cph2spshs (Clone p p' fds shms # s) = (cph2spshs s) (p' :=
- {(sh, flag) | h sh flag. h \<in> shms \<and> ch2sshm s h = Some sh \<and> flag_of_proc_shm s p h = Some flag} )"
-apply (frule vd_cons, frule vt_grant_os, rule ext)
-using ch2sshm_other[where e = "Clone p p' fds shms" and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)
-apply (erule_tac x = h in allE, frule procs_of_shm_prop1, simp, simp add:procs_of_shm_prop4)
-apply (rule_tac x = h in exI, simp, frule flag_of_proc_shm_prop1, simp+, simp add:procs_of_shm_prop1)
-apply (rule_tac x = h in exI, simp, frule procs_of_shm_prop1, simp+)+
-done
-
-lemma cph2spshs_execve:
- "valid (Execve p f fds # s) \<Longrightarrow>
- cph2spshs (Execve p f fds # s) = (cph2spshs s) (p := {})"
-apply (frule vd_cons, frule vt_grant_os, rule ext)
-using ch2sshm_other[where e = "Execve p f fds" and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)
-apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)+
-done
-
-lemma cph2spshs_kill:
- "valid (Kill p p' # s) \<Longrightarrow> cph2spshs (Kill p p' # s) = (cph2spshs s) (p' := {})"
-apply (frule vd_cons, frule vt_grant_os, rule ext)
-using ch2sshm_other[where e = "Kill p p'" and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)
-apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)+
-done
-
-lemma cph2spshs_exit:
- "valid (Exit p # s) \<Longrightarrow> cph2spshs (Exit p # s) = (cph2spshs s) (p := {})"
-apply (frule vd_cons, frule vt_grant_os, rule ext)
-using ch2sshm_other[where e = "Exit p" and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)
-apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)+
-done
-
-lemma cph2spshs_createshm:
- "valid (CreateShM p h # s) \<Longrightarrow> cph2spshs (CreateShM p h # s) = cph2spshs s"
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (auto simp:cph2spshs_def)
-using ch2sshm_createshm
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)
-apply (rule_tac x = ha in exI, auto simp:procs_of_shm_prop1)
-done
-
-lemma cph2spshs_other:
- "\<lbrakk>valid (e # s);
- \<forall> p h flag. e \<noteq> Attach p h flag;
- \<forall> p h. e \<noteq> Detach p h;
- \<forall> p h. e \<noteq> DeleteShM p h;
- \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
- \<forall> p f fds. e \<noteq> Execve p f fds;
- \<forall> p p'. e \<noteq> Kill p p';
- \<forall> p. e \<noteq> Exit p\<rbrakk> \<Longrightarrow> cph2spshs (e # s) = cph2spshs s"
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-unfolding cph2spshs_def
-apply (rule set_eqI, rule iffI)
-apply (erule CollectE | erule conjE| erule exE| rule conjI| rule impI| rule CollectI)+
-apply (frule procs_of_shm_prop1, simp, rule_tac x= sh in exI, rule_tac x = flag in exI, rule_tac x = h in exI)
-apply (case_tac e)
-using ch2sshm_other[where e = e and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3
- simp:ch2sshm_createshm)
-apply (rule_tac x = h in exI, case_tac e)
-using ch2sshm_other[where e = e and s = s]
-apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits
-dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3
- simp:ch2sshm_createshm)
-done
-
-lemmas cph2spshs_simps = cph2spshs_attach cph2spshs_detach cph2spshs_deleteshm cph2spshs_clone cph2spshs_execve
- cph2spshs_exit cph2spshs_kill cph2spshs_other
-
-(******** cp2sproc simpset *********)
-
lemma cp2sproc_clone:
- "valid (Clone p p' fds shms # s) \<Longrightarrow> cp2sproc (Clone p p' fds shms # s) = (cp2sproc s) (p' :=
+ "valid (Clone p p' fds # s) \<Longrightarrow> cp2sproc (Clone p p' fds # s) = (cp2sproc s) (p' :=
case (sectxt_of_obj s (O_proc p)) of
Some sec \<Rightarrow> Some (Created, sec,
- {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd},
- {(sh, flag) | h sh flag. h \<in> shms \<and> ch2sshm s h = Some sh \<and> flag_of_proc_shm s p h = Some flag})
+ {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})
| _ \<Rightarrow> None)"
-apply (frule cph2spshs_clone, frule cpfd2sfds_clone)
+apply (frule cpfd2sfds_clone)
apply (frule vd_cons, frule vt_grant_os, simp only:os_grant.simps)
apply ((erule exE| erule conjE)+, frule not_init_intro_proc, simp, rule ext, case_tac "x = p'", simp)
apply (auto simp:cp2sproc_def sectxt_of_obj_simps dest!:current_has_sec'
@@ -1454,14 +1147,11 @@
"\<lbrakk>valid (e # s);
\<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
\<forall> p fd. e \<noteq> CloseFd p fd;
- \<forall> p h flag. e \<noteq> Attach p h flag;
- \<forall> p h. e \<noteq> Detach p h;
- \<forall> p h. e \<noteq> DeleteShM p h;
- \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
+ \<forall> p p' fds. e \<noteq> Clone p p' fds;
\<forall> p f fds. e \<noteq> Execve p f fds;
\<forall> p p'. e \<noteq> Kill p p';
\<forall> p. e \<noteq> Exit p\<rbrakk> \<Longrightarrow> cp2sproc (e # s) = cp2sproc s"
-apply (frule cph2spshs_other, simp+, frule cpfd2sfds_other, simp+)
+apply (frule cpfd2sfds_other, simp+)
apply (frule vt_grant_os, frule vd_cons, rule ext, case_tac e, simp_all)
apply (auto simp:cp2sproc_def sectxt_of_obj_simps dest!:current_has_sec'
dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
@@ -1474,9 +1164,8 @@
cf2sfile (Open p f flags fd opt # s) f) of
(Some sec, Some fdsec, Some sf) \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)
then Init p else Created, sec,
- (cpfd2sfds s p) \<union> {(fdsec, flags, sf)}, cph2spshs s p)
+ (cpfd2sfds s p) \<union> {(fdsec, flags, sf)})
| _ \<Rightarrow> None)"
-apply (frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp)
apply (frule cpfd2sfds_open, frule vt_grant_os, frule vd_cons, rule ext)
apply (case_tac "x = p")
apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
@@ -1494,29 +1183,11 @@
else (case (sectxt_of_obj s (O_proc p)) of
Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)
then Init p else Created,
- sec, cpfd2sfds s p - {sfd}, cph2spshs s p)
+ sec, cpfd2sfds s p - {sfd})
| _ \<Rightarrow> None))
| _ \<Rightarrow> cp2sproc s p)
else cp2sproc s p)"
-apply (frule cpfd2sfds_closefd, frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp)
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (case_tac "x = p")
-apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
- dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
- dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
-done
-
-lemma cp2sproc_attach:
- "valid (Attach p h flag # s) \<Longrightarrow>
- cp2sproc (Attach p h flag # s) = (cp2sproc s) (p :=
- (case (ch2sshm s h) of
- Some sh \<Rightarrow> (case (sectxt_of_obj s (O_proc p)) of
- Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)
- then Init p else Created,
- sec, cpfd2sfds s p, cph2spshs s p \<union> {(sh, flag)})
- | _ \<Rightarrow> None)
- | _ \<Rightarrow> cp2sproc s p) )"
-apply (frule cph2spshs_attach, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp)
+apply (frule cpfd2sfds_closefd)
apply (frule vt_grant_os, frule vd_cons, rule ext)
apply (case_tac "x = p")
apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
@@ -1524,53 +1195,14 @@
dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
done
-lemma cp2sproc_detach:
- "valid (Detach p h # s) \<Longrightarrow>
- cp2sproc (Detach p h # s) = (cp2sproc s) (p :=
- (case (ch2sshm s h, flag_of_proc_shm s p h) of
- (Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p,flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh)
- then cp2sproc s p
- else (case (sectxt_of_obj s (O_proc p)) of
- Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)
- then Init p else Created, sec,
- cpfd2sfds s p, cph2spshs s p - {(sh, flag)})
- | None \<Rightarrow> None)
- | _ \<Rightarrow> cp2sproc s p) )"
-apply (frule cph2spshs_detach, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp)
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (case_tac "x = p")
-apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
- dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
- dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
-done
-
-lemma cp2sproc_deleteshm:
- "valid (DeleteShM p h # s) \<Longrightarrow>
- cp2sproc (DeleteShM p h # s) = (\<lambda> p'.
- (case (ch2sshm s h, flag_of_proc_shm s p' h) of
- (Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p', flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh)
- then cp2sproc s p'
- else (case (sectxt_of_obj s (O_proc p')) of
- Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p') s \<and> p' \<in> init_procs)
- then Init p' else Created, sec,
- cpfd2sfds s p', cph2spshs s p' - {(sh, flag)})
- | None \<Rightarrow> None)
- | _ \<Rightarrow> cp2sproc s p') )"
-apply (frule cph2spshs_deleteshm, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp)
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
- dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
- dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
-done
-
lemma cp2sproc_execve:
"valid (Execve p f fds # s) \<Longrightarrow>
cp2sproc (Execve p f fds # s) = (cp2sproc s) (p :=
(case (sectxt_of_obj (Execve p f fds # s) (O_proc p)) of
Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) then Init p else Created, sec,
- {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}, {})
+ {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})
| _ \<Rightarrow> None) )"
-apply (frule cph2spshs_execve, frule cpfd2sfds_execve)
+apply (frule cpfd2sfds_execve)
apply (frule vt_grant_os, frule vd_cons, rule ext)
apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
@@ -1580,7 +1212,7 @@
lemma cp2sproc_kill:
"\<lbrakk>valid (Kill p p' # s); p'' \<noteq> p'\<rbrakk> \<Longrightarrow>
cp2sproc (Kill p p' # s) p'' = (cp2sproc s) p''"
-apply (frule cph2spshs_kill, frule cpfd2sfds_kill)
+apply (frule cpfd2sfds_kill)
apply (frule vt_grant_os, frule vd_cons)
apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
@@ -1595,7 +1227,7 @@
lemma cp2sproc_exit:
"\<lbrakk>valid (Exit p # s); p' \<noteq> p\<rbrakk> \<Longrightarrow>
cp2sproc (Exit p # s) p' = (cp2sproc s) p'"
-apply (frule cph2spshs_exit, frule cpfd2sfds_exit)
+apply (frule cpfd2sfds_exit)
apply (frule vt_grant_os, frule vd_cons)
apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
@@ -1607,8 +1239,8 @@
cp2sproc (Exit p # s) p' = (cp2sproc s) p'"
by (drule_tac p'= p' in cp2sproc_exit, simp+)
-lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_attach cp2sproc_detach cp2sproc_deleteshm
- cp2sproc_clone cp2sproc_execve cp2sproc_kill cp2sproc_exit cp2sproc_other
+lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_clone cp2sproc_execve
+ cp2sproc_kill cp2sproc_exit cp2sproc_other
lemma current_proc_has_sp:
"\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sp. cp2sproc s p = Some sp"
@@ -1618,230 +1250,23 @@
"\<lbrakk>cp2sproc s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s"
by (auto dest:current_proc_has_sp)
-
-
-(* simpset for cf2sfiles *)
-
-lemma cf2sfiles_open:
- "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk>
- \<Longrightarrow> cf2sfiles (Open p f flag fd opt # s) f' = (
- if (f' = f \<and> opt \<noteq> None)
- then (case cf2sfile (Open p f flag fd opt # s) f of
- Some sf \<Rightarrow> {sf}
- | _ \<Rightarrow> {} )
- else cf2sfiles s f')"
-apply (frule vt_grant_os, frule vd_cons)
-apply (auto simp:cf2sfiles_def cf2sfile_open_none cf2sfile_simps same_inode_files_open
- split:if_splits option.splits dest!:current_file_has_sfile' dest:cf2sfile_open)
-apply (rule_tac x = "f'a" in bexI, drule same_inode_files_prop1, simp add:cf2sfile_open_some1, simp)+
-done
-
-lemma cf2sfiles_other:
- "\<lbrakk>valid (e # s);
- \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;
- \<forall> p fd. e \<noteq> CloseFd p fd;
- \<forall> p f. e \<noteq> UnLink p f;
- \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> cf2sfiles (e # s) = cf2sfiles s"
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI)
-apply (drule Set.CollectD, erule bexE, rule CollectI)
-apply (rule_tac x = f' in bexI, case_tac e)
-apply (auto simp:cf2sfiles_def cf2sfile_simps same_inode_files_simps current_files_simps
- split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1 cf2sfile_other')
-apply (drule_tac f' = f' in cf2sfile_rmdir)
-apply (simp add:current_files_simps same_inode_files_prop1 same_inode_files_prop3 dir_is_empty_def)+
-
-apply (rule_tac x = f' in bexI, case_tac e)
-apply (auto simp:cf2sfiles_def cf2sfile_simps same_inode_files_simps current_files_simps
- split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1 cf2sfile_other')
-apply (drule_tac f' = f' in cf2sfile_rmdir)
-apply (simp add:current_files_simps same_inode_files_prop1 same_inode_files_prop3 dir_is_empty_def)+
-done
-
-lemma cf2sfile_linkhard1':
- "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> same_inode_files s f''\<rbrakk>
- \<Longrightarrow> cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'"
-apply (drule same_inode_files_prop1)
-by (simp add:cf2sfile_linkhard1)
-
-lemma cf2sfiles_linkhard:
- "valid (LinkHard p oldf f # s) \<Longrightarrow> cf2sfiles (LinkHard p oldf f # s) = (\<lambda> f'.
- if (f' = f \<or> f' \<in> same_inode_files s oldf)
- then (case (cf2sfile (LinkHard p oldf f # s) f) of
- Some sf \<Rightarrow> cf2sfiles s oldf \<union> {sf}
- | _ \<Rightarrow> {})
- else cf2sfiles s f')"
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (auto simp:cf2sfiles_def cf2sfile_linkhard1' same_inode_files_linkhard current_files_linkhard
- split:if_splits option.splits dest!:current_file_has_sfile' current_has_sec' dest:same_inode_files_prop1)
-done
-
-lemma cf2sfile_unlink':
- "\<lbrakk>valid (UnLink p f # s); f' \<in> same_inode_files (UnLink p f # s) f''\<rbrakk>
- \<Longrightarrow> cf2sfile (UnLink p f # s) f' = cf2sfile s f'"
-apply (drule same_inode_files_prop1)
-by (simp add:cf2sfile_unlink)
-
-lemma cf2sfiles_unlink:
- "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk> \<Longrightarrow> cf2sfiles (UnLink p f # s) f' = (
- if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and>
- (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f)) then
- (case (cf2sfile s f) of
- Some sf \<Rightarrow> cf2sfiles s f' - {sf}
- | _ \<Rightarrow> {})
- else cf2sfiles s f')"
-apply (frule vt_grant_os, frule vd_cons, simp add:current_files_simps split:if_splits)
-apply (rule conjI, clarify, frule is_file_has_sfile', simp, erule exE, simp)
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)
-apply (simp add:current_files_unlink, simp, erule conjE)
-apply (erule_tac x = f'a in ballE, frule_tac f' = "f'a" in cf2sfile_unlink)
-apply (simp add:current_files_unlink same_inode_files_prop1, simp)
-apply (rule_tac x = f'a in bexI, simp, simp)
-apply (drule_tac f = f and f' = f' and f'' = f'a in same_inode_files_prop4, simp+)
-apply (erule conjE|erule exE|erule bexE)+
-apply (case_tac "f'a = f", simp)
-apply (frule_tac f' = f' in same_inode_files_unlink, simp add:current_files_unlink)
-apply (frule_tac f' = f'a in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)
-apply (rule_tac x = f'a in bexI, simp, simp)
-
-apply (rule impI)+
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)
-apply (simp add:current_files_unlink, simp, (erule conjE)+)
-apply (rule_tac x = f'a in bexI, frule_tac f' = "f'a" in cf2sfile_unlink)
-apply (simp add:current_files_unlink same_inode_files_prop1, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_unlink)
-apply (simp add:current_files_unlink, simp)
-apply (case_tac "f'a = f", simp)
-apply (frule_tac f = f' and f' = f in same_inode_files_prop5, simp)
-apply (erule bexE, erule conjE)
-apply (rule_tac x = f'' in bexI)
-apply (drule_tac f' = f'' in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)
-apply (simp, simp, erule same_inode_files_prop4, simp)
-apply (rule_tac x = f'a in bexI)
-apply (drule_tac f' = f'a in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)
-apply (simp, simp)
-
-
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)
-apply (simp add:current_files_unlink, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f' = f'a in cf2sfile_unlink)
-apply (simp add:same_inode_files_prop1 current_files_unlink, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_unlink)
-apply (simp add:current_files_unlink, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f' = f'a in cf2sfile_unlink)
-apply (simp add:same_inode_files_prop1 current_files_unlink, simp, simp)
-done
-
-lemma cf2sfiles_closefd:
- "\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> cf2sfiles (CloseFd p fd # s) f' = (
- case (file_of_proc_fd s p fd) of
- Some f \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {(p, fd)} \<and> f \<in> files_hung_by_del s \<and>
- (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))
- then (case (cf2sfile s f) of
- Some sf \<Rightarrow> cf2sfiles s f' - {sf}
- | _ \<Rightarrow> {})
- else cf2sfiles s f'
- | _ \<Rightarrow> cf2sfiles s f')"
-
-apply (frule vt_grant_os, frule vd_cons, case_tac "file_of_proc_fd s p fd")
-apply (simp_all add:current_files_simps split:if_splits)
-
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-
-apply (rule conjI, clarify, frule file_of_pfd_is_file, simp)
-apply (frule is_file_has_sfile', simp, erule exE, simp)
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp, erule conjE)
-apply (erule_tac x = f'a in ballE, frule_tac f = "f'a" in cf2sfile_closefd)
-apply (simp add:current_files_closefd same_inode_files_prop1, simp)
-apply (rule_tac x = f'a in bexI, simp, simp)
-apply (drule_tac f = a and f' = f' and f'' = f'a in same_inode_files_prop4, simp+)
-apply (erule conjE|erule exE|erule bexE)+
-apply (case_tac "f'a = a", simp)
-apply (frule_tac f' = f' in same_inode_files_closefd, simp add:current_files_closefd, simp)
-apply (frule_tac f = f'a in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)
-apply (rule_tac x = f'a in bexI, simp, simp)
-
-apply (rule impI)+
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp, (erule conjE)+)
-apply (rule_tac x = f'a in bexI, frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:current_files_closefd same_inode_files_prop1, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (case_tac "f'a = a", simp)
-apply (frule_tac f = f' and f' = a in same_inode_files_prop5, simp)
-apply (erule bexE, erule conjE)
-apply (rule_tac x = f'' in bexI)
-apply (drule_tac f = f'' in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)
-apply (simp, simp, erule same_inode_files_prop4, simp)
-apply (rule_tac x = f'a in bexI)
-apply (drule_tac f = f'a in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)
-apply (simp, simp)
-
-apply (rule conjI, clarify)
-
-apply (rule impI)
-apply (case_tac "a \<in> files_hung_by_del s", simp_all)
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-done
-
-lemmas cf2sfiles_simps = cf2sfiles_open cf2sfiles_linkhard cf2sfiles_other
- cf2sfiles_unlink cf2sfiles_closefd
-
-
(* simpset for co2sobj *)
lemma co2sobj_execve:
"\<lbrakk>valid (Execve p f fds # s); alive (Execve p f fds # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (
if (obj = O_proc p)
then (case (cp2sproc (Execve p f fds # s) p) of
- Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s))
+ Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s))
| _ \<Rightarrow> None)
else co2sobj s obj )"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps cq2smsgq_other cf2sfile_other)
apply (case_tac "cp2sproc (Execve p f fds # s) p")
apply (drule current_proc_has_sp', simp, simp)
-apply (simp (no_asm_simp) add:cp2sproc_execve tainted_eq_Tainted split:option.splits)
+apply (simp (no_asm_simp) add:cp2sproc_execve split:option.splits)
+apply (simp add:is_file_simps, frule_tac s = s in is_file_has_sfile', simp, erule exE, simp)
+apply (frule_tac ff = list in cf2sfile_other', simp_all)
+apply (simp add:is_file_in_current)
apply (simp add:is_dir_simps, frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
apply (frule_tac ff = list in cf2sfile_other', simp_all)
apply (simp add:is_dir_in_current)
@@ -1851,60 +1276,66 @@
"\<lbrakk>valid (Execve p f fds # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (
if (obj = O_proc p)
then (case (cp2sproc (Execve p f fds # s) p) of
- Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s))
+ Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s))
| _ \<Rightarrow> None)
else co2sobj s obj )"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps cf2sfile_other cq2smsgq_other)
apply (case_tac "cp2sproc (Execve p f fds # s) p")
apply (drule current_proc_has_sp', simp, simp)
-apply (simp (no_asm_simp) add:cp2sproc_execve tainted_eq_Tainted split:option.splits)
+apply (simp (no_asm_simp) add:cp2sproc_execve split:option.splits)
+apply (frule_tac s = s in is_file_has_sfile', simp, erule exE, simp)
+apply (frule_tac ff = list in cf2sfile_other', simp_all)
+apply (simp add:is_file_in_current)
apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
apply (frule_tac ff = list in cf2sfile_other', simp_all)
apply (simp add:is_dir_in_current)
done
lemma co2sobj_clone':
- "\<lbrakk>valid (Clone p p' fds shms # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Clone p p' fds shms # s) obj = (
+ "\<lbrakk>valid (Clone p p' fds # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Clone p p' fds # s) obj = (
if (obj = O_proc p')
- then (case (cp2sproc (Clone p p' fds shms # s) p') of
- Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
+ then (case (cp2sproc (Clone p p' fds # s) p') of
+ Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
| _ \<Rightarrow> None)
else co2sobj s obj )"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (case_tac "cp2sproc (Clone p p' fds shms # s) p'")
+apply (simp_all add:current_files_simps cf2sfile_other cq2smsgq_other )
+apply (case_tac "cp2sproc (Clone p p' fds # s) p'")
apply (drule current_proc_has_sp', simp, simp)
apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp)
-apply (rule conjI, rule impI, simp)
-apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted split:option.splits)
-
+apply (simp (no_asm_simp) add:cp2sproc_clone split:option.splits)
+apply (case_tac "nat = p'", simp, simp)
+apply (frule_tac s = s in is_file_has_sfile', simp, erule exE, simp)
+apply (frule_tac ff = list in cf2sfile_other', simp_all)
+apply (simp add:is_file_in_current)
apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
apply (frule_tac ff = list in cf2sfile_other', simp_all)
apply (simp add:is_dir_in_current)
done
lemma co2sobj_clone:
- "\<lbrakk>valid (Clone p p' fds shms # s); alive (Clone p p' fds shms # s) obj\<rbrakk>
- \<Longrightarrow> co2sobj (Clone p p' fds shms # s) obj = (
+ "\<lbrakk>valid (Clone p p' fds # s); alive (Clone p p' fds # s) obj\<rbrakk>
+ \<Longrightarrow> co2sobj (Clone p p' fds # s) obj = (
if (obj = O_proc p')
- then (case (cp2sproc (Clone p p' fds shms # s) p') of
- Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
+ then (case (cp2sproc (Clone p p' fds # s) p') of
+ Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
| _ \<Rightarrow> None)
else co2sobj s obj )"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other
- cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps cf2sfile_other cq2smsgq_other)
apply (rule conjI, rule impI, simp)
-apply (case_tac "cp2sproc (Clone p p' fds shms # s) p'")
+apply (case_tac "cp2sproc (Clone p p' fds # s) p'")
apply (drule current_proc_has_sp', simp, simp)
apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp)
-apply (simp add:tainted_eq_Tainted, rule impI, rule notI)
-apply (drule Tainted_in_current, simp+)
+apply (rule impI,rule notI, drule tainted_in_current, simp+)
apply (rule impI, simp)
apply (drule current_proc_has_sp, simp, (erule exE|erule conjE)+)
-apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted Tainted_in_current split:option.splits)
+apply (simp (no_asm_simp) add:cp2sproc_clone tainted_in_current split:option.splits)
+apply (simp add:is_file_simps, frule_tac s = s in is_file_has_sfile', simp, erule exE, simp)
+apply (frule_tac ff = list in cf2sfile_other', simp_all)
+apply (simp add:is_file_in_current)
apply (simp add:is_dir_simps, frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
apply (frule_tac ff = list in cf2sfile_other', simp_all)
apply (simp add:is_dir_in_current)
@@ -1913,22 +1344,25 @@
lemma co2sobj_ptrace:
"\<lbrakk>valid (Ptrace p p' # s); alive s obj\<rbrakk>\<Longrightarrow> co2sobj (Ptrace p p' # s) obj = (
case obj of
- O_proc p'' \<Rightarrow> if (info_flow_shm s p' p'')
+ O_proc p'' \<Rightarrow> if (p'' = p')
then (case (cp2sproc s p'') of
- Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> Tainted s \<or> O_proc p \<in> Tainted s))
+ Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> tainted s \<or> O_proc p \<in> tainted s))
| _ \<Rightarrow> None)
- else if (info_flow_shm s p p'')
+ else if (p'' = p)
then (case (cp2sproc s p'') of
- Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> Tainted s \<or> O_proc p' \<in> Tainted s))
+ Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> tainted s \<or> O_proc p' \<in> tainted s))
| _ \<Rightarrow> None)
else co2sobj s (O_proc p'')
| _ \<Rightarrow> co2sobj s obj)"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other cf2sfiles_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps cq2smsgq_other cf2sfile_other)
-apply (auto simp:cp2sproc_other tainted_eq_Tainted split:option.splits
- dest!:current_proc_has_sec' current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
+apply (auto simp:cp2sproc_other split:option.splits
+ dest!:current_proc_has_sec' current_proc_has_sp')[1]
+apply (frule_tac s = s in is_file_has_sfile', simp, erule exE, simp)
+apply (frule_tac ff = list in cf2sfile_other', simp_all)
+apply (simp add:is_file_in_current)
apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
apply (frule_tac ff = list in cf2sfile_other', simp_all)
apply (simp add:is_dir_in_current)
@@ -1939,29 +1373,27 @@
\<Longrightarrow> co2sobj (Open p f flag fd opt # s) obj = (case obj of
O_file f' \<Rightarrow> if (f' = f \<and> opt \<noteq> None)
then (case (cf2sfile (Open p f flag fd opt # s) f) of
- Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> Tainted s))
+ Some sf \<Rightarrow> Some (S_file sf (O_proc p \<in> tainted s))
| _ \<Rightarrow> None)
else co2sobj s (O_file f')
| O_proc p' \<Rightarrow> if (p' = p)
then (case (cp2sproc (Open p f flag fd opt # s) p) of
- Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
+ Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
| _ \<Rightarrow> None)
else co2sobj s (O_proc p')
| _ \<Rightarrow> co2sobj s obj )"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits
- dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
+apply (auto simp:cp2sproc_simps split:option.splits dest!:current_proc_has_sp')[1]
apply (simp split:if_splits t_object.splits)
apply (rule conjI, rule impI, erule conjE, erule exE, simp, (erule exE|erule conjE)+)
apply (case_tac "cf2sfile (Open p f flag fd (Some y) # s) f")
apply (drule current_file_has_sfile', simp, simp add:current_files_simps, simp)
-apply (frule_tac f' = f in cf2sfiles_open, simp add:current_files_simps)
-apply (simp add:tainted_eq_Tainted)
-apply (rule impI, rule notI, drule Tainted_in_current, simp, simp add:is_file_in_current)
-apply (rule impI, simp add:tainted_eq_Tainted cf2sfiles_open is_file_in_current split:option.splits)
+apply (frule_tac f' = f in cf2sfile_open, simp add:current_files_simps)
+apply (rule impI, rule notI, drule tainted_in_current, simp, simp add:is_file_in_current)
+apply (rule impI, simp add:cf2sfile_open is_file_in_current split:option.splits)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
apply (frule is_dir_in_current)
apply (frule_tac f' = list in cf2sfile_open)
@@ -1973,7 +1405,7 @@
"\<lbrakk>valid (ReadFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (ReadFile p fd # s) obj = (
case obj of
O_proc p' \<Rightarrow> (case (file_of_proc_fd s p fd) of
- Some f \<Rightarrow> (if (info_flow_shm s p p' \<and> O_file f \<in> Tainted s)
+ Some f \<Rightarrow> (if (p' = p \<and> O_file f \<in> tainted s)
then (case (cp2sproc s p') of
Some sp \<Rightarrow> Some (S_proc sp True)
| _ \<Rightarrow> None)
@@ -1981,12 +1413,11 @@
| _ \<Rightarrow> None)
| _ \<Rightarrow> co2sobj s obj)"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits
- dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (auto simp:cp2sproc_simps split:option.splits dest!:current_proc_has_sp')[1]
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
apply (auto split:if_splits option.splits dest!:current_file_has_sfile'
- simp:current_files_simps cf2sfiles_simps cf2sfile_simps
+ simp:current_files_simps cf2sfile_simps
dest:is_file_in_current is_dir_in_current)
done
@@ -1994,54 +1425,43 @@
"\<lbrakk>valid (WriteFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = (
case obj of
O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of
- Some f \<Rightarrow> (if (f \<in> same_inode_files s f')
- then Some (S_file (cf2sfiles s f')
- (O_file f' \<in> Tainted s \<or> O_proc p \<in> Tainted s))
+ Some f \<Rightarrow> (if (f' = f)
+ then (case cf2sfile s f of
+ Some sf \<Rightarrow> Some (S_file sf (O_file f \<in> tainted s \<or> O_proc p \<in> tainted s))
+ | _ \<Rightarrow> None)
else co2sobj s obj)
| _ \<Rightarrow> None)
| _ \<Rightarrow> co2sobj s obj)"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
- simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
- same_inode_files_prop6
+ simp:current_files_simps cf2sfile_simps cp2sproc_simps
dest:is_file_in_current is_dir_in_current)
-
-(* should delete has_same_inode !?!?*)
-by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
+done
lemma co2sobj_closefd:
"\<lbrakk>valid (CloseFd p fd # s); alive (CloseFd p fd # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CloseFd p fd # s) obj = (
case obj of
- O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of
- Some f \<Rightarrow> (if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {(p, fd)} \<and>
- f \<in> files_hung_by_del s \<and> (\<forall> f'' \<in> same_inode_files s f.
- f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))
- then (case (cf2sfile s f, co2sobj s (O_file f')) of
- (Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b)
- | _ \<Rightarrow> None)
- else co2sobj s obj)
- | _ \<Rightarrow> co2sobj s obj)
- | O_proc p' \<Rightarrow> (if (p = p')
+ O_proc p' \<Rightarrow> (if (p = p')
then (case (cp2sproc (CloseFd p fd # s) p) of
- Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
+ Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
| _ \<Rightarrow> None)
else co2sobj s obj)
| _ \<Rightarrow> co2sobj s obj) "
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
- dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
+apply (simp_all add:current_files_simps cq2smsgq_other)
+apply (auto simp:cp2sproc_simps split:option.splits if_splits dest!:current_proc_has_sp')[1]
apply (frule is_file_in_current)
apply (case_tac "file_of_proc_fd s p fd")
-apply (simp add:tainted_eq_Tainted)
-apply (drule_tac f' = list in cf2sfiles_closefd, simp add:current_files_closefd, simp)
-apply (frule_tac f' = list in cf2sfiles_closefd, simp)
-apply (simp add:is_file_simps current_files_simps)
-apply (auto simp add:tainted_eq_Tainted cf2sfile_closefd split:if_splits option.splits
- dest!:current_file_has_sfile' dest:hung_file_in_current)[1]
+apply (simp add:current_files_simps is_file_simps tainted.simps)
+apply (drule_tac f = list in cf2sfile_closefd, simp add:current_files_simps)
+apply (simp split:option.splits)
+apply (frule_tac f = list in cf2sfile_closefd, simp)
+apply (simp split:option.splits)
+apply (simp add:is_file_simps current_files_simps split:if_splits)
+apply (rule impI, simp)
apply (simp add:is_dir_simps, frule is_dir_in_current)
apply (frule_tac f = list in cf2sfile_closefd)
@@ -2050,25 +1470,14 @@
done
lemma co2sobj_unlink:
- "\<lbrakk>valid (UnLink p f # s); alive (UnLink p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (UnLink p f # s) obj = (
- case obj of
- O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and>
- (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))
- then (case (cf2sfile s f, co2sobj s (O_file f')) of
- (Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b)
- | _ \<Rightarrow> None)
- else co2sobj s obj
- | _ \<Rightarrow> co2sobj s obj)"
+ "\<lbrakk>valid (UnLink p f # s); alive (UnLink p f # s) obj\<rbrakk>
+ \<Longrightarrow> co2sobj (UnLink p f # s) obj = co2sobj s obj"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
- dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
+apply (simp_all add:current_files_simps cq2smsgq_other)
+apply (auto simp:cp2sproc_simps split:option.splits if_splits dest!:current_proc_has_sp')[1]
apply (frule is_file_in_current)
apply (frule_tac f' = list in cf2sfile_unlink, simp)
-apply (frule_tac f' = list in cf2sfiles_unlink, simp)
-apply (simp add:is_file_simps current_files_simps)
-apply (auto simp add:tainted_eq_Tainted is_file_in_current split:if_splits option.splits
- dest!:current_file_has_sfile')[1]
+apply (simp add:is_file_simps current_files_simps split:option.splits if_splits)
apply (simp add:is_dir_simps, frule is_dir_in_current)
apply (frule_tac f' = list in cf2sfile_unlink)
@@ -2079,13 +1488,13 @@
lemma co2sobj_rmdir:
"\<lbrakk>valid (Rmdir p f # s); alive (Rmdir p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Rmdir p f # s) obj = co2sobj s obj"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
- dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
+apply (simp_all add:current_files_simps cq2smsgq_other)
+apply (auto simp:cp2sproc_simps split:option.splits if_splits dest!:current_proc_has_sp')[1]
apply (simp add:is_file_simps dir_is_empty_def)
apply (case_tac "f = list", drule file_dir_conflict, simp, simp)
-apply (simp add:cf2sfiles_other)
-apply (auto simp:cf2sfile_simps dest:is_dir_in_current)
+apply (frule_tac f' = list in cf2sfile_rmdir, simp add:is_file_in_current current_files_simps)
+apply (simp split:option.splits)
+apply (auto simp:cf2sfile_simps cf2sfile_other dest:is_dir_in_current)
done
lemma co2sobj_mkdir:
@@ -2096,75 +1505,50 @@
| _ \<Rightarrow> None)
else co2sobj s obj)"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
- dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
-apply (frule_tac cf2sfiles_other, simp+)
+apply (simp_all add:current_files_simps cq2smsgq_other)
+apply (auto simp:cp2sproc_simps split:option.splits if_splits dest!:current_proc_has_sp')[1]
+apply (case_tac "f = list", simp add:is_file_simps is_file_in_current)
+apply (frule_tac f' = list in cf2sfile_mkdir)
+apply (simp add:is_file_in_current)
+apply (simp split:option.splits)
+
apply (frule is_dir_in_current, rule impI, simp add:current_files_mkdir)
apply (frule current_file_has_sfile, simp, erule exE, simp)
apply (drule cf2sfile_mkdir1, simp+)
done
-
-lemma co2sobj_linkhard:
- "\<lbrakk>valid (LinkHard p oldf f # s); alive (LinkHard p oldf f # s) obj\<rbrakk>
- \<Longrightarrow> co2sobj (LinkHard p oldf f # s) obj = (
- case obj of
- O_file f' \<Rightarrow> if (f' = f \<or> f' \<in> same_inode_files s oldf)
- then (case (cf2sfile (LinkHard p oldf f # s) f) of
- Some sf \<Rightarrow> Some (S_file (cf2sfiles s oldf \<union> {sf}) (O_file oldf \<in> Tainted s))
- | _ \<Rightarrow> None)
- else co2sobj s obj
- | _ \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
- dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
-apply (frule_tac cf2sfiles_linkhard, simp+)
-apply (frule_tac f' = f in cf2sfile_linkhard, simp add:current_files_linkhard)
-apply (auto simp:is_file_simps sectxt_of_obj_simps current_files_simps is_file_in_current same_inodes_Tainted
- split:option.splits if_splits dest:Tainted_in_current
- dest!:current_has_sec' current_file_has_sfile')[1]
-
-apply (frule is_dir_in_current, simp add:current_files_linkhard is_dir_simps is_dir_in_current)
-apply (frule is_dir_in_current)
-apply (frule current_file_has_sfile, simp)
-apply (drule cf2sfile_linkhard1, simp+)
-done
-
lemma co2sobj_truncate:
"\<lbrakk>valid (Truncate p f len # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Truncate p f len # s) obj = (
case obj of
- O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> len > 0)
- then Some (S_file (cf2sfiles s f') (O_file f' \<in> Tainted s \<or> O_proc p \<in> Tainted s))
+ O_file f' \<Rightarrow> if (f' = f \<and> len > 0)
+ then (case cf2sfile s f of
+ Some sf \<Rightarrow> Some (S_file sf (O_file f' \<in> tainted s \<or> O_proc p \<in> tainted s))
+ | _ \<Rightarrow> None)
else co2sobj s obj
| _ \<Rightarrow> co2sobj s obj)"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
- simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
- same_inode_files_prop6
+ simp:current_files_simps cf2sfile_simps cp2sproc_simps
dest:is_file_in_current is_dir_in_current)
done
lemma co2sobj_kill:
"\<lbrakk>valid (Kill p p' # s); alive (Kill p p' # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Kill p p' # s) obj = co2sobj s obj"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
- simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
- same_inode_files_prop6
+ simp:current_files_simps cf2sfile_simps cp2sproc_simps
dest:is_file_in_current is_dir_in_current)
done
lemma co2sobj_exit:
"\<lbrakk>valid (Exit p # s); alive (Exit p # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Exit p # s) obj = co2sobj s obj"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other )
apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
- simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
- same_inode_files_prop6
+ simp:current_files_simps cf2sfile_simps cp2sproc_simps
dest:is_file_in_current is_dir_in_current)
done
@@ -2177,10 +1561,9 @@
else co2sobj s obj
| _ \<Rightarrow> co2sobj s obj)"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other )
apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
- simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
- same_inode_files_prop6
+ simp:current_files_simps cf2sfile_simps cp2sproc_simps
dest!:current_has_smsgq'
dest:is_file_in_current is_dir_in_current cq2smsg_createmsgq)
done
@@ -2194,10 +1577,9 @@
else co2sobj s obj
| _ \<Rightarrow> co2sobj s obj)"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other )
apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
- simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
- same_inode_files_prop6
+ simp:current_files_simps cf2sfile_simps cp2sproc_simps
dest!:current_has_smsgq'
dest:is_file_in_current is_dir_in_current cq2smsg_sendmsg)
done
@@ -2209,17 +1591,16 @@
Some sq \<Rightarrow> Some (S_msgq sq)
| _ \<Rightarrow> None)
else co2sobj s obj
- | O_proc p' \<Rightarrow> if (info_flow_shm s p p' \<and> O_msg q m \<in> Tainted s)
+ | O_proc p' \<Rightarrow> if (p' = p \<and> O_msg q m \<in> tainted s)
then (case (cp2sproc s p') of
Some sp \<Rightarrow> Some (S_proc sp True)
| _ \<Rightarrow> None)
else co2sobj s obj
| _ \<Rightarrow> co2sobj s obj)"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
- simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
- same_inode_files_prop6
+ simp:current_files_simps cf2sfile_simps cp2sproc_simps
dest!:current_has_smsgq'
dest:is_file_in_current is_dir_in_current cq2smsg_recvmsg)
done
@@ -2228,118 +1609,20 @@
"\<lbrakk>valid (RemoveMsgq p q # s); alive (RemoveMsgq p q # s) obj\<rbrakk>
\<Longrightarrow> co2sobj (RemoveMsgq p q # s) obj = co2sobj s obj"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
- simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
- same_inode_files_prop6
+ simp:current_files_simps cf2sfile_simps cp2sproc_simps
dest!:current_has_smsgq'
dest:is_file_in_current is_dir_in_current cq2smsg_removemsgq)
done
-lemma co2sobj_createshm:
- "\<lbrakk>valid (CreateShM p h # s); alive (CreateShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = (
- case obj of
- O_shm h' \<Rightarrow> if (h' = h) then (case (ch2sshm (CreateShM p h # s) h) of
- Some sh \<Rightarrow> Some (S_shm sh)
- | _ \<Rightarrow> None)
- else co2sobj s obj
- | _ \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
- simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
- same_inode_files_prop6 ch2sshm_simps
- dest!:current_shm_has_sh'
- dest:is_file_in_current is_dir_in_current)
-done
-
-lemma co2sobj_detach:
- "\<lbrakk>valid (Detach p h # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Detach p h # s) obj = (
- case obj of
- O_proc p' \<Rightarrow> if (p' = p) then (case (cp2sproc (Detach p h # s) p) of
- Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
- | _ \<Rightarrow> None)
- else co2sobj s obj
- | _ \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
- simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
- same_inode_files_prop6 ch2sshm_simps
- dest!:current_shm_has_sh'
- dest:is_file_in_current is_dir_in_current)
-done
-
-lemma co2sobj_deleteshm:
- "\<lbrakk>valid (DeleteShM p h # s); alive (DeleteShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (DeleteShM p h # s) obj = (
- case obj of
- O_proc p' \<Rightarrow> (case (cp2sproc (DeleteShM p h # s) p') of
- Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> Tainted s))
- | _ \<Rightarrow> None)
- | _ \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
- simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted
- same_inode_files_prop6 ch2sshm_simps
- dest!:current_shm_has_sh'
- dest:is_file_in_current is_dir_in_current)
-done
declare Product_Type.split_paired_Ex Product_Type.split_paired_All [simp del]
-lemma info_flow_shm_prop1:
- "p \<in> current_procs s \<Longrightarrow> info_flow_shm s p p"
-by (simp add:info_flow_shm_def)
-
-lemma co2sobj_attach:
- "\<lbrakk>valid (Attach p h flag # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj = (
- case obj of
- O_proc p' \<Rightarrow> if (info_flow_shm s p p')
- then (case (cp2sproc (Attach p h flag # s) p') of
- Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> Tainted s \<or>
- (\<exists> p''. O_proc p'' \<in> Tainted s \<and> (p'', SHM_RDWR) \<in> procs_of_shm s h)))
- | _ \<Rightarrow> None)
- else if (\<exists> p'' flag'. (p'', flag') \<in> procs_of_shm s h \<and> flag = SHM_RDWR \<and> O_proc p \<in> Tainted s \<and>
- info_flow_shm s p'' p')
- then (case (cp2sproc s p') of
- Some sp \<Rightarrow> Some (S_proc sp True)
- | _ \<Rightarrow> None)
- else co2sobj s obj
- | _ \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-
-apply (rule conjI|rule impI|erule exE)+
-apply (simp split:option.splits del:split_paired_Ex)
-apply (rule impI, frule current_proc_has_sp, simp)
-apply ((erule exE)+, auto simp:tainted_eq_Tainted intro:info_flow_shm_Tainted)[1]
-apply (rule impI, simp add:tainted_eq_Tainted split:option.splits del:split_paired_Ex)
-apply (auto simp:info_flow_shm_prop1 cp2sproc_attach dest!:current_proc_has_sp')[1]
-
-apply (case_tac "cp2sproc (Attach p h flag # s) nat")
-apply (drule current_proc_has_sp', simp+)
-
-apply (rule conjI|erule exE|erule conjE|rule impI)+
-apply (simp add:tainted_eq_Tainted)
-apply (auto simp:info_flow_shm_prop1 cp2sproc_attach intro:info_flow_shm_Tainted dest!:current_proc_has_sp')[1]
-apply (auto simp:info_flow_shm_prop1 cp2sproc_attach tainted_eq_Tainted intro:info_flow_shm_Tainted dest!:current_proc_has_sp'
-split:option.splits if_splits)[1]
-
-
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile'
- simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted
- same_inode_files_prop6
- dest:is_file_in_current is_dir_in_current)
-done
-
-
lemma co2sobj_other:
"\<lbrakk>valid (e # s); alive (e # s) obj;
\<forall> p f fds. e \<noteq> Execve p f fds;
- \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
+ \<forall> p p' fds. e \<noteq> Clone p p' fds;
\<forall> p p'. e \<noteq> Ptrace p p';
\<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
\<forall> p fd. e \<noteq> ReadFile p fd;
@@ -2348,27 +1631,20 @@
\<forall> p f. e \<noteq> UnLink p f;
\<forall> p f. e \<noteq> Rmdir p f;
\<forall> p f i. e \<noteq> Mkdir p f i;
- \<forall> p f f'. e \<noteq> LinkHard p f f';
\<forall> p f len. e \<noteq> Truncate p f len;
\<forall> p q. e \<noteq> CreateMsgq p q;
\<forall> p q m. e \<noteq> SendMsg p q m;
\<forall> p q m. e \<noteq> RecvMsg p q m;
- \<forall> p q. e \<noteq> RemoveMsgq p q;
- \<forall> p h. e \<noteq> CreateShM p h;
- \<forall> p h flag. e \<noteq> Attach p h flag;
- \<forall> p h. e \<noteq> Detach p h;
- \<forall> p h. e \<noteq> DeleteShM p h
- \<rbrakk> \<Longrightarrow> co2sobj (e # s) obj = co2sobj s obj"
+ \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk>
+ \<Longrightarrow> co2sobj (e # s) obj = co2sobj s obj"
apply (frule vt_grant, case_tac e)
apply (auto intro:co2sobj_kill co2sobj_exit)
done
lemmas co2sobj_simps = co2sobj_execve co2sobj_clone co2sobj_ptrace co2sobj_open co2sobj_readfile
- co2sobj_writefile co2sobj_closefd co2sobj_unlink co2sobj_rmdir co2sobj_mkdir co2sobj_linkhard
+ co2sobj_writefile co2sobj_closefd co2sobj_unlink co2sobj_rmdir co2sobj_mkdir
co2sobj_truncate co2sobj_kill co2sobj_exit co2sobj_createmsgq co2sobj_sendmsg co2sobj_recvmsg
- co2sobj_removemsgq co2sobj_attach co2sobj_detach co2sobj_createshm co2sobj_deleteshm
-
-
+ co2sobj_removemsgq
end
--- a/simple_selinux/S2ss_prop.thy Mon Dec 02 10:52:40 2013 +0800
+++ b/simple_selinux/S2ss_prop.thy Tue Dec 03 22:42:48 2013 +0800
@@ -10,7 +10,7 @@
lemma co2sobj_some_case:
"\<lbrakk>co2sobj s obj = Some sobj; \<And> p. obj = O_proc p \<Longrightarrow> P (O_proc p);
- \<And> f. obj = O_file f \<Longrightarrow> P (O_file f); \<And> h. obj = O_shm h \<Longrightarrow> P (O_shm h);
+ \<And> f. obj = O_file f \<Longrightarrow> P (O_file f);
\<And> f. obj = O_dir f \<Longrightarrow> P (O_dir f); \<And> q. obj = O_msgq q \<Longrightarrow> P (O_msgq q)\<rbrakk>
\<Longrightarrow> P obj"
by (case_tac obj, auto)
@@ -25,11 +25,11 @@
"valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = (
if (\<exists> p'. p' \<noteq> p \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p))
then (case (cp2sproc (Execve p f fds # s) p) of
- Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)}
+ Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s)}
| _ \<Rightarrow> {} )
else (case (cp2sproc (Execve p f fds # s) p, cp2sproc s p) of
- (Some sp, Some sp') \<Rightarrow> s2ss s - {S_proc sp' (O_proc p \<in> Tainted s)}
- \<union> {S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)}
+ (Some sp, Some sp') \<Rightarrow> s2ss s - {S_proc sp' (O_proc p \<in> tainted s)}
+ \<union> {S_proc sp (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s)}
| _ \<Rightarrow> {} ) )"
apply (frule vd_cons, frule vt_grant_os, simp split:if_splits)
@@ -42,15 +42,15 @@
apply (simp add:s2ss_def, rule set_eqI, rule iffI)
apply (drule CollectD, (erule exE|erule conjE)+)
apply (case_tac "obj = O_proc p")
-apply (simp add:co2sobj_execve tainted_eq_Tainted split:if_splits)
+apply (simp add:co2sobj_execve split:if_splits)
apply (simp add:co2sobj_execve, rule disjI2)
apply (rule_tac x = obj in exI, case_tac obj, (simp add:alive_simps)+)[1]
apply (simp, erule disjE)
-apply (rule_tac x = "O_proc p" in exI, simp add:tainted_eq_Tainted)
+apply (rule_tac x = "O_proc p" in exI, simp)
apply (erule exE| erule conjE)+
apply (case_tac "x = S_proc sp (O_proc p \<in> tainted s)")
apply (rule_tac x = "O_proc p'" in exI)
-apply (simp add:alive_execve co2sobj_execve tainted_eq_Tainted cp2sproc_execve)
+apply (simp add:alive_execve co2sobj_execve cp2sproc_execve)
apply (case_tac "obj = O_proc p", simp)
apply (frule co2sobj_execve_alive, simp, simp)
apply (frule_tac obj = obj in co2sobj_execve, simp)
@@ -62,45 +62,45 @@
apply (erule exE, erule conjE, simp)
apply (simp add:s2ss_def, rule set_eqI, rule iffI)
apply (drule CollectD, (erule exE|erule conjE)+)
-apply (case_tac "obj = O_proc p", simp add:tainted_eq_Tainted)
+apply (case_tac "obj = O_proc p", simp)
apply (rule disjI1, simp split:if_splits)
apply (simp add:co2sobj_execve, rule disjI2)
apply (rule conjI,rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits)
apply (rule notI, simp, case_tac obj)
-apply (erule_tac x = nat in allE, simp add:tainted_eq_Tainted, (simp split:option.splits)+)
+apply (erule_tac x = nat in allE, simp, (simp split:option.splits)+)
apply (erule disjE, simp)
-apply (rule_tac x = "O_proc p" in exI, simp add:tainted_eq_Tainted)
+apply (rule_tac x = "O_proc p" in exI, simp)
apply (erule exE|erule conjE)+
apply (rule_tac x = obj in exI)
apply (drule_tac obj = obj in co2sobj_execve_alive, simp+)
apply (frule_tac obj = obj in co2sobj_execve, simp, simp)
-apply (rule impI, simp add:tainted_eq_Tainted, simp)
+apply (rule impI, simp, simp)
done
lemma s2ss_clone_alive:
- "\<lbrakk>co2sobj s obj = Some x; alive s obj; obj \<noteq> O_proc p'; valid (Clone p p' fds shms # s)\<rbrakk>
- \<Longrightarrow> alive (Clone p p' fds shms # s) obj"
+ "\<lbrakk>co2sobj s obj = Some x; alive s obj; obj \<noteq> O_proc p'; valid (Clone p p' fds # s)\<rbrakk>
+ \<Longrightarrow> alive (Clone p p' fds # s) obj"
by (erule co2sobj_some_case, auto simp:alive_clone)
lemma s2ss_clone:
- "valid (Clone p p' fds shms # s) \<Longrightarrow> s2ss (Clone p p' fds shms # s) = (
- case (cp2sproc (Clone p p' fds shms # s) p') of
- Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> Tainted s)}
+ "valid (Clone p p' fds # s) \<Longrightarrow> s2ss (Clone p p' fds # s) = (
+ case (cp2sproc (Clone p p' fds # s) p') of
+ Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> tainted s)}
| _ \<Rightarrow> {})"
apply (frule vd_cons, frule vt_grant_os, split option.splits)
apply (rule conjI, rule impI, drule current_proc_has_sp', simp, simp)
apply (rule allI, rule impI, simp add:s2ss_def)
apply (rule set_eqI, rule iffI, drule CollectD, (erule exE|erule conjE)+)
-apply (case_tac "obj = O_proc p'", simp add:tainted_eq_Tainted)
-apply (case_tac "O_proc p' \<in> Tainted s", drule Tainted_in_current, simp+)
+apply (case_tac "obj = O_proc p'", simp)
+apply (case_tac "O_proc p' \<in> tainted s", drule tainted_in_current, simp+)
apply (rule disjI1, simp split:if_splits)
-apply (simp add:tainted_eq_Tainted, rule disjI2)
+apply (simp, rule disjI2)
apply (frule co2sobj_clone, simp)
apply (rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits)
apply (simp, erule disjE, simp)
-apply (rule_tac x = "O_proc p'" in exI, simp add:tainted_eq_Tainted)
-apply (rule impI, rule notI, drule Tainted_in_current, simp+)
+apply (rule_tac x = "O_proc p'" in exI, simp)
+apply (rule impI, rule notI, drule tainted_in_current, simp+)
apply (erule exE| erule conjE)+
apply (case_tac "obj = O_proc p'", simp)
apply (rule_tac x = obj in exI)
@@ -108,46 +108,6 @@
apply (auto simp:co2sobj_clone alive_simps)
done
-definition s2ss_shm_no_backup:: "t_state \<Rightarrow> t_process \<Rightarrow> t_static_state"
-where
- "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>
- (\<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)))}"
-
-definition update_s2ss_shm:: "t_state \<Rightarrow> t_process \<Rightarrow> t_static_state"
-where
- "update_s2ss_shm s pfrom \<equiv> s2ss s
- \<union> {S_proc sp True| sp p. info_flow_shm s pfrom p \<and> cp2sproc s p = Some sp}
- - (s2ss_shm_no_backup s pfrom)"
-
-lemma s2ss_shm_no_bk_elim:
- "\<lbrakk>S_proc sp False \<notin> s2ss_shm_no_backup s pfrom; co2sobj s (O_proc p) = Some (S_proc sp False);
- valid s; info_flow_shm s pfrom p\<rbrakk>
- \<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)"
-apply (auto simp:s2ss_shm_no_backup_def co2sobj.simps tainted_eq_Tainted split:option.splits)
-apply (erule_tac x = p in allE, auto)
-apply (rule_tac x = p' in exI, auto)
-done
-
-lemma s2ss_shm_no_bk_intro1:
- "\<lbrakk>co2sobj s' obj = Some x; \<forall> p. obj \<noteq> O_proc p\<rbrakk> \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"
-apply (case_tac obj)
-apply (auto simp:co2sobj.simps s2ss_shm_no_backup_def split:option.splits)
-done
-
-lemma s2ss_shm_no_bk_intro2:
- "\<lbrakk>co2sobj s' obj = Some x; obj \<in> Tainted s'; valid s'\<rbrakk> \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"
-apply (case_tac obj)
-
-apply (auto simp:co2sobj.simps s2ss_shm_no_backup_def tainted_eq_Tainted split:option.splits)
-done
-
-lemma s2ss_shm_no_bk_intro3:
- "\<lbrakk>co2sobj s (O_proc p) = Some x; \<not> info_flow_shm s pfrom p; p \<in> current_procs s
- \<rbrakk> \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"
-apply (auto simp add:s2ss_shm_no_backup_def split:option.splits)
-apply (rule_tac x = p in exI, simp)
-done
-
lemma s2ss_shm_no_bk_intro4:
"\<lbrakk>co2sobj s (O_proc p) = Some x; info_flow_shm s pfrom p;
\<not> info_flow_shm s pfrom p'; p' \<in> current_procs s; co2sobj s (O_proc p') = Some x\<rbrakk>
@@ -156,14 +116,14 @@
apply (auto simp add:s2ss_shm_no_backup_def co2sobj.simps split:option.splits)
done
-lemma Tainted_ptrace':
- "valid s \<Longrightarrow> Tainted (Ptrace p p' # s) =
- (if (O_proc p \<in> Tainted s \<and> O_proc p' \<notin> Tainted s)
- then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p' p''}
- else if (O_proc p' \<in> Tainted s \<and> O_proc p \<notin> Tainted s)
- then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p p''}
- else Tainted s)"
-using info_flow_shm_Tainted by auto
+lemma tainted_ptrace':
+ "valid s \<Longrightarrow> tainted (Ptrace p p' # s) =
+ (if (O_proc p \<in> tainted s \<and> O_proc p' \<notin> tainted s)
+ then tainted s \<union> {O_proc p'' | p''. info_flow_shm s p' p''}
+ else if (O_proc p' \<in> tainted s \<and> O_proc p \<notin> tainted s)
+ then tainted s \<union> {O_proc p'' | p''. info_flow_shm s p p''}
+ else tainted s)"
+using info_flow_shm_tainted by auto
lemma co2sobj_some_caseD:
"\<lbrakk>co2sobj s obj = Some sobj; \<And> p. \<lbrakk>co2sobj s obj = Some sobj; obj = O_proc p\<rbrakk> \<Longrightarrow> P (O_proc p);
@@ -177,25 +137,25 @@
lemma s2ss_ptrace1_aux: "x \<notin> {x. P x} \<Longrightarrow> \<not> P x" by simp
lemma s2ss_ptrace1:
- "\<lbrakk>valid (Ptrace p p' # s); O_proc p \<in> Tainted s; O_proc p' \<notin> Tainted s\<rbrakk>
+ "\<lbrakk>valid (Ptrace p p' # s); O_proc p \<in> tainted s; O_proc p' \<notin> tainted s\<rbrakk>
\<Longrightarrow> s2ss (Ptrace p p' # s) = update_s2ss_shm s p'"
unfolding update_s2ss_shm_def s2ss_def s2ss_shm_no_backup_def
apply (frule vd_cons, rule set_eqI, rule iffI)
apply (drule CollectD, (erule exE|erule conjE)+)
apply (erule co2sobj_some_caseD)
apply (rule DiffI)
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
apply (case_tac "info_flow_shm s p' pa")
apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (rule_tac x = a in exI, rule_tac x = pa in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
apply (rule UnI1, simp)
apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
-apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
+apply (rule notI, clarsimp simp:cp2sproc_other split:option.splits)
apply (erule_tac x = pa in allE, simp)
apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
@@ -214,17 +174,17 @@
apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE)
apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (erule co2sobj_some_caseD)
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp add:tainted_eq_Tainted cp2sproc_other split:option.splits)
+apply (clarsimp simp cp2sproc_other split:option.splits)
apply (case_tac "info_flow_shm s p' pa", simp only:co2sobj.simps split:option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (drule Meson.not_exD, erule_tac x = a in allE, drule Meson.not_exD, erule_tac x = pa in allE)
-apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+)
+apply (simp, (erule exE|erule conjE)+)
apply (rule_tac x = "O_proc p'a" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
apply (rule_tac x = obj in exI,
auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
@@ -237,29 +197,29 @@
apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other info_shm_flow_in_procs)
done
lemma s2ss_ptrace2:
- "\<lbrakk>valid (Ptrace p p' # s); O_proc p' \<in> Tainted s; O_proc p \<notin> Tainted s\<rbrakk>
+ "\<lbrakk>valid (Ptrace p p' # s); O_proc p' \<in> tainted s; O_proc p \<notin> tainted s\<rbrakk>
\<Longrightarrow> s2ss (Ptrace p p' # s) = update_s2ss_shm s p"
unfolding update_s2ss_shm_def s2ss_def s2ss_shm_no_backup_def
apply (frule vd_cons, rule set_eqI, rule iffI)
apply (drule CollectD, (erule exE|erule conjE)+)
apply (erule co2sobj_some_caseD)
apply (rule DiffI)
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
apply (case_tac "info_flow_shm s p pa")
apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (rule_tac x = a in exI, rule_tac x = pa in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
apply (rule UnI1, simp)
apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
-apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
+apply (rule notI, clarsimp simp:cp2sproc_other split:option.splits)
apply (erule_tac x = pa in allE, simp)
apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
@@ -278,17 +238,17 @@
apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE)
apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (erule co2sobj_some_caseD)
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp add:tainted_eq_Tainted cp2sproc_other split:option.splits)
+apply (clarsimp simp cp2sproc_other split:option.splits)
apply (case_tac "info_flow_shm s p pa", simp only:co2sobj.simps split:option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (drule Meson.not_exD, erule_tac x = a in allE, drule Meson.not_exD, erule_tac x = pa in allE)
-apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+)
+apply (simp, (erule exE|erule conjE)+)
apply (rule_tac x = "O_proc p'a" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)
apply (rule_tac x = obj in exI,
auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
@@ -301,11 +261,11 @@
apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other info_shm_flow_in_procs)
done
lemma s2ss_ptrace3:
- "\<lbrakk>valid (Ptrace p p' # s); (O_proc p' \<in> Tainted s) = (O_proc p \<in> Tainted s)\<rbrakk>
+ "\<lbrakk>valid (Ptrace p p' # s); (O_proc p' \<in> tainted s) = (O_proc p \<in> tainted s)\<rbrakk>
\<Longrightarrow> s2ss (Ptrace p p' # s) = s2ss s"
unfolding s2ss_def
apply (frule vd_cons, rule set_eqI, rule iffI)
@@ -313,22 +273,22 @@
apply (rule_tac x = obj in exI)
apply (frule alive_other, simp+)
apply (frule_tac obj = obj in co2sobj_ptrace, simp)
-apply (auto simp add:tainted_eq_Tainted split:t_object.splits option.splits if_splits
- intro:info_flow_shm_Tainted)[1]
+apply (auto simp split:t_object.splits option.splits if_splits
+ intro:info_flow_shm_tainted)[1]
apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (rule_tac x = obj in exI)
apply (frule alive_other, simp+)
apply (frule_tac obj = obj in co2sobj_ptrace, simp)
-apply (auto simp add:tainted_eq_Tainted split:t_object.splits option.splits if_splits
- intro:info_flow_shm_Tainted)
+apply (auto simp split:t_object.splits option.splits if_splits
+ intro:info_flow_shm_tainted)
done
lemma s2ss_ptrace:
"valid (Ptrace p p' # s) \<Longrightarrow> s2ss (Ptrace p p' # s) = (
- if (O_proc p \<in> Tainted s \<and> O_proc p' \<notin> Tainted s)
+ if (O_proc p \<in> tainted s \<and> O_proc p' \<notin> tainted s)
then update_s2ss_shm s p'
- else if (O_proc p' \<in> Tainted s \<and> O_proc p \<notin> Tainted s)
+ else if (O_proc p' \<in> tainted s \<and> O_proc p \<notin> tainted s)
then update_s2ss_shm s p
else s2ss s )"
apply (frule vt_grant_os, frule vd_cons)
@@ -351,15 +311,15 @@
apply (simp split: option.splits, (erule conjE)+)
apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (rule_tac x = obj in exI)
-apply (simp add:co2sobj_kill tainted_eq_Tainted alive_kill split:t_object.splits if_splits)
+apply (simp add:co2sobj_kill alive_kill split:t_object.splits if_splits)
apply (erule CollectE, erule exE, erule conjE, rule CollectI)
apply (erule co2sobj_some_caseD)
apply (case_tac "pa = p'")
apply (rule_tac x = "O_proc p''" in exI)
-apply (simp add:cp2sproc_kill tainted_eq_Tainted alive_kill
+apply (simp add:cp2sproc_kill alive_kill
split:t_object.splits if_splits option.splits)
apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp add:cp2sproc_kill tainted_eq_Tainted alive_kill
+apply (clarsimp simp add:cp2sproc_kill alive_kill
split:t_object.splits if_splits option.splits)
apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+
@@ -367,18 +327,18 @@
apply (rule set_eqI, rule iffI)
apply (erule CollectE, erule exE, erule conjE, rule DiffI)
apply (rule CollectI, rule_tac x = obj in exI)
-apply (simp add:co2sobj_kill tainted_eq_Tainted alive_kill split:t_object.splits if_splits)
+apply (simp add:co2sobj_kill alive_kill split:t_object.splits if_splits)
apply (rule notI, simp, case_tac obj)
apply (erule_tac x = nat in allE)
-apply (simp add:co2sobj_kill cp2sproc_kill tainted_eq_Tainted split:option.splits)
+apply (simp add:co2sobj_kill cp2sproc_kill split:option.splits)
apply (simp split:option.splits)+
apply (erule co2sobj_some_caseD)
apply (case_tac "pa = p'")
apply (rule_tac x = "O_proc p''" in exI)
-apply (simp add:cp2sproc_kill tainted_eq_Tainted alive_kill
+apply (simp add:cp2sproc_kill alive_kill
split:t_object.splits if_splits option.splits)
apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp add:cp2sproc_kill tainted_eq_Tainted alive_kill
+apply (clarsimp simp add:cp2sproc_kill alive_kill
split:t_object.splits if_splits option.splits)
apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+
done
@@ -399,15 +359,15 @@
apply (simp split: option.splits, (erule conjE)+)
apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (rule_tac x = obj in exI)
-apply (simp add:co2sobj_exit tainted_eq_Tainted alive_exit split:t_object.splits if_splits)
+apply (simp add:co2sobj_exit alive_exit split:t_object.splits if_splits)
apply (erule CollectE, erule exE, erule conjE, rule CollectI)
apply (erule co2sobj_some_caseD)
apply (case_tac "pa = p")
apply (rule_tac x = "O_proc p'" in exI)
-apply (simp add:cp2sproc_exit tainted_eq_Tainted alive_exit
+apply (simp add:cp2sproc_exit alive_exit
split:t_object.splits if_splits option.splits)
apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp add:cp2sproc_exit tainted_eq_Tainted alive_exit
+apply (clarsimp simp add:cp2sproc_exit alive_exit
split:t_object.splits if_splits option.splits)
apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+
@@ -415,18 +375,18 @@
apply (rule set_eqI, rule iffI)
apply (erule CollectE, erule exE, erule conjE, rule DiffI)
apply (rule CollectI, rule_tac x = obj in exI)
-apply (simp add:co2sobj_exit tainted_eq_Tainted alive_exit split:t_object.splits if_splits)
+apply (simp add:co2sobj_exit alive_exit split:t_object.splits if_splits)
apply (rule notI, simp, case_tac obj)
apply (erule_tac x = nat in allE)
-apply (simp add:co2sobj_exit cp2sproc_exit tainted_eq_Tainted split:option.splits)
+apply (simp add:co2sobj_exit cp2sproc_exit split:option.splits)
apply (simp split:option.splits)+
apply (erule co2sobj_some_caseD)
apply (case_tac "pa = p")
apply (rule_tac x = "O_proc p'" in exI)
-apply (simp add:cp2sproc_exit tainted_eq_Tainted alive_exit
+apply (simp add:cp2sproc_exit alive_exit
split:t_object.splits if_splits option.splits)
apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp add:cp2sproc_exit tainted_eq_Tainted alive_exit
+apply (clarsimp simp add:cp2sproc_exit alive_exit
split:t_object.splits if_splits option.splits)
apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+
done
@@ -443,7 +403,7 @@
"\<lbrakk>valid (Open p f flag fd None # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Open p f flag fd None # s) obj = (
if (obj = O_proc p)
then (case (cp2sproc (Open p f flag fd None # s) p) of
- Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
+ Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
| _ \<Rightarrow> None)
else co2sobj s obj)"
apply (frule vt_grant_os, frule vd_cons)
@@ -455,11 +415,11 @@
"\<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 = (
if (obj = O_proc p)
then (case (cp2sproc (Open p f flag fd (Some i) # s) p) of
- Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
+ Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
| _ \<Rightarrow> None)
else if (obj = O_file f)
then (case (cf2sfile (Open p f flag fd (Some i) # s) f) of
- Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> Tainted s))
+ Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> tainted s))
| _ \<Rightarrow> None)
else co2sobj s obj)"
apply (frule vt_grant_os, frule vd_cons)
@@ -607,7 +567,7 @@
lemma s2ss_readfile:
"valid (ReadFile p fd # s) \<Longrightarrow> s2ss (ReadFile p fd # s) = (
case (file_of_proc_fd s p fd) of
- Some f \<Rightarrow> if (O_file f \<in> Tainted s)
+ Some f \<Rightarrow> if (O_file f \<in> tainted s)
then update_s2ss_shm s p
else s2ss s
| _ \<Rightarrow> {})"
@@ -618,18 +578,18 @@
apply (drule CollectD, (erule exE|erule conjE)+)
apply (erule co2sobj_some_caseD)
apply (rule DiffI)
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
+apply (clarsimp simp:cp2sproc_other co2sobj.simps split:option.splits)
apply (case_tac "info_flow_shm s p pa")
apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (rule_tac x = ab in exI, rule_tac x = pa in exI)
-apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (clarsimp simp:cp2sproc_other split:option.splits)
apply (rule UnI1, simp)
apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
-apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
+apply (clarsimp simp:cp2sproc_other co2sobj.simps split:option.splits)
+apply (rule notI, clarsimp simp:cp2sproc_other co2sobj.simps split:option.splits)
apply (erule_tac x = pa in allE, simp)
apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI)
@@ -644,17 +604,17 @@
apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE)
apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (erule co2sobj_some_caseD)
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:tainted_eq_Tainted cp2sproc_other co2sobj.simps split:option.splits)
+apply (clarsimp simp:tainted_eq_tainted cp2sproc_other co2sobj.simps split:option.splits)
apply (case_tac "info_flow_shm s p pa", simp only:co2sobj.simps split:option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (drule Meson.not_exD, erule_tac x = ab in allE, drule Meson.not_exD, erule_tac x = pa in allE)
-apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+)
+apply (simp, (erule exE|erule conjE)+)
apply (rule_tac x = "O_proc p'" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other co2sobj.simps split:option.splits)
apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other co2sobj.simps split:option.splits)
apply (rule_tac x = obj in exI,
auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1]
@@ -667,7 +627,7 @@
apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs co2sobj.simps)
+apply (clarsimp simp:tainted_ptrace' cp2sproc_other info_shm_flow_in_procs co2sobj.simps)
apply (rule impI, rule impI)
@@ -695,18 +655,18 @@
lemma co2sobj_writefile_unchange:
"\<lbrakk>valid (WriteFile p fd # s); alive s obj; file_of_proc_fd s p fd = Some f;
- O_proc p \<in> Tainted s \<longrightarrow> O_file f \<in> Tainted s\<rbrakk>
+ O_proc p \<in> tainted s \<longrightarrow> O_file f \<in> tainted s\<rbrakk>
\<Longrightarrow> co2sobj (WriteFile p fd # s) obj = co2sobj s obj"
apply (frule vd_cons, frule co2sobj_writefile, simp, simp split:t_object.splits if_splits)
apply (simp add:co2sobj.simps)
-apply (case_tac "O_proc p \<in> Tainted s")
-apply (simp add:tainted_eq_Tainted same_inodes_Tainted)+
+apply (case_tac "O_proc p \<in> tainted s")
+apply (simp same_inodes_tainted)+
done
lemma s2ss_writefile:
"valid (WriteFile p fd # s) \<Longrightarrow> s2ss (WriteFile p fd # s) = (
case (file_of_proc_fd s p fd) of
- Some f \<Rightarrow> if (O_proc p \<in> Tainted s \<and> O_file f \<notin> Tainted s)
+ Some f \<Rightarrow> if (O_proc p \<in> tainted s \<and> O_file f \<notin> tainted s)
then (if (\<exists> f'. f' \<notin> same_inode_files s f \<and> is_file s f' \<and>
co2sobj s (O_file f') = co2sobj s (O_file f))
then s2ss s \<union> {S_file (cf2sfiles s f) True}
@@ -744,7 +704,7 @@
apply (frule_tac f = fa and f' = aa in cf2sfiles_prop, simp)
apply (rule_tac x = "O_file f'" in exI, simp add:co2sobj_writefile is_file_simps)
apply (rule conjI, rule impI, simp add:same_inode_files_prop5)
-apply (rule impI, simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)
+apply (rule impI, simp add:co2sobj.simps same_inodes_tainted)
apply (rule_tac x = "O_file fa" in exI, simp add:co2sobj_writefile is_file_simps)
apply (rule impI, simp add:same_inode_files_prop5)
apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
@@ -754,8 +714,8 @@
apply (rule impI, rule impI, simp, rule set_eqI, rule iffI, erule CollectE, (erule conjE|erule exE)+)
apply (rule CollectI, rule_tac x = obj in exI, simp add:alive_simps)
apply (simp add:co2sobj_writefile split:t_object.splits if_splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)
-apply (case_tac "O_proc p \<in> Tainted s", simp, simp)
+apply (simp add:co2sobj.simps same_inodes_tainted)
+apply (case_tac "O_proc p \<in> tainted s", simp, simp)
apply (erule CollectE, (erule conjE|erule exE)+, rule CollectI)
apply (rule_tac x = obj in exI)
apply (simp add:co2sobj_writefile_unchange alive_simps)
@@ -769,7 +729,7 @@
apply (rule disjI1, simp add:cf2sfiles_prop)
apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp)
apply (rule notI, simp add:co2sobj.simps split:option.splits)
-apply (erule_tac x = list in allE, simp add:tainted_eq_Tainted same_inode_files_prop5)
+apply (erule_tac x = list in allE, simp same_inode_files_prop5)
apply (simp add:co2sobj.simps)
apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,
rule notI, simp add:co2sobj.simps split:option.splits)
@@ -789,7 +749,7 @@
apply (erule co2sobj_some_caseD)
apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
apply (case_tac "fa \<in> same_inode_files s aa")
-apply (frule cf2sfiles_prop, simp, simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)
+apply (frule cf2sfiles_prop, simp, simp add:co2sobj.simps same_inodes_tainted)
apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_file_simps)
apply (rule impI, simp add:same_inode_files_prop5)
apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
@@ -818,7 +778,7 @@
"update_s2ss_sfile_del s ss f sf \<equiv>
if (same_inode_files s f = {f})
then ss
- else ss \<union> {S_file (cf2sfiles s f - {sf}) (O_file f \<in> Tainted s)}"
+ else ss \<union> {S_file (cf2sfiles s f - {sf}) (O_file f \<in> tainted s)}"
definition del_s2ss_file:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
where
@@ -827,7 +787,7 @@
then ss
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))
then update_s2ss_sfile_del s ss f sf
- else update_s2ss_sfile_del s (ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)}) f sf)"
+ else update_s2ss_sfile_del s (ss - {S_file (cf2sfiles s f) (O_file f \<in> tainted s)}) f sf)"
lemma alive_co2sobj_closefd1:
"\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj;
@@ -921,14 +881,14 @@
(Some sf, Some sp, Some sp') \<Rightarrow>
(del_s2ss_file s (
update_s2ss_obj s (s2ss s) (O_proc p)
- (S_proc sp (O_proc p \<in> Tainted s))
- (S_proc sp' (O_proc p \<in> Tainted s))) f sf)
+ (S_proc sp (O_proc p \<in> tainted s))
+ (S_proc sp' (O_proc p \<in> tainted s))) f sf)
| _ \<Rightarrow> {})
else (case (cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of
(Some sp, Some sp') \<Rightarrow>
(update_s2ss_obj s (s2ss s) (O_proc p)
- (S_proc sp (O_proc p \<in> Tainted s))
- (S_proc sp' (O_proc p \<in> Tainted s)))
+ (S_proc sp (O_proc p \<in> tainted s))
+ (S_proc sp' (O_proc p \<in> tainted s)))
| _ \<Rightarrow> {})
| _ \<Rightarrow> s2ss s)"
apply (frule vd_cons, frule vt_grant_os)
@@ -942,12 +902,12 @@
apply (frule co2sobj_closefd, simp)
apply (frule cp2sproc_closefd, simp)
apply (simp add:proc_file_fds_def split:t_object.splits)
-apply (simp split:if_splits add:co2sobj.simps tainted_eq_Tainted)
+apply (simp split:if_splits add:co2sobj.simps)
apply (erule CollectE, erule exE, erule conjE, rule CollectI)
apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd2)
apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd2)
apply (frule cp2sproc_closefd, simp)
-apply (auto simp add:proc_file_fds_def co2sobj.simps tainted_eq_Tainted
+apply (auto simp add:proc_file_fds_def co2sobj.simps
split:t_object.splits option.splits if_splits)[1]
apply (case_tac "cp2sproc (CloseFd p fd # s) p")
@@ -965,58 +925,58 @@
apply (tactic {*my_seteq_tac 1*})
apply simp
apply (case_tac "obj = O_proc p")
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (rule disjI2, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_simps)
-apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
apply (tactic {*my_setiff_tac 1*})
apply (rule_tac x = "O_proc p" in exI)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (tactic {*my_setiff_tac 1*})
apply (case_tac "obj = O_proc p")
apply (rule_tac x = obj' in exI)
apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (case_tac "obj = O_file a")
apply (rule_tac x = "O_file f'" in exI)
apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
-apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
apply (rule_tac x = obj in exI)
apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (auto simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)[1]
apply (rule impI)+
apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_proc p", rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_proc p", rule disjI1, simp add:co2sobj.simps)
apply (rule disjI2)
apply (case_tac "obj = O_file a", simp add:alive_simps)
apply (rule DiffI, simp)
apply (rule_tac x = obj in exI)
apply (frule_tac obj = obj in alive_co2sobj_closefd', simp+)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
apply (simp, rule notI, simp, frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
apply (erule_tac x = "O_proc pa" in allE, simp)
apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_proc p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_proc p", simp add:co2sobj.simps)
apply (case_tac "obj = O_file a", rule_tac x = "O_file f'" in exI)
apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
-apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
apply (rule_tac x = obj in exI)
apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
apply (rule impI, tactic {*my_seteq_tac 1*})
apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def)
apply (rule conjI| rule impI|erule exE|erule conjE)+
apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "pa = p", simp add:co2sobj.simps)
apply (rule disjI2, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (case_tac "f = a", simp add:alive_simps)
@@ -1030,14 +990,14 @@
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (rule conjI| rule impI|erule exE|erule conjE)+
apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "pa = p", simp add:co2sobj.simps)
apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
apply (case_tac "f = a", simp add:alive_simps)
apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)
apply (erule bexE, erule conjE)
apply (erule_tac x = f'' in ballE, simp, simp)
apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
@@ -1050,7 +1010,7 @@
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (rule impI, rule conjI, rule impI)
apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "pa = p", simp add:co2sobj.simps)
apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_file_simps)
@@ -1069,16 +1029,16 @@
apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
apply (rule impI)
apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "pa = p", simp add:co2sobj.simps)
apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
apply (rule notI, simp add:co2sobj_closefd)
apply (erule_tac x = obj in allE, simp)
apply (case_tac "f = a", simp add:alive_simps)
apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)
apply (erule bexE, erule conjE)
apply (erule_tac x = f'' in ballE, simp, simp)
apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
@@ -1095,34 +1055,34 @@
apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
apply (simp add:update_s2ss_sfile_del_def update_s2ss_obj_def split:if_splits)
-apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
apply (erule exE, erule conjE)
apply (case_tac "obj = O_proc p")
apply (rule_tac x = obj' in exI)
apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (case_tac "obj = O_file a")
apply (rule_tac x = "O_file f'" in exI)
apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
-apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
apply (rule_tac x = obj in exI)
apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
-apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (auto simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)[1]
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
apply (erule conjE, erule exE, erule conjE)
apply (case_tac "obj = O_proc p")
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (case_tac "obj = O_file a")
apply (rule_tac x = "O_file f'" in exI)
apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
-apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
apply (rule_tac x = obj in exI)
apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (auto simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)[1]
apply (erule disjE)
apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE)
apply (rule_tac x = "O_file f'a" in exI)
@@ -1130,16 +1090,16 @@
apply (frule_tac obj = "O_file f'a" in co2sobj_closefd)
apply (simp add:alive_simps)+
apply (frule_tac f = "f'a" in is_file_has_sfile', simp, erule exE)
-apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits)
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted split:if_splits)
apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
apply (erule disjE)
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
apply (erule exE, erule conjE)
apply (case_tac "obj = O_proc p")
apply (rule_tac x = obj' in exI)
apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (erule_tac obj = obj in co2sobj_some_caseD)
apply (rule_tac x = obj in exI)
apply (simp add:co2sobj_closefd)
@@ -1147,7 +1107,7 @@
apply (rule_tac x = "O_file f'" in exI)
apply (simp add:co2sobj_simps is_file_simps split:if_splits option.splits t_sobject.splits)
apply (rule conjI, rule notI, simp add:same_inode_files_prop9)
-apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)
+apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
apply (rule_tac x = obj in exI)
apply (simp add:co2sobj_closefd is_file_simps)
apply (rule notI, simp add:same_inode_files_prop9)
@@ -1162,15 +1122,15 @@
apply (frule_tac obj = "O_file f'a" in co2sobj_closefd)
apply (simp add:alive_simps)+
apply (frule_tac f = "f'a" in is_file_has_sfile', simp, erule exE)
-apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits)
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted split:if_splits)
apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
apply (erule disjE)
apply (rule_tac x = "O_proc p" in exI)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (erule conjE, erule exE, erule conjE)
apply (case_tac "obj = O_proc p")
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (erule_tac obj = obj in co2sobj_some_caseD)
apply (rule_tac x = obj in exI)
apply (simp add:co2sobj_closefd)
@@ -1178,7 +1138,7 @@
apply (rule_tac x = "O_file f'" in exI)
apply (simp add:co2sobj_simps is_file_simps split:if_splits option.splits t_sobject.splits)
apply (rule conjI, rule notI, simp add:same_inode_files_prop9)
-apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)
+apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
apply (rule_tac x = obj in exI)
apply (simp add:co2sobj_closefd is_file_simps)
apply (rule notI, simp add:same_inode_files_prop9)
@@ -1191,7 +1151,7 @@
apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def)
apply (rule conjI| rule impI|erule exE|erule conjE)+
apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "pa = p", simp add:co2sobj.simps)
apply (rule disjI2, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (case_tac "f = a", simp add:alive_simps)
@@ -1205,18 +1165,18 @@
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (rule conjI| rule impI|erule exE|erule conjE)+
apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "pa = p", simp add:co2sobj.simps)
apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
apply (rule notI, simp, erule_tac x = "O_proc pa" in allE, simp add:co2sobj_closefd)
apply (case_tac "f = a", simp add:alive_simps)
apply (case_tac "f \<in> same_inode_files s a", rule disjI2)
apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)
apply (erule bexE, erule conjE)
apply (rule conjI, rule_tac x = "O_file f''" in exI)
-apply (simp add:same_inode_files_prop11 co2sobj.simps tainted_eq_Tainted cf2sfiles_prop same_inodes_Tainted)
+apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_tainted)
apply (rule notI, simp)
apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
@@ -1233,47 +1193,47 @@
apply (erule bexE, erule conjE)
apply (simp add:update_s2ss_obj_def split:if_splits)
-apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
apply (erule exE, erule conjE)
apply (case_tac "obj = O_proc p")
apply (rule_tac x = obj' in exI)
apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (case_tac "obj = O_file a")
apply (rule_tac x = "O_file f'" in exI)
apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11)
-apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
apply (rule conjI)
apply (rule impI)
apply (rule_tac x = f' in ballE, simp, simp, simp)
-apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted)
+apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_tainted)
apply (rule_tac x = obj in exI)
apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
-apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (auto simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)[1]
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
apply (erule conjE, erule exE, erule conjE)
apply (case_tac "obj = O_proc p")
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (case_tac "obj = O_file a")
apply (rule_tac x = "O_file f'" in exI)
apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11)
-apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
apply (rule conjI)
apply (rule impI)
apply (rule_tac x = f' in ballE, simp, simp, simp)
-apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted)
+apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_tainted)
apply (rule_tac x = obj in exI)
apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (auto simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)[1]
apply (rule impI)
apply (tactic {*my_seteq_tac 1*})
apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def)
apply (rule conjI| rule impI|erule exE|erule conjE)+
apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "pa = p", simp add:co2sobj.simps)
apply (rule disjI2, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (case_tac "f = a", simp add:alive_simps)
@@ -1287,25 +1247,25 @@
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (frule_tac obj = obj in co2sobj_closefd, simp, rule notI, simp)
apply (frule_tac obj = obj in co2sobj_sfile_imp, erule exE, simp add:is_file_simps split:if_splits)
-apply (erule_tac x= f in allE, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule_tac x= f in allE, simp add:co2sobj.simps)
apply (rule conjI| rule impI|erule exE|erule conjE)+
apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "pa = p", simp add:co2sobj.simps)
apply (rule disjI2, rule notI, simp)
apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
apply (rule notI, simp add:co2sobj.simps split:option.splits)
apply (case_tac "f = a", simp add:alive_simps)
apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)
apply (erule bexE, erule conjE)
apply (erule_tac x = f'' in ballE, simp, simp)
apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI)
-apply (simp add:is_file_simps co2sobj_closefd tainted_eq_Tainted)
+apply (simp add:is_file_simps co2sobj_closefd)
apply (rule notI, simp add:co2sobj_closefd)
-apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps tainted_eq_Tainted)
+apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps)
apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (rule notI, simp add:co2sobj.simps split:option.splits)
@@ -1318,11 +1278,11 @@
apply (rule impI, rule conjI, rule impI)
apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "pa = p", simp add:co2sobj.simps)
apply (rule notI, simp)
apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
apply (erule_tac x = obj in allE, simp add:co2sobj_closefd)
apply (rule notI, simp add:co2sobj.simps split:option.splits)
apply (case_tac "f = a", simp add:alive_simps)
@@ -1331,10 +1291,10 @@
apply (simp add:co2sobj.simps)
apply (rule notI, simp add:co2sobj.simps)
apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (simp add:is_file_simps co2sobj_closefd tainted_eq_Tainted)
+apply (simp add:is_file_simps co2sobj_closefd)
apply (rule notI, simp add:co2sobj.simps)
-apply (rule notI, simp add:co2sobj_closefd tainted_eq_Tainted)
-apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps tainted_eq_Tainted)
+apply (rule notI, simp add:co2sobj_closefd)
+apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps)
apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (rule notI, simp add:co2sobj.simps split:option.splits)+
@@ -1346,23 +1306,23 @@
apply (rule notI, simp add:co2sobj.simps split:option.splits)+
apply (rule impI)
apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "pa = p", simp add:co2sobj.simps)
apply (rule disjI2, rule notI, simp)
apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
apply (erule_tac x = obj in allE, simp add:co2sobj_closefd)
apply (rule notI, simp add:co2sobj.simps split:option.splits)
apply (case_tac "f = a", simp add:alive_simps)
apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
apply (simp add:co2sobj_closefd split:if_splits option.splits t_sobject.splits)
-apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_Tainted tainted_eq_Tainted)
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
apply (erule bexE, erule conjE, erule_tac x = "f''" in ballE, simp, simp)
apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (simp add:is_file_simps co2sobj_closefd tainted_eq_Tainted)
+apply (simp add:is_file_simps co2sobj_closefd)
apply (rule notI, simp add:co2sobj.simps)
-apply (rule notI, simp add:co2sobj_closefd tainted_eq_Tainted)
-apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps tainted_eq_Tainted)
+apply (rule notI, simp add:co2sobj_closefd)
+apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps)
apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (rule notI, simp add:co2sobj.simps split:option.splits)+
@@ -1375,26 +1335,26 @@
apply (simp add:update_s2ss_sfile_del_def update_s2ss_obj_def split:if_splits)
apply (erule conjE, erule disjE)
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
apply (erule exE, erule conjE)
-apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_file a", simp add:co2sobj.simps)
apply (case_tac "obj = O_proc p")
apply (rule_tac x = obj' in exI, frule_tac obj = obj' in co2sobj_sproc_imp, erule exE)
apply (frule_tac obj = obj' in alive_co2sobj_closefd3, simp+)
apply (simp add:co2sobj_closefd)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
-apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
apply (erule conjE|erule exE|erule disjE)+
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
apply (erule conjE, erule exE, erule conjE)
-apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_file a", simp add:co2sobj.simps)
apply (case_tac "obj = O_proc p")
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
-apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
apply (erule conjE|erule exE|erule disjE)+
apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE)
apply (rule_tac x = "O_file f'" in exI)
@@ -1402,26 +1362,26 @@
apply (frule_tac obj = "O_file f'" in co2sobj_closefd)
apply (simp add:alive_simps)+
apply (frule_tac f = "f'" in is_file_has_sfile', simp, erule exE)
-apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits)
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted split:if_splits)
apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
apply (erule conjE, erule disjE)
apply (rule_tac x = "O_proc p" in exI)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (erule exE, erule conjE)
apply (case_tac "obj = O_proc p")
apply (rule_tac x = "obj'" in exI, simp, frule_tac obj = obj' in co2sobj_sproc_imp, erule exE)
apply (frule_tac obj = obj' in alive_co2sobj_closefd3, simp+)
-apply (simp add:co2sobj_closefd tainted_eq_Tainted)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
-apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj_closefd)
+apply (simp add:co2sobj.simps)
+apply (case_tac "obj = O_file a", simp add:co2sobj.simps)
apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
apply (erule_tac obj = obj in co2sobj_some_caseD)
apply (rule_tac x = obj in exI)
apply (simp add:co2sobj_closefd)
apply (case_tac "f = a", simp add:alive_simps)
apply (case_tac "f \<in> same_inode_files s a")
-apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
@@ -1433,20 +1393,20 @@
apply (frule_tac obj = "O_file f'" in co2sobj_closefd)
apply (simp add:alive_simps)+
apply (frule_tac f = "f'" in is_file_has_sfile', simp, erule exE)
-apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits)
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted split:if_splits)
apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
apply (erule conjE, erule disjE)
apply (rule_tac x = "O_proc p" in exI)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (erule conjE, erule exE, erule conjE)
-apply (case_tac "obj = O_proc p", simp add:co2sobj.simps tainted_eq_Tainted)
-apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_proc p", simp add:co2sobj.simps)
+apply (case_tac "obj = O_file a", simp add:co2sobj.simps)
apply (erule_tac obj = obj in co2sobj_some_caseD)
apply (rule_tac x = obj in exI)
apply (simp add:co2sobj_closefd)
apply (case_tac "f \<in> same_inode_files s a")
-apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_file_simps)
apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_dir_simps)
@@ -1459,40 +1419,40 @@
apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
apply (simp)
apply (case_tac "obj = O_proc p")
-apply (simp add:co2sobj.simps tainted_eq_Tainted split:if_splits)
+apply (simp add:co2sobj.simps split:if_splits)
apply (rule disjI2, rule_tac x = obj in exI, erule conjE)
apply (simp add:alive_co2sobj_closefd')
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp split:t_object.splits if_splits)
apply (simp, erule disjE)
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
apply (erule exE, erule conjE)
apply (case_tac "obj = O_proc p")
apply (rule_tac x = obj' in exI, simp add:alive_co2sobj_closefd1)
apply (frule_tac obj = obj' in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
-apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps)
+apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_tainted co2sobj.simps)
apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd1)
apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
-apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps)
+apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_tainted co2sobj.simps)
apply (rule impI)
apply (simp add:s2ss_def)
apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
apply (simp)
apply (case_tac "obj = O_proc p")
-apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted split:if_splits)
+apply (rule disjI1, simp add:co2sobj.simps split:if_splits)
apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp add:alive_co2sobj_closefd')
apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
-apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps)
+apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_tainted co2sobj.simps)
apply (rule notI, erule_tac x = obj in allE, simp add:alive_co2sobj_closefd')
apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
apply (clarsimp split:t_object.splits if_splits option.splits)
apply (simp)
apply (erule disjE)
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
apply (erule exE|erule conjE)+
apply (rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
apply (clarsimp split:t_object.splits if_splits option.splits
- simp:tainted_eq_Tainted co2sobj.simps alive_co2sobj_closefd1)
+ simp:tainted_eq_tainted co2sobj.simps alive_co2sobj_closefd1)
done
lemma alive_co2sobj_unlink:
@@ -1525,13 +1485,13 @@
apply (rule notI, simp, frule_tac obj = obj in co2sobj_sfile_imp, erule exE, simp)
apply (frule_tac obj = obj in co2sobj_unlink, simp)
apply (erule_tac x = fa in allE, simp add:is_file_simps)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_file f", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_file f", simp add:co2sobj.simps)
apply (frule_tac alive_co2sobj_unlink, simp, simp)
apply (frule_tac obj = obj in co2sobj_unlink, simp)
apply (rule_tac x = obj in exI)
-apply (simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps split:t_object.splits if_splits)
apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ defer
@@ -1545,7 +1505,7 @@
apply (case_tac "fa \<in> same_inode_files s f")
apply (rule disjI1)
apply (simp add:co2sobj_unlink)
-apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop split:if_splits)
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop split:if_splits)
apply (erule bexE, erule_tac x = f'' in ballE, simp, simp)
apply (rule disjI2, simp, rule_tac x = obj in exI)
apply (simp add:co2sobj_unlink is_file_simps)
@@ -1556,7 +1516,7 @@
apply (drule same_inode_files_prop10, simp, erule exE, erule conjE)
apply (rule_tac x = "O_file f'a" in exI, simp add:is_file_simps)
apply (frule_tac obj = "O_file f'a" in co2sobj_unlink, simp add:same_inode_files_prop11 is_file_simps)
-apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop
is_file_simps same_inode_files_prop11 split:if_splits)
apply (rule impI, erule bexE, erule_tac x = f'' in ballE, simp, simp)
apply (erule bexE, erule_tac x = f'' in ballE, simp, simp)
@@ -1566,13 +1526,13 @@
apply (case_tac "obj= O_file f")
apply (rule_tac x = "O_file f'" in exI, simp add:is_file_simps)
apply (frule_tac f' = f' in cf2sfiles_unlink, simp add:current_files_simps is_file_in_current)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (erule_tac obj = obj in co2sobj_some_caseD)
apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
apply (case_tac "fa \<in> same_inode_files s f")
apply (rule_tac x = "O_file f'" in exI)
apply (frule_tac f' = f' in cf2sfiles_unlink, simp add:current_files_simps is_file_in_current)
-apply (simp add:co2sobj.simps tainted_eq_Tainted is_file_simps cf2sfiles_prop same_inodes_Tainted)
+apply (simp add:co2sobj.simps is_file_simps cf2sfiles_prop same_inodes_tainted)
apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps)
apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
@@ -1591,12 +1551,12 @@
apply (case_tac "fa \<in> same_inode_files s f")
apply (rule disjI1)
apply (simp add:co2sobj_unlink)
-apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop split:if_splits)
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop split:if_splits)
apply (erule bexE, erule_tac x = f'' in ballE, simp, simp)
apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI)
apply (simp add:co2sobj_unlink is_file_simps)
-apply (rule notI, simp add:co2sobj_unlink tainted_eq_Tainted)
-apply (erule_tac x = fa in allE, simp add:co2sobj.simps is_file_simps tainted_eq_Tainted)
+apply (rule notI, simp add:co2sobj_unlink)
+apply (erule_tac x = fa in allE, simp add:co2sobj.simps is_file_simps)
apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink)
apply (rule notI, simp add:co2sobj.simps split:option.splits)
apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
@@ -1607,16 +1567,16 @@
apply (drule same_inode_files_prop10, simp, erule exE, erule conjE)
apply (rule_tac x = "O_file f'" in exI, simp add:is_file_simps)
apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp add:same_inode_files_prop11 is_file_simps)
-apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop
is_file_simps same_inode_files_prop11 split:if_splits)
apply (rule impI, erule bexE, erule_tac x = f'' in ballE, simp, simp)
apply (erule bexE, erule_tac x = f'' in ballE, simp, simp)
apply (tactic {*my_setiff_tac 1*}, simp)
-apply (case_tac "obj = O_file f", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_file f", simp add:co2sobj.simps)
apply (erule_tac obj = obj in co2sobj_some_caseD)
apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
apply (case_tac "fa \<in> same_inode_files s f")
-apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_Tainted tainted_eq_Tainted)
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps)
apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
@@ -1668,7 +1628,7 @@
apply (rule conjI, rule notI, simp add:same_inode_files_prop9)
apply (rule impI, frule_tac f' = f' in cf2sfiles_unlink)
apply (simp add:current_files_simps is_file_simps is_file_in_current)
-apply (simp add:tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
+apply (simp: same_inodes_tainted cf2sfiles_prop)
apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps)
apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
@@ -1687,7 +1647,7 @@
apply (frule same_inode_files_prop11, frule_tac f = f' in is_file_has_sfile', simp add:vd_cons, erule exE)
apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp)
apply (simp split:if_splits option.splits add:is_file_simps)
-apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_Tainted tainted_eq_Tainted)
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
apply (auto split:t_sobject.splits)[1]
apply (simp add:is_file_simps same_inode_files_prop11)
apply (erule_tac obj = obj in co2sobj_some_caseD)
@@ -1698,7 +1658,7 @@
apply (frule same_inode_files_prop11, frule_tac f = f' in is_file_has_sfile', simp add:vd_cons, erule exE)
apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp)
apply (simp split:if_splits option.splits add:is_file_simps)
-apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_Tainted tainted_eq_Tainted)
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
apply (auto split:t_sobject.splits)[1]
apply (simp add:is_file_simps same_inode_files_prop11)
apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps)
@@ -1783,97 +1743,9 @@
where
"update_s2ss_sfile s ss f sf \<equiv>
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))
- then ss \<union> {S_file (cf2sfiles s f \<union> {sf}) (O_file f \<in> Tainted s)}
- else ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)}
- \<union> {S_file (cf2sfiles s f \<union> {sf}) (O_file f \<in> Tainted s)}"
-
-lemma s2ss_linkhard: "valid (LinkHard p f f' # s) \<Longrightarrow> s2ss (LinkHard p f f' # s) = (
- case (cf2sfile (LinkHard p f f' # s) f') of
- Some sf \<Rightarrow> update_s2ss_sfile s (s2ss s) f sf
- | _ \<Rightarrow> {})"
-apply (frule vt_grant_os, frule vd_cons, clarsimp)
-apply (split option.splits)
-apply (rule conjI, rule impI, drule current_file_has_sfile', simp, simp add:current_files_simps)
-apply (rule allI, rule impI)
-
-apply (simp add:update_s2ss_sfile_def)
-apply (rule conjI, rule impI, erule exE, erule conjE, erule conjE)
-apply (simp add:s2ss_def)
-apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_file f'")
-apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted
- same_inode_files_linkhard split:if_splits)
-apply (case_tac "O_file f' \<in> Tainted s")
-apply (drule Tainted_in_current, simp, simp add:is_file_in_current alive.simps, simp)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (rule disjI2, simp, rule_tac x = obj in exI)
-apply (simp add:co2sobj_linkhard alive_linkhard)
-apply (case_tac "fa \<in> same_inode_files s f")
-apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted
- same_inodes_Tainted split:if_splits)
-apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_file_simps)
-apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard)
-apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_dir_simps)
-apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard)
-apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_file f" in exI)
-apply (frule_tac obj = "O_file f" in co2sobj_linkhard)
-apply (simp add:alive_linkhard)
-apply (simp add:alive_linkhard same_inode_files_prop9 split:t_object.splits)
-apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_file f'", simp add:alive_linkhard is_file_in_current)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
-apply (case_tac "fa \<in> same_inode_files s f")
-apply (rule_tac x = "O_file f'a" in exI, simp add:co2sobj_linkhard alive_linkhard)
-apply (rule conjI, rule impI, simp add:is_file_in_current)
-apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
-
-apply (rule impI)
-apply (simp add:s2ss_def)
-apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_file f'", simp)
-apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted
- same_inode_files_linkhard split:if_splits)
-apply (case_tac "O_file f' \<in> Tainted s")
-apply (drule Tainted_in_current, simp, simp add:is_file_in_current alive.simps, simp)
-apply (erule_tac obj = obj in co2sobj_some_caseD, simp)
-apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (simp add:co2sobj_linkhard alive_linkhard)
-apply (rule notI, simp add:co2sobj.simps split:option.splits)
-apply (case_tac "fa \<in> same_inode_files s f")
-apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted
- same_inodes_Tainted split:if_splits)
-apply (simp, rule disjI2, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_file_simps)
-apply (erule_tac x = fa in allE, rule notI)
-apply (simp add:co2sobj_linkhard is_file_simps)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
-apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard)
-apply (rule notI, simp add:co2sobj.simps split:option.splits)
-apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_dir_simps)
-apply (rule notI, simp add:co2sobj.simps split:option.splits)
-apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard)
-apply (rule notI, simp add:co2sobj.simps split:option.splits)
-apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_file f" in exI)
-apply (frule_tac obj = "O_file f" in co2sobj_linkhard)
-apply (simp add:alive_linkhard)
-apply (simp add:alive_linkhard same_inode_files_prop9 split:t_object.splits)
-apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_file f'", simp add:alive_linkhard is_file_in_current)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
-apply (case_tac "fa \<in> same_inode_files s f")
-apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
-done
+ then ss \<union> {S_file (cf2sfiles s f \<union> {sf}) (O_file f \<in> tainted s)}
+ else ss - {S_file (cf2sfiles s f) (O_file f \<in> tainted s)}
+ \<union> {S_file (cf2sfiles s f \<union> {sf}) (O_file f \<in> tainted s)}"
lemma same_inode_files_prop12:
"is_file s f \<Longrightarrow> f \<in> same_inode_files s f "
@@ -1889,7 +1761,7 @@
\<union> {S_file (cf2sfiles s f) True}"
lemma s2ss_truncate: "valid (Truncate p f len # s) \<Longrightarrow> s2ss (Truncate p f len # s) = (
- if (O_file f \<notin> Tainted s \<and> O_proc p \<in> Tainted s \<and> len > 0)
+ if (O_file f \<notin> tainted s \<and> O_proc p \<in> tainted s \<and> len > 0)
then update_s2ss_sfile_tainted s (s2ss s) f True
else s2ss s)"
apply (frule vt_grant_os, frule vd_cons, simp split:if_splits)
@@ -1900,11 +1772,11 @@
apply (simp add:s2ss_def)
apply (tactic {*my_seteq_tac 1*})
apply (case_tac "obj = O_file f")
-apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted same_inode_files_prop12 cf2sfiles_other)
+apply (rule disjI1, simp add:co2sobj.simps same_inode_files_prop12 cf2sfiles_other)
apply (erule_tac obj = obj in co2sobj_some_caseD)
apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps)
apply (case_tac "fa \<in> same_inode_files s f")
-apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other)
+apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_prop cf2sfiles_other)
apply (rule disjI2, simp, rule_tac x = obj in exI)
apply (simp add:co2sobj_truncate is_file_simps)
apply (rule disjI2, simp, rule_tac x = obj in exI)
@@ -1915,14 +1787,14 @@
apply (simp add:co2sobj_truncate)
apply (tactic {*my_setiff_tac 1*})
apply (rule_tac x = "O_file f" in exI)
-apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other same_inode_files_prop12)
+apply (simp add:co2sobj.simps is_file_simps cf2sfiles_other same_inode_files_prop12)
apply (tactic {*my_setiff_tac 1*})
apply (erule_tac obj = obj in co2sobj_some_caseD)
apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
apply (case_tac "fa \<in> same_inode_files s f")
apply (rule_tac x = "O_file f'" in exI)
apply (auto simp:co2sobj_truncate is_file_simps is_dir_simps split:t_object.splits)[1]
-apply (simp add:co2sobj.simps same_inodes_Tainted tainted_eq_Tainted cf2sfiles_prop)
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)
apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_file_simps)
apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_dir_simps)
@@ -1932,12 +1804,12 @@
apply (simp add:s2ss_def)
apply (tactic {*my_seteq_tac 1*})
apply (case_tac "obj = O_file f")
-apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted same_inode_files_prop12 cf2sfiles_other)
+apply (rule disjI1, simp add:co2sobj.simps same_inode_files_prop12 cf2sfiles_other)
apply (erule_tac obj = obj in co2sobj_some_caseD)
apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps)
apply (rule notI, simp add:co2sobj.simps split:option.splits)
apply (case_tac "fa \<in> same_inode_files s f")
-apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other)
+apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_prop cf2sfiles_other)
apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
apply (simp add:co2sobj_truncate is_file_simps)
apply (rule notI, simp add:co2sobj_truncate is_file_simps)
@@ -1954,12 +1826,12 @@
apply (rule notI, simp add:co2sobj.simps split:option.splits)
apply (tactic {*my_setiff_tac 1*})
apply (rule_tac x = "O_file f" in exI)
-apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other same_inode_files_prop12)
+apply (simp add:co2sobj.simps is_file_simps cf2sfiles_other same_inode_files_prop12)
apply (tactic {*my_setiff_tac 1*})
apply (erule_tac obj = obj in co2sobj_some_caseD)
apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
apply (case_tac "fa \<in> same_inode_files s f")
-apply (simp add:co2sobj.simps same_inodes_Tainted tainted_eq_Tainted cf2sfiles_prop)
+apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)
apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_file_simps)
apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_dir_simps)
@@ -1969,13 +1841,13 @@
apply (tactic {*my_seteq_tac 1*})
apply (rule_tac x = obj in exI)
apply (simp add:alive_simps co2sobj_truncate)
-apply (simp split:t_object.splits if_splits add:co2sobj.simps tainted_eq_Tainted)
-apply (case_tac "O_proc p \<in> Tainted s", simp add:same_inodes_Tainted)
+apply (simp split:t_object.splits if_splits add:co2sobj.simps)
+apply (case_tac "O_proc p \<in> tainted s", simp add:same_inodes_tainted)
apply simp
apply (tactic {*my_setiff_tac 1*})
apply (rule_tac x = obj in exI)
apply (simp add:alive_simps co2sobj_truncate)
-apply (auto split:t_object.splits if_splits simp:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)
+apply (auto split:t_object.splits if_splits simp:co2sobj.simps same_inodes_tainted)
done
lemma s2ss_createmsgq: "valid (CreateMsgq p q # s) \<Longrightarrow> s2ss (CreateMsgq p q # s) =
@@ -2116,17 +1988,17 @@
declare Product_Type.split_paired_Ex Product_Type.split_paired_All [simp del]
lemma s2ss_shm_no_bk_elim':
- "\<lbrakk>x \<notin> s2ss_shm_no_backup s pfrom; co2sobj s (O_proc p) = Some x; O_proc p \<notin> Tainted s;
+ "\<lbrakk>x \<notin> s2ss_shm_no_backup s pfrom; co2sobj s (O_proc p) = Some x; O_proc p \<notin> tainted s;
valid s; info_flow_shm s pfrom p\<rbrakk>
\<Longrightarrow> \<exists> p'. \<not> info_flow_shm s pfrom p' \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = Some x"
-apply (auto simp:s2ss_shm_no_backup_def co2sobj.simps tainted_eq_Tainted split:option.splits)
+apply (auto simp:s2ss_shm_no_backup_def co2sobj.simps split:option.splits)
apply (erule_tac x = p in allE, auto)
apply (rule_tac x = p' in exI, auto)
done
lemma s2ss_recvmsg: "valid (RecvMsg p q m # s) \<Longrightarrow> s2ss (RecvMsg p q m # s) = (
case (cq2smsgq s q, cq2smsgq (RecvMsg p q m # s) q) of
- (Some sq, Some sq') \<Rightarrow> if (O_msg q m \<in> Tainted s \<and> O_proc p \<notin> Tainted s)
+ (Some sq, Some sq') \<Rightarrow> if (O_msg q m \<in> tainted s \<and> O_proc p \<notin> tainted s)
then update_s2ss_obj s (update_s2ss_shm s p) (O_msgq q) (S_msgq sq) (S_msgq sq')
else update_s2ss_obj s (s2ss s) (O_msgq q) (S_msgq sq) (S_msgq sq')
| _ \<Rightarrow> {})"
@@ -2175,7 +2047,7 @@
split:t_object.splits if_splits option.splits)
apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1]
apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> Tainted s")
+apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> tainted s")
apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+)
apply (erule exE|erule conjE)+
apply (rule_tac x = "O_proc p'" in exI)
@@ -2184,7 +2056,7 @@
apply (case_tac "info_flow_shm s p pa", simp)
apply (frule_tac obj = obj in co2sobj_recvmsg, simp+)
apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps)
-apply (simp, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp, simp add:co2sobj.simps)
apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+)
apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps)
apply (rule_tac x = obj in exI)
@@ -2203,7 +2075,7 @@
apply (rule disjI1, simp add:co2sobj.simps)
apply (rule disjI2, simp, rule_tac x = obj in exI)
apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps split:t_object.splits if_splits option.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted)
+apply (simp add:co2sobj.simps info_flow_shm_tainted)
apply (simp add:co2sobj.simps)
apply (simp add:co2sobj.simps)
apply (case_tac "msgs_of_queue s q", simp, simp)
@@ -2219,7 +2091,7 @@
apply (rule_tac x = obj in exI)
apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg
split:t_object.splits if_splits option.splits)
-apply (auto simp:co2sobj.simps is_file_simps is_dir_simps tainted_eq_Tainted info_flow_shm_Tainted)[1]
+apply (auto simp:co2sobj.simps is_file_simps is_dir_simps info_flow_shm_tainted)[1]
apply (tactic {*my_clarify_tac 1*})
apply (tactic {*my_seteq_tac 1*})
@@ -2228,14 +2100,14 @@
apply (rule disjI2)
apply (erule_tac obj = obj in co2sobj_some_caseD)
apply (case_tac "info_flow_shm s p pa")
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
apply (rule DiffI, rule UnI1, simp)
apply (rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (erule s2ss_shm_no_bk_intro2, simp, simp)
apply (rule DiffI, rule UnI2, rule CollectI)
-apply (simp only:co2sobj.simps tainted_eq_Tainted split:option.splits, simp)
+apply (simp only:co2sobj.simps split:option.splits, simp)
apply (rule_tac x = ab in exI, simp)
apply (rule_tac x = pa in exI, simp add:cp2sproc_other)
apply (rule s2ss_shm_no_bk_intro2, simp, simp, simp)
@@ -2272,7 +2144,7 @@
split:t_object.splits if_splits option.splits)
apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1]
apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> Tainted s")
+apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> tainted s")
apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+)
apply (erule exE|erule conjE)+
apply (rule_tac x = "O_proc p'" in exI)
@@ -2281,7 +2153,7 @@
apply (case_tac "info_flow_shm s p pa", simp)
apply (frule_tac obj = obj in co2sobj_recvmsg, simp+)
apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps)
-apply (simp, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp, simp add:co2sobj.simps)
apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+)
apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps)
apply (rule_tac x = obj in exI)
@@ -2301,7 +2173,7 @@
apply (rule_tac x = obj in exI)
apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg
split:t_object.splits if_splits option.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted)
+apply (simp add:co2sobj.simps info_flow_shm_tainted)
apply (simp add:co2sobj_recvmsg)
apply (simp add:alive_recvmsg split:if_splits)
apply (erule_tac x = obj in allE, simp split:t_object.splits if_splits option.splits)
@@ -2322,7 +2194,7 @@
apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
apply (rule conjI)
apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
-apply (auto simp:co2sobj.simps tainted_eq_Tainted split:t_object.splits option.splits if_splits)[1]
+apply (auto simp:co2sobj.simps split:t_object.splits option.splits if_splits)[1]
apply (tactic {*my_clarify_tac 1*})
apply (tactic {*my_seteq_tac 1*})
@@ -2331,14 +2203,14 @@
apply (rule disjI2)
apply (erule_tac obj = obj in co2sobj_some_caseD)
apply (case_tac "info_flow_shm s p pa")
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
apply (rule DiffI, rule UnI1, simp)
apply (rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (erule s2ss_shm_no_bk_intro2, simp, simp)
apply (rule DiffI, rule UnI2, rule CollectI)
-apply (simp only:co2sobj.simps tainted_eq_Tainted split:option.splits, simp)
+apply (simp only:co2sobj.simps split:option.splits, simp)
apply (rule_tac x = ab in exI, simp)
apply (rule_tac x = pa in exI, simp add:cp2sproc_other)
apply (rule s2ss_shm_no_bk_intro2, simp, simp, simp)
@@ -2374,7 +2246,7 @@
split:t_object.splits if_splits option.splits)
apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1]
apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> Tainted s")
+apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> tainted s")
apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+)
apply (erule exE|erule conjE)+
apply (rule_tac x = "O_proc p'" in exI)
@@ -2383,7 +2255,7 @@
apply (case_tac "info_flow_shm s p pa", simp)
apply (frule_tac obj = obj in co2sobj_recvmsg, simp+)
apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps)
-apply (simp, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp, simp add:co2sobj.simps)
apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+)
apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps)
apply (rule_tac x = obj in exI)
@@ -2403,7 +2275,7 @@
apply (rule_tac x = obj in exI)
apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg
split:t_object.splits if_splits option.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted)
+apply (simp add:co2sobj.simps info_flow_shm_tainted)
apply (tactic {*my_setiff_tac 1*})
apply (rule_tac x = "O_msgq q" in exI)
apply (simp add:co2sobj.simps)
@@ -2418,7 +2290,7 @@
apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
apply (rule conjI)
apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
-apply (auto simp:co2sobj.simps tainted_eq_Tainted split:t_object.splits option.splits if_splits)[1]
+apply (auto simp:co2sobj.simps split:t_object.splits option.splits if_splits)[1]
apply (tactic {*my_clarify_tac 1*})
apply (tactic {*my_seteq_tac 1*})
@@ -2427,15 +2299,15 @@
apply (rule disjI2)
apply (erule_tac obj = obj in co2sobj_some_caseD)
apply (case_tac "info_flow_shm s p pa")
-apply (case_tac "O_proc pa \<in> Tainted s")
+apply (case_tac "O_proc pa \<in> tainted s")
apply (rule DiffI, rule DiffI, rule UnI1, simp)
apply (rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:co2sobj.simps)
apply (erule s2ss_shm_no_bk_intro2, simp, simp)
apply (simp, rule notI, simp add:co2sobj.simps split:option.splits)
apply (rule DiffI, rule DiffI, rule UnI2, rule CollectI)
-apply (simp only:co2sobj.simps tainted_eq_Tainted split:option.splits, simp)
+apply (simp only:co2sobj.simps split:option.splits, simp)
apply (rule_tac x = ab in exI, simp)
apply (rule_tac x = pa in exI, simp add:cp2sproc_other)
apply (rule s2ss_shm_no_bk_intro2, simp, simp, simp)
@@ -2475,7 +2347,7 @@
apply (case_tac "obj = O_msgq q")
apply (simp add:co2sobj.simps)
apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> Tainted s")
+apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> tainted s")
apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+)
apply (erule exE|erule conjE)+
apply (rule_tac x = "O_proc p'" in exI)
@@ -2484,7 +2356,7 @@
apply (case_tac "info_flow_shm s p pa", simp)
apply (frule_tac obj = obj in co2sobj_recvmsg, simp+)
apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps)
-apply (simp, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp, simp add:co2sobj.simps)
apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+)
apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps)
apply (rule_tac x = obj in exI)
@@ -2504,7 +2376,7 @@
apply (rule_tac x = obj in exI)
apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg
split:t_object.splits if_splits option.splits)
-apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted)
+apply (simp add:co2sobj.simps info_flow_shm_tainted)
apply (rule notI, simp)
apply (frule co2sobj_smsgq_imp, erule exE, simp)
apply (simp add:co2sobj_recvmsg)
@@ -2521,7 +2393,7 @@
apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
apply (rule conjI)
apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
-apply (auto simp:co2sobj.simps tainted_eq_Tainted intro: info_flow_shm_Tainted
+apply (auto simp:co2sobj.simps intro: info_flow_shm_tainted
split:t_object.splits option.splits if_splits)[1]
done