73 apply (frule vd_cons, frule valid_Tainted_obj, simp, frule vt_grant_os, case_tac a) |
73 apply (frule vd_cons, frule valid_Tainted_obj, simp, frule vt_grant_os, case_tac a) |
74 apply (auto simp:alive_simps split:if_splits option.splits t_object.splits |
74 apply (auto simp:alive_simps split:if_splits option.splits t_object.splits |
75 intro:has_same_inode_prop2 has_same_inode_prop1 dest:info_shm_flow_in_procs) |
75 intro:has_same_inode_prop2 has_same_inode_prop1 dest:info_shm_flow_in_procs) |
76 done |
76 done |
77 |
77 |
78 |
78 lemma Tainted_proc_in_current: |
79 lemma has_inode_Tainted_aux: |
79 "\<lbrakk>O_proc p \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s" |
80 "\<lbrakk>O_file f \<in> tainted s; has_same_inode s f f'\<rbrakk> \<Longrightarrow> O_file f' \<in> tainted s" |
80 by (drule Tainted_in_current, simp+) |
|
81 |
|
82 lemma has_inode_tainted_aux: |
|
83 "O_file f \<in> tainted s \<Longrightarrow> \<forall> f'. has_same_inode s f f' \<longrightarrow> O_file f' \<in> tainted s" |
81 apply (erule tainted.induct) |
84 apply (erule tainted.induct) |
82 apply (auto intro:tainted.intros simp:has_same_inode_def) |
85 apply (auto intro:tainted.intros simp:has_same_inode_def) |
83 (*?? need simpset for tainted *) |
86 (*?? need simpset for tainted *) |
|
87 |
|
88 |
|
89 sorry |
|
90 |
|
91 lemma has_inode_Tainted_aux: |
|
92 "\<lbrakk>O_file f \<in> Tainted s; has_same_inode s f f'\<rbrakk> \<Longrightarrow> O_file f' \<in> Tainted s" |
|
93 apply (induct s, auto) |
|
94 apply (auto intro:tainted.intros simp:has_same_inode_def) |
|
95 (*?? need simpset for tainted *) |
84 sorry |
96 sorry |
85 |
97 |
86 lemma info_flow_shm_Tainted: |
98 lemma info_flow_shm_Tainted: |
87 "\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s" |
99 "\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s" |
88 proof (induct s) |
100 proof (induct s arbitrary:p p') |
89 case Nil |
101 case Nil |
90 thus ?case |
102 thus ?case by (simp add:flow_shm_in_seeds) |
91 apply simp |
103 next |
92 apply (induct s) |
104 case (Cons e s) |
|
105 hence p1: "O_proc p \<in> Tainted (e # s)" and p2: "info_flow_shm (e # s) p p'" and p3: "valid (e # s)" |
|
106 and p4: "\<And> p p'. \<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s" |
|
107 and p5: "valid s" and p6: "os_grant s e" |
|
108 by (auto dest:vd_cons intro:vd_cons vt_grant_os) |
|
109 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> |
|
111 \<Longrightarrow> O_proc p' \<in> Tainted s" |
|
112 by (rule p4, auto simp:info_flow_shm_def) |
|
113 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) |
|
115 show ?case |
|
116 proof (cases "p = p'") |
|
117 case True with p1 show ?thesis by simp |
|
118 next |
|
119 case False |
|
120 with p1 p2 p5 p6 p7 p8 p3 show ?thesis |
|
121 apply (case_tac e) |
|
122 prefer 7 |
|
123 apply (simp add:info_flow_shm_def split:if_splits option.splits) |
|
124 apply (rule allI|rule impI|rule conjI)+ |
|
125 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) |
|
127 apply ((erule exE|erule conjE)+) |
|
128 |
|
129 |
|
130 apply (auto simp:info_flow_shm_def dest:p4' |
|
131 procs_of_shm_prop2 Tainted_in_current split:if_splits option.splits)[1] |
|
132 apply (drule_tac p = p and p' = p' in p4') |
|
133 apply (erule_tac x = ha in allE, simp) |
|
134 apply (drule_tac p = "nat1" and p' = p' in p4') |
|
135 apply (auto dest:p4'[where p = nat1 and p' = p']) |
|
136 |
|
137 apply (induct s) (* |
93 apply simp defer |
138 apply simp defer |
94 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
139 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
95 apply (auto simp:info_flow_shm_def elim!:disjE) |
140 apply (auto simp:info_flow_shm_def elim!:disjE) |
96 sorry |
141 sorry *) |
|
142 sorry |
|
143 next |
|
144 case (Cons e s) |
|
145 show ?case |
|
146 sorry |
|
147 qed |
97 |
148 |
98 lemma tainted_imp_Tainted: |
149 lemma tainted_imp_Tainted: |
99 "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s" |
150 "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s" |
100 apply (induct rule:tainted.induct) |
151 apply (induct rule:tainted.induct) |
101 apply (auto intro:info_flow_shm_Tainted dest:vd_cons) |
152 apply (auto intro:info_flow_shm_Tainted dest:vd_cons) |