20 |
20 |
21 lemma d2s_main': |
21 lemma d2s_main': |
22 "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)" |
22 "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)" |
23 by (simp add:s2ss_def, rule_tac x = obj in exI, simp) |
23 by (simp add:s2ss_def, rule_tac x = obj in exI, simp) |
24 |
24 |
25 lemma alive_has_sobj: |
25 lemma tainted_has_sobj: |
26 "\<lbrakk>alive s obj; valid s\<rbrakk> \<Longrightarrow> \<exists> sobj. co2sobj s obj = Some sobj" |
26 "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> \<exists> sobj. co2sobj s obj = Some sobj" |
27 sorry |
27 sorry |
28 |
28 |
29 lemma t2ts: |
29 lemma t2ts: |
30 "obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj" |
30 "obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj" |
31 apply (frule tainted_in_current, frule tainted_is_valid) |
31 apply (frule tainted_in_current, frule tainted_is_valid) |
35 apply (rule_tac x = "O_proc nat" in exI, simp) |
35 apply (rule_tac x = "O_proc nat" in exI, simp) |
36 apply (rule_tac x = "O_file list" in exI, simp) |
36 apply (rule_tac x = "O_file list" in exI, simp) |
37 apply (drule dir_not_tainted, simp) |
37 apply (drule dir_not_tainted, simp) |
38 apply (drule msgq_not_tainted, simp) |
38 apply (drule msgq_not_tainted, simp) |
39 apply (drule shm_not_tainted, simp) |
39 apply (drule shm_not_tainted, simp) |
40 apply (case_tac prod1, simp, case_tac prod2, clarsimp) |
40 done |
41 apply (rule conjI) |
|
42 apply (rule_tac x = "O_msgq nat1" in exI, simp) |
|
43 apply (rule conjI) defer |
|
44 apply (simp add:cm2smsg_def split:option.splits) |
|
45 sorry |
|
46 |
41 |
47 lemma delq_imp_delqm: |
42 lemma delq_imp_delqm: |
48 "deleted (O_msgq q) s \<Longrightarrow> deleted (O_msg q m) s" |
43 "deleted (O_msgq q) s \<Longrightarrow> deleted (O_msg q m) s" |
49 apply (induct s, simp) |
44 apply (induct s, simp) |
50 by (case_tac a, auto) |
45 by (case_tac a, auto) |
55 proof- |
50 proof- |
56 from tbl obtain s where tainted: "obj \<in> tainted s" |
51 from tbl obtain s where tainted: "obj \<in> tainted s" |
57 by (auto simp:taintable_def) |
52 by (auto simp:taintable_def) |
58 hence vs: "valid s" by (simp add:tainted_is_valid) |
53 hence vs: "valid s" by (simp add:tainted_is_valid) |
59 hence static: "s2ss s \<in> static" using d2s_main by auto |
54 hence static: "s2ss s \<in> static" using d2s_main by auto |
60 from tainted have alive: "alive s obj" |
55 from tainted obtain sobj where sobj: "co2sobj s obj = Some sobj" |
61 using tainted_in_current by auto |
56 using vs tainted_has_sobj by blast |
62 then obtain sobj where sobj: "co2sobj s obj = Some sobj" |
|
63 using vs alive_has_sobj by blast |
|
64 from undel vs have "\<not> deleted obj s" and init_alive: "init_alive obj" |
57 from undel vs have "\<not> deleted obj s" and init_alive: "init_alive obj" |
65 by (auto simp:undeletable_def) |
58 by (auto simp:undeletable_def) |
66 with vs sobj have "init_obj_related sobj obj" |
59 with vs sobj have "init_obj_related sobj obj" |
67 apply (case_tac obj, case_tac [!] sobj) |
60 apply (case_tac obj, case_tac [!] sobj) |
68 apply (auto split:option.splits if_splits simp:cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm) |
61 apply (auto split:option.splits if_splits simp:cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm) |
69 apply (frule not_deleted_init_file, simp+) (* |
62 apply (frule not_deleted_init_file, simp+) |
70 apply (drule is_file_has_sfile, erule exE) |
63 apply (drule is_file_has_sfile', simp, erule exE) |
71 apply (rule_tac x = sf in bexI) |
64 apply (rule_tac x = sf in bexI) |
72 apply (case_tac list, auto split:option.splits simp:is_init_file_props)[1] |
65 apply (case_tac list, auto split:option.splits simp:is_init_file_props)[1] |
73 apply (simp add:same_inode_files_def cfs2sfiles_def) *) |
66 apply (drule root_is_init_dir', simp) |
74 sorry |
67 apply (frule not_deleted_init_file, simp, simp) |
|
68 apply (simp add:cf2sfile_def split:option.splits if_splits) |
|
69 apply (simp add:cf2sfiles_def) |
|
70 apply (rule_tac x = list in bexI, simp, simp add:same_inode_files_def not_deleted_init_file) |
|
71 |
|
72 apply (frule not_deleted_init_dir, simp+) |
|
73 apply (simp add:cf2sfile_def split:option.splits if_splits) |
|
74 apply (case_tac list, simp add:sroot_def, simp) |
|
75 apply (drule file_dir_conflict, simp+) |
|
76 done |
75 with tainted t2ts init_alive sobj static |
77 with tainted t2ts init_alive sobj static |
76 show ?thesis unfolding taintable_s_def |
78 show ?thesis unfolding taintable_s_def |
77 apply (rule_tac x = "s2ss s" in bexI, simp) |
79 apply (rule_tac x = "s2ss s" in bexI, simp) |
78 apply (rule_tac x = "sobj" in exI, auto) |
80 apply (rule_tac x = "sobj" in exI, auto) |
79 done |
81 done |
187 by auto |
189 by auto |
188 |
190 |
189 lemma cqm2sms_prop1: |
191 lemma cqm2sms_prop1: |
190 "\<lbrakk>cqm2sms s q queue = Some sms; sm \<in> set sms\<rbrakk> \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm" |
192 "\<lbrakk>cqm2sms s q queue = Some sms; sm \<in> set sms\<rbrakk> \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm" |
191 apply (induct queue arbitrary:sms) |
193 apply (induct queue arbitrary:sms) |
192 apply (auto split:option.splits) |
194 apply (auto simp:cqm2sms.simps split:option.splits) |
193 done |
195 done |
194 |
196 |
195 lemma sq_sm_prop: |
197 lemma sq_sm_prop: |
196 "\<lbrakk>sm \<in> set sms; cq2smsgq s q = Some (qi, qsec, sms); valid s\<rbrakk> |
198 "\<lbrakk>sm \<in> set sms; cq2smsgq s q = Some (qi, qsec, sms); valid s\<rbrakk> |
197 \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm" |
199 \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm" |
214 apply (case_tac prod1, case_tac prod2, simp) |
216 apply (case_tac prod1, case_tac prod2, simp) |
215 apply ((erule conjE)+, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) |
217 apply ((erule conjE)+, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) |
216 apply (case_tac obj, simp_all split:option.splits if_splits) |
218 apply (case_tac obj, simp_all split:option.splits if_splits) |
217 apply (drule_tac sm = "(aa, ba, True)" in sq_sm_prop, simp+, erule exE) |
219 apply (drule_tac sm = "(aa, ba, True)" in sq_sm_prop, simp+, erule exE) |
218 apply (rule_tac x = "O_msg nat m" in exI) |
220 apply (rule_tac x = "O_msg nat m" in exI) |
219 apply (simp add:cm2smsg_def split:option.splits) |
221 apply (rule conjI) |
|
222 apply simp |
|
223 apply (simp add |
|
224 apply (simp add:co2sobj.simps) |
|
225 apply (simp add:cm2smsg_def split:option.splits if_splits) |
220 done |
226 done |
221 |
227 |
222 lemma has_inode_tainted_aux: |
228 lemma has_inode_tainted_aux: |
223 "O_file f \<in> tainted s \<Longrightarrow> \<forall> f'. has_same_inode s f f' \<longrightarrow> O_file f' \<in> tainted s" |
229 "O_file f \<in> tainted s \<Longrightarrow> \<forall> f'. has_same_inode s f f' \<longrightarrow> O_file f' \<in> tainted s" |
224 apply (erule tainted.induct) |
230 apply (erule tainted.induct) |