|
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 |
|
232 |
|
233 lemma s2ss_attach1: |
|
234 "\<lbrakk>valid (Attach p h SHM_RDWR # s); O_proc p \<in> Tainted s\<rbrakk>\<Longrightarrow> s2ss (Attach p h SHM_RDWR # s) = ( |
|
235 |
|
236 " |
|
237 |
|
238 lemma s2ss_attach1: |
|
239 "\<lbrakk>valid (Attach p h flag # s); O_proc p \<notin> Tainted s; (p', SHM_RDWR) \<in> procs_of_shm s; O_proc p' \<in> Tainted s\<rbrakk> |
|
240 \<Longrightarrow> s2ss (Attach p h SHM_RDONLY # s) = " |
|
241 |
|
242 lemma s2ss_attach1: |
|
243 "valid (Attach p h flag # s) \<Longrightarrow> s2ss (Attach p h flag # s) = " |
|
244 |
|
245 lemma s2ss_Detach: |
|
246 "valid (Detach p h # s) \<Longrightarrow> s2ss (Detach p h # s) = " |
|
247 |
|
248 |
|
249 |
|
250 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open |
|
251 s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard |
|
252 s2ss_truncate s2ss_createmsgq s2ss_sendmsg s2ss_removemsgq s2ss_recvmsg |
|
253 s2ss_createshm |
|
254 |
|
255 |
|
256 end |
|
257 |
|
258 end |