110 lemma init_deled_imp_deled_s: |
110 lemma init_deled_imp_deled_s: |
111 "\<lbrakk>deleted obj s; init_alive obj; sobj \<in> (s2ss s); valid s\<rbrakk> \<Longrightarrow> \<not> init_obj_related sobj obj" |
111 "\<lbrakk>deleted obj s; init_alive obj; sobj \<in> (s2ss s); valid s\<rbrakk> \<Longrightarrow> \<not> init_obj_related sobj obj" |
112 apply (rule notI) |
112 apply (rule notI) |
113 apply (clarsimp simp:s2ss_def) |
113 apply (clarsimp simp:s2ss_def) |
114 apply (case_tac obj, case_tac [!] obja, case_tac sobj) |
114 apply (case_tac obj, case_tac [!] obja, case_tac sobj) |
115 apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi) |
115 apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi) |
116 |
116 apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_prop1' is_file_def is_dir_def |
|
117 split:option.splits t_inode_tag.splits dest!:cf2sfile_fi) |
117 done |
118 done |
118 |
119 |
119 lemma deleted_imp_deletable_s: |
120 lemma deleted_imp_deletable_s: |
120 "\<lbrakk>deleted obj s; init_alive obj; valid s\<rbrakk> \<Longrightarrow> deletable_s obj" |
121 "\<lbrakk>deleted obj s; init_alive obj; valid s\<rbrakk> \<Longrightarrow> deletable_s obj" |
121 apply (simp add:deletable_s_def) |
122 apply (simp add:deletable_s_def) |
165 apply (erule static.induct) |
166 apply (erule static.induct) |
166 apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros) |
167 apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros) |
167 |
168 |
168 apply (erule exE|erule conjE)+ |
169 apply (erule exE|erule conjE)+ |
169 |
170 |
170 apply (erule exE, erule conjE)+ |
171 sorry |
171 |
172 |
172 sorry |
173 lemma tainted_s_in_ss: |
173 |
174 "tainted_s ss sobj \<Longrightarrow> sobj \<in> ss" |
174 |
175 apply (case_tac sobj, simp_all) |
|
176 apply (case_tac bool, simp+) |
|
177 apply (case_tac bool, simp+) |
|
178 apply (case_tac prod1, case_tac prod2, simp) |
|
179 thm tainted_s.simps |
|
180 oops |
|
181 |
|
182 lemma set_eq_D: |
|
183 "\<lbrakk>x \<in> S; {x. P x} = S\<rbrakk> \<Longrightarrow> P x" |
|
184 by auto |
|
185 |
|
186 lemma cqm2sms_prop1: |
|
187 "\<lbrakk>cqm2sms s q queue = Some sms; sm \<in> set sms\<rbrakk> \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm" |
|
188 apply (induct queue arbitrary:sms) |
|
189 apply (auto split:option.splits) |
|
190 done |
|
191 |
|
192 lemma sq_sm_prop: |
|
193 "\<lbrakk>sm \<in> set sms; cq2smsgq s q = Some (qi, qsec, sms); valid s\<rbrakk> |
|
194 \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm" |
|
195 by (auto simp:cq2smsgq_def split: option.splits intro:cqm2sms_prop1) |
175 |
196 |
176 lemma tainted_s_imp_tainted: |
197 lemma tainted_s_imp_tainted: |
177 "\<lbrakk>tainted_s ss sobj; ss \<in> static\<rbrakk> \<Longrightarrow> \<exists> obj s. s2ss s = ss \<and> valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s" |
198 "\<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" |
178 sorry |
199 apply (drule s2d_main) |
179 |
200 apply (erule exE, erule conjE, simp add:s2ss_def) |
|
201 apply (rule_tac x = s in exI, simp) |
|
202 apply (case_tac sobj, simp_all) |
|
203 apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) |
|
204 apply (rule_tac x = obj in exI, simp) |
|
205 apply (case_tac obj, (simp split:option.splits if_splits)+) |
|
206 |
|
207 apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) |
|
208 apply (rule_tac x = obj in exI, simp) |
|
209 apply (case_tac obj, (simp split:option.splits if_splits)+) |
|
210 |
|
211 apply (case_tac prod1, case_tac prod2, simp) |
|
212 apply ((erule conjE)+, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) |
|
213 apply (case_tac obj, simp_all split:option.splits if_splits) |
|
214 apply (drule_tac sm = "(aa, ba, True)" in sq_sm_prop, simp+, erule exE) |
|
215 apply (rule_tac x = "O_msg nat m" in exI) |
|
216 apply (simp) |
|
217 |
|
218 apply (case_tac obj, (simp split:option.splits if_splits)+) |
|
219 apply (erule conjE, drule_tac ) |
|
220 |
|
221 |
|
222 |
|
223 lemma has_inode_tainted_aux: |
|
224 "O_file f \<in> tainted s \<Longrightarrow> \<forall> f'. has_same_inode s f f' \<longrightarrow> O_file f' \<in> tainted s" |
|
225 apply (erule tainted.induct) |
|
226 apply (auto intro:tainted.intros simp:has_same_inode_def) |
|
227 (*?? need simpset for tainted *) |
|
228 sorry |
|
229 |
|
230 lemma has_same_inode_tainted: |
|
231 "\<lbrakk>has_same_inode s f f'; O_file f' \<in> tainted s\<rbrakk> \<Longrightarrow> O_file f \<in> tainted s" |
|
232 by (drule has_inode_tainted_aux, auto simp:has_same_inode_def) |
180 |
233 |
181 theorem static_sound: |
234 theorem static_sound: |
182 assumes tbl_s: "taintable_s obj" |
235 assumes tbl_s: "taintable_s obj" |
183 shows "taintable obj" |
236 shows "taintable obj" |
184 proof- |
237 proof- |
185 from tbl_s obtain ss sobj where static: "ss \<in> static" |
238 from tbl_s obtain ss sobj where static: "ss \<in> static" |
186 and sobj: "tainted_s ss sobj" and related: "init_obj_related sobj obj" |
239 and sobj: "tainted_s ss sobj" and related: "init_obj_related sobj obj" |
187 and init_alive: "init_alive obj" by (auto simp:taintable_s_def) |
240 and init_alive: "init_alive obj" by (auto simp:taintable_s_def) |
188 from static sobj tainted_s_imp_tainted |
241 from static sobj tainted_s_imp_tainted |
189 obtain s obj' where s2ss: "s2ss s = ss" and co2sobj: "co2sobj s obj' = Some sobj" |
242 obtain s obj' where co2sobj: "co2sobj s obj' = Some sobj" |
190 and tainted: "obj' \<in> tainted s" and vs: "valid s" by blast |
243 and tainted': "obj' \<in> tainted s" and vs: "valid s" by blast |
191 |
244 |
192 from co2sobj related |
245 from co2sobj related vs |
193 have eq:"obj = obj'" |
246 have eq:"obj = obj' \<or> (\<exists> f f'. obj = O_file f \<and> obj' = O_file f' \<and> has_same_inode s f f')" |
194 apply (case_tac obj', case_tac [!] obj, case_tac [!] sobj) |
247 apply (case_tac obj', case_tac [!] obj) |
195 apply auto |
248 apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi) |
196 apply (auto split:option.splits if_splits) |
249 apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_def is_file_def is_dir_def |
197 apply (case_tac a, simp+) |
250 split:option.splits t_inode_tag.splits dest!:cf2sfile_fi) |
198 apply (simp add:cp2sproc_def split:option.splits if_splits) |
251 done |
199 apply simp |
252 with tainted' have tainted: "obj \<in> tainted s" |
200 sorry |
253 by (auto intro:has_same_inode_tainted) |
201 with tainted vs init_alive |
254 with vs init_alive |
202 show ?thesis by (auto simp:taintable_def) |
255 show ?thesis by (auto simp:taintable_def) |
203 qed |
256 qed |
204 |
257 |
205 |
258 |
206 |
259 |