53 |
53 |
54 |
54 |
55 sorry |
55 sorry |
56 |
56 |
57 |
57 |
58 lemma tainted_has_sobj: |
|
59 "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> \<exists> sobj. co2sobj s obj = Some sobj" |
|
60 apply (frule tainted_in_current, case_tac obj) |
|
61 apply (auto dest:valid_tainted_obj simp:co2sobj.simps split:option.splits) |
|
62 oops |
|
63 |
|
64 lemma t2ts: |
58 lemma t2ts: |
65 "obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj" |
59 "obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj" |
66 apply (frule tainted_in_current, frule tainted_is_valid) |
60 apply (frule tainted_in_current, frule tainted_is_valid) |
67 apply (frule d2s_main', simp) |
61 apply (frule s2ss_included_sobj, simp) |
68 apply (case_tac sobj, simp_all) |
62 apply (case_tac sobj, simp_all) |
69 apply (case_tac [!] obj, simp_all add:co2sobj.simps split:option.splits if_splits) |
63 apply (case_tac [!] obj, simp_all add:co2sobj.simps split:option.splits if_splits) |
70 apply (drule dir_not_tainted, simp) |
64 apply (drule dir_not_tainted, simp) |
71 apply (drule msgq_not_tainted, simp) |
65 apply (drule msgq_not_tainted, simp) |
72 apply (drule shm_not_tainted, simp) |
66 apply (drule shm_not_tainted, simp) |
89 proof- |
83 proof- |
90 from tbl obtain s where tainted: "obj \<in> tainted s" |
84 from tbl obtain s where tainted: "obj \<in> tainted s" |
91 by (auto simp:taintable_def) |
85 by (auto simp:taintable_def) |
92 hence vs: "valid s" by (simp add:tainted_is_valid) |
86 hence vs: "valid s" by (simp add:tainted_is_valid) |
93 hence static: "s2ss s \<propto> static" using d2s_main by auto |
87 hence static: "s2ss s \<propto> static" using d2s_main by auto |
94 from tainted obtain sobj where sobj: "co2sobj s obj = Some sobj" sorry |
88 from tainted tbl vs obtain sobj where sobj: "co2sobj s obj = Some sobj" |
95 (* should constrain undeletable with file/dir/process only, while msg and fd are excluded |
89 apply (clarsimp simp add:taintable_def) |
96 using vs tainted_has_sobj by blast *) |
90 apply (frule tainted_in_current) |
|
91 apply (case_tac obj, simp_all add:co2sobj.simps) |
|
92 apply (frule current_proc_has_sp, simp, auto) |
|
93 done |
97 from undel vs have "\<not> deleted obj s" and init_alive: "init_alive obj" |
94 from undel vs have "\<not> deleted obj s" and init_alive: "init_alive obj" |
98 by (auto simp:undeletable_def) |
95 by (auto simp:undeletable_def) |
99 with vs sobj have "init_obj_related sobj obj" |
96 with vs sobj have "init_obj_related sobj obj" |
100 apply (case_tac obj, case_tac [!] sobj) |
97 apply (case_tac obj, case_tac [!] sobj) |
101 apply (auto split:option.splits if_splits simp:co2sobj.simps cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm) |
98 apply (auto split:option.splits if_splits simp:co2sobj.simps cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm) |
180 apply auto |
177 apply auto |
181 apply (rule_tac x = "(Init list, (aa, ab, b), ac, ba)" in bexI) |
178 apply (rule_tac x = "(Init list, (aa, ab, b), ac, ba)" in bexI) |
182 apply auto |
179 apply auto |
183 done |
180 done |
184 |
181 |
|
182 lemma init_related_imp_init_sobj: |
|
183 "init_obj_related sobj obj \<Longrightarrow> is_init_sobj sobj" |
|
184 apply (case_tac sobj, case_tac [!] obj, auto) |
|
185 apply (rule_tac x = "(Init list, (aa, ab, b), ac, ba)" in bexI, auto) |
|
186 done |
|
187 |
185 theorem undeletable_s_complete: |
188 theorem undeletable_s_complete: |
186 assumes undel_s: "undeletable_s obj" |
189 assumes undel_s: "undeletable_s obj" |
187 shows "undeletable obj" |
190 shows "undeletable obj" |
188 proof- |
191 proof- |
189 from undel_s have init_alive: "init_alive obj" |
192 from undel_s have init_alive: "init_alive obj" |
193 proof |
196 proof |
194 assume "\<exists> s. valid s \<and> deleted obj s" |
197 assume "\<exists> s. valid s \<and> deleted obj s" |
195 then obtain s where vs: "valid s" and del: "deleted obj s" by auto |
198 then obtain s where vs: "valid s" and del: "deleted obj s" by auto |
196 from vs have vss: "s2ss s \<propto> static" by (rule d2s_main) |
199 from vs have vss: "s2ss s \<propto> static" by (rule d2s_main) |
197 with alive_s obtain sobj where in_ss: "sobj \<in> (s2ss s)" |
200 with alive_s obtain sobj where in_ss: "sobj \<in> (s2ss s)" |
198 and related: "init_obj_related sobj obj" apply auto |
201 and related: "init_obj_related sobj obj" |
|
202 apply (simp add:init_ss_in_def init_ss_eq_def) |
|
203 apply (erule bexE, erule_tac x= ss' in ballE) |
|
204 apply (auto dest:init_related_imp_init_sobj) |
|
205 done |
199 from init_alive del vs have "deletable_s obj" |
206 from init_alive del vs have "deletable_s obj" |
200 by (auto elim:deleted_imp_deletable_s) |
207 by (auto elim:deleted_imp_deletable_s) |
201 with alive_s |
208 with alive_s |
202 show False by (auto simp:deletable_s_def) |
209 show False by (auto simp:deletable_s_def) |
203 qed |
210 qed |
208 theorem final_offer: |
215 theorem final_offer: |
209 "\<lbrakk>undeletable_s obj; \<not> taintable_s obj; init_alive obj\<rbrakk> \<Longrightarrow> \<not> taintable obj" |
216 "\<lbrakk>undeletable_s obj; \<not> taintable_s obj; init_alive obj\<rbrakk> \<Longrightarrow> \<not> taintable obj" |
210 apply (erule swap) |
217 apply (erule swap) |
211 by (simp add:static_complete undeletable_s_complete) |
218 by (simp add:static_complete undeletable_s_complete) |
212 |
219 |
213 |
|
214 |
|
215 (************** static \<rightarrow> dynamic ***************) |
220 (************** static \<rightarrow> dynamic ***************) |
216 |
|
217 lemma created_can_have_many: |
|
218 "\<lbrakk>valid s; alive s obj; \<not> init_alive obj\<rbrakk> \<Longrightarrow> \<exists> s'. valid s' \<and> alive s' obj \<and> alive s' obj' \<and> s2ss s = s2ss s'" |
|
219 sorry |
|
220 |
221 |
221 lemma s2d_main: |
222 lemma s2d_main: |
222 "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss" |
223 "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss" |
223 apply (erule static.induct) |
224 apply (erule static.induct) |
224 apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros) |
225 apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros) |
225 |
226 |
226 apply (erule exE|erule conjE)+ |
227 apply (erule exE|erule conjE)+ |
227 |
228 |
228 sorry |
229 sorry |
229 |
230 |
230 lemma tainted_s_in_ss: |
|
231 "tainted_s ss sobj \<Longrightarrow> sobj \<in> ss" |
|
232 apply (case_tac sobj, simp_all) |
|
233 apply (case_tac bool, simp+) |
|
234 apply (case_tac bool, simp+) |
|
235 apply (case_tac prod1, case_tac prod2, simp) |
|
236 thm tainted_s.simps |
|
237 oops |
|
238 |
|
239 lemma set_eq_D: |
231 lemma set_eq_D: |
240 "\<lbrakk>x \<in> S; {x. P x} = S\<rbrakk> \<Longrightarrow> P x" |
232 "\<lbrakk>x \<in> S; {x. P x} = S\<rbrakk> \<Longrightarrow> P x" |
241 by auto |
233 by auto |
242 |
234 |
243 lemma cqm2sms_prop1: |
235 lemma cqm2sms_prop1: |
248 |
240 |
249 lemma sq_sm_prop: |
241 lemma sq_sm_prop: |
250 "\<lbrakk>sm \<in> set sms; cq2smsgq s q = Some (qi, qsec, sms); valid s\<rbrakk> |
242 "\<lbrakk>sm \<in> set sms; cq2smsgq s q = Some (qi, qsec, sms); valid s\<rbrakk> |
251 \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm" |
243 \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm" |
252 by (auto simp:cq2smsgq_def split: option.splits intro:cqm2sms_prop1) |
244 by (auto simp:cq2smsgq_def split: option.splits intro:cqm2sms_prop1) |
|
245 |
|
246 declare co2sobj.simps [simp add] |
253 |
247 |
254 lemma tainted_s_imp_tainted: |
248 lemma tainted_s_imp_tainted: |
255 "\<lbrakk>tainted_s ss sobj; ss \<in> static\<rbrakk> \<Longrightarrow> \<exists> s obj. valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s" |
249 "\<lbrakk>tainted_s ss sobj; ss \<in> static\<rbrakk> \<Longrightarrow> \<exists> s obj. valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s" |
256 apply (drule s2d_main) |
250 apply (drule s2d_main) |
257 apply (erule exE, erule conjE, simp add:s2ss_def) |
251 apply (erule exE, erule conjE, simp add:s2ss_def) |
262 apply (case_tac obj, (simp split:option.splits if_splits)+) |
256 apply (case_tac obj, (simp split:option.splits if_splits)+) |
263 |
257 |
264 apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) |
258 apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) |
265 apply (rule_tac x = obj in exI, simp) |
259 apply (rule_tac x = obj in exI, simp) |
266 apply (case_tac obj, (simp split:option.splits if_splits)+) |
260 apply (case_tac obj, (simp split:option.splits if_splits)+) |
267 |
261 done |
268 apply (case_tac prod1, case_tac prod2, simp) |
262 |
269 apply ((erule conjE)+, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) |
263 lemma has_same_inode_prop3: |
270 apply (case_tac obj, simp_all split:option.splits if_splits) |
264 "has_same_inode s f f' \<Longrightarrow> has_same_inode s f' f" |
271 apply (drule_tac sm = "(aa, ba, True)" in sq_sm_prop, simp+, erule exE) |
265 by (auto simp:has_same_inode_def) |
272 apply (rule_tac x = "O_msg nat m" in exI) |
|
273 apply (rule conjI) |
|
274 apply simp |
|
275 apply (simp add |
|
276 apply (simp add:co2sobj.simps) |
|
277 apply (simp add:cm2smsg_def split:option.splits if_splits) |
|
278 done |
|
279 |
|
280 lemma has_inode_tainted_aux: |
|
281 "O_file f \<in> tainted s \<Longrightarrow> \<forall> f'. has_same_inode s f f' \<longrightarrow> O_file f' \<in> tainted s" |
|
282 apply (erule tainted.induct) |
|
283 apply (auto intro:tainted.intros simp:has_same_inode_def) |
|
284 (*?? need simpset for tainted *) |
|
285 sorry |
|
286 |
|
287 lemma has_same_inode_tainted: |
|
288 "\<lbrakk>has_same_inode s f f'; O_file f' \<in> tainted s\<rbrakk> \<Longrightarrow> O_file f \<in> tainted s" |
|
289 by (drule has_inode_tainted_aux, auto simp:has_same_inode_def) |
|
290 |
266 |
291 theorem static_sound: |
267 theorem static_sound: |
292 assumes tbl_s: "taintable_s obj" |
268 assumes tbl_s: "taintable_s obj" |
293 shows "taintable obj" |
269 shows "taintable obj" |
294 proof- |
270 proof- |
304 apply (case_tac obj', case_tac [!] obj) |
280 apply (case_tac obj', case_tac [!] obj) |
305 apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi) |
281 apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi) |
306 apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_def is_file_def is_dir_def |
282 apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_def is_file_def is_dir_def |
307 split:option.splits t_inode_tag.splits dest!:cf2sfile_fi) |
283 split:option.splits t_inode_tag.splits dest!:cf2sfile_fi) |
308 done |
284 done |
309 with tainted' have tainted: "obj \<in> tainted s" |
285 with tainted' vs have tainted: "obj \<in> tainted s" |
310 by (auto intro:has_same_inode_tainted) |
286 by (auto dest:has_same_inode_prop3 intro:has_same_inode_tainted) |
311 with vs init_alive |
287 from sobj related init_alive have "appropriate obj" |
|
288 by (case_tac obj, case_tac [!] sobj, auto) |
|
289 with vs init_alive tainted |
312 show ?thesis by (auto simp:taintable_def) |
290 show ?thesis by (auto simp:taintable_def) |
313 qed |
291 qed |
314 |
292 |
315 |
|
316 |
|
317 lemma ts2t: |
|
318 "obj \<in> tainted_s ss \<Longrightarrow> \<exists> s. obj \<in> tainted s" |
|
319 "obj \<in> tainted_s ss \<Longrightarrow> \<exists> so. so True \<in> ss \<Longrightarrow> so True \<in> ss \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss \<Longrightarrow> so True \<in> s2ss s \<Longrightarrow> tainted s obj. " |
|
320 |
|
321 |
|
322 |
|
323 |
|
324 end |
293 end |
|
294 |
|
295 end |