|
1 theory Final_theorem |
|
2 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2 Dynamic_static |
|
3 begin |
|
4 |
|
5 context tainting_s begin |
|
6 |
|
7 lemma t2ts: |
|
8 "obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj" |
|
9 apply (frule tainted_in_current, frule tainted_is_valid) |
|
10 apply (frule s2ss_included_sobj, simp) |
|
11 apply (case_tac sobj, simp_all) |
|
12 apply (case_tac [!] obj, simp_all add:co2sobj.simps split:option.splits if_splits) |
|
13 apply (drule dir_not_tainted, simp) |
|
14 apply (drule msgq_not_tainted, simp) |
|
15 apply (drule shm_not_tainted, simp) |
|
16 done |
|
17 |
|
18 lemma delq_imp_delqm: |
|
19 "deleted (O_msgq q) s \<Longrightarrow> deleted (O_msg q m) s" |
|
20 apply (induct s, simp) |
|
21 by (case_tac a, auto) |
|
22 |
|
23 lemma tainted_s_subset_prop: |
|
24 "\<lbrakk>tainted_s ss sobj; ss \<subseteq> ss'\<rbrakk> \<Longrightarrow> tainted_s ss' sobj" |
|
25 apply (case_tac sobj) |
|
26 apply auto |
|
27 done |
|
28 |
|
29 theorem static_complete: |
|
30 assumes undel: "undeletable obj" and tbl: "taintable obj" |
|
31 shows "taintable_s obj" |
|
32 proof- |
|
33 from tbl obtain s where tainted: "obj \<in> tainted s" |
|
34 by (auto simp:taintable_def) |
|
35 hence vs: "valid s" by (simp add:tainted_is_valid) |
|
36 hence static: "s2ss s \<propto> static" using d2s_main by auto |
|
37 from tainted tbl vs obtain sobj where sobj: "co2sobj s obj = Some sobj" |
|
38 apply (clarsimp simp add:taintable_def) |
|
39 apply (frule tainted_in_current) |
|
40 apply (case_tac obj, simp_all add:co2sobj.simps) |
|
41 apply (frule current_proc_has_sp, simp, auto) |
|
42 done |
|
43 from undel vs have "\<not> deleted obj s" and init_alive: "init_alive obj" |
|
44 by (auto simp:undeletable_def) |
|
45 with vs sobj have "init_obj_related sobj obj" |
|
46 apply (case_tac obj, case_tac [!] sobj) |
|
47 apply (auto split:option.splits if_splits simp:co2sobj.simps cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm) |
|
48 apply (frule not_deleted_init_file, simp+) |
|
49 apply (drule is_file_has_sfile', simp, erule exE) |
|
50 apply (rule_tac x = sf in bexI) |
|
51 apply (case_tac list, auto split:option.splits simp:is_init_file_props)[1] |
|
52 apply (drule root_is_init_dir', simp) |
|
53 apply (frule not_deleted_init_file, simp, simp) |
|
54 apply (simp add:cf2sfile_def split:option.splits if_splits) |
|
55 apply (simp add:cf2sfiles_def) |
|
56 apply (rule_tac x = list in bexI, simp, simp add:same_inode_files_def not_deleted_init_file) |
|
57 |
|
58 apply (frule not_deleted_init_dir, simp+) |
|
59 apply (simp add:cf2sfile_def split:option.splits if_splits) |
|
60 apply (case_tac list, simp add:sroot_def, simp) |
|
61 apply (drule file_dir_conflict, simp+) |
|
62 done |
|
63 with tainted t2ts init_alive sobj static |
|
64 show ?thesis unfolding taintable_s_def |
|
65 apply (simp add:init_ss_in_def) |
|
66 apply (erule bexE) |
|
67 apply (simp add:init_ss_eq_def) |
|
68 apply (rule_tac x = "ss'" in bexI) |
|
69 apply (rule_tac x = "sobj" in exI) |
|
70 by (auto intro:tainted_s_subset_prop) |
|
71 qed |
|
72 |
|
73 lemma cp2sproc_pi: |
|
74 "\<lbrakk>cp2sproc s p = Some (Init p', sec, fds, shms); valid s\<rbrakk> \<Longrightarrow> p = p' \<and> \<not> deleted (O_proc p) s \<and> p \<in> init_procs" |
|
75 by (simp add:cp2sproc_def split:option.splits if_splits) |
|
76 |
|
77 lemma cq2smsgq_qi: |
|
78 "\<lbrakk>cq2smsgq s q = Some (Init q', sec, sms); valid s\<rbrakk> \<Longrightarrow> q = q' \<and> \<not> deleted (O_msgq q) s \<and> q \<in> init_msgqs" |
|
79 by (simp add:cq2smsgq_def split:option.splits if_splits) |
|
80 |
|
81 lemma cm2smsg_mi: |
|
82 "\<lbrakk>cm2smsg s q m = Some (Init m', sec, ttag); q \<in> init_msgqs; valid s\<rbrakk> |
|
83 \<Longrightarrow> m = m' \<and> \<not> deleted (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs" |
|
84 by (clarsimp simp add:cm2smsg_def split:if_splits option.splits) |
|
85 |
|
86 lemma ch2sshm_hi: |
|
87 "\<lbrakk>ch2sshm s h = Some (Init h', sec); valid s\<rbrakk> \<Longrightarrow> h = h' \<and> \<not> deleted (O_shm h) s \<and> h \<in> init_shms" |
|
88 by (clarsimp simp:ch2sshm_def split:if_splits option.splits) |
|
89 |
|
90 lemma root_not_deleted: |
|
91 "\<lbrakk>deleted (O_dir []) s; valid s\<rbrakk> \<Longrightarrow> False" |
|
92 apply (induct s, simp) |
|
93 apply (frule vd_cons, frule vt_grant_os, case_tac a, auto) |
|
94 done |
|
95 |
|
96 lemma cf2sfile_fi: |
|
97 "\<lbrakk>cf2sfile s f = Some (Init f', sec, psecopt, asecs); valid s\<rbrakk> \<Longrightarrow> f = f' \<and> |
|
98 (if (is_file s f) then \<not> deleted (O_file f) s \<and> is_init_file f |
|
99 else \<not> deleted (O_dir f) s \<and> is_init_dir f)" |
|
100 apply (case_tac f) |
|
101 by (auto simp:sroot_def cf2sfile_def root_is_init_dir dest!:root_is_dir' root_not_deleted |
|
102 split:if_splits option.splits) |
|
103 |
|
104 lemma init_deled_imp_deled_s: |
|
105 "\<lbrakk>deleted obj s; init_alive obj; sobj \<in> (s2ss s); valid s\<rbrakk> \<Longrightarrow> \<not> init_obj_related sobj obj" |
|
106 apply (rule notI) |
|
107 apply (clarsimp simp:s2ss_def) |
|
108 apply (case_tac obj, case_tac [!] obja, case_tac sobj) |
|
109 apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi simp:co2sobj.simps) |
|
110 apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_prop1' is_file_def is_dir_def co2sobj.simps |
|
111 split:option.splits t_inode_tag.splits dest!:cf2sfile_fi) |
|
112 done |
|
113 |
|
114 lemma deleted_imp_deletable_s: |
|
115 "\<lbrakk>deleted obj s; init_alive obj; valid s\<rbrakk> \<Longrightarrow> deletable_s obj" |
|
116 apply (simp add:deletable_s_def) |
|
117 apply (frule d2s_main) |
|
118 apply (simp add:init_ss_in_def) |
|
119 apply (erule bexE) |
|
120 apply (rule_tac x = ss' in bexI) |
|
121 apply (auto simp add: init_ss_eq_def dest!:init_deled_imp_deled_s) |
|
122 apply (case_tac obj, case_tac [!] sobj) |
|
123 apply auto |
|
124 apply (erule set_mp) |
|
125 apply (simp) |
|
126 apply auto |
|
127 apply (rule_tac x = "(Init list, (aa, ab, b), ac, ba)" in bexI) |
|
128 apply auto |
|
129 done |
|
130 |
|
131 lemma init_related_imp_init_sobj: |
|
132 "init_obj_related sobj obj \<Longrightarrow> is_init_sobj sobj" |
|
133 apply (case_tac sobj, case_tac [!] obj, auto) |
|
134 apply (rule_tac x = "(Init list, (aa, ab, b), ac, ba)" in bexI, auto) |
|
135 done |
|
136 |
|
137 theorem undeletable_s_complete: |
|
138 assumes undel_s: "undeletable_s obj" |
|
139 shows "undeletable obj" |
|
140 proof- |
|
141 from undel_s have init_alive: "init_alive obj" |
|
142 and alive_s: "\<forall> ss \<in> static. \<exists> sobj \<in> ss. init_obj_related sobj obj" |
|
143 using undeletable_s_def by auto |
|
144 have "\<not> (\<exists> s. valid s \<and> deleted obj s)" |
|
145 proof |
|
146 assume "\<exists> s. valid s \<and> deleted obj s" |
|
147 then obtain s where vs: "valid s" and del: "deleted obj s" by auto |
|
148 from vs have vss: "s2ss s \<propto> static" by (rule d2s_main) |
|
149 with alive_s obtain sobj where in_ss: "sobj \<in> (s2ss s)" |
|
150 and related: "init_obj_related sobj obj" |
|
151 apply (simp add:init_ss_in_def init_ss_eq_def) |
|
152 apply (erule bexE, erule_tac x= ss' in ballE) |
|
153 apply (auto dest:init_related_imp_init_sobj) |
|
154 done |
|
155 from init_alive del vs have "deletable_s obj" |
|
156 by (auto elim:deleted_imp_deletable_s) |
|
157 with alive_s |
|
158 show False by (auto simp:deletable_s_def) |
|
159 qed |
|
160 with init_alive show ?thesis |
|
161 by (simp add:undeletable_def) |
|
162 qed |
|
163 |
|
164 theorem final_offer: |
|
165 "\<lbrakk>undeletable_s obj; \<not> taintable_s obj; init_alive obj\<rbrakk> \<Longrightarrow> \<not> taintable obj" |
|
166 apply (erule swap) |
|
167 by (simp add:static_complete undeletable_s_complete) |
|
168 |
|
169 (************** static \<rightarrow> dynamic ***************) |
|
170 |
|
171 |
|
172 lemma set_eq_D: |
|
173 "\<lbrakk>x \<in> S; {x. P x} = S\<rbrakk> \<Longrightarrow> P x" |
|
174 by auto |
|
175 |
|
176 lemma cqm2sms_prop1: |
|
177 "\<lbrakk>cqm2sms s q queue = Some sms; sm \<in> set sms\<rbrakk> \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm" |
|
178 apply (induct queue arbitrary:sms) |
|
179 apply (auto simp:cqm2sms.simps split:option.splits) |
|
180 done |
|
181 |
|
182 lemma sq_sm_prop: |
|
183 "\<lbrakk>sm \<in> set sms; cq2smsgq s q = Some (qi, qsec, sms); valid s\<rbrakk> |
|
184 \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm" |
|
185 by (auto simp:cq2smsgq_def split: option.splits intro:cqm2sms_prop1) |
|
186 |
|
187 declare co2sobj.simps [simp add] |
|
188 |
|
189 lemma tainted_s_imp_tainted: |
|
190 "\<lbrakk>tainted_s ss sobj; ss \<in> static\<rbrakk> \<Longrightarrow> \<exists> s obj. valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s" |
|
191 apply (drule s2d_main) |
|
192 apply (erule exE, erule conjE, simp add:s2ss_def) |
|
193 apply (rule_tac x = s in exI, simp) |
|
194 apply (case_tac sobj, simp_all) |
|
195 apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) |
|
196 apply (rule_tac x = obj in exI, simp) |
|
197 apply (case_tac obj, (simp split:option.splits if_splits)+) |
|
198 |
|
199 apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) |
|
200 apply (rule_tac x = obj in exI, simp) |
|
201 apply (case_tac obj, (simp split:option.splits if_splits)+) |
|
202 done |
|
203 |
|
204 lemma has_same_inode_prop3: |
|
205 "has_same_inode s f f' \<Longrightarrow> has_same_inode s f' f" |
|
206 by (auto simp:has_same_inode_def) |
|
207 |
|
208 theorem static_sound: |
|
209 assumes tbl_s: "taintable_s obj" |
|
210 shows "taintable obj" |
|
211 proof- |
|
212 from tbl_s obtain ss sobj where static: "ss \<in> static" |
|
213 and sobj: "tainted_s ss sobj" and related: "init_obj_related sobj obj" |
|
214 and init_alive: "init_alive obj" by (auto simp:taintable_s_def) |
|
215 from static sobj tainted_s_imp_tainted |
|
216 obtain s obj' where co2sobj: "co2sobj s obj' = Some sobj" |
|
217 and tainted': "obj' \<in> tainted s" and vs: "valid s" by blast |
|
218 |
|
219 from co2sobj related vs |
|
220 have eq:"obj = obj' \<or> (\<exists> f f'. obj = O_file f \<and> obj' = O_file f' \<and> has_same_inode s f f')" |
|
221 apply (case_tac obj', case_tac [!] obj) |
|
222 apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi) |
|
223 apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_def is_file_def is_dir_def |
|
224 split:option.splits t_inode_tag.splits dest!:cf2sfile_fi) |
|
225 done |
|
226 with tainted' vs have tainted: "obj \<in> tainted s" |
|
227 by (auto dest:has_same_inode_prop3 intro:has_same_inode_tainted) |
|
228 from sobj related init_alive have "appropriate obj" |
|
229 by (case_tac obj, case_tac [!] sobj, auto) |
|
230 with vs init_alive tainted |
|
231 show ?thesis by (auto simp:taintable_def) |
|
232 qed |
|
233 |
|
234 end |
|
235 |
|
236 end |