34 else Tainted s |
34 else Tainted s |
35 | None \<Rightarrow> Tainted s)" |
35 | None \<Rightarrow> Tainted s)" |
36 | "Tainted (WriteFile p fd # s) = |
36 | "Tainted (WriteFile p fd # s) = |
37 (case (file_of_proc_fd s p fd) of |
37 (case (file_of_proc_fd s p fd) of |
38 Some f \<Rightarrow> if (O_proc p) \<in> Tainted s |
38 Some f \<Rightarrow> if (O_proc p) \<in> Tainted s |
39 then Tainted s \<union> {O_file f' | f'. has_same_inode s f f'} |
39 then Tainted s \<union> {O_file f' | f'. f' \<in> same_inode_files s f} |
40 else Tainted s |
40 else Tainted s |
41 | None \<Rightarrow> Tainted s)" |
41 | None \<Rightarrow> Tainted s)" |
42 | "Tainted (CloseFd p fd # s) = |
42 | "Tainted (CloseFd p fd # s) = |
43 (case (file_of_proc_fd s p fd) of |
43 (case (file_of_proc_fd s p fd) of |
44 Some f \<Rightarrow> ( if ((proc_fd_of_file s f = {(p,fd)}) \<and> (f \<in> files_hung_by_del s)) |
44 Some f \<Rightarrow> ( if ((proc_fd_of_file s f = {(p,fd)}) \<and> (f \<in> files_hung_by_del s)) |
48 (if (proc_fd_of_file s f = {}) then Tainted s - {O_file f} else Tainted s)" |
48 (if (proc_fd_of_file s f = {}) then Tainted s - {O_file f} else Tainted s)" |
49 | "Tainted (LinkHard p f f' # s) = |
49 | "Tainted (LinkHard p f f' # s) = |
50 (if (O_file f \<in> Tainted s) then Tainted s \<union> {O_file f'} else Tainted s)" |
50 (if (O_file f \<in> Tainted s) then Tainted s \<union> {O_file f'} else Tainted s)" |
51 | "Tainted (Truncate p f len # s) = |
51 | "Tainted (Truncate p f len # s) = |
52 (if (len > 0 \<and> O_proc p \<in> Tainted s) |
52 (if (len > 0 \<and> O_proc p \<in> Tainted s) |
53 then Tainted s \<union> {O_file f' | f'. has_same_inode s f f'} |
53 then Tainted s \<union> {O_file f' | f'. f' \<in> same_inode_files s f} |
54 else Tainted s)" |
54 else Tainted s)" |
55 | "Tainted (Attach p h flag # s) = |
55 | "Tainted (Attach p h flag # s) = |
56 (if (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR) |
56 (if (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR) |
57 then Tainted s \<union> {O_proc p'' | p' flag' p''. (p', flag') \<in> procs_of_shm s h \<and> info_flow_shm s p' p''} |
57 then Tainted s \<union> {O_proc p'' | p' flag' p''. (p', flag') \<in> procs_of_shm s h \<and> info_flow_shm s p' p''} |
58 else if (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h) |
58 else if (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h) |
78 "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj" |
78 "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj" |
79 apply (induct s, simp) |
79 apply (induct s, simp) |
80 apply (drule seeds_in_init, case_tac obj, simp_all add:is_file_nil) |
80 apply (drule seeds_in_init, case_tac obj, simp_all add:is_file_nil) |
81 apply (frule vd_cons, frule valid_Tainted_obj, simp, frule vt_grant_os, case_tac a) |
81 apply (frule vd_cons, frule valid_Tainted_obj, simp, frule vt_grant_os, case_tac a) |
82 apply (auto simp:alive_simps split:if_splits option.splits t_object.splits |
82 apply (auto simp:alive_simps split:if_splits option.splits t_object.splits |
83 intro:has_same_inode_prop2 has_same_inode_prop1 procs_of_shm_prop2 |
83 intro:same_inode_files_prop1 procs_of_shm_prop2 |
84 dest:info_shm_flow_in_procs) |
84 dest:info_shm_flow_in_procs) |
|
85 apply (auto simp:same_inode_files_def is_file_def split:if_splits) |
85 done |
86 done |
86 |
87 |
87 lemma Tainted_proc_in_current: |
88 lemma Tainted_proc_in_current: |
88 "\<lbrakk>O_proc p \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s" |
89 "\<lbrakk>O_proc p \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s" |
89 by (drule Tainted_in_current, simp+) |
90 by (drule Tainted_in_current, simp+) |
159 sorry *) |
160 sorry *) |
160 sorry |
161 sorry |
161 qed |
162 qed |
162 qed |
163 qed |
163 |
164 |
|
165 lemma has_same_inode_comm: |
|
166 "has_same_inode s f f' = has_same_inode s f' f" |
|
167 by (auto simp add:has_same_inode_def same_inode_files_def is_file_def) |
|
168 |
164 lemma tainted_imp_Tainted: |
169 lemma tainted_imp_Tainted: |
165 "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s" |
170 "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s" |
166 apply (induct rule:tainted.induct) (* |
171 apply (induct rule:tainted.induct) (* |
167 apply (simp_all add:vd_cons) |
172 apply (simp_all add:vd_cons) |
168 apply (rule impI) |
173 apply (rule impI) |
169 |
174 |
170 apply (rule disjI2, rule_tac x = flag' in exI, simp) |
175 apply (rule disjI2, rule_tac x = flag' in exI, simp) |
171 apply ((rule impI)+, erule_tac x = p' in allE, simp) |
176 apply ((rule impI)+, erule_tac x = p' in allE, simp) |
172 *) |
177 *) |
173 apply (auto intro:info_flow_shm_Tainted dest:vd_cons) |
178 apply (auto intro:info_flow_shm_Tainted simp:has_same_inode_def dest:vd_cons) |
174 apply (case_tac e, auto split:option.splits if_splits simp:alive_simps) |
179 apply (case_tac e, auto split:option.splits if_splits simp:alive_simps) |
175 done |
180 done |
176 |
181 |
177 lemma Tainted_imp_tainted_aux_remain: |
182 lemma Tainted_imp_tainted_aux_remain: |
178 "\<lbrakk>obj \<in> Tainted s; valid (e # s); alive (e # s) obj; \<And> obj. obj \<in> Tainted s \<Longrightarrow> obj \<in> tainted s\<rbrakk> |
183 "\<lbrakk>obj \<in> Tainted s; valid (e # s); alive (e # s) obj; \<And> obj. obj \<in> Tainted s \<Longrightarrow> obj \<in> tainted s\<rbrakk> |
182 lemma Tainted_imp_tainted: |
187 lemma Tainted_imp_tainted: |
183 "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> obj \<in> tainted s" |
188 "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> obj \<in> tainted s" |
184 apply (induct s arbitrary:obj, simp add:t_init) |
189 apply (induct s arbitrary:obj, simp add:t_init) |
185 apply (frule Tainted_in_current, simp+) |
190 apply (frule Tainted_in_current, simp+) |
186 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
191 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
187 apply (auto split:if_splits option.splits elim:Tainted_imp_tainted_aux_remain intro:tainted.intros) |
192 apply (auto split:if_splits option.splits elim:Tainted_imp_tainted_aux_remain intro:tainted.intros |
|
193 simp:has_same_inode_def) |
188 done |
194 done |
189 |
195 |
190 lemma tainted_eq_Tainted: |
196 lemma tainted_eq_Tainted: |
191 "valid s \<Longrightarrow> (obj \<in> tainted s) = (obj \<in> Tainted s)" |
197 "valid s \<Longrightarrow> (obj \<in> tainted s) = (obj \<in> Tainted s)" |
192 by (rule iffI, auto intro:Tainted_imp_tainted tainted_imp_Tainted) |
198 by (rule iffI, auto intro:Tainted_imp_tainted tainted_imp_Tainted) |
193 |
199 |
194 lemma info_flow_shm_tainted: |
200 lemma info_flow_shm_tainted: |
195 "\<lbrakk>O_proc p \<in> tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> tainted s" |
201 "\<lbrakk>O_proc p \<in> tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> tainted s" |
196 by (simp only:tainted_eq_Tainted info_flow_shm_Tainted) |
202 by (simp only:tainted_eq_Tainted info_flow_shm_Tainted) |
197 |
203 |
|
204 |
|
205 lemma same_inode_files_Tainted: |
|
206 "\<lbrakk>O_file f \<in> Tainted s; f' \<in> same_inode_files s f; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> Tainted s" |
|
207 apply (induct s arbitrary:f f', simp add:same_inode_in_seeds has_same_inode_def) |
|
208 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
|
209 prefer 6 |
|
210 apply (simp split:if_splits option.splits add:same_inode_files_open current_files_simps) |
|
211 prefer 8 |
|
212 apply (frule Tainted_in_current, simp, simp add:alive.simps, drule is_file_in_current) |
|
213 apply (auto simp add:same_inode_files_closefd split:option.splits if_splits)[1] |
|
214 prefer 8 |
|
215 apply (frule Tainted_in_current, simp, simp add:alive.simps, drule is_file_in_current) |
|
216 apply (auto simp add:same_inode_files_unlink split:option.splits if_splits)[1] |
|
217 prefer 10 |
|
218 apply (auto split:if_splits option.splits simp:same_inode_files_linkhard current_files_simps)[1] |
|
219 apply (drule Tainted_in_current, simp, simp add:alive.simps is_file_in_current) |
|
220 apply (drule same_inode_files_prop5, simp) |
|
221 apply (drule same_inode_files_prop5, drule_tac f' = list1 and f'' = f' in same_inode_files_prop4, simp, simp) |
|
222 |
|
223 apply (auto simp:same_inode_files_other split:if_splits) |
|
224 apply (drule_tac f'' = f' and f' = f and f = fa in same_inode_files_prop4, simp+) |
|
225 apply (drule_tac f'' = f' and f' = f and f = list in same_inode_files_prop4, simp+) |
|
226 done |
|
227 |
198 lemma has_same_inode_Tainted: |
228 lemma has_same_inode_Tainted: |
199 "\<lbrakk>O_file f \<in> Tainted s; has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> Tainted s" |
229 "\<lbrakk>O_file f \<in> Tainted s; has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> Tainted s" |
200 apply (induct s arbitrary:f f', simp add:same_inode_in_seeds) |
230 by (simp add:has_same_inode_def same_inode_files_Tainted) |
201 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
|
202 apply (auto split:if_splits option.splits simp:has_same_inode_def dest:iof's_im_in_cim) |
|
203 apply (drule_tac obj = "O_file list2" in Tainted_in_current, simp, simp add:is_file_in_current) |
|
204 done |
|
205 |
231 |
206 lemma has_same_inode_tainted: |
232 lemma has_same_inode_tainted: |
207 "\<lbrakk>O_file f \<in> tainted s; has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> tainted s" |
233 "\<lbrakk>O_file f \<in> tainted s; has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> tainted s" |
208 by (simp add:has_same_inode_Tainted tainted_eq_Tainted) |
234 by (simp add:has_same_inode_Tainted tainted_eq_Tainted) |
209 |
235 |
210 |
236 lemma same_inodes_Tainted: |
|
237 "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> (O_file f \<in> Tainted s) = (O_file f' \<in> Tainted s)" |
|
238 apply (frule same_inode_files_prop8, frule same_inode_files_prop7) |
|
239 apply (auto intro:has_same_inode_Tainted) |
|
240 done |
211 |
241 |
212 |
242 |
213 |
243 |
214 lemma tainted_in_current: |
244 lemma tainted_in_current: |
215 "obj \<in> tainted s \<Longrightarrow> alive s obj" |
245 "obj \<in> tainted s \<Longrightarrow> alive s obj" |