93 apply (induct s, auto) |
93 apply (induct s, auto) |
94 apply (auto intro:tainted.intros simp:has_same_inode_def) |
94 apply (auto intro:tainted.intros simp:has_same_inode_def) |
95 (*?? need simpset for tainted *) |
95 (*?? need simpset for tainted *) |
96 sorry |
96 sorry |
97 |
97 |
|
98 lemma info_flow_shm_intro: |
|
99 "\<lbrakk>(p, SHM_RDWR) \<in> procs_of_shm s h; (p', flag) \<in> procs_of_shm s h; valid s\<rbrakk> |
|
100 \<Longrightarrow> info_flow_shm s p p'" |
|
101 apply (rule_tac p = p and p' = p in info_flow_shm.intros(2)) |
|
102 apply (auto intro!:info_flow_shm.intros(1) procs_of_shm_prop2) |
|
103 done |
|
104 |
98 lemma info_flow_shm_Tainted: |
105 lemma info_flow_shm_Tainted: |
99 "\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s" |
106 "\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s" |
100 proof (induct s arbitrary:p p') |
107 proof (induct s arbitrary:p p') |
101 case Nil |
108 case Nil |
102 thus ?case by (simp add:flow_shm_in_seeds) |
109 thus ?case by (simp add:flow_shm_in_seeds) |
107 and p5: "valid s" and p6: "os_grant s e" |
114 and p5: "valid s" and p6: "os_grant s e" |
108 by (auto dest:vd_cons intro:vd_cons vt_grant_os) |
115 by (auto dest:vd_cons intro:vd_cons vt_grant_os) |
109 have p4': |
116 have p4': |
110 "\<And> p p' h flag. \<lbrakk>O_proc p \<in> Tainted s; (p, SHM_RDWR) \<in> procs_of_shm s h; (p', flag) \<in> procs_of_shm s h\<rbrakk> |
117 "\<And> p p' h flag. \<lbrakk>O_proc p \<in> Tainted s; (p, SHM_RDWR) \<in> procs_of_shm s h; (p', flag) \<in> procs_of_shm s h\<rbrakk> |
111 \<Longrightarrow> O_proc p' \<in> Tainted s" |
118 \<Longrightarrow> O_proc p' \<in> Tainted s" |
112 by (rule p4, auto simp:info_flow_shm_def) |
119 by (rule p4, auto intro!:info_flow_shm_intro p5) |
113 from p2 p3 have p7: "p \<in> current_procs (e # s)" and p8: "p' \<in> current_procs (e # s)" |
120 from p2 p3 have p7: "p \<in> current_procs (e # s)" and p8: "p' \<in> current_procs (e # s)" |
114 by (auto dest:info_shm_flow_in_procs) |
121 by (auto dest:info_shm_flow_in_procs) |
115 show ?case |
122 show ?case |
116 proof (cases "p = p'") |
123 proof (cases "p = p'") |
117 case True with p1 show ?thesis by simp |
124 case True with p1 show ?thesis by simp |
118 next |
125 next |
119 case False |
126 case False |
120 with p1 p2 p5 p6 p7 p8 p3 show ?thesis |
127 with p1 p2 p5 p6 p7 p8 p3 show ?thesis |
121 apply (case_tac e) |
128 apply (case_tac e) |
122 prefer 7 |
129 prefer 7 |
123 apply (simp add:info_flow_shm_def split:if_splits option.splits) |
130 apply (simp split:if_splits option.splits) |
124 apply (rule allI|rule impI|rule conjI)+ |
131 apply (rule allI|rule impI|rule conjI)+ |
|
132 |
|
133 |
|
134 apply (auto dest:p4' procs_of_shm_prop2 Tainted_in_current split:if_splits option.splits)[1] |
|
135 |
125 apply (erule disjE, drule_tac p = p and p' = p' in p4', simp+) |
136 apply (erule disjE, drule_tac p = p and p' = p' in p4', simp+) |
126 apply (erule disjE, rule disjI2, rule disjI2, rule_tac x = h in exI, simp, rule_tac x= toflag in exI, simp) |
137 apply (erule disjE, rule disjI2, rule disjI2, rule_tac x = h in exI, simp, rule_tac x= toflag in exI, simp) |
127 apply ((erule exE|erule conjE)+) |
138 apply ((erule exE|erule conjE)+) |
128 |
139 |
129 |
140 |