37 apply (rule_tac x = "O_proc p" in exI, simp add:tainted_eq_Tainted) |
49 apply (rule_tac x = "O_proc p" in exI, simp add:tainted_eq_Tainted) |
38 apply (erule exE| erule conjE)+ |
50 apply (erule exE| erule conjE)+ |
39 apply (case_tac "x = S_proc sp (O_proc p \<in> tainted s)") |
51 apply (case_tac "x = S_proc sp (O_proc p \<in> tainted s)") |
40 apply (rule_tac x = "O_proc p'" in exI) |
52 apply (rule_tac x = "O_proc p'" in exI) |
41 apply (simp add:alive_execve co2sobj_execve tainted_eq_Tainted cp2sproc_execve) |
53 apply (simp add:alive_execve co2sobj_execve tainted_eq_Tainted cp2sproc_execve) |
42 |
54 apply (case_tac "obj = O_proc p", simp) |
43 apply (case_tac obj, simp_all add:co2sobj_execve alive_simps) |
55 apply (frule co2sobj_execve_alive, simp, simp) |
44 thm alive_execve |
56 apply (frule_tac obj = obj in co2sobj_execve, simp) |
45 thm co2sobj_execve |
57 apply (rule_tac x = obj in exI, simp, simp) |
|
58 |
|
59 apply (erule conjE, frule current_proc_has_sp, simp, erule exE, rule impI, simp) |
|
60 apply (subgoal_tac "p \<in> current_procs (Execve p f fds # s)") |
|
61 apply (drule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp, simp) |
|
62 apply (erule exE, erule conjE, simp) |
|
63 apply (simp add:s2ss_def, rule set_eqI, rule iffI) |
|
64 apply (drule CollectD, (erule exE|erule conjE)+) |
|
65 apply (case_tac "obj = O_proc p", simp add:tainted_eq_Tainted) |
|
66 apply (rule disjI1, simp split:if_splits) |
46 apply (simp add:co2sobj_execve, rule disjI2) |
67 apply (simp add:co2sobj_execve, rule disjI2) |
47 apply (rule_tac x = obj in exI, simp split:t_object.splits) |
68 apply (rule conjI,rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits) |
48 thm co2sobj_execve |
69 apply (rule notI, simp, case_tac obj) |
49 apply (case_tac obj, auto simp:co2sobj_execve alive_simps tainted_eq_Tainted split:option.splits dest!:current_proc_has_sp')[1] |
70 apply (erule_tac x = nat in allE, simp add:tainted_eq_Tainted, (simp split:option.splits)+) |
50 apply (simp add:co2sobj_execve) |
71 apply (erule disjE, simp) |
51 apply clarsimp |
72 apply (rule_tac x = "O_proc p" in exI, simp add:tainted_eq_Tainted) |
52 thm current_proc_has_sp |
73 apply (erule exE|erule conjE)+ |
53 |
74 apply (rule_tac x = obj in exI) |
54 apply (auto simp:s2ss_def co2sobj_execve split:option.splits) |
75 apply (drule_tac obj = obj in co2sobj_execve_alive, simp+) |
55 |
76 apply (frule_tac obj = obj in co2sobj_execve, simp, simp) |
56 |
77 apply (rule impI, simp add:tainted_eq_Tainted, simp) |
57 |
78 done |
58 apply (rule conjI, clarify) |
79 |
59 apply (frule_tac p = p in current_proc_has_sp, simp, erule exE) |
80 lemma s2ss_clone_alive: |
60 apply (frule_tac p = p' in current_proc_has_sp, simp, erule exE) |
81 "\<lbrakk>co2sobj s obj = Some x; alive s obj; obj \<noteq> O_proc p'; valid (Clone p p' fds shms # s)\<rbrakk> |
61 apply (simp, (erule conjE)+) |
82 \<Longrightarrow> alive (Clone p p' fds shms # s) obj" |
62 apply (split option.splits, rule conjI, rule impI, drule current_proc_has_sp', simp, simp) |
83 by (erule co2sobj_some_case, auto simp:alive_clone) |
63 apply (rule allI, rule impI) |
84 |
|
85 lemma s2ss_clone: |
|
86 "valid (Clone p p' fds shms # s) \<Longrightarrow> s2ss (Clone p p' fds shms # s) = ( |
|
87 case (cp2sproc (Clone p p' fds shms # s) p') of |
|
88 Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> Tainted s)} |
|
89 | _ \<Rightarrow> {})" |
|
90 apply (frule vd_cons, frule vt_grant_os, split option.splits) |
|
91 apply (rule conjI, rule impI, drule current_proc_has_sp', simp, simp) |
|
92 apply (rule allI, rule impI, simp add:s2ss_def) |
|
93 apply (rule set_eqI, rule iffI, drule CollectD, (erule exE|erule conjE)+) |
|
94 apply (case_tac "obj = O_proc p'", simp add:tainted_eq_Tainted) |
|
95 apply (case_tac "O_proc p' \<in> Tainted s", drule Tainted_in_current, simp+) |
|
96 apply (rule disjI1, simp split:if_splits) |
|
97 apply (simp add:tainted_eq_Tainted, rule disjI2) |
|
98 apply (frule co2sobj_clone, simp) |
|
99 apply (rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits) |
|
100 |
|
101 apply (simp, erule disjE, simp) |
|
102 apply (rule_tac x = "O_proc p'" in exI, simp add:tainted_eq_Tainted) |
|
103 apply (rule impI, rule notI, drule Tainted_in_current, simp+) |
|
104 apply (erule exE| erule conjE)+ |
|
105 apply (case_tac "obj = O_proc p'", simp) |
|
106 apply (rule_tac x = obj in exI) |
|
107 apply (frule s2ss_clone_alive, simp+) |
|
108 apply (auto simp:co2sobj_clone alive_simps) |
|
109 done |
|
110 |
|
111 definition update_s2ss_shm:: "t_state \<Rightarrow> t_process \<Rightarrow> t_static_state" |
|
112 where |
|
113 "update_s2ss_shm s pfrom \<equiv> s2ss s |
|
114 \<union> {S_proc sp True| sp p. info_flow_shm s pfrom p \<and> cp2sproc s p = Some sp} |
|
115 - {S_proc sp False | sp p. info_flow_shm s pfrom p \<and> cp2sproc s p = Some sp \<and> |
|
116 (\<not> (\<exists> p'. \<not> info_flow_shm s pfrom p' \<and> p' \<in> current_procs s \<and> |
|
117 cp2sproc s p' = Some sp \<and> O_proc p' \<notin> Tainted s))}" |
|
118 |
|
119 lemma Tainted_ptrace': |
|
120 "valid s \<Longrightarrow> Tainted (Ptrace p p' # s) = |
|
121 (if (O_proc p \<in> Tainted s \<and> O_proc p' \<notin> Tainted s) |
|
122 then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p' p''} |
|
123 else if (O_proc p' \<in> Tainted s \<and> O_proc p \<notin> Tainted s) |
|
124 then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p p''} |
|
125 else Tainted s)" |
|
126 using info_flow_shm_Tainted by auto |
|
127 |
|
128 lemma co2sobj_some_caseD: |
|
129 "\<lbrakk>co2sobj s obj = Some sobj; \<And> p. \<lbrakk>co2sobj s obj = Some sobj; obj = O_proc p\<rbrakk> \<Longrightarrow> P (O_proc p); |
|
130 \<And> f. \<lbrakk>co2sobj s obj = Some sobj; obj = O_file f\<rbrakk> \<Longrightarrow> P (O_file f); |
|
131 \<And> h. \<lbrakk>co2sobj s obj = Some sobj; obj = O_shm h\<rbrakk> \<Longrightarrow> P (O_shm h); |
|
132 \<And> f. \<lbrakk>co2sobj s obj = Some sobj; obj = O_dir f\<rbrakk> \<Longrightarrow> P (O_dir f); |
|
133 \<And> q. \<lbrakk>co2sobj s obj = Some sobj; obj = O_msgq q\<rbrakk> \<Longrightarrow> P (O_msgq q)\<rbrakk> |
|
134 \<Longrightarrow> P obj" |
|
135 by (case_tac obj, auto) |
|
136 |
|
137 lemma s2ss_ptrace1_aux: "x \<notin> {x. P x} \<Longrightarrow> \<not> P x" by simp |
|
138 |
|
139 lemma s2ss_ptrace1: |
|
140 "\<lbrakk>valid (Ptrace p p' # s); O_proc p \<in> Tainted s; O_proc p' \<notin> Tainted s\<rbrakk> |
|
141 \<Longrightarrow> s2ss (Ptrace p p' # s) = update_s2ss_shm s p'" |
|
142 unfolding update_s2ss_shm_def s2ss_def |
|
143 apply (frule vd_cons, rule set_eqI, rule iffI) |
|
144 apply (drule CollectD, (erule exE|erule conjE)+) |
|
145 apply (erule co2sobj_some_caseD) |
|
146 apply (rule DiffI) |
|
147 apply (case_tac "O_proc pa \<in> Tainted s") |
|
148 apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI) |
|
149 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) |
|
150 apply (case_tac "info_flow_shm s p' pa") |
|
151 apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits) |
|
152 apply (drule current_proc_has_sp', simp, simp) |
|
153 apply (rule_tac x = a in exI, rule_tac x = pa in exI) |
|
154 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) |
|
155 apply (rule UnI1, simp) |
|
156 apply (rule_tac x = "O_proc pa" in exI) |
|
157 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) |
|
158 apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits) |
|
159 apply (erule_tac x = pa in allE, simp) |
|
160 |
|
161 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, |
|
162 auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] |
|
163 apply (simp) |
|
164 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, |
|
165 auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] |
|
166 apply (simp split:option.splits) |
|
167 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, |
|
168 auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] |
|
169 apply (simp split:option.splits) |
|
170 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, |
|
171 auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] |
|
172 apply (simp split:option.splits) |
|
173 |
|
174 apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE) |
|
175 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI) |
|
176 apply (erule co2sobj_some_caseD) |
|
177 apply (case_tac "O_proc pa \<in> Tainted s") |
|
178 apply (rule_tac x = "O_proc pa" in exI) |
|
179 apply (clarsimp simp add:tainted_eq_Tainted cp2sproc_other split:option.splits) |
|
180 apply (case_tac "info_flow_shm s p' pa", simp only:co2sobj.simps split:option.splits) |
|
181 apply (drule current_proc_has_sp', simp, simp) |
|
182 apply (drule Meson.not_exD, erule_tac x = a in allE, drule Meson.not_exD, erule_tac x = pa in allE) |
|
183 apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+) |
|
184 apply (rule_tac x = "O_proc p'a" in exI) |
|
185 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) |
|
186 apply (rule_tac x = "O_proc pa" in exI) |
|
187 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) |
|
188 |
|
189 apply (rule_tac x = obj in exI, |
|
190 auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] |
|
191 apply (rule_tac x = obj in exI, |
|
192 auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] |
|
193 apply (rule_tac x = obj in exI, |
|
194 auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] |
|
195 apply (rule_tac x = obj in exI, |
|
196 auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] |
|
197 |
|
198 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI) |
|
199 apply (rule_tac x = "O_proc pa" in exI) |
|
200 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs) |
|
201 done |
|
202 |
|
203 lemma s2ss_ptrace2: |
|
204 "\<lbrakk>valid (Ptrace p p' # s); O_proc p' \<in> Tainted s; O_proc p \<notin> Tainted s\<rbrakk> |
|
205 \<Longrightarrow> s2ss (Ptrace p p' # s) = update_s2ss_shm s p" |
|
206 unfolding update_s2ss_shm_def s2ss_def |
|
207 apply (frule vd_cons, rule set_eqI, rule iffI) |
|
208 apply (drule CollectD, (erule exE|erule conjE)+) |
|
209 apply (erule co2sobj_some_caseD) |
|
210 apply (rule DiffI) |
|
211 apply (case_tac "O_proc pa \<in> Tainted s") |
|
212 apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI) |
|
213 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) |
|
214 apply (case_tac "info_flow_shm s p pa") |
|
215 apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits) |
|
216 apply (drule current_proc_has_sp', simp, simp) |
|
217 apply (rule_tac x = a in exI, rule_tac x = pa in exI) |
|
218 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) |
|
219 apply (rule UnI1, simp) |
|
220 apply (rule_tac x = "O_proc pa" in exI) |
|
221 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) |
|
222 apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits) |
|
223 apply (erule_tac x = pa in allE, simp) |
|
224 |
|
225 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, |
|
226 auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] |
|
227 apply (simp) |
|
228 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, |
|
229 auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] |
|
230 apply (simp split:option.splits) |
|
231 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, |
|
232 auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] |
|
233 apply (simp split:option.splits) |
|
234 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, |
|
235 auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] |
|
236 apply (simp split:option.splits) |
|
237 |
|
238 apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE) |
|
239 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI) |
|
240 apply (erule co2sobj_some_caseD) |
|
241 apply (case_tac "O_proc pa \<in> Tainted s") |
|
242 apply (rule_tac x = "O_proc pa" in exI) |
|
243 apply (clarsimp simp add:tainted_eq_Tainted cp2sproc_other split:option.splits) |
|
244 apply (case_tac "info_flow_shm s p pa", simp only:co2sobj.simps split:option.splits) |
|
245 apply (drule current_proc_has_sp', simp, simp) |
|
246 apply (drule Meson.not_exD, erule_tac x = a in allE, drule Meson.not_exD, erule_tac x = pa in allE) |
|
247 apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+) |
|
248 apply (rule_tac x = "O_proc p'a" in exI) |
|
249 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) |
|
250 apply (rule_tac x = "O_proc pa" in exI) |
|
251 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) |
|
252 |
|
253 apply (rule_tac x = obj in exI, |
|
254 auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] |
|
255 apply (rule_tac x = obj in exI, |
|
256 auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] |
|
257 apply (rule_tac x = obj in exI, |
|
258 auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] |
|
259 apply (rule_tac x = obj in exI, |
|
260 auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] |
|
261 |
|
262 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI) |
|
263 apply (rule_tac x = "O_proc pa" in exI) |
|
264 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs) |
|
265 done |
|
266 |
|
267 lemma s2ss_ptrace3: |
|
268 "\<lbrakk>valid (Ptrace p p' # s); (O_proc p' \<in> Tainted s) = (O_proc p \<in> Tainted s)\<rbrakk> |
|
269 \<Longrightarrow> s2ss (Ptrace p p' # s) = s2ss s" |
|
270 unfolding s2ss_def |
|
271 apply (frule vd_cons, rule set_eqI, rule iffI) |
|
272 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI) |
|
273 apply (rule_tac x = obj in exI) |
|
274 apply (frule alive_other, simp+) |
|
275 apply (frule_tac obj = obj in co2sobj_ptrace, simp) |
|
276 apply (auto simp add:tainted_eq_Tainted split:t_object.splits option.splits if_splits |
|
277 intro:info_flow_shm_Tainted)[1] |
|
278 |
|
279 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI) |
|
280 apply (rule_tac x = obj in exI) |
|
281 apply (frule alive_other, simp+) |
|
282 apply (frule_tac obj = obj in co2sobj_ptrace, simp) |
|
283 apply (auto simp add:tainted_eq_Tainted split:t_object.splits option.splits if_splits |
|
284 intro:info_flow_shm_Tainted) |
|
285 done |
|
286 |
|
287 lemma s2ss_ptrace: |
|
288 "valid (Ptrace p p' # s) \<Longrightarrow> s2ss (Ptrace p p' # s) = ( |
|
289 if (O_proc p \<in> Tainted s \<and> O_proc p' \<notin> Tainted s) |
|
290 then update_s2ss_shm s p' |
|
291 else if (O_proc p' \<in> Tainted s \<and> O_proc p \<notin> Tainted s) |
|
292 then update_s2ss_shm s p |
|
293 else s2ss s )" |
|
294 apply (frule vt_grant_os, frule vd_cons) |
|
295 apply (simp add:s2ss_ptrace2 s2ss_ptrace1 split:if_splits) |
|
296 by (auto dest:s2ss_ptrace3) |
|
297 |
|
298 lemma s2ss_kill: |
|
299 "valid (Kill p p' # s) \<Longrightarrow> s2ss (Kill p p' # s) = ( |
|
300 if (\<exists> p''. p'' \<in> current_procs s \<and> p'' \<noteq> p' \<and> co2sobj s (O_proc p'') = co2sobj s (O_proc p')) |
|
301 then s2ss s |
|
302 else (case (co2sobj s (O_proc p')) of |
|
303 Some sp \<Rightarrow> s2ss s - {sp} |
|
304 | _ \<Rightarrow> {}))" |
|
305 apply (frule vt_grant_os, frule vd_cons) |
|
306 unfolding s2ss_def |
|
307 apply (simp split:if_splits, rule conjI) |
|
308 apply (rule impI, (erule exE|erule conjE)+) |
|
309 apply (split option.splits) |
|
310 apply (drule current_proc_has_sp', simp, simp) |
|
311 apply (simp split: option.splits, (erule conjE)+) |
|
312 apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI) |
|
313 apply (rule_tac x = obj in exI) |
|
314 apply (simp add:co2sobj_kill tainted_eq_Tainted alive_kill split:t_object.splits if_splits) |
|
315 apply (erule CollectE, erule exE, erule conjE, rule CollectI) |
|
316 apply (erule co2sobj_some_caseD) |
|
317 apply (case_tac "pa = p'") |
|
318 apply (rule_tac x = "O_proc p''" in exI) |
|
319 apply (simp add:cp2sproc_kill tainted_eq_Tainted alive_kill |
|
320 split:t_object.splits if_splits option.splits) |
|
321 apply (rule_tac x = "O_proc pa" in exI) |
|
322 apply (clarsimp simp add:cp2sproc_kill tainted_eq_Tainted alive_kill |
|
323 split:t_object.splits if_splits option.splits) |
|
324 apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+ |
|
325 |
|
326 apply (rule impI, erule conjE, frule current_proc_has_sp, simp, erule exE, simp) |
64 apply (rule set_eqI, rule iffI) |
327 apply (rule set_eqI, rule iffI) |
65 |
328 apply (erule CollectE, erule exE, erule conjE, rule DiffI) |
66 apply (simp split:option.splits) |
329 apply (rule CollectI, rule_tac x = obj in exI) |
67 apply (frule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp) |
330 apply (simp add:co2sobj_kill tainted_eq_Tainted alive_kill split:t_object.splits if_splits) |
68 thm current_proc_has_sp |
331 apply (rule notI, simp, case_tac obj) |
69 |
332 apply (erule_tac x = nat in allE) |
70 |
333 apply (simp add:co2sobj_kill cp2sproc_kill tainted_eq_Tainted split:option.splits) |
71 apply (simp split:option.splits) |
334 apply (simp split:option.splits)+ |
72 apply (drule current_proc_has_sp', simp, simp) |
335 apply (erule co2sobj_some_caseD) |
73 apply (rule conjI, rule impI, drule current_proc_has_sp', simp, simp) |
336 apply (case_tac "pa = p'") |
74 apply (simp add:s2ss_def) |
337 apply (rule_tac x = "O_proc p''" in exI) |
75 apply (rule allI|rule impI)+ |
338 apply (simp add:cp2sproc_kill tainted_eq_Tainted alive_kill |
|
339 split:t_object.splits if_splits option.splits) |
|
340 apply (rule_tac x = "O_proc pa" in exI) |
|
341 apply (clarsimp simp add:cp2sproc_kill tainted_eq_Tainted alive_kill |
|
342 split:t_object.splits if_splits option.splits) |
|
343 apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+ |
|
344 done |
|
345 |
|
346 lemma s2ss_exit: |
|
347 "valid (Exit p # s) \<Longrightarrow> s2ss (Exit p # s) = ( |
|
348 if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p)) |
|
349 then s2ss s |
|
350 else (case (co2sobj s (O_proc p)) of |
|
351 Some sp \<Rightarrow> s2ss s - {sp} |
|
352 | _ \<Rightarrow> {}))" |
|
353 apply (frule vt_grant_os, frule vd_cons) |
|
354 unfolding s2ss_def |
|
355 apply (simp split:if_splits, rule conjI) |
|
356 apply (rule impI, (erule exE|erule conjE)+) |
|
357 apply (split option.splits) |
|
358 apply (drule current_proc_has_sp', simp, simp) |
|
359 apply (simp split: option.splits, (erule conjE)+) |
|
360 apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI) |
|
361 apply (rule_tac x = obj in exI) |
|
362 apply (simp add:co2sobj_exit tainted_eq_Tainted alive_exit split:t_object.splits if_splits) |
|
363 apply (erule CollectE, erule exE, erule conjE, rule CollectI) |
|
364 apply (erule co2sobj_some_caseD) |
|
365 apply (case_tac "pa = p") |
|
366 apply (rule_tac x = "O_proc p'" in exI) |
|
367 apply (simp add:cp2sproc_exit tainted_eq_Tainted alive_exit |
|
368 split:t_object.splits if_splits option.splits) |
|
369 apply (rule_tac x = "O_proc pa" in exI) |
|
370 apply (clarsimp simp add:cp2sproc_exit tainted_eq_Tainted alive_exit |
|
371 split:t_object.splits if_splits option.splits) |
|
372 apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+ |
|
373 |
|
374 apply (rule impI, frule current_proc_has_sp, simp, erule exE, simp) |
76 apply (rule set_eqI, rule iffI) |
375 apply (rule set_eqI, rule iffI) |
77 apply (auto simp:alive_simps) |
376 apply (erule CollectE, erule exE, erule conjE, rule DiffI) |
78 apply (case_tac obj, auto split:option.splits simp:cp2sproc_execve) |
377 apply (rule CollectI, rule_tac x = obj in exI) |
79 apply (auto split:if_splits) |
378 apply (simp add:co2sobj_exit tainted_eq_Tainted alive_exit split:t_object.splits if_splits) |
|
379 apply (rule notI, simp, case_tac obj) |
|
380 apply (erule_tac x = nat in allE) |
|
381 apply (simp add:co2sobj_exit cp2sproc_exit tainted_eq_Tainted split:option.splits) |
|
382 apply (simp split:option.splits)+ |
|
383 apply (erule co2sobj_some_caseD) |
|
384 apply (case_tac "pa = p") |
|
385 apply (rule_tac x = "O_proc p'" in exI) |
|
386 apply (simp add:cp2sproc_exit tainted_eq_Tainted alive_exit |
|
387 split:t_object.splits if_splits option.splits) |
|
388 apply (rule_tac x = "O_proc pa" in exI) |
|
389 apply (clarsimp simp add:cp2sproc_exit tainted_eq_Tainted alive_exit |
|
390 split:t_object.splits if_splits option.splits) |
|
391 apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+ |
|
392 done |
|
393 |
|
394 lemma alive_has_sobj': |
|
395 "\<lbrakk>co2sobj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj" |
|
396 apply (case_tac obj) |
|
397 apply (auto split:option.splits) |
|
398 oops |
|
399 |
|
400 declare co2sobj.simps [simp del] |
|
401 |
|
402 lemma co2sobj_open_none: |
|
403 "\<lbrakk>valid (Open p f flag fd None # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Open p f flag fd None # s) obj = ( |
|
404 if (obj = O_proc p) |
|
405 then (case (cp2sproc (Open p f flag fd None # s) p) of |
|
406 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s)) |
|
407 | _ \<Rightarrow> None) |
|
408 else co2sobj s obj)" |
|
409 apply (frule vt_grant_os, frule vd_cons) |
|
410 apply (frule_tac obj = obj in co2sobj_open, simp add:alive_open) |
|
411 apply (auto split:t_object.splits option.splits dest!:current_proc_has_sp') |
|
412 done |
|
413 |
|
414 lemma co2sobj_open_some: |
|
415 "\<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 = ( |
|
416 if (obj = O_proc p) |
|
417 then (case (cp2sproc (Open p f flag fd (Some i) # s) p) of |
|
418 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s)) |
|
419 | _ \<Rightarrow> None) |
|
420 else if (obj = O_file f) |
|
421 then (case (cf2sfile (Open p f flag fd (Some i) # s) f) of |
|
422 Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> Tainted s)) |
|
423 | _ \<Rightarrow> None) |
|
424 else co2sobj s obj)" |
|
425 apply (frule vt_grant_os, frule vd_cons) |
|
426 apply (frule_tac obj = obj in co2sobj_open, simp add:alive_open) |
|
427 apply (auto split:t_object.splits option.splits dest!:current_proc_has_sp') |
|
428 done |
|
429 |
|
430 lemma alive_co2sobj_some_open_none: |
|
431 "\<lbrakk>co2sobj s obj = Some sobj; alive s obj; valid (Open p f flag fd None # s)\<rbrakk> |
|
432 \<Longrightarrow> alive (Open p f flag fd None # s) obj" |
|
433 by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps) |
|
434 |
|
435 lemma alive_co2sobj_some_open_none': |
|
436 "\<lbrakk>co2sobj (Open p f flag fd None # s) obj = Some sobj; alive (Open p f flag fd None # s) obj; |
|
437 valid (Open p f flag fd None # s)\<rbrakk> \<Longrightarrow> alive s obj" |
|
438 by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps) |
|
439 |
|
440 lemma co2sobj_proc_obj: |
|
441 "\<lbrakk>co2sobj s obj = Some x; co2sobj s (O_proc p) = Some x\<rbrakk> |
|
442 \<Longrightarrow> \<exists> p'. obj = O_proc p'" |
|
443 by (case_tac obj, auto simp:co2sobj.simps split:option.splits) |
|
444 |
|
445 lemma s2ss_open_none: |
|
446 "valid (Open p f flag fd None # s) \<Longrightarrow> s2ss (Open p f flag fd None # s) = ( |
|
447 case (co2sobj s (O_proc p), co2sobj (Open p f flag fd None # s) (O_proc p)) of |
|
448 (Some sp, Some sp') \<Rightarrow> |
|
449 if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp) |
|
450 then s2ss s \<union> {sp'} |
|
451 else s2ss s - {sp} \<union> {sp'} |
|
452 | _ \<Rightarrow> {} )" |
|
453 unfolding s2ss_def |
|
454 apply (frule vt_grant_os, frule vd_cons) |
|
455 apply (case_tac "co2sobj s (O_proc p)", simp add:co2sobj.simps split:option.splits) |
|
456 apply (drule current_proc_has_sp', simp, simp) |
|
457 apply (case_tac "co2sobj (Open p f flag fd None # s) (O_proc p)") |
|
458 apply (simp add:co2sobj.simps split:option.splits) |
|
459 apply (drule current_proc_has_sp', simp, simp) |
|
460 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, simp) |
|
461 apply (frule_tac obj = obj in alive_co2sobj_some_open_none', simp, simp) |
|
462 apply (rule conjI, rule impI, erule exE, (erule conjE)+) |
|
463 apply (rule Meson.disj_comm, rule disjCI, case_tac "obj = O_proc p", simp) |
|
464 apply (rule_tac x = obj in exI, simp add:co2sobj_open_none) |
|
465 apply (rule impI) |
|
466 apply (case_tac "obj = O_proc p", simp) |
|
467 apply (rule Meson.disj_comm, rule disjCI, rule conjI) |
|
468 apply (rule_tac x = obj in exI, simp add:co2sobj_open_none) |
|
469 apply (simp add:co2sobj_open_none split:option.splits) |
|
470 apply (rule notI) |
|
471 apply (frule co2sobj_proc_obj, simp, erule exE) |
|
472 apply (erule_tac x = p' in allE, simp) |
|
473 |
|
474 apply (simp split:if_splits) |
|
475 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp) |
|
476 apply (erule exE, erule conjE, case_tac "obj = O_proc p") |
|
477 apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_none) |
|
478 apply (rule_tac x = obj in exI, simp add:co2sobj_open_none alive_co2sobj_some_open_none) |
|
479 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp) |
|
480 apply (erule conjE, erule exE, erule conjE, case_tac "obj = O_proc p") |
|
481 apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_none) |
|
482 apply (rule_tac x = obj in exI, simp add:co2sobj_open_none alive_co2sobj_some_open_none) |
|
483 done |
|
484 |
|
485 lemma alive_co2sobj_some_open_some: |
|
486 "\<lbrakk>alive s obj; valid (Open p f flag fd (Some i) # s)\<rbrakk> |
|
487 \<Longrightarrow> alive (Open p f flag fd (Some i) # s) obj" |
|
488 by (case_tac obj, auto simp:alive_simps is_file_simps is_dir_simps) |
|
489 |
|
490 lemma alive_co2sobj_some_open_some': |
|
491 "\<lbrakk>co2sobj (Open p f flag fd (Some i) # s) obj = Some sobj; alive (Open p f flag fd (Some i) # s) obj; |
|
492 valid (Open p f flag fd (Some i) # s); obj \<noteq> O_file f\<rbrakk> \<Longrightarrow> alive s obj" |
|
493 by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps) |
|
494 |
|
495 lemma s2ss_open_some: |
|
496 "valid (Open p f flag fd (Some i) # s) \<Longrightarrow> s2ss (Open p f flag fd (Some i) # s) = ( |
|
497 case (co2sobj s (O_proc p), co2sobj (Open p f flag fd (Some i) # s) (O_proc p), |
|
498 co2sobj (Open p f flag fd (Some i) # s) (O_file f)) of |
|
499 (Some sp, Some sp', Some sf) \<Rightarrow> |
|
500 if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp) |
|
501 then s2ss s \<union> {sp', sf} |
|
502 else s2ss s - {sp} \<union> {sp', sf} |
|
503 | _ \<Rightarrow> {} )" |
|
504 unfolding s2ss_def |
|
505 apply (frule vt_grant_os, frule vd_cons) |
|
506 apply (case_tac "co2sobj s (O_proc p)", simp add:co2sobj.simps split:option.splits) |
|
507 apply (drule current_proc_has_sp', simp, simp) |
|
508 apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (O_proc p)") |
|
509 apply (simp add:co2sobj.simps split:option.splits) |
|
510 apply (drule current_proc_has_sp', simp, simp) |
|
511 apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (O_file f)") |
|
512 apply (simp add:co2sobj.simps split:option.splits) |
|
513 apply (clarsimp split del:if_splits) |
|
514 |
|
515 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE) |
|
516 apply (split if_splits, rule conjI, rule impI, erule exE, erule conjE, erule conjE) |
|
517 apply (case_tac "obj = O_proc p", simp, case_tac "obj = O_file f", simp) |
|
518 apply (rule UnI1, rule CollectI, rule_tac x = obj in exI) |
|
519 apply (frule_tac obj = obj in alive_co2sobj_some_open_some', simp+) |
|
520 apply (simp add:co2sobj_open split:t_object.splits) |
|
521 apply (rule impI, case_tac "obj = O_proc p", simp, case_tac "obj = O_file f", simp) |
|
522 apply (rule UnI1, rule DiffI, rule CollectI, rule_tac x = obj in exI) |
|
523 apply (frule_tac obj = obj in alive_co2sobj_some_open_some', simp+) |
|
524 apply (simp add:co2sobj_open split:t_object.splits) |
|
525 apply (frule_tac obj = obj in co2sobj_open_some, simp+) |
|
526 apply (simp add:alive_co2sobj_some_open_some', simp) |
|
527 apply (rule notI) |
|
528 apply (frule_tac obj = obj and p = p in co2sobj_proc_obj, simp+, erule exE) |
|
529 apply (erule_tac x = p' in allE, simp) |
|
530 |
|
531 apply (simp split:if_splits, erule disjE) |
|
532 apply (rule_tac x = "O_proc p" in exI, simp) |
|
533 apply (erule disjE, rule_tac x = "O_file f" in exI, simp add:is_file_simps) |
|
534 apply (erule exE, erule conjE) |
|
535 apply (case_tac "obj = O_proc p", simp) |
|
536 apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_some) |
|
537 apply (case_tac "obj = O_file f", simp add:is_file_in_current) |
|
538 apply (rule_tac x = obj in exI, simp add:co2sobj_open_some alive_co2sobj_some_open_some) |
|
539 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp) |
|
540 apply (erule disjE, rule_tac x = "O_file f" in exI, simp add:is_file_simps) |
|
541 apply (erule conjE, erule exE, erule conjE) |
|
542 apply (case_tac "obj = O_proc p", simp) |
|
543 apply (case_tac "obj = O_file f", simp add:is_file_in_current) |
|
544 apply (rule_tac x = obj in exI, simp add:co2sobj_open_some alive_co2sobj_some_open_some) |
|
545 done |
|
546 |
|
547 lemma s2ss_open: |
|
548 "valid (Open p f flag fd opt # s) \<Longrightarrow> s2ss (Open p f flag fd opt # s) = ( |
|
549 if opt = None |
|
550 then (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p)) of |
|
551 (Some sp, Some sp') \<Rightarrow> |
|
552 if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp) |
|
553 then s2ss s \<union> {sp'} |
|
554 else s2ss s - {sp} \<union> {sp'} |
|
555 | _ \<Rightarrow> {} ) |
|
556 else (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p), |
|
557 co2sobj (Open p f flag fd opt # s) (O_file f)) of |
|
558 (Some sp, Some sp', Some sf) \<Rightarrow> |
|
559 if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp) |
|
560 then s2ss s \<union> {sp', sf} |
|
561 else s2ss s - {sp} \<union> {sp', sf} |
|
562 | _ \<Rightarrow> {} ) )" |
|
563 apply (case_tac opt) |
|
564 apply (simp add:s2ss_open_some s2ss_open_none)+ |
|
565 done |
|
566 |
|
567 lemma |
|
568 |
|
569 |
|
570 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open |
|
571 |