1042 case (Shutdown p fd how) |
1038 case (Shutdown p fd how) |
1043 show ?thesis using grant |
1039 show ?thesis using grant |
1044 by (simp add:Shutdown) |
1040 by (simp add:Shutdown) |
1045 qed |
1041 qed |
1046 |
1042 |
1047 |
1043 lemma not_all_procs_prop2: |
1048 |
1044 "p' \<notin> all_procs s \<Longrightarrow> p' \<notin> init_procs" |
1049 |
1045 apply (induct s, simp) |
1050 |
1046 by (case_tac a, auto) |
1051 |
1047 |
1052 |
1048 lemma not_all_procs_prop3: |
1053 |
1049 "p' \<notin> all_procs s \<Longrightarrow> p' \<notin> current_procs s" |
1054 |
1050 apply (induct s, simp) |
1055 |
1051 by (case_tac a, auto) |
1056 |
1052 |
1057 |
1053 definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool" |
1058 |
1054 where |
1059 |
1055 "is_created_proc s p \<equiv> p \<in> current_procs s \<and> (p \<in> init_procs \<longrightarrow> died (O_proc p) s)" |
1060 |
1056 |
1061 lemma enrich_proc_prop: |
1057 lemma created_proc_clone: |
1062 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> |
1058 "valid (Clone p p' fds # s) \<Longrightarrow> |
1063 \<Longrightarrow> valid (enrich_proc s p p') \<and> |
1059 is_created_proc (Clone p p' fds # s) tp = (if (tp = p') then True else is_created_proc s tp)" |
|
1060 apply (drule vt_grant_os) |
|
1061 apply (auto simp:is_created_proc_def dest:not_all_procs_prop2) |
|
1062 using not_died_init_proc |
|
1063 by auto |
|
1064 |
|
1065 lemma created_proc_exit: |
|
1066 "is_created_proc (Exit p # s) tp = (if (tp = p) then False else is_created_proc s tp)" |
|
1067 by (simp add:is_created_proc_def) |
|
1068 |
|
1069 lemma created_proc_kill: |
|
1070 "is_created_proc (Kill p p' # s) tp = (if (tp = p') then False else is_created_proc s tp)" |
|
1071 by (simp add:is_created_proc_def) |
|
1072 |
|
1073 lemma created_proc_other: |
|
1074 "\<lbrakk>\<And> p p' fds. e \<noteq> Clone p p' fds; |
|
1075 \<And> p. e \<noteq> Exit p; |
|
1076 \<And> p p'. e \<noteq> Kill p p'\<rbrakk> \<Longrightarrow> is_created_proc (e # s) tp = is_created_proc s tp" |
|
1077 by (case_tac e, auto simp:is_created_proc_def) |
|
1078 |
|
1079 lemmas is_created_proc_simps = created_proc_clone created_proc_exit created_proc_kill created_proc_other |
|
1080 (* |
|
1081 |
|
1082 |
|
1083 |
|
1084 |
1064 (p \<in> current_procs s \<longrightarrow> co2sobj (enrich_proc s p p') (O_proc p') = co2sobj (enrich_proc s p p') (O_proc p)) \<and> |
1085 (p \<in> current_procs s \<longrightarrow> co2sobj (enrich_proc s p p') (O_proc p') = co2sobj (enrich_proc s p p') (O_proc p)) \<and> |
1065 (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and> |
1086 (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and> |
1066 (\<forall> p'. p' \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and> |
1087 (\<forall> p'. p' \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and> |
1067 (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and> |
1088 (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and> |
1068 (Tainted (enrich_proc s p p') = (Tainted s \<union> (if (O_proc p \<in> Tainted s) then {O_proc p'} else {})))" |
1089 (Tainted (enrich_proc s p p') = (Tainted s \<union> (if (O_proc p \<in> Tainted s) then {O_proc p'} else {})))"*) |
|
1090 |
|
1091 lemma enrich_proc_dup_in: |
|
1092 "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk> |
|
1093 \<Longrightarrow> p' \<in> current_procs (enrich_proc s p p')" |
|
1094 apply (induct s, simp add:is_created_proc_def) |
|
1095 apply (frule vt_grant_os, frule vd_cons) |
|
1096 apply (case_tac a, auto simp:is_created_proc_def dest:not_all_procs_prop3) |
|
1097 done |
|
1098 |
|
1099 lemma enrich_proc_dup_ffd: |
|
1100 "\<lbrakk>file_of_proc_fd s p fd = Some f; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk> |
|
1101 \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') p' fd = Some f" |
|
1102 apply (induct s, simp add:is_created_proc_def) |
|
1103 apply (frule vt_grant_os, frule vd_cons) |
|
1104 apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def |
|
1105 dest:not_all_procs_prop3 split:if_splits option.splits) |
|
1106 done |
|
1107 |
|
1108 lemma current_fflag_in_fds: |
|
1109 "\<lbrakk>flags_of_proc_fd s p fd = Some flag; valid s\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds s p" |
|
1110 apply (induct s arbitrary:p) |
|
1111 apply (simp add:flags_of_proc_fd.simps file_of_proc_fd.simps init_oflags_prop2) |
|
1112 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
1113 apply (auto split:if_splits option.splits dest:proc_fd_in_fds) |
|
1114 apply (auto simp:proc_file_fds_def) |
|
1115 sorry |
|
1116 |
|
1117 |
|
1118 lemma current_fflag_has_ffd: |
|
1119 "\<lbrakk>flags_of_proc_fd s p fd = Some flag; valid s\<rbrakk> \<Longrightarrow> \<exists> f. file_of_proc_fd s p fd = Some f" |
|
1120 apply (induct s arbitrary:p) |
|
1121 apply (simp add: file_of_proc_fd.simps init_fileflag_valid) |
|
1122 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
1123 apply (auto split:if_splits option.splits dest:proc_fd_in_fds) |
|
1124 apply (auto simp:proc_file_fds_def) |
|
1125 sorry |
|
1126 |
|
1127 lemma enrich_proc_dup_fflags: |
|
1128 "\<lbrakk>flags_of_proc_fd s p fd = Some f; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk> |
|
1129 \<Longrightarrow> flags_of_proc_fd (enrich_proc s p p') p' fd = Some f" |
|
1130 apply (induct s, simp add:is_created_proc_def) |
|
1131 apply (frule vt_grant_os, frule vd_cons) |
|
1132 apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def |
|
1133 dest:not_all_procs_prop3 split:if_splits option.splits) |
|
1134 sorry |
|
1135 |
|
1136 lemma enrich_proc_prop: |
|
1137 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> |
|
1138 \<Longrightarrow> valid (enrich_proc s p p') \<and> |
|
1139 (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and> |
|
1140 (\<forall> obj. enrich_not_alive s obj \<longrightarrow> enrich_not_alive (enrich_proc s p p') obj) \<and> |
|
1141 (files_hung_by_del (enrich_proc s p p') = files_hung_by_del s) \<and> |
|
1142 (\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp) \<and> |
|
1143 (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and> |
|
1144 (\<forall> q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q) \<and> |
|
1145 (\<forall> tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> file_of_proc_fd (enrich_proc s p p') tp fd = Some f) \<and> |
|
1146 (\<forall> tp fd flags. flags_of_proc_fd s tp fd = Some flags \<longrightarrow> |
|
1147 flags_of_proc_fd (enrich_proc s p p') tp fd = Some flags) \<and> |
|
1148 (\<forall> q. msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q) \<and> |
|
1149 (\<forall> tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd) \<and> |
|
1150 (cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and> |
|
1151 (\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd)" |
1069 proof (induct s) |
1152 proof (induct s) |
1070 case Nil |
1153 case Nil |
1071 thus ?case by (auto simp:is_created_proc_def) |
1154 thus ?case by (auto simp:is_created_proc_def) |
1072 next |
1155 next |
1073 case (Cons e s) |
1156 case (Cons e s) |
1074 hence p1: "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> |
1157 hence vd_cons: "valid (e # s)" and created_cons: "is_created_proc (e # s) p" |
1075 \<Longrightarrow> valid (enrich_proc s p p') \<and> |
1158 and all_procs_cons: "p' \<notin> all_procs (e # s)" and vd: "valid s" |
1076 (p \<in> current_procs s \<longrightarrow> co2sobj (enrich_proc s p p') (O_proc p') = co2sobj (enrich_proc s p p') (O_proc p)) \<and> |
1159 and os: "os_grant s e" and grant: "grant s e" |
1077 (alive s obj \<longrightarrow> alive (enrich_proc s p p') obj \<and> co2sobj (enrich_proc s p p') obj = co2sobj s obj)" |
1160 by (auto dest:vd_cons vt_grant_os vt_grant) |
1078 and p2: "valid (e # s)" and p3: "is_created_proc (e # s) p" and p4: "p' \<notin> all_procs (e # s)" |
1161 from all_procs_cons have all_procs: "p' \<notin> all_procs s" by (case_tac e, auto) |
|
1162 from Cons have pre: "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p') \<and> |
|
1163 (\<forall>obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and> |
|
1164 (\<forall>obj. enrich_not_alive s obj \<longrightarrow> enrich_not_alive (enrich_proc s p p') obj) \<and> |
|
1165 files_hung_by_del (enrich_proc s p p') = files_hung_by_del s \<and> |
|
1166 (\<forall>tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp) \<and> |
|
1167 (\<forall>f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and> |
|
1168 (\<forall>q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q) \<and> |
|
1169 (\<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> file_of_proc_fd (enrich_proc s p p') tp fd = Some f) \<and> |
|
1170 (\<forall>tp fd flags. |
|
1171 flags_of_proc_fd s tp fd = Some flags \<longrightarrow> flags_of_proc_fd (enrich_proc s p p') tp fd = Some flags) \<and> |
|
1172 (\<forall>q. msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q) \<and> |
|
1173 (\<forall>tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd)" |
|
1174 using vd all_procs by auto |
|
1175 have "valid (enrich_proc (e # s) p p')" |
|
1176 proof- |
|
1177 from pre have pre': "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p')" by simp |
|
1178 have "is_created_proc s p \<Longrightarrow> valid (e # enrich_proc s p p')" |
|
1179 apply (frule pre') |
|
1180 apply (erule_tac s = s in enrich_valid_intro_cons) |
|
1181 apply (simp_all add:os grant vd pre) |
|
1182 done |
|
1183 moreover have "\<And>f fds. \<lbrakk>valid (Execve p f fds # enrich_proc s p p'); is_created_proc s p\<rbrakk> |
|
1184 \<Longrightarrow> valid (Execve p' f (fds \<inter> proc_file_fds s p) # Execve p f fds # enrich_proc s p p')" |
|
1185 apply (frule vt_grant_os, frule vt_grant) |
|
1186 apply (rule valid.intros(2)) |
|
1187 apply (simp_all split:option.splits add:sectxt_of_obj_simps is_file_simps) |
|
1188 apply (auto simp add:proc_file_fds_def)[1] |
|
1189 |
|
1190 sorry |
|
1191 moreover have "\<And>tp fds. \<lbrakk>valid (Clone tp p fds # s); p' \<noteq> p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> |
|
1192 valid (Clone tp p' (fds \<inter> proc_file_fds s tp) # Clone tp p fds # s)" |
|
1193 apply (frule vt_grant_os, frule vt_grant, drule not_all_procs_prop3) |
|
1194 apply (rule valid.intros(2)) |
|
1195 apply (simp_all split:option.splits add:sectxt_of_obj_simps) |
|
1196 apply (auto simp add:proc_file_fds_def)[1] |
|
1197 apply (auto simp:inherit_fds_check_def sectxt_of_obj_simps sectxts_of_fds_def inherit_fds_check_ctxt_def) |
|
1198 done |
|
1199 moreover have "\<And>f flags fd inum. |
|
1200 \<lbrakk>valid (Open p f flags fd inum # enrich_proc s p p'); is_created_proc s p\<rbrakk> |
|
1201 \<Longrightarrow> valid (Open p' f (remove_create_flag flags) fd inum # Open p f flags fd inum # enrich_proc s p p')" |
|
1202 sorry |
|
1203 moreover have "\<And>fd. \<lbrakk>valid (CloseFd p fd # enrich_proc s p p'); is_created_proc s p\<rbrakk> |
|
1204 \<Longrightarrow> valid (CloseFd p' fd # CloseFd p fd # enrich_proc s p p')" |
|
1205 sorry |
|
1206 thus ?thesis using created_cons vd_cons all_procs_cons |
|
1207 apply (case_tac e) |
|
1208 apply (auto simp:is_created_proc_simps split:if_splits) |
|
1209 |
|
1210 ultimately show ?thesis using created_cons vd_cons all_procs_cons |
|
1211 apply (case_tac e) |
|
1212 apply (auto simp:is_created_proc_simps split:if_splits) |
|
1213 done |
|
1214 qed |
|
1215 moreover have "\<forall>obj. alive (e # s) obj \<longrightarrow> alive (enrich_proc (e # s) p p') obj" |
|
1216 sorry |
|
1217 moreover have "\<forall>obj. enrich_not_alive (e # s) obj \<longrightarrow> enrich_not_alive (enrich_proc (e # s) p p') obj" |
|
1218 sorry |
|
1219 moreover have "files_hung_by_del (enrich_proc (e # s) p p') = files_hung_by_del (e # s)" |
|
1220 sorry |
|
1221 moreover have "\<forall>p. p \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_proc (e # s) p p') p = cp2sproc (e # s) p" |
|
1222 sorry |
|
1223 moreover have "\<forall>f. f \<in> current_files (e # s) \<longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f" |
|
1224 sorry |
|
1225 moreover have "\<forall>q. q \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q" |
|
1226 sorry |
|
1227 moreover have "\<forall>p fd f. file_of_proc_fd (e # s) p fd = Some f \<longrightarrow> |
|
1228 file_of_proc_fd (enrich_proc (e # s) p p') p fd = Some f" |
|
1229 sorry |
|
1230 moreover have "\<forall>p fd flags. flags_of_proc_fd (e # s) p fd = Some flags \<longrightarrow> |
|
1231 flags_of_proc_fd (enrich_proc (e # s) p p') p fd = Some flags" |
|
1232 sorry |
|
1233 moreover have "\<forall>q. msgs_of_queue (enrich_proc (e # s) p p') q = msgs_of_queue (e # s) q" |
|
1234 sorry |
|
1235 moreover have "\<forall>p fd. fd \<in> proc_file_fds (e # s) p \<longrightarrow> |
|
1236 cfd2sfd (enrich_proc (e # s) p p') p fd = cfd2sfd (e # s) p fd" |
|
1237 sorry |
|
1238 ultimately show ?case |
1079 by auto |
1239 by auto |
1080 from p2 have vd: "valid s" and os: "os_grant s e" and grant: "grant s e" |
|
1081 by (auto dest:vd_cons vt_grant vt_grant_os) |
|
1082 from p4 have p4': "p' \<notin> all_procs s" by (case_tac e, auto) |
|
1083 from p1 p4' have a1: "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p')" by (auto simp:vd) |
|
1084 have c1: "valid (enrich_proc (e # s) p p')" |
|
1085 apply (case_tac e) |
|
1086 using a1 os p3 |
|
1087 apply (auto simp:is_created_proc_def) |
|
1088 sorry |
|
1089 moreover have c2: "p' \<in> current_procs (enrich_proc (e # s) p p')" |
|
1090 sorry |
|
1091 moreover have c3: "co2sobj (enrich_proc (e # s) p p') (O_proc p') = co2sobj (enrich_proc (e # s) p p') (O_proc p)" |
|
1092 sorry |
|
1093 moreover have c4: "alive (e # s) obj \<longrightarrow> |
|
1094 alive (enrich_proc (e # s) p p') obj \<and> co2sobj (enrich_proc (e # s) p p') obj = co2sobj (e # s) obj" |
|
1095 sorry |
|
1096 ultimately show ?case by auto |
|
1097 qed |
1240 qed |
1098 |
1241 |
|
1242 |
|
1243 lemma enrich_proc_valid: |
|
1244 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> valid (enrich_proc s p p')" |
|
1245 by (auto dest:enrich_proc_prop) |
|
1246 |
|
1247 lemma enrich_proc_valid: |
|
1248 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> " |
|
1249 |
|
1250 |
|
1251 |