equal
deleted
inserted
replaced
103 from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)" |
103 from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)" |
104 using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc) |
104 using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc) |
105 with p2 have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s" |
105 with p2 have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s" |
106 by (auto simp:obj2sobj.simps cp2sproc.simps) |
106 by (auto simp:obj2sobj.simps cp2sproc.simps) |
107 show ?case using p3 sproc os rc TP |
107 show ?case using p3 sproc os rc TP |
108 by (auto simp:ni_init_deled obj2sobj.simps cp2sproc.simps |
108 by (auto simp:obj2sobj.simps cp2sproc.simps dest:not_deleted_imp_exists |
109 split:option.splits intro!:ts_cipc) |
109 split:option.splits intro!:ts_cipc) |
110 next |
110 next |
111 case (t_read f s p) |
111 case (t_read f s p) |
112 assume p1: "File f \<in> tainted s" and p2: "obj2sobj s (File f) \<in> tainted_s" |
112 assume p1: "File f \<in> tainted s" and p2: "obj2sobj s (File f) \<in> tainted_s" |
113 and p3: "valid (ReadFile p f # s)" |
113 and p3: "valid (ReadFile p f # s)" |
209 qed |
209 qed |
210 with File t_remain(2) show ?thesis by simp |
210 with File t_remain(2) show ?thesis by simp |
211 next |
211 next |
212 case (IPC i) |
212 case (IPC i) |
213 have "obj2sobj (e # s) (IPC i) = obj2sobj s (IPC i)" using p5 t_remain(3,4) os IPC |
213 have "obj2sobj (e # s) (IPC i) = obj2sobj s (IPC i)" using p5 t_remain(3,4) os IPC |
214 by (case_tac e, auto simp:ni_init_deled ni_notin_curi obj2sobj.simps |
214 by (case_tac e, auto simp:obj2sobj.simps dest:not_deleted_imp_exists |
215 split:option.splits |
215 split:option.splits dest!:current_proc_has_role') |
216 dest!:current_proc_has_role') |
|
217 with IPC t_remain(2) show ?thesis by simp |
216 with IPC t_remain(2) show ?thesis by simp |
218 next |
217 next |
219 case (Proc p) |
218 case (Proc p) |
220 show ?thesis |
219 show ?thesis |
221 proof- |
220 proof- |
296 qed |
295 qed |
297 qed moreover |
296 qed moreover |
298 have "\<lbrakk>\<forall> f. e \<noteq> Execute p f; \<forall> r. e \<noteq> ChangeRole p r; \<forall> u. e \<noteq> ChangeOwner p u\<rbrakk> |
297 have "\<lbrakk>\<forall> f. e \<noteq> Execute p f; \<forall> r. e \<noteq> ChangeRole p r; \<forall> u. e \<noteq> ChangeOwner p u\<rbrakk> |
299 \<Longrightarrow> obj2sobj (e # s) (Proc p) \<in> tainted_s" |
298 \<Longrightarrow> obj2sobj (e # s) (Proc p) \<in> tainted_s" |
300 using t_remain(2,3,4) os p5 Proc |
299 using t_remain(2,3,4) os p5 Proc |
301 by (case_tac e, auto simp add:obj2sobj.simps cp2sproc_simps np_notin_curp |
300 by (case_tac e, auto simp add:obj2sobj.simps cp2sproc_simps dest:not_deleted_imp_exists |
302 simp del:cp2sproc.simps split:option.splits) |
301 simp del:cp2sproc.simps split:option.splits) |
303 ultimately show ?thesis using Proc |
302 ultimately show ?thesis using Proc |
304 by (case_tac e, auto simp del:obj2sobj.simps) |
303 by (case_tac e, auto simp del:obj2sobj.simps) |
305 qed |
304 qed |
306 qed |
305 qed |
586 obtain e where ev: "e = CreateIPC p (new_ipc s)" by simp |
585 obtain e where ev: "e = CreateIPC p (new_ipc s)" by simp |
587 |
586 |
588 have valid: "valid (e # s)" |
587 have valid: "valid (e # s)" |
589 proof- |
588 proof- |
590 have "os_grant s e" |
589 have "os_grant s e" |
591 using ev exp by (simp) |
590 using ev exp by (simp add:ni_notin_curi) |
592 moreover have "rc_grant s e" |
591 moreover have "rc_grant s e" |
593 using ev ts'_cipc(3) SP |
592 using ev ts'_cipc(3) SP |
594 by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) |
593 by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) |
595 ultimately show ?thesis using vds |
594 ultimately show ?thesis using vds |
596 by (rule_tac vs_step, simp+) |
595 by (rule_tac vs_step, simp+) |
1139 obtain e where ev: "e = CreateIPC p (new_ipc s)" by simp |
1138 obtain e where ev: "e = CreateIPC p (new_ipc s)" by simp |
1140 |
1139 |
1141 have valid: "valid (e # s)" |
1140 have valid: "valid (e # s)" |
1142 proof- |
1141 proof- |
1143 have "os_grant s e" |
1142 have "os_grant s e" |
1144 using ev exp by (simp) |
1143 using ev exp by (simp add:ni_notin_curi) |
1145 moreover have "rc_grant s e" |
1144 moreover have "rc_grant s e" |
1146 using ev ts'_cipc(3) SP |
1145 using ev ts'_cipc(3) SP |
1147 by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) |
1146 by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) |
1148 ultimately show ?thesis using vds |
1147 ultimately show ?thesis using vds |
1149 by (rule_tac vs_step, simp+) |
1148 by (rule_tac vs_step, simp+) |