equal
deleted
inserted
replaced
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 Current_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 fun Tainted :: "t_state \<Rightarrow> t_object set" |
7 fun Tainted :: "t_state \<Rightarrow> t_object set" |
78 apply (drule seeds_in_init, case_tac obj, simp_all add:is_file_nil) |
78 apply (drule seeds_in_init, case_tac obj, simp_all add:is_file_nil) |
79 apply (frule vd_cons, frule valid_Tainted_obj, simp, frule vt_grant_os, case_tac a) |
79 apply (frule vd_cons, frule valid_Tainted_obj, simp, frule vt_grant_os, case_tac a) |
80 apply (auto simp:alive_simps split:if_splits option.splits t_object.splits |
80 apply (auto simp:alive_simps split:if_splits option.splits t_object.splits |
81 intro:has_same_inode_prop2 has_same_inode_prop1 procs_of_shm_prop2 |
81 intro:has_same_inode_prop2 has_same_inode_prop1 procs_of_shm_prop2 |
82 dest:info_shm_flow_in_procs) |
82 dest:info_shm_flow_in_procs) |
83 done |
83 done |
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 |
100 apply (induct s, auto) |
100 apply (induct s, auto) |
101 apply (auto intro:tainted.intros simp:has_same_inode_def) |
101 apply (auto intro:tainted.intros simp:has_same_inode_def) |
102 (*?? need simpset for tainted *) |
102 (*?? need simpset for tainted *) |
103 sorry |
103 sorry |
104 |
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 |
105 |
110 |
106 lemma info_flow_shm_Tainted: |
111 lemma info_flow_shm_Tainted: |
107 "\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s" |
112 "\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s" |
108 proof (induct s arbitrary:p p') |
113 proof (induct s arbitrary:p p') |
109 case Nil |
114 case Nil |
115 and p5: "valid s" and p6: "os_grant s e" |
120 and p5: "valid s" and p6: "os_grant s e" |
116 by (auto dest:vd_cons intro:vd_cons vt_grant_os) |
121 by (auto dest:vd_cons intro:vd_cons vt_grant_os) |
117 have p4': |
122 have p4': |
118 "\<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> |
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> |
119 \<Longrightarrow> O_proc p' \<in> Tainted s" |
124 \<Longrightarrow> O_proc p' \<in> Tainted s" |
120 by (rule p4, auto simp:info_flow_shm_def one_flow_shm_def) |
125 apply (rule p4, auto simp:info_flow_shm_def one_flow_shm_def ) (* procs_of_shm_prop2 *) |
121 from p2 p3 have p7: "p \<in> current_procs (e # s)" and p8: "p' \<in> current_procs (e # s)" |
126 sorry |
122 by (auto dest:info_shm_flow_in_procs) |
127 from p2 p3 have p7: "p \<in> current_procs (e # s)" and p8: "p' \<in> current_procs (e # s)" (* |
|
128 by (auto dest:info_shm_flow_in_procs) *) sorry |
123 show ?case |
129 show ?case |
124 proof (cases "self_shm s p p'") |
130 proof (cases "self_shm s p p'") |
125 case True with p1 show ?thesis by simp |
131 case True with p1 show ?thesis by simp |
126 next |
132 next |
127 case False |
133 case False |