|
1 theory Enrich |
|
2 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2 |
|
3 Temp Enrich |
|
4 begin |
|
5 |
|
6 context tainting_s begin |
|
7 |
|
8 lemma get_parentfs_ctxts_prop: |
|
9 "\<lbrakk>get_parentfs_ctxts s (a # f) = Some ctxts; sectxt_of_obj s (O_dir f) = Some ctxt; valid s\<rbrakk> |
|
10 \<Longrightarrow> ctxt \<in> set (ctxts)" |
|
11 apply (induct f) |
|
12 apply (auto split:option.splits) |
|
13 done |
|
14 |
|
15 lemma search_check_allp_intro: |
|
16 "\<lbrakk>search_check s sp pf; get_parentfs_ctxts s pf = Some ctxts; valid s; is_dir s pf\<rbrakk> |
|
17 \<Longrightarrow> search_check_allp sp (set ctxts)" |
|
18 apply (case_tac pf) |
|
19 apply (simp split:option.splits if_splits add:search_check_allp_def) |
|
20 apply (rule ballI) |
|
21 apply (auto simp:search_check_ctxt_def search_check_dir_def split:if_splits option.splits) |
|
22 apply (auto simp:search_check_allp_def search_check_file_def) |
|
23 apply (frule is_dir_not_file, simp) |
|
24 done |
|
25 |
|
26 lemma search_check_leveling_f: |
|
27 "\<lbrakk>search_check s sp pf; parent f = Some pf; is_file s f; valid s; |
|
28 sectxt_of_obj s (O_file f) = Some fctxt; search_check_file sp fctxt\<rbrakk> |
|
29 \<Longrightarrow> search_check s sp f" |
|
30 apply (case_tac f, simp+) |
|
31 apply (auto split:option.splits simp:search_check_ctxt_def) |
|
32 apply (frule parentf_is_dir_prop2, simp) |
|
33 apply (erule get_pfs_secs_prop, simp) |
|
34 apply (erule_tac search_check_allp_intro, simp_all) |
|
35 apply (simp add:parentf_is_dir_prop2) |
|
36 done |
|
37 |
|
38 lemma enrich_proc_prop: |
|
39 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> |
|
40 \<Longrightarrow> valid (enrich_proc s p p') \<and> |
|
41 (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and> |
|
42 (\<forall> obj. enrich_not_alive s obj \<longrightarrow> enrich_not_alive (enrich_proc s p p') obj) \<and> |
|
43 (files_hung_by_del (enrich_proc s p p') = files_hung_by_del s) \<and> |
|
44 (\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp) \<and> |
|
45 (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and> |
|
46 (\<forall> q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q) \<and> |
|
47 (\<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> |
|
48 (\<forall> tp fd flags. flags_of_proc_fd s tp fd = Some flags \<longrightarrow> |
|
49 flags_of_proc_fd (enrich_proc s p p') tp fd = Some flags) \<and> |
|
50 (\<forall> q. msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q) \<and> |
|
51 (\<forall> tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd) \<and> |
|
52 (cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and> |
|
53 (\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd)" |
|
54 proof (induct s) |
|
55 case Nil |
|
56 thus ?case by (auto simp:is_created_proc_def) |
|
57 next |
|
58 case (Cons e s) |
|
59 hence vd_cons: "valid (e # s)" and created_cons: "is_created_proc (e # s) p" |
|
60 and all_procs_cons: "p' \<notin> all_procs (e # s)" and vd: "valid s" |
|
61 and os: "os_grant s e" and grant: "grant s e" |
|
62 by (auto dest:vd_cons vt_grant_os vt_grant) |
|
63 from all_procs_cons have all_procs: "p' \<notin> all_procs s" by (case_tac e, auto) |
|
64 from Cons have pre: "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p') \<and> |
|
65 (\<forall>obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and> |
|
66 (\<forall>obj. enrich_not_alive s obj \<longrightarrow> enrich_not_alive (enrich_proc s p p') obj) \<and> |
|
67 files_hung_by_del (enrich_proc s p p') = files_hung_by_del s \<and> |
|
68 (\<forall>tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp) \<and> |
|
69 (\<forall>f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and> |
|
70 (\<forall>q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q) \<and> |
|
71 (\<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> |
|
72 (\<forall>tp fd flags. |
|
73 flags_of_proc_fd s tp fd = Some flags \<longrightarrow> flags_of_proc_fd (enrich_proc s p p') tp fd = Some flags) \<and> |
|
74 (\<forall>q. msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q) \<and> |
|
75 (\<forall>tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd) \<and> |
|
76 (cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and> |
|
77 (\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd)" |
|
78 using vd all_procs by auto |
|
79 have alive_pre: "is_created_proc s p \<Longrightarrow> (\<forall>obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj)" |
|
80 using pre by simp |
|
81 hence curf_pre: "is_created_proc s p \<Longrightarrow> (\<forall>f. f \<in> current_files s \<longrightarrow> f \<in> current_files (enrich_proc s p p'))" |
|
82 using vd apply auto |
|
83 apply (drule is_file_or_dir, simp) |
|
84 apply (erule disjE) |
|
85 apply (erule_tac x = "O_file f" in allE, simp add:is_file_in_current) |
|
86 apply (erule_tac x = "O_dir f" in allE, simp add:is_dir_in_current) |
|
87 done |
|
88 have vd_enrich_cons: "valid (enrich_proc (e # s) p p')" |
|
89 proof- |
|
90 from pre have pre': "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p')" by simp |
|
91 have "is_created_proc s p \<Longrightarrow> valid (e # enrich_proc s p p')" |
|
92 apply (frule pre') |
|
93 apply (erule_tac s = s in enrich_valid_intro_cons) |
|
94 apply (simp_all add:os grant vd pre) |
|
95 done |
|
96 moreover have "\<And>f fds. \<lbrakk>valid (Execve p f fds # enrich_proc s p p'); is_created_proc s p; |
|
97 valid (Execve p f fds # s); p' \<notin> all_procs s\<rbrakk> |
|
98 \<Longrightarrow> valid (Execve p' f (fds \<inter> proc_file_fds s p) # Execve p f fds # enrich_proc s p p')" |
|
99 proof- |
|
100 fix f fds |
|
101 assume a1: "valid (Execve p f fds # enrich_proc s p p')" and a2: "is_created_proc s p" |
|
102 and a3: "valid (Execve p f fds # s)" and a0: "p' \<notin> all_procs s" |
|
103 have cp2sp: "\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp" |
|
104 and cf2sf: "\<forall> tf. tf \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') tf = cf2sfile s tf" |
|
105 and cfd2sfd: "\<forall> tp tfd. tfd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp tfd = cfd2sfd s tp tfd" |
|
106 and ffd_remain: "\<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> |
|
107 file_of_proc_fd (enrich_proc s p p') tp fd = Some f" |
|
108 and dup_sp: "cp2sproc (enrich_proc s p p') p' = cp2sproc s p" |
|
109 and dup_sfd: "\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd" |
|
110 using pre a2 by auto |
|
111 show "valid (Execve p' f (fds \<inter> proc_file_fds s p) # Execve p f fds # enrich_proc s p p')" |
|
112 proof- |
|
113 from a0 a3 have a0': "p' \<noteq> p" by (auto dest!:vt_grant_os not_all_procs_prop3) |
|
114 from a3 have grant: "grant s (Execve p f fds)" and os: "os_grant s (Execve p f fds)" |
|
115 by (auto dest:vt_grant_os vt_grant simp del:os_grant.simps) |
|
116 have f_in: "is_file (enrich_proc s p p') f" |
|
117 proof- |
|
118 from pre a2 |
|
119 have a4: "\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj" |
|
120 by (auto) |
|
121 show ?thesis using a3 a4 |
|
122 apply (erule_tac x = "O_file f" in allE) |
|
123 by (auto dest:vt_grant_os) |
|
124 qed |
|
125 moreover have a5: "proc_file_fds s p \<subseteq> proc_file_fds (Execve p f fds # enrich_proc s p p') p'" |
|
126 using a3 a0' |
|
127 apply (frule_tac vt_grant_os) |
|
128 apply (auto simp:proc_file_fds_def) |
|
129 apply (rule_tac x = fa in exI) |
|
130 apply (erule enrich_proc_dup_ffd) |
|
131 apply (simp_all add:vd all_procs a2) |
|
132 done |
|
133 ultimately have "os_grant (Execve p f fds # enrich_proc s p p') (Execve p' f (fds \<inter> proc_file_fds s p))" |
|
134 apply (auto simp:is_file_simps enrich_proc_dup_in a2 vd all_procs a1 enrich_proc_dup_ffds) |
|
135 done |
|
136 moreover have "grant (Execve p f fds # enrich_proc s p p') (Execve p' f (fds \<inter> proc_file_fds s p))" |
|
137 proof- |
|
138 from grant obtain up rp tp uf rf tf |
|
139 where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" |
|
140 and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" |
|
141 by (simp split:option.splits, blast) |
|
142 with grant obtain pu nr nt where p3: "npctxt_execve (up, rp, tp) (uf, rf, tf) = Some (pu, nr, nt)" |
|
143 by (simp split:option.splits del:npctxt_execve.simps, blast) |
|
144 have p1': "sectxt_of_obj (Execve p f fds # enrich_proc s p p') (O_proc p') = Some (up, rp, tp)" |
|
145 using p1 dup_sp a1 a0' |
|
146 apply (simp add:sectxt_of_obj_simps) |
|
147 by (simp add:cp2sproc_def split:option.splits) |
|
148 from os have f_in': "is_file s f" by simp |
|
149 from vd os have "\<exists> sf. cf2sfile s f = Some sf" |
|
150 by (auto dest!:is_file_in_current current_file_has_sfile) |
|
151 hence p2': "sectxt_of_obj (Execve p f fds # enrich_proc s p p') (O_file f) = Some (uf, rf, tf)" |
|
152 using f_in p2 cf2sf os a1 |
|
153 apply (erule_tac x = f in allE) |
|
154 apply (auto dest:is_file_in_current simp:cf2sfile_def sectxt_of_obj_simps split:option.splits) |
|
155 apply (case_tac f, simp) |
|
156 apply (drule_tac s = s in root_is_dir', simp add:vd, simp+) |
|
157 done |
|
158 from dup_sfd a5 have "\<forall>fd. fd \<in> proc_file_fds s p \<longrightarrow> |
|
159 cfd2sfd (Execve p f fds # enrich_proc s p p') p' fd = cfd2sfd s p fd" |
|
160 apply (rule_tac allI) |
|
161 apply (erule_tac x = fd in allE, clarsimp) |
|
162 apply (drule set_mp, simp) |
|
163 apply (auto simp:cfd2sfd_execve proc_file_fds_def a1) |
|
164 done |
|
165 hence "inherit_fds_check (Execve p f fds # enrich_proc s p p') (up, nr, nt) p' (fds \<inter> proc_file_fds s p)" |
|
166 using grant os p1 p2 p3 vd |
|
167 apply (clarsimp) |
|
168 apply (rule_tac s = s and p = p and fds = fds in enrich_inherit_fds_check_dup) |
|
169 apply simp_all |
|
170 done |
|
171 moreover have "search_check (Execve p f fds # enrich_proc s p p') (up, rp, tp) f" |
|
172 using p1 p2 p2' vd cf2sf f_in f_in' grant p3 f_in a1 |
|
173 apply (rule_tac s = s in enrich_search_check) |
|
174 apply (simp_all add:is_file_simps) |
|
175 apply (rule allI, rule impI, erule_tac x = fa in allE, simp) |
|
176 apply (drule_tac ff = fa in cf2sfile_other') |
|
177 by (auto simp:a2 curf_pre) |
|
178 ultimately show ?thesis |
|
179 using p1' p2' p3 |
|
180 apply (simp split:option.splits) |
|
181 using grant p1 p2 |
|
182 apply simp |
|
183 done |
|
184 qed |
|
185 ultimately show ?thesis using a1 |
|
186 by (erule_tac valid.intros(2), auto) |
|
187 qed |
|
188 qed |
|
189 moreover have "\<And>tp fds. \<lbrakk>valid (Clone tp p fds # s); p' \<noteq> p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> |
|
190 valid (Clone tp p' (fds \<inter> proc_file_fds s tp) # Clone tp p fds # s)" |
|
191 apply (frule vt_grant_os, frule vt_grant, drule not_all_procs_prop3) |
|
192 apply (rule valid.intros(2)) |
|
193 apply (simp_all split:option.splits add:sectxt_of_obj_simps) |
|
194 apply (auto simp add:proc_file_fds_def)[1] |
|
195 apply (auto simp:inherit_fds_check_def sectxt_of_obj_simps sectxts_of_fds_def inherit_fds_check_ctxt_def) |
|
196 done |
|
197 moreover have "\<And>f flags fd opt. \<lbrakk>valid (Open p f flags fd opt # enrich_proc s p p'); |
|
198 is_created_proc s p; valid (Open p f flags fd opt # s); p' \<notin> all_procs s\<rbrakk> |
|
199 \<Longrightarrow> valid (Open p' f (remove_create_flag flags) fd None # Open p f flags fd opt # enrich_proc s p p')" |
|
200 proof- |
|
201 fix f flags fd opt |
|
202 assume a1: "valid (Open p f flags fd opt # enrich_proc s p p')" and a2: "is_created_proc s p" |
|
203 and a3: "valid (Open p f flags fd opt # s)" and a4: "p' \<notin> all_procs s" |
|
204 have cp2sp: "\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp" |
|
205 and cf2sf: "\<forall> tf. tf \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') tf = cf2sfile s tf" |
|
206 and cfd2sfd: "\<forall> tp tfd. tfd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp tfd = cfd2sfd s tp tfd" |
|
207 and ffd_remain: "\<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> |
|
208 file_of_proc_fd (enrich_proc s p p') tp fd = Some f" |
|
209 and dup_sp: "cp2sproc (enrich_proc s p p') p' = cp2sproc s p" |
|
210 and dup_sfd: "\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd" |
|
211 using pre a2 by auto |
|
212 from a4 a3 have a0: "p' \<noteq> p" by (auto dest!:vt_grant_os not_all_procs_prop3 split:option.splits) |
|
213 have a5: "p' \<in> current_procs (enrich_proc s p p')" |
|
214 using a2 a3 vd |
|
215 apply (erule_tac enrich_proc_dup_in) |
|
216 by (simp_all add:vd a4) |
|
217 have a6: "is_file (Open p f flags fd opt # enrich_proc s p p') f" |
|
218 using a1 a3 |
|
219 by (auto simp:is_file_open dest:vt_grant_os) |
|
220 have a7: "fd \<notin> current_proc_fds (enrich_proc s p p') p'" |
|
221 using a2 a4 vd |
|
222 apply (simp add:enrich_proc_dup_ffds_eq_fds) |
|
223 apply (rule notI) |
|
224 apply (drule_tac p = p in file_fds_subset_pfds) |
|
225 apply (drule set_mp, simp) |
|
226 using a3 |
|
227 apply (drule_tac vt_grant_os) |
|
228 apply (auto split:option.splits) |
|
229 done |
|
230 from a1 have a8: "valid (enrich_proc s p p')" by (erule_tac valid.cases, auto) |
|
231 from a3 have grant: "grant s (Open p f flags fd opt)" and os: "os_grant s (Open p f flags fd opt)" |
|
232 by (auto dest:vt_grant_os vt_grant) |
|
233 show "valid (Open p' f (remove_create_flag flags) fd None # Open p f flags fd opt # enrich_proc s p p')" |
|
234 proof (cases opt) |
|
235 case None |
|
236 have f_in: "is_file (enrich_proc s p p') f" |
|
237 proof- |
|
238 from pre a2 |
|
239 have a4: "\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj" |
|
240 by (auto) |
|
241 show ?thesis using a3 a4 None |
|
242 apply (erule_tac x = "O_file f" in allE) |
|
243 by (auto dest:vt_grant_os) |
|
244 qed |
|
245 from grant None obtain up rp tp uf rf tf |
|
246 where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" |
|
247 and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" |
|
248 apply (simp split:option.splits) |
|
249 by (case_tac a, case_tac aa, blast) |
|
250 have p1': "sectxt_of_obj (Open p f flags fd opt # enrich_proc s p p') (O_proc p') = Some (up, rp, tp)" |
|
251 using p1 dup_sp a1 |
|
252 apply (simp add:sectxt_of_obj_simps) |
|
253 by (simp add:cp2sproc_def split:option.splits) |
|
254 from os None have f_in': "is_file s f" by simp |
|
255 from vd os None have "\<exists> sf. cf2sfile s f = Some sf" |
|
256 by (auto dest!:is_file_in_current current_file_has_sfile) |
|
257 hence p2': "sectxt_of_obj (Open p f flags fd opt # enrich_proc s p p') (O_file f) = Some (uf, rf, tf)" |
|
258 using p2 cf2sf os a1 None f_in' vd f_in |
|
259 apply (erule_tac x = f in allE) |
|
260 apply (auto dest:is_file_in_current simp:cf2sfile_def sectxt_of_obj_simps split:option.splits) |
|
261 apply (case_tac f, simp) |
|
262 apply (drule_tac s = s in root_is_dir', simp add:vd, simp+) |
|
263 done |
|
264 have "search_check (Open p f flags fd opt # enrich_proc s p p') (up, rp, tp) f" |
|
265 using p1 p2 p2' vd cf2sf f_in f_in' grant f_in a1 None |
|
266 apply (rule_tac s = s in enrich_search_check) |
|
267 apply (simp_all add:is_file_simps) |
|
268 apply (rule allI, rule impI, erule_tac x = fa in allE, simp) |
|
269 apply (simp add:cf2sfile_open_none) |
|
270 done |
|
271 thus ?thesis using a0 a5 a6 a7 None a1 |
|
272 apply (rule_tac valid.intros(2)) |
|
273 apply (simp_all add:a1) |
|
274 apply (case_tac flags, simp add:is_creat_excl_flag_def) |
|
275 using p1' p2' |
|
276 apply simp |
|
277 using grant p1 p2 |
|
278 apply (simp add:oflags_check_remove_create) |
|
279 done |
|
280 next |
|
281 case (Some inum) |
|
282 with os obtain pf where parent: "parent f = Some pf" by auto |
|
283 with grant Some obtain pu rp pt pfu pfr pft where |
|
284 p1: "sectxt_of_obj s (O_proc p) = Some (pu, rp, pt)" |
|
285 and p2: "sectxt_of_obj s (O_dir pf) = Some (pfu, pfr, pft)" |
|
286 apply (simp split:option.splits) |
|
287 apply (case_tac a, case_tac aa, blast) |
|
288 done |
|
289 from p1 have p1': "sectxt_of_obj (enrich_proc s p p') (O_proc p) = Some (pu, rp, pt)" |
|
290 using cp2sp os |
|
291 apply (erule_tac x = p in allE) |
|
292 apply (auto split:option.splits simp:cp2sproc_def) |
|
293 done |
|
294 from os parent Some |
|
295 have pf_in: "is_dir s pf" by auto |
|
296 hence "\<exists> sf. cf2sfile s pf = Some sf" using vd |
|
297 by (auto dest!:is_dir_in_current current_file_has_sfile) |
|
298 from a1 parent Some have pf_in': "is_dir (enrich_proc s p p') pf" |
|
299 apply (frule_tac vt_grant_os) |
|
300 by (clarsimp) |
|
301 have p2': "sectxt_of_obj (enrich_proc s p p') (O_dir pf) = Some (pfu, pfr, pft)" |
|
302 proof- |
|
303 have "cf2sfile (enrich_proc s p p') pf = cf2sfile s pf" |
|
304 using cf2sf pf_in |
|
305 apply (drule_tac is_dir_in_current) |
|
306 apply (erule_tac x = pf in allE) |
|
307 by simp |
|
308 with pf_in pf_in' p2 vd Some a8 |
|
309 show ?thesis |
|
310 apply (frule_tac is_dir_not_file) |
|
311 apply (frule_tac s = "enrich_proc s p p'" in is_dir_not_file) |
|
312 apply (simp add:cf2sfile_def) |
|
313 apply (case_tac pf, simp) |
|
314 apply (simp add:sroot_def root_sec_remains) |
|
315 by (auto split:option.splits dest!:current_has_sec' get_pfs_secs_prop' dest:parentf_is_dir_prop1) |
|
316 qed |
|
317 from p1 have dup: "sectxt_of_obj (Open p f flags fd (Some inum) # enrich_proc s p p') (O_proc p') |
|
318 = Some (pu, rp, pt)" |
|
319 using a1 Some |
|
320 apply (simp add:sec_open) |
|
321 using dup_sp |
|
322 apply (auto split:option.splits if_splits simp:cp2sproc_def) |
|
323 done |
|
324 have nsf: "sectxt_of_obj (Open p f flags fd (Some inum) # enrich_proc s p p') (O_file f) |
|
325 = Some (pu, R_object, type_transition pt pft C_file True)" |
|
326 using a1 Some p1 p2 parent p2' p1' |
|
327 by (simp add:sec_open) |
|
328 have "search_check (Open p f flags fd (Some inum) # enrich_proc s p p') (pu, rp, pt) f" |
|
329 proof- |
|
330 have "search_check (Open p f flags fd (Some inum) # enrich_proc s p p') (pu, rp, pt) pf" |
|
331 using grant Some parent p1 p2 vd a1 pf_in pf_in' p2' |
|
332 apply simp |
|
333 apply (rule_tac s = s in enrich_search_check') |
|
334 apply (simp_all add:is_dir_simps sectxt_of_obj_simps) |
|
335 apply (rule allI, rule impI) |
|
336 apply (case_tac "fa = f") |
|
337 using os Some |
|
338 apply simp |
|
339 apply (drule_tac f' = fa in cf2sfile_open) |
|
340 apply (simp add:current_files_simps) |
|
341 using curf_pre a2 |
|
342 apply simp |
|
343 apply simp |
|
344 using cf2sf |
|
345 apply simp |
|
346 done |
|
347 moreover have "is_file (Open p f flags fd (Some inum) # enrich_proc s p p') f" |
|
348 using a1 Some |
|
349 by (simp add:is_file_open) |
|
350 ultimately |
|
351 show ?thesis |
|
352 using parent a1 Some nsf |
|
353 apply (erule_tac search_check_leveling_f) |
|
354 apply (simp_all) |
|
355 apply (simp add:search_check_file_def) |
|
356 apply (simp add:permission_check.simps) |
|
357 sorry |
|
358 qed |
|
359 thus ?thesis using a0 a5 a6 a7 a1 Some |
|
360 apply (rule_tac valid.intros(2)) |
|
361 apply (simp add:a1) |
|
362 apply simp |
|
363 apply (case_tac flags, simp add:is_creat_excl_flag_def) |
|
364 using grant p1 p2 parent dup nsf |
|
365 apply (simp add:oflags_check_remove_create) |
|
366 done |
|
367 qed |
|
368 qed |
|
369 moreover have "\<And>fd. \<lbrakk>valid (CloseFd p fd # enrich_proc s p p'); is_created_proc s p; |
|
370 valid (CloseFd p fd # s); p' \<notin> all_procs s; fd \<in> proc_file_fds s p\<rbrakk> |
|
371 \<Longrightarrow> valid (CloseFd p' fd # CloseFd p fd # enrich_proc s p p')" |
|
372 proof- |
|
373 fix fd |
|
374 assume a1: "valid (CloseFd p fd # enrich_proc s p p')" and a2: "is_created_proc s p" |
|
375 and a3: "p' \<notin> all_procs s" and a4: "valid (CloseFd p fd # s)" |
|
376 and a5: "fd \<in> proc_file_fds s p" |
|
377 from a4 a3 have a0: "p' \<noteq> p" by (auto dest!:vt_grant_os not_all_procs_prop3) |
|
378 have "p' \<in> current_procs (enrich_proc s p p')" |
|
379 using a2 a3 vd |
|
380 by (auto intro:enrich_proc_dup_in) |
|
381 moreover have "fd \<in> current_proc_fds (enrich_proc s p p') p'" |
|
382 using a5 a2 a3 vd pre' |
|
383 apply (simp) |
|
384 apply (drule_tac s = "enrich_proc s p p'" and p = p' in file_fds_subset_pfds) |
|
385 apply (erule set_mp) |
|
386 apply (simp add:enrich_proc_dup_ffds) |
|
387 done |
|
388 ultimately show "valid (CloseFd p' fd # CloseFd p fd # enrich_proc s p p')" |
|
389 apply (rule_tac valid.intros(2)) |
|
390 apply (simp_all add:a1 a0 a2 pre') |
|
391 done |
|
392 qed |
|
393 moreover have "\<And> fd. \<lbrakk>valid (ReadFile p fd # enrich_proc s p p'); |
|
394 is_created_proc s p; valid (ReadFile p fd # s); p' \<notin> all_procs s\<rbrakk> |
|
395 \<Longrightarrow> valid (ReadFile p' fd # ReadFile p fd # enrich_proc s p p')" |
|
396 proof- |
|
397 fix fd |
|
398 assume a1: "valid (ReadFile p fd # enrich_proc s p p')" and a2: "is_created_proc s p" |
|
399 and a3: "valid (ReadFile p fd # s)" and a4: "p' \<notin> all_procs s" |
|
400 from a3 have os: "os_grant s (ReadFile p fd)" and grant: "grant s (ReadFile p fd)" |
|
401 by (auto dest:vt_grant_os vt_grant) |
|
402 have cp2sp: "\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp" |
|
403 and cf2sf: "\<forall> tf. tf \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') tf = cf2sfile s tf" |
|
404 and cfd2sfd: "\<forall> tp tfd. tfd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp tfd = cfd2sfd s tp tfd" |
|
405 and ffd_remain: "\<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> |
|
406 file_of_proc_fd (enrich_proc s p p') tp fd = Some f" |
|
407 and dup_sp: "cp2sproc (enrich_proc s p p') p' = cp2sproc s p" |
|
408 and dup_sfd: "\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd" |
|
409 using pre a2 by auto |
|
410 have vd_enrich: "valid (enrich_proc s p p')" using a1 by (auto dest:valid.cases) |
|
411 show "valid (ReadFile p' fd # ReadFile p fd # enrich_proc s p p')" |
|
412 proof- |
|
413 have "os_grant (ReadFile p fd # enrich_proc s p p') (ReadFile p' fd)" |
|
414 using a1 a2 a4 vd os |
|
415 apply (clarsimp simp:current_files_simps enrich_proc_dup_in enrich_proc_dup_ffds_eq_fds) |
|
416 apply (simp add:proc_file_fds_def) |
|
417 apply (rule conjI) |
|
418 apply (rule_tac x = f in exI, simp add:enrich_proc_dup_ffd) |
|
419 using curf_pre |
|
420 apply (simp) |
|
421 apply (drule enrich_proc_dup_fflags) |
|
422 apply simp_all |
|
423 apply (erule disjE) |
|
424 apply auto |
|
425 apply (simp add:is_read_flag_def) |
|
426 done |
|
427 moreover have "grant (ReadFile p fd # enrich_proc s p p') (ReadFile p' fd)" |
|
428 proof- |
|
429 from grant obtain f sp sfd sf where p1: "file_of_proc_fd s p fd = Some f" |
|
430 and p2: "sectxt_of_obj s (O_proc p) = Some sp" |
|
431 and p3: "sectxt_of_obj s (O_fd p fd) = Some sfd" |
|
432 and p4: "sectxt_of_obj s (O_file f) = Some sf" |
|
433 by (auto split:option.splits) |
|
434 from os obtain flag where p0: "flags_of_proc_fd s p fd = Some flag" |
|
435 by auto |
|
436 from os have f_in_s: "f \<in> current_files s" using p1 by simp |
|
437 from p1 vd have isfile_s: "is_file s f" by (erule_tac file_of_pfd_is_file, simp) |
|
438 with alive_pre a2 have isfile_s': "is_file (enrich_proc s p p') f" |
|
439 apply simp |
|
440 apply (erule_tac x = "O_file f" in allE, simp) |
|
441 done |
|
442 from p0 obtain flag' where p0': "flags_of_proc_fd (enrich_proc s p p') p' fd = Some flag'" |
|
443 and p0'': "(flag' = flag) \<or> (flag' = remove_create_flag flag)" |
|
444 using a2 a4 vd |
|
445 apply (drule_tac enrich_proc_dup_fflags) |
|
446 apply auto |
|
447 apply (case_tac flag, auto) |
|
448 apply (case_tac flag, auto) |
|
449 done |
|
450 from p1 have p1': "file_of_proc_fd (enrich_proc s p p') p' fd = Some f" |
|
451 using a2 a4 vd |
|
452 by (simp add:enrich_proc_dup_ffd) |
|
453 from p2 have p2': "sectxt_of_obj (enrich_proc s p p') (O_proc p') = Some sp" |
|
454 using dup_sp |
|
455 by (auto simp:cp2sproc_def split:option.splits) |
|
456 from p3 p1 p1' p0 p0' os have p3': "sectxt_of_obj (enrich_proc s p p') (O_fd p' fd) = Some sfd" |
|
457 using dup_sfd |
|
458 apply (erule_tac x = fd in allE) |
|
459 apply (auto simp:proc_file_fds_def cfd2sfd_def split:option.splits) |
|
460 apply (drule current_file_has_sfile') |
|
461 apply (simp add:vd, simp) |
|
462 apply (drule current_file_has_sfile') |
|
463 apply (simp add:vd, simp) |
|
464 done |
|
465 from p4 have p4': "sectxt_of_obj (enrich_proc s p p') (O_file f) = Some sf" |
|
466 using f_in_s cf2sf isfile_s isfile_s' a1 vd_enrich vd |
|
467 apply (erule_tac x = f in allE) |
|
468 apply (simp) |
|
469 apply (auto simp:cf2sfile_def split:option.splits |
|
470 dest!:current_has_sec' get_pfs_secs_prop' dest:parentf_is_dir is_file_in_current) |
|
471 apply (case_tac f, simp, drule root_is_dir', simp, simp, simp) |
|
472 done |
|
473 show ?thesis using p1' p2' p3' p4' a1 |
|
474 apply (simp add:sectxt_of_obj_simps) |
|
475 using grant p1 p2 p3 p4 |
|
476 apply simp |
|
477 done |
|
478 qed |
|
479 ultimately show ?thesis |
|
480 using a1 |
|
481 by (erule_tac valid.intros(2), simp+) |
|
482 qed |
|
483 qed |
|
484 ultimately show ?thesis |
|
485 using created_cons vd_cons all_procs_cons |
|
486 apply (case_tac e) |
|
487 apply (auto simp:is_created_proc_simps split:if_splits) |
|
488 done |
|
489 qed |
|
490 moreover have "\<forall>obj. alive (e # s) obj \<longrightarrow> alive (enrich_proc (e # s) p p') obj" |
|
491 sorry |
|
492 moreover have "\<forall>obj. enrich_not_alive (e # s) obj \<longrightarrow> enrich_not_alive (enrich_proc (e # s) p p') obj" |
|
493 sorry |
|
494 moreover have "files_hung_by_del (enrich_proc (e # s) p p') = files_hung_by_del (e # s)" |
|
495 sorry |
|
496 moreover have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_proc (e # s) p p') tp = cp2sproc (e # s) tp" |
|
497 sorry |
|
498 moreover have "\<forall>f. f \<in> current_files (e # s) \<longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f" |
|
499 sorry |
|
500 moreover have "\<forall>q. q \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q" |
|
501 sorry |
|
502 moreover have "\<forall>tp fd f. file_of_proc_fd (e # s) tp fd = Some f \<longrightarrow> |
|
503 file_of_proc_fd (enrich_proc (e # s) p p') tp fd = Some f" |
|
504 sorry |
|
505 moreover have "\<forall>tp fd flags. flags_of_proc_fd (e # s) tp fd = Some flags \<longrightarrow> |
|
506 flags_of_proc_fd (enrich_proc (e # s) p p') tp fd = Some flags" |
|
507 sorry |
|
508 moreover have "\<forall>q. msgs_of_queue (enrich_proc (e # s) p p') q = msgs_of_queue (e # s) q" |
|
509 sorry |
|
510 moreover have "\<forall>tp fd. fd \<in> proc_file_fds (e # s) tp \<longrightarrow> |
|
511 cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd" |
|
512 sorry |
|
513 moreover have "cp2sproc (enrich_proc (e # s) p p') p' = cp2sproc (e # s) p" |
|
514 proof- |
|
515 from pre have b0: "is_created_proc s p \<Longrightarrow> cp2sproc (enrich_proc s p p') p' = cp2sproc s p" by simp |
|
516 have b1: "\<And> tp f fds. \<lbrakk>valid (enrich_proc (Execve tp f fds # s) p p'); valid (Execve tp f fds # s); |
|
517 is_created_proc (Execve tp f fds # s) p; p' \<notin> all_procs (Execve tp f fds # s)\<rbrakk> |
|
518 \<Longrightarrow> cp2sproc (enrich_proc (Execve tp f fds # s) p p') p' = cp2sproc (Execve tp f fds # s) p" |
|
519 proof- |
|
520 fix tp f fds |
|
521 assume a1: "valid (enrich_proc (Execve tp f fds # s) p p')" |
|
522 and a2: "valid (Execve tp f fds # s)" and a3: "is_created_proc (Execve tp f fds # s) p" |
|
523 and a4: "p' \<notin> all_procs (Execve tp f fds # s)" |
|
524 show "cp2sproc (enrich_proc (Execve tp f fds # s) p p') p' = cp2sproc (Execve tp f fds # s) p" |
|
525 proof (cases "tp = p") |
|
526 case True |
|
527 show ?thesis using True a1 a2 a3 a4 |
|
528 thm not_all_procs_prop3 |
|
529 apply (auto simp add:cp2sproc_execve is_created_proc_def split:option.splits dest!:current_has_sec' |
|
530 dest:vt_grant_os not_all_procs_prop2 not_all_procs_prop3) |
|
531 |
|
532 sorry |
|
533 next |
|
534 case False |
|
535 show ?thesis sorry |
|
536 qed |
|
537 qed |
|
538 have b2: "\<And> tp fd. cp2sproc (enrich_proc (ReadFile tp fd # s) p p') p' = cp2sproc (ReadFile tp fd # s) p" |
|
539 sorry |
|
540 have b3: "\<And> tp. cp2sproc (enrich_proc (Exit tp # s) p p') p' = cp2sproc (Exit tp # s) p" |
|
541 sorry |
|
542 have b4: "\<And> tp tp'. cp2sproc (enrich_proc (Kill tp tp' # s) p p') p' = cp2sproc (Kill tp tp' # s) p" |
|
543 sorry |
|
544 have b5: "\<And> tp tp' fds. cp2sproc (enrich_proc (Clone tp tp' fds # s) p p') p' = |
|
545 cp2sproc (Clone tp tp' fds # s) p" |
|
546 sorry |
|
547 have b6: "\<And> tp f flags fd opt. cp2sproc (enrich_proc (Open tp f flags fd opt # s) p p') p' = |
|
548 cp2sproc (Open tp f flags fd opt # s) p" |
|
549 sorry |
|
550 have b7: "\<And> tp fd. cp2sproc (enrich_proc (CloseFd tp fd # s) p p') p' = cp2sproc (CloseFd tp fd # s) p" |
|
551 sorry |
|
552 show ?thesis using vd_enrich_cons |
|
553 apply (case_tac e) |
|
554 apply (simp_all only:b1 b2 b3 b4 b5 b6 b7) |
|
555 using created_cons vd_enrich_cons vd_cons b0 |
|
556 apply (auto simp:cp2sproc_other is_created_proc_def) |
|
557 done |
|
558 qed |
|
559 moreover have "\<forall> fd. fd \<in> proc_file_fds (e # s) p \<longrightarrow> |
|
560 cfd2sfd (enrich_proc (e # s) p p') p' fd = cfd2sfd (e # s) p fd" |
|
561 sorry |
|
562 ultimately show ?case |
|
563 by simp |
|
564 qed |
|
565 |
|
566 |
|
567 lemma enrich_proc_valid: |
|
568 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> valid (enrich_proc s p p')" |
|
569 by (auto dest:enrich_proc_prop) |
|
570 |
|
571 lemma enrich_proc_valid: |
|
572 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> " |
|
573 |
|
574 |
|
575 |
|
576 lemma enrich_proc_tainted: |
|
577 "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk> |
|
578 \<Longrightarrow> tainted (enrich_proc s p p') = (if (O_proc p \<in> tainted s) |
|
579 then tainted s \<union> {O_proc p'} else tainted s)" |
|
580 apply (induct s) |
|
581 apply (simp add:is_created_proc_def) |
|
582 apply (frule vt_grant_os, frule vd_cons, simp) |
|
583 apply (frule enrich_proc_dup_in, simp+) |
|
584 apply (frule not_all_procs_prop3) |
|
585 apply (case_tac a) |
|
586 prefer 3 |
|
587 apply (simp split:if_splits) |
|
588 apply (rule impI|rule conjI)+ |
|
589 apply (simp add:is_created_proc_def) |
|
590 apply (auto simp:is_created_proc_def split:if_splits dest:tainted_in_current)[1] |
|
591 apply (simp add:is_created_proc_def) |
|
592 |
|
593 prefer 4 |
|
594 apply (simp split:if_splits) |
|
595 apply (rule impI|rule conjI)+ |
|
596 apply (simp add:is_created_proc_def) |
|
597 apply (auto simp:is_created_proc_def split:if_splits dest:tainted_in_current)[1] |
|
598 apply (simp add:is_created_proc_def) |
|
599 |
|
600 prefer 4 |
|
601 apply (auto simp:is_created_proc_def split:if_splits option.splits dest:tainted_in_current)[1] |
|
602 |
|
603 prefer 4 |
|
604 apply (auto simp:is_created_proc_def split:if_splits option.splits dest:tainted_in_current enrich_proc_dup_ffd enrich_proc_dup_ffd')[1] |
|
605 |
|
606 |
|
607 |
|
608 lemma enrich_proc_dup_tainted: |
|
609 "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk> |
|
610 \<Longrightarrow> (O_proc p' \<in> tainted (enrich_proc s p p')) = (O_proc p \<in> tainted s)" |
|
611 apply (induct s) |
|
612 apply (simp add:is_created_proc_def) |
|
613 apply (frule vt_grant_os, frule vd_cons) |
|
614 apply (case_tac a) |
|
615 apply (auto simp:is_created_proc_def)[1] |
|
616 |
|
617 |
|
618 lemma enrich_proc_tainted: |
|
619 "" |
|
620 |
|
621 |
|
622 end |
|
623 |
|
624 end |