84 |
84 |
85 lemma Tainted_proc_in_current: |
85 lemma Tainted_proc_in_current: |
86 "\<lbrakk>O_proc p \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s" |
86 "\<lbrakk>O_proc p \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s" |
87 by (drule Tainted_in_current, simp+) |
87 by (drule Tainted_in_current, simp+) |
88 |
88 |
89 lemma has_inode_tainted_aux: |
|
90 "O_file f \<in> tainted s \<Longrightarrow> \<forall> f'. has_same_inode s f f' \<longrightarrow> O_file f' \<in> tainted s" |
|
91 apply (erule tainted.induct) |
|
92 apply (auto intro:tainted.intros simp:has_same_inode_def) |
|
93 (*?? need simpset for tainted *) |
|
94 |
|
95 |
|
96 sorry |
|
97 |
|
98 lemma has_inode_Tainted_aux: |
|
99 "\<lbrakk>O_file f \<in> Tainted s; has_same_inode s f f'\<rbrakk> \<Longrightarrow> O_file f' \<in> Tainted s" |
|
100 apply (induct s, auto) |
|
101 apply (auto intro:tainted.intros simp:has_same_inode_def) |
|
102 (*?? need simpset for tainted *) |
|
103 sorry |
|
104 |
|
105 lemma "\<lbrakk>info_flow_shm s pa pb; info_flow_shm s pb pc; valid s\<rbrakk> \<Longrightarrow> info_flow_shm s pa pc" |
|
106 apply (auto simp add:info_flow_shm_def one_flow_shm_def procs_of_shm_prop2) |
|
107 apply (erule_tac x = h in allE, simp) |
|
108 apply (case_tac "h = ha", simp+) |
|
109 sorry |
|
110 |
89 |
111 lemma info_flow_shm_Tainted: |
90 lemma info_flow_shm_Tainted: |
112 "\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s" |
91 "\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s" |
113 proof (induct s arbitrary:p p') |
92 proof (induct s arbitrary:p p') |
114 case Nil |
93 case Nil |
120 and p5: "valid s" and p6: "os_grant s e" |
99 and p5: "valid s" and p6: "os_grant s e" |
121 by (auto dest:vd_cons intro:vd_cons vt_grant_os) |
100 by (auto dest:vd_cons intro:vd_cons vt_grant_os) |
122 have p4': |
101 have p4': |
123 "\<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> |
102 "\<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> |
124 \<Longrightarrow> O_proc p' \<in> Tainted s" |
103 \<Longrightarrow> O_proc p' \<in> Tainted s" |
125 apply (rule p4, auto simp:info_flow_shm_def one_flow_shm_def ) (* procs_of_shm_prop2 *) |
104 by (rule p4, auto simp:info_flow_shm_def one_flow_shm_def procs_of_shm_prop2 p5) |
126 sorry |
105 from p2 p3 have p7: "p \<in> current_procs (e # s)" and p8: "p' \<in> current_procs (e # s)" |
127 from p2 p3 have p7: "p \<in> current_procs (e # s)" and p8: "p' \<in> current_procs (e # s)" (* |
106 by (auto dest:info_shm_flow_in_procs) |
128 by (auto dest:info_shm_flow_in_procs) *) sorry |
|
129 show ?case |
107 show ?case |
130 proof (cases "self_shm s p p'") |
108 proof (cases "self_shm s p p'") |
131 case True with p1 show ?thesis by simp |
109 case True with p1 show ?thesis by simp |
132 next |
110 next |
133 case False |
111 case False |
134 with p1 p2 p5 p6 p7 p8 p3 show ?thesis |
112 with p1 p2 p5 p6 p7 p8 p3 show ?thesis |
135 apply (case_tac e) |
113 apply (case_tac e)(* |
136 prefer 7 |
114 prefer 7 |
137 apply (simp add:info_flow_shm_simps split:if_splits option.splits) |
115 apply (simp add:info_flow_shm_simps split:if_splits option.splits) |
138 apply (rule allI|rule impI|rule conjI)+ |
116 apply (rule allI|rule impI|rule conjI)+ |
139 apply simp |
117 apply simp |
140 apply (case_tac "O_proc p \<in> Tainted s", drule_tac p'=p' in p4, simp+) |
118 apply (case_tac "O_proc p \<in> Tainted s", drule_tac p'=p' in p4, simp+) |
173 apply (drule_tac p = p and p' = p' in p4') |
148 apply (drule_tac p = p and p' = p' in p4') |
174 apply (erule_tac x = ha in allE, simp) |
149 apply (erule_tac x = ha in allE, simp) |
175 apply (drule_tac p = "nat1" and p' = p' in p4') |
150 apply (drule_tac p = "nat1" and p' = p' in p4') |
176 apply (auto dest:p4'[where p = nat1 and p' = p']) |
151 apply (auto dest:p4'[where p = nat1 and p' = p']) |
177 |
152 |
178 apply (induct s) (* |
153 apply (induct s) |
179 apply simp defer |
154 apply simp defer |
180 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
155 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
181 apply (auto simp:info_flow_shm_def elim!:disjE) |
156 apply (auto simp:info_flow_shm_def elim!:disjE) |
182 sorry *) |
157 sorry *) |
183 sorry |
158 sorry |
184 next |
159 qed |
185 case (Cons e s) |
|
186 show ?case |
|
187 sorry |
|
188 qed |
160 qed |
189 |
161 |
190 lemma tainted_imp_Tainted: |
162 lemma tainted_imp_Tainted: |
191 "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s" |
163 "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s" |
192 apply (induct rule:tainted.induct) |
164 apply (induct rule:tainted.induct) (* |
|
165 apply (simp_all add:vd_cons) |
|
166 apply (rule impI) |
|
167 |
|
168 apply (rule disjI2, rule_tac x = flag' in exI, simp) |
|
169 apply ((rule impI)+, erule_tac x = p' in allE, simp) |
|
170 *) |
193 apply (auto intro:info_flow_shm_Tainted dest:vd_cons) |
171 apply (auto intro:info_flow_shm_Tainted dest:vd_cons) |
194 apply (case_tac e, auto split:option.splits if_splits simp:alive_simps) |
172 apply (case_tac e, auto split:option.splits if_splits simp:alive_simps) |
195 done |
173 done |
196 |
174 |
|
175 lemma Tainted_imp_tainted_aux_remain: |
|
176 "\<lbrakk>obj \<in> Tainted s; valid (e # s); alive (e # s) obj; \<And> obj. obj \<in> Tainted s \<Longrightarrow> obj \<in> tainted s\<rbrakk> |
|
177 \<Longrightarrow> obj \<in> tainted (e # s)" |
|
178 by (rule t_remain, auto) |
|
179 |
197 lemma Tainted_imp_tainted: |
180 lemma Tainted_imp_tainted: |
198 "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> obj \<in> tainted s" |
181 "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> obj \<in> tainted s" |
199 proof (induct s arbitrary:obj) |
182 apply (induct s arbitrary:obj, simp add:t_init) |
200 case Nil |
183 apply (frule Tainted_in_current, simp+) |
201 thus ?case by (auto intro:t_init) |
184 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
202 next |
185 apply (auto split:if_splits option.splits elim:Tainted_imp_tainted_aux_remain intro:tainted.intros) |
203 case (Cons e s) |
186 done |
204 hence p1: "\<And> obj. obj \<in> Tainted s \<Longrightarrow> obj \<in> tainted s" |
187 |
205 and p2: "obj \<in> Tainted (e # s)" and p3: "valid (e # s)" |
188 lemma tainted_eq_Tainted: |
206 and p4: "valid s" and p5: "os_grant s e" |
189 "valid s \<Longrightarrow> (obj \<in> tainted s) = (obj \<in> Tainted s)" |
207 by (auto dest:vd_cons intro:vd_cons vt_grant_os) |
190 by (rule iffI, auto intro:Tainted_imp_tainted tainted_imp_Tainted) |
208 from p1 have p6: "" |
191 |
209 apply (frule vd_cons, frule vt_grant_os, frule valid_Tainted_obj, simp) |
192 lemma info_flow_shm_tainted: |
210 apply (case_tac a) |
193 "\<lbrakk>O_proc p \<in> tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> tainted s" |
211 apply (auto intro!:t_init t_clone t_execve t_cfile t_read t_write t_link t_trunc t_sendmsg t_recvmsg |
194 by (simp only:tainted_eq_Tainted info_flow_shm_Tainted) |
212 intro:t_remain |
195 |
213 split:if_splits option.splits dest:Tainted_in_current) |
196 lemma has_same_inode_Tainted: |
214 pr 25 |
197 "\<lbrakk>O_file f \<in> Tainted s; has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> Tainted s" |
215 |
198 apply (induct s arbitrary:f f', simp add:same_inode_in_seeds) |
216 lemma tainted_imp_Tainted: |
199 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
217 "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s" |
200 apply (auto split:if_splits option.splits simp:has_same_inode_def dest:iof's_im_in_cim) |
218 |
201 apply (drule_tac obj = "O_file list2" in Tainted_in_current, simp, simp add:is_file_in_current) |
|
202 done |
|
203 |
|
204 lemma has_same_inode_tainted: |
|
205 "\<lbrakk>O_file f \<in> tainted s; has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> tainted s" |
|
206 by (simp add:has_same_inode_Tainted tainted_eq_Tainted) |
219 |
207 |
220 |
208 |
221 |
209 |
222 |
210 |
223 |
211 |
224 lemma tainted_in_current: |
212 lemma tainted_in_current: |
225 "obj \<in> tainted s \<Longrightarrow> alive s obj" |
213 "obj \<in> tainted s \<Longrightarrow> alive s obj" |
226 apply (erule tainted.induct, auto dest:vt_grant_os vd_cons simp:is_file_simps) |
214 apply (erule tainted.induct) |
|
215 apply (auto dest:vt_grant_os vd_cons info_shm_flow_in_procs procs_of_shm_prop2 simp:is_file_simps) |
227 apply (drule seeds_in_init, simp add:tobj_in_alive) |
216 apply (drule seeds_in_init, simp add:tobj_in_alive) |
228 apply (erule has_same_inode_prop2, simp, simp add:vd_cons) |
217 apply (erule has_same_inode_prop2, simp, simp add:vd_cons) |
229 apply (frule vt_grant_os, simp) |
218 apply (frule vt_grant_os, simp) |
230 apply (erule has_same_inode_prop1, simp, simp add:vd_cons) |
219 apply (erule has_same_inode_prop1, simp, simp add:vd_cons) |
231 done |
220 done |