|
1 (*<*) |
|
2 theory S2ss_prop2 |
|
3 imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop S2ss_prop |
|
4 begin |
|
5 (*>*) |
|
6 |
|
7 context tainting_s begin |
|
8 |
|
9 definition unbackuped_sprocs :: "t_state \<Rightarrow> t_event \<Rightarrow> t_process set \<Rightarrow> t_sobject set" |
|
10 where |
|
11 "unbackuped_sprocs s e procs \<equiv> |
|
12 {sp | p sp. p \<in> procs \<and> co2sobj s (O_proc p) = Some sp \<and> |
|
13 (\<forall> p' \<in> procs. co2sobj (e # s) (O_proc p') \<noteq> Some sp) \<and> |
|
14 (\<forall> p' \<in> (current_procs s - procs). co2sobj s (O_proc p') \<noteq> Some sp)}" |
|
15 |
|
16 definition update_s2ss_procs :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_event \<Rightarrow> t_process set \<Rightarrow> t_static_state" |
|
17 where |
|
18 "update_s2ss_procs s ss e procs \<equiv> |
|
19 ss \<union> {sp | p sp. p \<in> procs \<and> co2sobj (e # s) (O_proc p) = Some sp} |
|
20 - unbackuped_sprocs s e procs" |
|
21 (* new sp after event may exists as same before the event in procs *) |
|
22 |
|
23 lemma unbked_sps_D: |
|
24 "\<lbrakk>x \<in> unbackuped_sprocs s e procs; p \<in> procs\<rbrakk> \<Longrightarrow> co2sobj (e # s) (O_proc p) \<noteq> Some x" |
|
25 by (auto simp add:unbackuped_sprocs_def) |
|
26 |
|
27 lemma unbked_sps_D': |
|
28 "\<lbrakk>x \<in> unbackuped_sprocs s e procs; p \<notin> procs; p \<in> current_procs s; |
|
29 co2sobj (e # s) (O_proc p) = co2sobj s (O_proc p)\<rbrakk> |
|
30 \<Longrightarrow> co2sobj (e # s) (O_proc p) \<noteq> Some x" |
|
31 by (auto simp:unbackuped_sprocs_def) |
|
32 |
|
33 lemma not_unbked_sps_D: |
|
34 "\<lbrakk>x \<notin> unbackuped_sprocs s e procs; p \<in> procs; co2sobj s (O_proc p) = Some x\<rbrakk> |
|
35 \<Longrightarrow> (\<exists> p' \<in> procs. co2sobj (e # s) (O_proc p') = Some x) \<or> |
|
36 (\<exists> p' \<in> current_procs s - procs. co2sobj s (O_proc p') = Some x)" |
|
37 by (auto simp:unbackuped_sprocs_def) |
|
38 |
|
39 lemma unbked_sps_I: |
|
40 "\<lbrakk>co2sobj s obj = Some x; \<forall> p. obj \<noteq> O_proc p\<rbrakk> \<Longrightarrow> x \<notin> unbackuped_sprocs s' e procs" |
|
41 apply (case_tac obj) |
|
42 apply (auto simp add:unbackuped_sprocs_def co2sobj.simps split:option.splits) |
|
43 done |
|
44 |
|
45 lemma co2sobj_proc_deleteshm: |
|
46 "\<lbrakk>valid (DeleteShM p h # s); \<forall>flag. (pa, flag) \<notin> procs_of_shm s h; pa \<in> current_procs s\<rbrakk> |
|
47 \<Longrightarrow> co2sobj (DeleteShM p h # s) (O_proc pa) = co2sobj s (O_proc pa)" |
|
48 thm co2sobj_deleteshm |
|
49 apply (frule_tac obj = "O_proc pa" in co2sobj_deleteshm, simp) |
|
50 apply (frule vd_cons, frule_tac p = pa in current_proc_has_sp, simp, erule exE) |
|
51 apply (auto dest!:current_proc_has_sp' current_has_sec' current_shm_has_sh' |
|
52 split:t_object.splits option.splits if_splits dest:flag_of_proc_shm_prop1 |
|
53 simp:co2sobj.simps tainted_eq_Tainted cp2sproc_deleteshm) |
|
54 done |
|
55 |
|
56 lemma s2ss_deleteshm: |
|
57 "valid (DeleteShM p h # s) \<Longrightarrow> s2ss (DeleteShM p h # s) = |
|
58 (case ch2sshm s h of |
|
59 Some sh \<Rightarrow> del_s2ss_obj s |
|
60 (update_s2ss_procs s (s2ss s) (DeleteShM p h) {p'| p' flag. (p', flag) \<in> procs_of_shm s h}) |
|
61 (O_shm h) (S_shm sh) |
|
62 | _ \<Rightarrow> {})" |
|
63 apply (frule vt_grant_os, frule vd_cons) |
|
64 apply (case_tac "ch2sshm s h") |
|
65 apply (drule current_shm_has_sh', simp, simp) |
|
66 apply (simp add:del_s2ss_obj_def) |
|
67 apply (tactic {*my_clarify_tac 1*}) |
|
68 |
|
69 unfolding update_s2ss_procs_def |
|
70 apply (tactic {*my_seteq_tac 1*}) |
|
71 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
72 apply (case_tac "\<exists> flag. (pa, flag) \<in> procs_of_shm s h") |
|
73 apply (erule exE, rule DiffI, rule UnI2, simp) |
|
74 apply (rule_tac x = pa in exI, simp, rule_tac x = flag in exI, simp) |
|
75 apply (rule notI, drule_tac p = pa in unbked_sps_D, simp) |
|
76 apply (rule_tac x = flag in exI, simp, simp) |
|
77 apply (rule DiffI, rule UnI1, simp) |
|
78 apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm split:option.splits) |
|
79 apply (simp add:cp2sproc_deleteshm split:option.splits if_splits) |
|
80 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
|
81 apply (drule current_has_sec', simp, simp) |
|
82 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
|
83 apply (drule flag_of_proc_shm_prop1, simp, simp) |
|
84 apply (drule flag_of_proc_shm_prop1, simp, simp) |
|
85 apply (rule notI, drule_tac p = pa in unbked_sps_D', simp+) |
|
86 apply (simp add:co2sobj_proc_deleteshm) |
|
87 apply (simp add:co2sobj_proc_deleteshm) |
|
88 apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_file_simps) |
|
89 apply (erule unbked_sps_I, simp) |
|
90 apply (rule DiffI,rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm) |
|
91 apply (erule unbked_sps_I, simp) |
|
92 apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_dir_simps) |
|
93 apply (erule unbked_sps_I, simp) |
|
94 apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm) |
|
95 apply (erule unbked_sps_I, simp) |
|
96 |
|
97 apply (erule DiffE, erule UnE) |
|
98 apply (tactic {*my_setiff_tac 1*}) |
|
99 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
100 apply (case_tac "\<exists> flag. (pa, flag) \<in> procs_of_shm s h", erule exE) |
|
101 apply (drule_tac p = pa in not_unbked_sps_D, simp) |
|
102 apply (rule_tac x = flag in exI, simp) |
|
103 apply (simp, erule disjE, clarsimp) |
|
104 apply (rule_tac x = "O_proc p'" in exI, simp add:procs_of_shm_prop2) |
|
105 apply (erule bexE, simp, (erule conjE)+) |
|
106 apply (frule_tac pa = p' in co2sobj_proc_deleteshm, simp+) |
|
107 apply (rule_tac x = "O_proc p'" in exI, simp) |
|
108 apply (frule_tac pa = pa in co2sobj_proc_deleteshm, simp+) |
|
109 apply (rule_tac x = "O_proc pa" in exI, simp) |
|
110 apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_file_simps) |
|
111 apply (frule_tac co2sobj_sshm_imp, erule exE) |
|
112 apply (case_tac "ha = h") |
|
113 apply (rule_tac x = obj' in exI, simp add:co2sobj_deleteshm) |
|
114 apply (simp add:co2sobj.simps) |
|
115 apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm) |
|
116 apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_dir_simps) |
|
117 apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm) |
|
118 apply (tactic {*my_setiff_tac 1*}, clarsimp) |
|
119 apply (rule_tac x = "O_proc pa" in exI, simp add:procs_of_shm_prop2) |
|
120 |
|
121 apply (tactic {*my_clarify_tac 1*}) |
|
122 unfolding update_s2ss_procs_def |
|
123 apply (tactic {*my_seteq_tac 1*}) |
|
124 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
125 apply (case_tac "\<exists> flag. (pa, flag) \<in> procs_of_shm s h") |
|
126 apply (erule exE, rule DiffI, rule DiffI, rule UnI2, simp) |
|
127 apply (rule_tac x = pa in exI, simp, rule_tac x = flag in exI, simp) |
|
128 apply (rule notI, drule_tac p = pa in unbked_sps_D, simp) |
|
129 apply (rule_tac x = flag in exI, simp, simp) |
|
130 apply (rule notI, simp add:co2sobj.simps split:option.splits) |
|
131 apply (rule DiffI, rule DiffI, rule UnI1, simp) |
|
132 apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm split:option.splits) |
|
133 apply (simp add:cp2sproc_deleteshm split:option.splits if_splits) |
|
134 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
|
135 apply (drule current_has_sec', simp, simp) |
|
136 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
|
137 apply (drule flag_of_proc_shm_prop1, simp, simp) |
|
138 apply (drule flag_of_proc_shm_prop1, simp, simp) |
|
139 apply (rule notI, drule_tac p = pa in unbked_sps_D', simp+) |
|
140 apply (simp add:co2sobj_proc_deleteshm) |
|
141 apply (simp add:co2sobj_proc_deleteshm) |
|
142 apply (rule notI, simp add:co2sobj.simps split:option.splits) |
|
143 apply (rule DiffI, rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_file_simps) |
|
144 apply (erule unbked_sps_I, simp, rule notI, simp add:co2sobj.simps) |
|
145 apply (case_tac "ha = h", simp) |
|
146 apply (rule DiffI, rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm) |
|
147 apply (erule unbked_sps_I, simp) |
|
148 apply (rule notI, simp add:co2sobj_deleteshm, erule_tac x = "O_shm ha" in allE, simp) |
|
149 apply (rule DiffI, rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_dir_simps) |
|
150 apply (erule unbked_sps_I, simp, rule notI, simp add:co2sobj.simps split:option.splits) |
|
151 apply (rule DiffI, rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm) |
|
152 apply (erule unbked_sps_I, simp, rule notI, simp add:co2sobj.simps split:option.splits) |
|
153 |
|
154 apply (erule DiffE, erule DiffE, erule UnE) |
|
155 apply (tactic {*my_setiff_tac 1*}) |
|
156 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
157 apply (case_tac "\<exists> flag. (pa, flag) \<in> procs_of_shm s h", erule exE) |
|
158 apply (drule_tac p = pa in not_unbked_sps_D, simp) |
|
159 apply (rule_tac x = flag in exI, simp) |
|
160 apply (simp, erule disjE, clarsimp) |
|
161 apply (rule_tac x = "O_proc p'" in exI, simp add:procs_of_shm_prop2) |
|
162 apply (erule bexE, simp, (erule conjE)+) |
|
163 apply (frule_tac pa = p' in co2sobj_proc_deleteshm, simp+) |
|
164 apply (rule_tac x = "O_proc p'" in exI, simp) |
|
165 apply (frule_tac pa = pa in co2sobj_proc_deleteshm, simp+) |
|
166 apply (rule_tac x = "O_proc pa" in exI, simp) |
|
167 apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_file_simps) |
|
168 apply (case_tac "ha = h", simp add:co2sobj.simps) |
|
169 apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm) |
|
170 apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_dir_simps) |
|
171 apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm) |
|
172 apply (tactic {*my_setiff_tac 1*}, clarsimp) |
|
173 apply (rule_tac x = "O_proc pa" in exI, simp add:procs_of_shm_prop2) |
|
174 done |
|
175 |
|
176 lemma s2ss_detach: |
|
177 "valid (Detach p h # s) \<Longrightarrow> s2ss (Detach p h # s) = ( |
|
178 case (cp2sproc s p, cp2sproc (Detach p h # s) p) of |
|
179 (Some sp, Some sp') \<Rightarrow> update_s2ss_obj s (s2ss s) (O_proc p) |
|
180 (S_proc sp (O_proc p \<in> Tainted s)) (S_proc sp' (O_proc p \<in> Tainted s)) |
|
181 | _ \<Rightarrow> {} )" |
|
182 apply (frule vd_cons, frule vt_grant_os) |
|
183 apply (case_tac "cp2sproc s p") |
|
184 apply (drule current_proc_has_sp', simp+) |
|
185 apply (case_tac "cp2sproc (Detach p h # s) p") |
|
186 apply (drule current_proc_has_sp', simp+) |
|
187 apply (erule exE|erule conjE)+ |
|
188 apply (simp add:update_s2ss_obj_def) |
|
189 apply (tactic {*my_clarify_tac 1*}) |
|
190 |
|
191 apply (tactic {*my_seteq_tac 1*}) |
|
192 apply (case_tac "obj = O_proc p") |
|
193 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted) |
|
194 apply (rule disjI2, simp, rule_tac x = obj in exI) |
|
195 apply (frule_tac obj = obj in co2sobj_detach, simp add:alive_simps) |
|
196 apply (simp add:is_file_simps is_dir_simps split:t_object.splits) |
|
197 apply (simp add:co2sobj.simps, simp add:co2sobj.simps) |
|
198 apply (tactic {*my_setiff_tac 1*}) |
|
199 apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) |
|
200 apply (tactic {*my_setiff_tac 1*}) |
|
201 apply (case_tac "obj = O_proc p") |
|
202 apply (rule_tac x = obj' in exI) |
|
203 apply (frule_tac obj = obj' in co2sobj_detach, simp) |
|
204 apply (auto simp add:co2sobj.simps tainted_eq_Tainted is_file_simps is_dir_simps split:t_object.splits)[1] |
|
205 apply (rule_tac x = obj in exI) |
|
206 apply (simp add:co2sobj_detach) |
|
207 apply (auto simp add:co2sobj.simps tainted_eq_Tainted is_file_simps is_dir_simps split:t_object.splits)[1] |
|
208 |
|
209 apply (tactic {*my_clarify_tac 1*}) |
|
210 apply (tactic {*my_seteq_tac 1*}) |
|
211 apply (case_tac "obj = O_proc p") |
|
212 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted) |
|
213 apply (rule disjI2, rule DiffI, simp, rule_tac x = obj in exI) |
|
214 apply (frule_tac obj = obj in co2sobj_detach, simp add:alive_simps) |
|
215 apply (simp add:is_file_simps is_dir_simps split:t_object.splits) |
|
216 apply (simp add:co2sobj.simps, simp add:co2sobj.simps) |
|
217 apply (rule notI, simp, erule_tac x = obj in allE, erule impE, simp add:alive_simps, simp) |
|
218 apply (frule_tac obj = obj in co2sobj_detach) |
|
219 apply (simp add:alive_simps) |
|
220 apply (simp split:t_object.splits) |
|
221 apply (tactic {*my_setiff_tac 1*}) |
|
222 apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) |
|
223 apply (tactic {*my_setiff_tac 1*}, simp) |
|
224 apply (case_tac "obj = O_proc p") |
|
225 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
|
226 apply (rule_tac x = obj in exI) |
|
227 apply (simp add:co2sobj_detach) |
|
228 apply (auto simp add:co2sobj.simps tainted_eq_Tainted is_file_simps is_dir_simps split:t_object.splits)[1] |
|
229 done |
|
230 |
|
231 definition attach_Tainted_procs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm \<Rightarrow> t_shm_attach_flag \<Rightarrow> t_process set" |
|
232 where |
|
233 "attach_Tainted_procs s p h flag \<equiv> |
|
234 (if (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR) |
|
235 then {p''. \<exists> p' flag'. (p', flag') \<in> procs_of_shm s h \<and> info_flow_shm s p' p'' \<and> |
|
236 O_proc p'' \<notin> Tainted s} |
|
237 else if (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h) |
|
238 then {p'. info_flow_shm s p p' \<and> O_proc p' \<notin> Tainted s} |
|
239 else {})" |
|
240 |
|
241 lemma attach_Tainted_procs_prop1: |
|
242 "valid s \<Longrightarrow> Tainted (Attach p h flag # s) = Tainted s \<union> {O_proc p' | p'. p' \<in> attach_Tainted_procs s p h flag}" |
|
243 apply (auto simp:attach_Tainted_procs_def intro:info_flow_shm_Tainted) |
|
244 done |
|
245 |
|
246 lemma attach_Tainted_procs_prop2: |
|
247 "valid (Attach p h flag # s) \<Longrightarrow> {O_proc p'| p'. p' \<in> attach_Tainted_procs s p h flag} \<inter> Tainted s = {}" |
|
248 by (auto simp:attach_Tainted_procs_def) |
|
249 |
|
250 lemma attach_Tainted_procs_prop3: |
|
251 "\<lbrakk>p' \<in> attach_Tainted_procs s p h flag; valid s\<rbrakk> \<Longrightarrow> p' \<in> current_procs s" |
|
252 by (auto simp:attach_Tainted_procs_def info_shm_flow_in_procs split:if_splits) |
|
253 |
|
254 lemma co2sobj_attach': |
|
255 "\<lbrakk>valid (Attach p h flag # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj = |
|
256 (case obj of |
|
257 O_proc p' \<Rightarrow> if (p' = p) |
|
258 then (case cp2sproc (Attach p h flag # s) p of |
|
259 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> p \<in> attach_Tainted_procs s p h flag)) |
|
260 | _ \<Rightarrow> None) |
|
261 else if (p' \<in> attach_Tainted_procs s p h flag) |
|
262 then case cp2sproc s p' of |
|
263 None \<Rightarrow> None |
|
264 | Some sp \<Rightarrow> Some (S_proc sp True) |
|
265 else co2sobj s obj |
|
266 | _ \<Rightarrow> co2sobj s obj)" |
|
267 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
268 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted co2sobj.simps) |
|
269 |
|
270 apply (frule current_proc_has_sp, simp, erule exE, (erule conjE)+) |
|
271 apply (case_tac "cp2sproc (Attach p h flag # s) nat", drule current_proc_has_sp', simp+) |
|
272 apply (case_tac "cp2sproc (Attach p h flag # s) p", drule current_proc_has_sp', simp+) |
|
273 apply (simp add:tainted_eq_Tainted attach_Tainted_procs_prop1 del:Tainted.simps) |
|
274 apply (simp add:cp2sproc_attach split:if_splits) |
|
275 |
|
276 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' |
|
277 simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted |
|
278 same_inode_files_prop6 |
|
279 dest:is_file_in_current is_dir_in_current) |
|
280 done |
|
281 |
|
282 lemma s2ss_attach: |
|
283 "valid (Attach p h flag # s) \<Longrightarrow> s2ss (Attach p h flag # s) = |
|
284 update_s2ss_procs s (s2ss s) (Attach p h flag) (attach_Tainted_procs s p h flag \<union> {p})" |
|
285 apply (frule vt_grant_os, frule vd_cons) |
|
286 apply (case_tac "cp2sproc s p", drule current_proc_has_sp', simp, simp) |
|
287 apply (case_tac "ch2sshm s h", drule current_shm_has_sh', simp, simp) |
|
288 apply (case_tac "cp2sproc (Attach p h flag # s) p", drule current_proc_has_sp', simp, simp) |
|
289 |
|
290 unfolding update_s2ss_procs_def |
|
291 apply (tactic {*my_seteq_tac 1*}) |
|
292 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
293 apply (case_tac "pa = p") |
|
294 apply (rule DiffI, rule UnI2, simp, rule_tac x = pa in exI, simp) |
|
295 apply (rule notI, drule_tac p = pa in unbked_sps_D, simp, simp) |
|
296 apply (case_tac "pa \<in> attach_Tainted_procs s p h flag") |
|
297 apply (rule DiffI, rule UnI2, simp) |
|
298 apply (rule_tac x = pa in exI, simp) |
|
299 apply (rule notI, drule_tac p = pa in unbked_sps_D, simp, simp) |
|
300 apply (rule DiffI, rule UnI1, simp) |
|
301 apply (rule_tac x = obj in exI, simp add:co2sobj_attach') |
|
302 apply (rule notI, drule_tac p = pa in unbked_sps_D', simp+) |
|
303 apply (simp add:co2sobj_attach') |
|
304 apply (simp add:co2sobj_attach') |
|
305 apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach' is_file_simps) |
|
306 apply (erule unbked_sps_I, simp) |
|
307 apply (rule DiffI,rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach') |
|
308 apply (erule unbked_sps_I, simp) |
|
309 apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach' is_dir_simps) |
|
310 apply (erule unbked_sps_I, simp) |
|
311 apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach') |
|
312 apply (erule unbked_sps_I, simp) |
|
313 |
|
314 apply (erule DiffE, erule UnE) |
|
315 apply (tactic {*my_setiff_tac 1*}) |
|
316 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
317 apply (case_tac "pa \<in> attach_Tainted_procs s p h flag \<union> {p}") |
|
318 apply (drule_tac p = pa in not_unbked_sps_D, simp, simp) |
|
319 apply (erule disjE, erule bexE) |
|
320 apply (rule_tac x = "O_proc p'" in exI, simp) |
|
321 apply (erule disjE, simp, simp add:attach_Tainted_procs_prop3) |
|
322 apply (erule bexE, simp, (erule conjE)+) |
|
323 apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_attach') |
|
324 apply (rule_tac x = "O_proc pa" in exI, simp add:co2sobj_attach') |
|
325 apply (rule_tac x = obj in exI, simp add:co2sobj_attach' is_file_simps) |
|
326 apply (rule_tac x = obj in exI, simp add:co2sobj_attach') |
|
327 apply (rule_tac x = obj in exI, simp add:co2sobj_attach' is_dir_simps) |
|
328 apply (rule_tac x = obj in exI, simp add:co2sobj_attach') |
|
329 apply (tactic {*my_setiff_tac 1*}, clarsimp) |
|
330 apply (rule_tac x = "O_proc pa" in exI, simp) |
|
331 apply (erule disjE, simp, simp add:attach_Tainted_procs_prop3) |
|
332 done |
|
333 |
|
334 |
|
335 (* should be modified when socket is model in static *) |
|
336 lemma s2ss_createsock: |
|
337 "valid (CreateSock p af st fd inum # s) \<Longrightarrow> s2ss (CreateSock p af st fd inum # s) = s2ss s" |
|
338 apply (simp add:s2ss_def) |
|
339 apply (tactic {*my_seteq_tac 1*}) |
|
340 apply (rule_tac x = obj in exI) |
|
341 apply (simp add:co2sobj_other) |
|
342 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
343 apply (tactic {*my_setiff_tac 1*}) |
|
344 apply (rule_tac x = obj in exI) |
|
345 apply (frule_tac obj = obj in co2sobj_other) |
|
346 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
347 done |
|
348 |
|
349 lemma s2ss_bind: |
|
350 "valid (Bind p fd addr # s) \<Longrightarrow> s2ss (Bind p fd addr # s) = s2ss s" |
|
351 apply (simp add:s2ss_def) |
|
352 apply (tactic {*my_seteq_tac 1*}) |
|
353 apply (rule_tac x = obj in exI) |
|
354 apply (simp add:co2sobj_other) |
|
355 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
356 apply (tactic {*my_setiff_tac 1*}) |
|
357 apply (rule_tac x = obj in exI) |
|
358 apply (frule_tac obj = obj in co2sobj_other) |
|
359 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
360 done |
|
361 |
|
362 lemma s2ss_connect: |
|
363 "valid (Connect p fd addr # s) \<Longrightarrow> s2ss (Connect p fd addr # s) = s2ss s" |
|
364 apply (simp add:s2ss_def) |
|
365 apply (tactic {*my_seteq_tac 1*}) |
|
366 apply (rule_tac x = obj in exI) |
|
367 apply (simp add:co2sobj_other) |
|
368 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
369 apply (tactic {*my_setiff_tac 1*}) |
|
370 apply (rule_tac x = obj in exI) |
|
371 apply (frule_tac obj = obj in co2sobj_other) |
|
372 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
373 done |
|
374 |
|
375 lemma s2ss_listen: |
|
376 "valid (Listen p fd # s) \<Longrightarrow> s2ss (Listen p fd # s) = s2ss s" |
|
377 apply (simp add:s2ss_def) |
|
378 apply (tactic {*my_seteq_tac 1*}) |
|
379 apply (rule_tac x = obj in exI) |
|
380 apply (simp add:co2sobj_other) |
|
381 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
382 apply (tactic {*my_setiff_tac 1*}) |
|
383 apply (rule_tac x = obj in exI) |
|
384 apply (frule_tac obj = obj in co2sobj_other) |
|
385 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
386 done |
|
387 |
|
388 lemma s2ss_accept: |
|
389 "valid (Accept p fd addr port fd' inum # s) \<Longrightarrow> s2ss (Accept p fd addr port fd' inum # s) = s2ss s" |
|
390 apply (simp add:s2ss_def) |
|
391 apply (tactic {*my_seteq_tac 1*}) |
|
392 apply (rule_tac x = obj in exI) |
|
393 apply (simp add:co2sobj_other) |
|
394 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
395 apply (tactic {*my_setiff_tac 1*}) |
|
396 apply (rule_tac x = obj in exI) |
|
397 apply (frule_tac obj = obj in co2sobj_other) |
|
398 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
399 done |
|
400 |
|
401 lemma s2ss_send: |
|
402 "valid (SendSock p fd # s) \<Longrightarrow> s2ss (SendSock p fd # s) = s2ss s" |
|
403 apply (simp add:s2ss_def) |
|
404 apply (tactic {*my_seteq_tac 1*}) |
|
405 apply (rule_tac x = obj in exI) |
|
406 apply (simp add:co2sobj_other) |
|
407 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
408 apply (tactic {*my_setiff_tac 1*}) |
|
409 apply (rule_tac x = obj in exI) |
|
410 apply (frule_tac obj = obj in co2sobj_other) |
|
411 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
412 done |
|
413 |
|
414 lemma s2ss_recv: |
|
415 "valid (RecvSock p fd # s) \<Longrightarrow> s2ss (RecvSock p fd # s) = s2ss s" |
|
416 apply (simp add:s2ss_def) |
|
417 apply (tactic {*my_seteq_tac 1*}) |
|
418 apply (rule_tac x = obj in exI) |
|
419 apply (simp add:co2sobj_other) |
|
420 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
421 apply (tactic {*my_setiff_tac 1*}) |
|
422 apply (rule_tac x = obj in exI) |
|
423 apply (frule_tac obj = obj in co2sobj_other) |
|
424 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
425 done |
|
426 |
|
427 lemma s2ss_shutdown: |
|
428 "valid (Shutdown p fd how # s) \<Longrightarrow> s2ss (Shutdown p fd how # s) = s2ss s" |
|
429 apply (simp add:s2ss_def) |
|
430 apply (tactic {*my_seteq_tac 1*}) |
|
431 apply (rule_tac x = obj in exI) |
|
432 apply (simp add:co2sobj_other) |
|
433 apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
434 apply (tactic {*my_setiff_tac 1*}) |
|
435 apply (rule_tac x = obj in exI) |
|
436 apply (frule_tac obj = obj in co2sobj_other) |
|
437 apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits) |
|
438 done |
|
439 |
|
440 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open |
|
441 s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard |
|
442 s2ss_truncate s2ss_createmsgq s2ss_sendmsg s2ss_removemsgq s2ss_recvmsg |
|
443 s2ss_createshm s2ss_detach s2ss_deleteshm s2ss_attach |
|
444 s2ss_createsock s2ss_bind s2ss_connect s2ss_listen s2ss_accept s2ss_send |
|
445 s2ss_recv s2ss_shutdown |
|
446 |
|
447 end |
|
448 |
|
449 end |