1 theory Tainted_prop |
1 theory Tainted_prop |
2 imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop |
2 imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop |
3 begin |
3 begin |
4 |
4 |
5 context tainting begin |
5 context tainting begin |
6 |
6 |
7 lemma tainted_in_current: |
7 lemma tainted_in_current: |
8 "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj" |
8 "obj \<in> tainted s \<Longrightarrow> alive s obj" |
9 apply (erule tainted.induct, auto dest:vt_grant_os simp:is_file_simps) |
9 apply (erule tainted.induct, auto dest:vt_grant_os vd_cons simp:is_file_simps) |
|
10 apply (drule seeds_in_init, simp add:tobj_in_alive) |
|
11 apply (erule has_same_inode_prop2, simp, simp add:vd_cons) |
|
12 apply (frule vt_grant_os, simp) |
|
13 apply (erule has_same_inode_prop1, simp, simp add:vd_cons) |
|
14 done |
10 |
15 |
|
16 lemma tainted_is_valid: |
|
17 "obj \<in> tainted s \<Longrightarrow> valid s" |
|
18 by (erule tainted.induct, auto intro:valid.intros) |
11 |
19 |
|
20 lemma t_remain_app: |
|
21 "\<lbrakk>obj \<in> tainted s; \<not> deleted obj (s' @ s); valid (s' @ s)\<rbrakk> |
|
22 \<Longrightarrow> obj \<in> tainted (s' @ s)" |
|
23 apply (induct s', simp) |
|
24 apply (simp (no_asm) only:cons_app_simp_aux, rule t_remain) |
|
25 apply (simp_all add:not_deleted_cons_D vd_cons) |
|
26 apply (drule tainted_in_current, simp add:not_deleted_imp_alive_cons) |
|
27 done |
12 |
28 |
|
29 lemma valid_tainted_obj: |
|
30 "obj \<in> tainted s \<Longrightarrow> (\<forall> f. obj \<noteq> O_dir f) \<and> (\<forall> q. obj \<noteq> O_msgq q) \<and> (\<forall> h. obj \<noteq> O_shm h)" |
|
31 apply (erule tainted.induct) |
|
32 apply (drule seeds_in_init) |
|
33 by auto |
|
34 |
|
35 lemma dir_not_tainted: "O_dir f \<in> tainted s \<Longrightarrow> False" |
|
36 by (auto dest:valid_tainted_obj) |
|
37 |
|
38 lemma msgq_not_tainted: "O_msgq q \<in> tainted s \<Longrightarrow> False" |
|
39 by (auto dest:valid_tainted_obj) |
|
40 |
|
41 lemma shm_not_tainted: "O_shm h \<in> tainted s \<Longrightarrow> False" |
|
42 by (auto dest:valid_tainted_obj) |
13 |
43 |
14 end |
44 end |
15 |
45 |
16 end |
46 end |
17 |
|
18 |
|
19 |
|
20 |
|