65 apply (simp add:init_ss_in_def) |
65 apply (simp add:init_ss_in_def) |
66 apply (erule bexE) |
66 apply (erule bexE) |
67 apply (simp add:init_ss_eq_def) |
67 apply (simp add:init_ss_eq_def) |
68 apply (rule_tac x = "ss'" in bexI) |
68 apply (rule_tac x = "ss'" in bexI) |
69 apply (rule_tac x = "sobj" in exI) |
69 apply (rule_tac x = "sobj" in exI) |
|
70 thm tainted_s_subset_prop |
70 by (auto intro:tainted_s_subset_prop) |
71 by (auto intro:tainted_s_subset_prop) |
71 qed |
72 qed |
72 |
73 |
73 lemma cp2sproc_pi: |
74 lemma cp2sproc_pi: |
74 "\<lbrakk>cp2sproc s p = Some (Init p', sec, fds, shms); valid s\<rbrakk> \<Longrightarrow> p = p' \<and> \<not> deleted (O_proc p) s \<and> p \<in> init_procs" |
75 "\<lbrakk>cp2sproc s p = Some (Init p', sec, fds, shms); valid s\<rbrakk> \<Longrightarrow> p = p' \<and> \<not> deleted (O_proc p) s \<and> p \<in> init_procs" |
184 \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm" |
185 \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm" |
185 by (auto simp:cq2smsgq_def split: option.splits intro:cqm2sms_prop1) |
186 by (auto simp:cq2smsgq_def split: option.splits intro:cqm2sms_prop1) |
186 |
187 |
187 declare co2sobj.simps [simp add] |
188 declare co2sobj.simps [simp add] |
188 |
189 |
|
190 lemma subseteq_D: |
|
191 "\<lbrakk> S \<subseteq> {x. P x}; x \<in> S\<rbrakk> \<Longrightarrow> P x" |
|
192 by auto |
|
193 |
|
194 lemma "\<lbrakk>tainted_s ss sobj; ss \<in> static; is_init_sobj sobj\<rbrakk> |
|
195 \<Longrightarrow> \<exists> s. valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s" |
|
196 apply (drule s2d_main') |
|
197 apply (erule exE, erule conjE, simp add:s2ss_def init_ss_eq_def, erule conjE) |
|
198 apply (rule_tac x = s in exI, simp) |
|
199 apply (case_tac sobj, simp_all only:tainted_s.simps) |
|
200 thm set_eq_D |
|
201 apply (simp split:option.splits) |
|
202 apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) |
|
203 apply (rule_tac x = obj in exI, simp) |
|
204 apply (case_tac obj, (simp split:option.splits if_splits)+) |
|
205 |
|
206 lemma tainted_s_imp_tainted: |
|
207 "\<lbrakk>tainted_s ss sobj; ss \<in> static; init_obj_related sobj obj\<rbrakk> |
|
208 \<Longrightarrow> \<exists> s. valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s" |
|
209 apply (drule s2d_main') |
|
210 apply (erule exE, erule conjE, simp add:s2ss_def init_ss_eq_def, erule conjE) |
|
211 apply (rule_tac x = s in exI, simp) |
|
212 apply (case_tac sobj, simp_all) |
|
213 apply (case_tac[!] obj, simp_all del:co2sobj.simps) |
|
214 apply (simp split:option.splits) |
|
215 apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) |
|
216 apply (rule_tac x = obj in exI, simp) |
|
217 apply (case_tac obj, (simp split:option.splits if_splits)+) |
|
218 |
|
219 apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) |
|
220 apply (rule_tac x = obj in exI, simp) |
|
221 apply (case_tac obj, (simp split:option.splits if_splits)+) |
|
222 sorry |
|
223 |
|
224 |
|
225 |
|
226 |
189 lemma tainted_s_imp_tainted: |
227 lemma tainted_s_imp_tainted: |
190 "\<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" |
228 "\<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" |
191 apply (drule s2d_main) |
229 apply (drule s2d_main) |
192 apply (erule exE, erule conjE, simp add:s2ss_def) |
230 apply (erule exE, erule conjE, simp add:s2ss_def) |
193 apply (rule_tac x = s in exI, simp) |
231 apply (rule_tac x = s in exI, simp) |