Mercurial Mercurial > hg > selinux / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
S2ss_prop.thy
changeset 48 bf8c09ec1186
parent 47 0960686df575
child 49 68649272054c
equal deleted inserted replaced
47:0960686df575 48:bf8c09ec1186 
   786   "del_s2ss_file s ss f sf = 
   786   "del_s2ss_file s ss f sf = 
   787      (if (\<exists> f' \<in> same_inode_files s f. f' \<noteq> f \<and> cf2sfile s f' = Some sf)
 
   787      (if (\<exists> f' \<in> same_inode_files s f. f' \<noteq> f \<and> cf2sfile s f' = Some sf)
 
   788       then ss
 
   788       then ss
 
   789       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))
 
   789       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))
 
   790            then update_s2ss_sfile s ss f sf
 
   790            then update_s2ss_sfile s ss f sf
 
   791            else update_s2ss_sfile s (ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)}) f sf"
 
   791            else update_s2ss_sfile s (ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)}) f sf)"
 
   792 
   792 
   793 lemma alive_co2sobj_closefd1:
 
   793 lemma alive_co2sobj_closefd1:
 
   794   "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; 
   794   "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; 
   795     file_of_proc_fd s p fd = Some f; \<not> (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})\<rbrakk>
 
   795     file_of_proc_fd s p fd = Some f; \<not> (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})\<rbrakk>
 
   796    \<Longrightarrow> alive (CloseFd p fd # s) obj"
 
   796    \<Longrightarrow> alive (CloseFd p fd # s) obj"
 
   859 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
 
   859 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
 
   860 
   860 
   861 lemma co2sobj_smsgq_imp:
 
   861 lemma co2sobj_smsgq_imp:
 
   862   "co2sobj s obj = Some (S_msgq sq) \<Longrightarrow> \<exists> q. obj = O_msgq q"
 
   862   "co2sobj s obj = Some (S_msgq sq) \<Longrightarrow> \<exists> q. obj = O_msgq q"
 
   863 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
 
   863 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
 
       
   864 
       
   865 lemma same_inode_files_prop10:
 
       
   866   "\<lbrakk>same_inode_files s f \<noteq> {f}; is_file s f\<rbrakk> \<Longrightarrow> \<exists> f'. f' \<in> same_inode_files s f \<and> f' \<noteq> f"
 
       
   867 by (auto simp:same_inode_files_def split:if_splits)
 
       
   868 
       
   869 lemma same_inode_files_prop11:
 
       
   870   "f \<in> same_inode_files s f' \<Longrightarrow> is_file s f"
 
       
   871 by (auto simp:same_inode_files_def is_file_def split:if_splits)
 
       
   872 
       
   873 lemma same_inode_files_prop11':
 
       
   874   "f \<in> same_inode_files s f' \<Longrightarrow> is_file s f'"
 
       
   875 by (auto simp:same_inode_files_def is_file_def split:if_splits)
 
   864 
   876 
   865 lemma s2ss_closefd:
 
   877 lemma s2ss_closefd:
 
   866   "valid (CloseFd p fd # s) \<Longrightarrow> s2ss (CloseFd p fd # s) = (
 
   878   "valid (CloseFd p fd # s) \<Longrightarrow> s2ss (CloseFd p fd # s) = (
 
   867      case (file_of_proc_fd s p fd) of
 
   879      case (file_of_proc_fd s p fd) of
 
   868        Some f \<Rightarrow> if (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})
 
   880        Some f \<Rightarrow> if (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})
 
   960 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
 
   972 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
 
   961 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
   973 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
   962 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
   974 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
   963 
   975 
   964 apply (rule impI, tactic {*my_seteq_tac 1*})
 
   976 apply (rule impI, tactic {*my_seteq_tac 1*})
 
   965 apply (simp add:update_s2ss_obj_def)
 
   977 apply (simp add:update_s2ss_obj_def update_s2ss_sfile_def)
 
   966 apply (rule conjI, rule impI, (erule exE|erule conjE)+)
 
   978 apply (rule conjI| rule impI|erule exE|erule conjE)+
 
       
   979 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
       
   980 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
 
       
   981 apply (rule disjI2, rule_tac x = obj in exI)
 
       
   982 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
   983 apply (case_tac "f = a", simp add:alive_simps)
 
       
   984 apply (rule disjI2, rule_tac x = obj in exI)
 
       
   985 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
   986 apply (rule disjI2, rule_tac x = obj in exI)
 
       
   987 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
   988 apply (rule disjI2, rule_tac x = obj in exI)
 
       
   989 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
   990 apply (rule disjI2, rule_tac x = obj in exI)
 
       
   991 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
   992 apply (rule conjI| rule impI|erule exE|erule conjE)+
 
   967 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
   993 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
   968 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
 
   994 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
 
   969 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
 
   995 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
 
   970 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
   996 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
   971 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
   997 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
   981 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
  1007 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
   982 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
 
  1008 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
 
   983 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
  1009 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
   984 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
 
  1010 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
 
   985 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
  1011 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1012 apply (rule impI, rule conjI, rule impI)
 
       
  1013 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
       
  1014 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1015 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
 
       
  1016 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1017 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_file_simps)
 
       
  1018 apply (case_tac "f = a", simp add:alive_simps)
 
       
  1019 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
 
       
  1020 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1021 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_file_simps)
 
       
  1022 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
 
       
  1023 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1024 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
 
       
  1025 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
 
       
  1026 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1027 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_dir_simps)
 
       
  1028 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
 
       
  1029 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1030 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
 
   986 apply (rule impI)
 
  1031 apply (rule impI)
 
   987 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
  1032 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
   988 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
 
  1033 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
 
   989 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
 
  1034 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
 
   990 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
  1035 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
  1007 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
  1052 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
  1008 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_dir_simps)
 
  1053 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_dir_simps)
 
  1009 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
 
  1054 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
 
  1010 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
  1055 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
  1011 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
 
  1056 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
 
  1012 apply (tactic {*my_setiff_tac 1*})
 
  1057 
  1013 
  1058 apply (simp add:update_s2ss_sfile_def update_s2ss_obj_def split:if_splits)
 
  1014 
  1059 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
 
  1015 
  1060 apply (erule exE, erule conjE)
 
       
  1061 apply (case_tac "obj = O_proc p")
 
       
  1062 apply (rule_tac x = obj' in exI)
 
       
  1063 apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
 
       
  1064 apply (simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1065 apply (case_tac "obj = O_file a")
 
       
  1066 apply (rule_tac x = "O_file f'" in exI)
 
       
  1067 apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
 
       
  1068 apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
 
       
  1069 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
 
       
  1070 apply (rule_tac x = obj in exI)
 
       
  1071 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
 
       
  1072 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
       
  1073 apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
       
  1074 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1075 apply (erule conjE, erule exE, erule conjE)
 
       
  1076 apply (case_tac "obj = O_proc p")
 
       
  1077 apply (simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1078 apply (case_tac "obj = O_file a")
 
       
  1079 apply (rule_tac x = "O_file f'" in exI)
 
       
  1080 apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
 
       
  1081 apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
 
       
  1082 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
 
       
  1083 apply (rule_tac x = obj in exI)
 
       
  1084 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
 
       
  1085 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
       
  1086 apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
       
  1087 apply (erule disjE)
 
       
  1088 apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE)
 
       
  1089 apply (rule_tac x = "O_file f'a" in exI)
 
       
  1090 apply (frule same_inode_files_prop11)
 
       
  1091 apply (frule_tac obj = "O_file f'a" in co2sobj_closefd)
 
       
  1092 apply (simp add:alive_simps)+
 
       
  1093 apply (frule_tac f = "f'a" in is_file_has_sfile', simp, erule exE)
 
       
  1094 apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits)
 
       
  1095 apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
 
       
  1096 apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
 
       
  1097 apply (erule disjE)
 
       
  1098 apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1099 apply (erule exE, erule conjE)
 
       
  1100 apply (case_tac "obj = O_proc p")
 
       
  1101 apply (rule_tac x = obj' in exI)
 
       
  1102 apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
 
       
  1103 apply (simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1104 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
       
  1105 apply (rule_tac x = obj in exI)
 
       
  1106 apply (simp add:co2sobj_closefd)
 
       
  1107 apply (case_tac "f \<in> same_inode_files s a")
 
       
  1108 apply (rule_tac x = "O_file f'" in exI)
 
       
  1109 apply (simp add:co2sobj_simps is_file_simps split:if_splits option.splits t_sobject.splits)
 
       
  1110 apply (rule conjI, rule notI, simp add:same_inode_files_prop9)
 
       
  1111 apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)
 
       
  1112 apply (rule_tac x = obj in exI)
 
       
  1113 apply (simp add:co2sobj_closefd is_file_simps)
 
       
  1114 apply (rule notI, simp add:same_inode_files_prop9)
 
       
  1115 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
 
       
  1116 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_dir_simps)
 
       
  1117 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
 
       
  1118 
       
  1119 apply (erule disjE)
 
       
  1120 apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE)
 
       
  1121 apply (rule_tac x = "O_file f'a" in exI)
 
       
  1122 apply (frule same_inode_files_prop11)
 
       
  1123 apply (frule_tac obj = "O_file f'a" in co2sobj_closefd)
 
       
  1124 apply (simp add:alive_simps)+
 
       
  1125 apply (frule_tac f = "f'a" in is_file_has_sfile', simp, erule exE)
 
       
  1126 apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits)
 
       
  1127 apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
 
       
  1128 apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
 
       
  1129 apply (erule disjE)
 
       
  1130 apply (rule_tac x = "O_proc p" in exI)
 
       
  1131 apply (simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1132 apply (erule conjE, erule exE, erule conjE)
 
       
  1133 apply (case_tac "obj = O_proc p")
 
       
  1134 apply (simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1135 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
       
  1136 apply (rule_tac x = obj in exI)
 
       
  1137 apply (simp add:co2sobj_closefd)
 
       
  1138 apply (case_tac "f \<in> same_inode_files s a")
 
       
  1139 apply (rule_tac x = "O_file f'" in exI)
 
       
  1140 apply (simp add:co2sobj_simps is_file_simps split:if_splits option.splits t_sobject.splits)
 
       
  1141 apply (rule conjI, rule notI, simp add:same_inode_files_prop9)
 
       
  1142 apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)
 
       
  1143 apply (rule_tac x = obj in exI)
 
       
  1144 apply (simp add:co2sobj_closefd is_file_simps)
 
       
  1145 apply (rule notI, simp add:same_inode_files_prop9)
 
       
  1146 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
 
       
  1147 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_dir_simps)
 
       
  1148 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
 
       
  1149 
       
  1150 apply (rule impI, rule conjI, rule impI)
 
       
  1151 apply (tactic {*my_seteq_tac 1*})
 
       
  1152 apply (simp add:update_s2ss_obj_def update_s2ss_sfile_def)
 
       
  1153 apply (rule conjI| rule impI|erule exE|erule conjE)+
 
       
  1154 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
       
  1155 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1156 apply (rule disjI2, rule_tac x = obj in exI)
 
       
  1157 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1158 apply (case_tac "f = a", simp add:alive_simps)
 
       
  1159 apply (rule disjI2, rule_tac x = obj in exI)
 
       
  1160 apply (frule_tac obj = obj in co2sobj_closefd, simp, clarsimp simp:alive_simps split:if_splits)
 
       
  1161 apply (rule disjI2, rule_tac x = obj in exI)
 
       
  1162 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1163 apply (rule disjI2, rule_tac x = obj in exI)
 
       
  1164 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1165 apply (rule disjI2, rule_tac x = obj in exI)
 
       
  1166 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1167 apply (rule conjI| rule impI|erule exE|erule conjE)+
 
       
  1168 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
       
  1169 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1170 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
 
       
  1171 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
       
  1172 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
       
  1173 apply (rule notI, simp, erule_tac x = "O_proc pa" in allE, simp add:co2sobj_closefd)
 
       
  1174 apply (case_tac "f = a", simp add:alive_simps)
 
       
  1175 apply (case_tac "f \<in> same_inode_files s a", rule disjI2)
 
       
  1176 apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
 
       
  1177 apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
 
       
  1178 apply (erule bexE, erule conjE)
 
       
  1179 apply (rule conjI, rule_tac x = "O_file f''" in exI)
 
       
  1180 apply (simp add:same_inode_files_prop11 co2sobj.simps tainted_eq_Tainted cf2sfiles_prop same_inodes_Tainted)
 
       
  1181 apply (rule notI, simp)
 
       
  1182 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
 
       
  1183 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1184 apply (rule notI, simp add:co2sobj.simps)
 
       
  1185 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
 
       
  1186 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1187 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 
       
  1188 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
 
       
  1189 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1190 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 
       
  1191 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
 
       
  1192 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1193 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 
       
  1194 
       
  1195 apply (erule bexE, erule conjE)
 
       
  1196 apply (simp add:update_s2ss_obj_def split:if_splits)
 
       
  1197 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1198 apply (erule exE, erule conjE)
 
       
  1199 apply (case_tac "obj = O_proc p")
 
       
  1200 apply (rule_tac x = obj' in exI)
 
       
  1201 apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
 
       
  1202 apply (simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1203 apply (case_tac "obj = O_file a")
 
       
  1204 apply (rule_tac x = "O_file f'" in exI)
 
       
  1205 apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11)
 
       
  1206 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
 
       
  1207 apply (rule conjI)
 
       
  1208 apply (rule impI)
 
       
  1209 apply (rule_tac x = f' in ballE, simp, simp, simp)
 
       
  1210 apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted)
 
       
  1211 apply (rule_tac x = obj in exI)
 
       
  1212 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
 
       
  1213 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
       
  1214 apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
       
  1215 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1216 apply (erule conjE, erule exE, erule conjE)
 
       
  1217 apply (case_tac "obj = O_proc p")
 
       
  1218 apply (simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1219 apply (case_tac "obj = O_file a")
 
       
  1220 apply (rule_tac x = "O_file f'" in exI)
 
       
  1221 apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11)
 
       
  1222 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
 
       
  1223 apply (rule conjI)
 
       
  1224 apply (rule impI)
 
       
  1225 apply (rule_tac x = f' in ballE, simp, simp, simp)
 
       
  1226 apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted)
 
       
  1227 apply (rule_tac x = obj in exI)
 
       
  1228 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
 
       
  1229 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
       
  1230 apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
       
  1231 
       
  1232 apply (rule impI)
 
       
  1233 apply (tactic {*my_seteq_tac 1*})
 
       
  1234 apply (simp add:update_s2ss_obj_def update_s2ss_sfile_def)
 
       
  1235 apply (rule conjI| rule impI|erule exE|erule conjE)+
 
       
  1236 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
       
  1237 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1238 apply (rule disjI2, rule_tac x = obj in exI)
 
       
  1239 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1240 apply (case_tac "f = a", simp add:alive_simps)
 
       
  1241 apply (rule disjI2, rule_tac x = obj in exI)
 
       
  1242 apply (frule_tac obj = obj in co2sobj_closefd, simp, clarsimp simp:alive_simps split:if_splits)
 
       
  1243 apply (rule disjI2, rule_tac x = obj in exI)
 
       
  1244 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1245 apply (rule disjI2, rule_tac x = obj in exI)
 
       
  1246 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1247 apply (rule disjI2, rule_tac x = obj in exI)
 
       
  1248 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1249 apply (frule_tac obj = obj in co2sobj_closefd, simp, rule notI, simp)
 
       
  1250 apply (frule_tac obj = obj in co2sobj_sfile_imp, erule exE, simp add:is_file_simps split:if_splits)
 
       
  1251 apply (erule_tac x= f in allE, simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1252 apply (rule conjI| rule impI|erule exE|erule conjE)+
 
       
  1253 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
       
  1254 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1255 apply (rule disjI2, rule notI, simp)
 
       
  1256 apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI)
 
       
  1257 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
       
  1258 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
       
  1259 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 
       
  1260 apply (case_tac "f = a", simp add:alive_simps)
 
       
  1261 apply (case_tac "f \<in> same_inode_files s a", rule disjI2)
 
       
  1262 apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
 
       
  1263 apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
 
       
  1264 
       
  1265 
       
  1266 apply (erule bexE, erule conjE)
 
       
  1267 apply (rule conjI, rule_tac x = "O_file f''" in exI)
 
       
  1268 apply (simp add:same_inode_files_prop11 co2sobj.simps tainted_eq_Tainted cf2sfiles_prop same_inodes_Tainted)
 
       
  1269 apply (rule notI, simp)
 
       
  1270 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
 
       
  1271 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1272 apply (rule notI, simp add:co2sobj.simps)
 
       
  1273 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
 
       
  1274 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1275 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 
       
  1276 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
 
       
  1277 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1278 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 
       
  1279 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
 
       
  1280 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
       
  1281 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 
       
  1282 
       
  1283 apply (erule bexE, erule conjE)
 
       
  1284 apply (simp add:update_s2ss_obj_def split:if_splits)
 
       
  1285 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1286 apply (erule exE, erule conjE)
 
       
  1287 apply (case_tac "obj = O_proc p")
 
       
  1288 apply (rule_tac x = obj' in exI)
 
       
  1289 apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
 
       
  1290 apply (simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1291 apply (case_tac "obj = O_file a")
 
       
  1292 apply (rule_tac x = "O_file f'" in exI)
 
       
  1293 apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11)
 
       
  1294 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
 
       
  1295 apply (rule conjI)
 
       
  1296 apply (rule impI)
 
       
  1297 apply (rule_tac x = f' in ballE, simp, simp, simp)
 
       
  1298 apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted)
 
       
  1299 apply (rule_tac x = obj in exI)
 
       
  1300 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
 
       
  1301 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
       
  1302 apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
       
  1303 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1304 apply (erule conjE, erule exE, erule conjE)
 
       
  1305 apply (case_tac "obj = O_proc p")
 
       
  1306 apply (simp add:co2sobj.simps tainted_eq_Tainted)
 
       
  1307 apply (case_tac "obj = O_file a")
 
       
  1308 apply (rule_tac x = "O_file f'" in exI)
 
       
  1309 apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11)
 
       
  1310 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
 
       
  1311 apply (rule conjI)
 
       
  1312 apply (rule impI)
 
       
  1313 apply (rule_tac x = f' in ballE, simp, simp, simp)
 
       
  1314 apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted)
 
       
  1315 apply (rule_tac x = obj in exI)
 
       
  1316 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
 
       
  1317 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
       
  1318 apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
       
  1319 
       
  1320 
       
  1321 
       
  1322 
       
  1323 
       
  1324 apply 
  1016 
  1325 
  1017 defer
 
  1326 defer
 
  1018 apply (rule impI)
 
  1327 apply (rule impI)
 
  1019 apply (simp add:update_s2ss_obj_def)
 
  1328 apply (simp add:update_s2ss_obj_def)
 
  1020 apply (rule conjI, rule impI, erule exE, erule conjE)
 
  1329 apply (rule conjI, rule impI, erule exE, erule conjE)
selinux