1 (*<*) |
1 (*<*) |
2 theory Co2sobj_prop |
2 theory Co2sobj_prop |
3 imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop |
3 imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop |
4 begin |
4 begin |
5 (*<*) |
5 (*<*) |
6 |
6 |
7 context tainting_s begin |
7 context tainting_s begin |
8 |
8 |
9 (************ simpset for cf2sfile ***************) |
9 (************ simpset for cf2sfile ***************) |
10 |
10 |
11 declare get_parentfs_ctxts.simps [simp del] |
11 declare get_parentfs_ctxts.simps [simp del] |
|
12 |
|
13 lemma sroot_only: |
|
14 "cf2sfile s [] = Some sroot" |
|
15 by (simp add:cf2sfile_def) |
|
16 |
|
17 lemma not_file_is_dir: |
|
18 "\<lbrakk>\<not> is_file s f; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_dir s f" |
|
19 by (auto simp:is_file_def current_files_def is_dir_def |
|
20 dest:finum_has_itag finum_has_ftag' split:t_inode_tag.splits option.splits) |
|
21 |
|
22 lemma not_dir_is_file: |
|
23 "\<lbrakk>\<not> is_dir s f; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_file s f" |
|
24 by (auto simp:is_file_def current_files_def is_dir_def |
|
25 dest:finum_has_itag finum_has_ftag' split:t_inode_tag.splits option.splits) |
|
26 |
|
27 lemma is_file_or_dir: |
|
28 "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_file s f \<or> is_dir s f" |
|
29 by (auto dest:not_dir_is_file) |
|
30 |
|
31 lemma current_file_has_sfile: |
|
32 "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf" |
|
33 apply (induct f) |
|
34 apply (rule_tac x = "sroot" in exI, simp add:sroot_only) |
|
35 apply (frule parentf_in_current', simp, clarsimp) |
|
36 apply (frule parentf_is_dir'', simp) |
|
37 apply (frule is_file_or_dir, simp) |
|
38 apply (auto dest!:current_has_sec' |
|
39 simp:cf2sfile_def split:option.splits if_splits dest!:get_pfs_secs_prop) |
|
40 done |
|
41 |
|
42 definition sectxt_of_pf :: "t_state \<Rightarrow> t_file \<Rightarrow> security_context_t option" |
|
43 where |
|
44 "sectxt_of_pf s f = (case f of [] \<Rightarrow> None | (a # pf) \<Rightarrow> sectxt_of_obj s (O_dir pf))" |
|
45 |
|
46 definition get_parentfs_ctxts' :: "t_state \<Rightarrow> t_file \<Rightarrow> (security_context_t list) option" |
|
47 where |
|
48 "get_parentfs_ctxts' s f = (case f of [] \<Rightarrow> None | (a # pf) \<Rightarrow> get_parentfs_ctxts s pf)" |
|
49 |
|
50 lemma is_file_has_sfile: |
|
51 "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sec psec asecs. cf2sfile s f = Some |
|
52 (if (\<not> deleted (O_file f) s \<and> is_init_file f) then Init f else Created, |
|
53 sec, Some psec, set asecs) \<and> (sectxt_of_obj s (O_file f) = Some sec) \<and> |
|
54 (sectxt_of_pf s f = Some psec) \<and> (get_parentfs_ctxts' s f = Some asecs)" |
|
55 apply (case_tac f, simp, drule root_is_dir', simp, simp) |
|
56 apply (frule is_file_in_current) |
|
57 apply (drule current_file_has_sfile, simp) |
|
58 apply (auto simp:cf2sfile_def sectxt_of_pf_def get_parentfs_ctxts'_def split:if_splits option.splits) |
|
59 done |
|
60 |
|
61 lemma is_dir_has_sfile: |
|
62 "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> (case f of |
|
63 [] \<Rightarrow> cf2sfile s f = Some sroot |
|
64 | a # pf \<Rightarrow> (\<exists> sec psec asecs. cf2sfile s f = Some |
|
65 (if (\<not> deleted (O_dir f) s \<and> is_init_dir f) then Init f else Created, |
|
66 sec, Some psec, set asecs) \<and> (sectxt_of_obj s (O_dir f) = Some sec) \<and> |
|
67 (sectxt_of_obj s (O_dir pf) = Some psec) \<and> (get_parentfs_ctxts s pf = Some asecs)))" |
|
68 apply (case_tac f, simp add:sroot_only) |
|
69 apply (frule is_dir_in_current, frule is_dir_not_file) |
|
70 apply (drule current_file_has_sfile, simp) |
|
71 apply (auto simp:cf2sfile_def split:if_splits option.splits) |
|
72 done |
|
73 |
|
74 lemma cf2sfile_path: |
|
75 "\<lbrakk>f # pf \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = ( |
|
76 case (cf2sfile s pf) of |
|
77 Some (pfi, pfsec, psec, asecs) \<Rightarrow> (if (is_file s (f # pf)) |
|
78 then (case (sectxt_of_obj s (O_file (f # pf))) of |
|
79 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf) |
|
80 else Created, fsec, Some pfsec, asecs \<union> {pfsec}) |
|
81 | None \<Rightarrow> None) |
|
82 else (case (sectxt_of_obj s (O_dir (f # pf))) of |
|
83 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf) |
|
84 else Created, fsec, Some pfsec, asecs \<union> {pfsec}) |
|
85 | None \<Rightarrow> None) ) |
|
86 | None \<Rightarrow> None)" |
|
87 apply (frule parentf_is_dir'', simp) |
|
88 apply (frule parentf_in_current', simp) |
|
89 apply (frule is_file_or_dir, simp) |
|
90 apply (frule_tac f = pf in current_file_has_sfile, simp, erule exE) |
|
91 apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop |
|
92 simp:cf2sfile_def split:option.splits if_splits) |
|
93 apply (case_tac "is_file s (f # pf)") |
|
94 apply (frule is_file_has_sec, simp) |
|
95 apply (frule is_dir_has_sec, simp) |
|
96 apply (frule is_dir_not_file) |
|
97 apply (erule exE)+ |
|
98 apply (auto split:option.splits)[1] |
|
99 apply simp |
|
100 |
|
101 apply (rule ext) |
|
102 apply (subst (1) cf2sfile_def) |
|
103 apply (auto simp del:deleted.simps get_parentfs_ctxts.simps split:option.splits if_splits) |
12 |
104 |
13 lemma cf2sfile_open_none1: |
105 lemma cf2sfile_open_none1: |
14 "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f b = cf2sfile s f b" |
106 "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f b = cf2sfile s f b" |
15 apply (frule vd_cons, frule vt_grant_os) |
107 apply (frule vd_cons, frule vt_grant_os) |
16 apply (frule noroot_events, case_tac f, simp) |
108 apply (frule noroot_events, case_tac f, simp) |
30 lemma cf2sfile_open_none: |
122 lemma cf2sfile_open_none: |
31 "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) = cf2sfile s" |
123 "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) = cf2sfile s" |
32 apply (rule ext, rule ext) |
124 apply (rule ext, rule ext) |
33 apply (simp add:cf2sfile_open_none1 cf2sfile_open_none2) |
125 apply (simp add:cf2sfile_open_none1 cf2sfile_open_none2) |
34 done |
126 done |
35 |
|
36 lemma sroot_only: |
|
37 "cf2sfile s [] = (\<lambda> b. if b then None else Some sroot)" |
|
38 by (rule ext, simp add:cf2sfile_def) |
|
39 |
127 |
40 lemma cf2sfile_open_some1: |
128 lemma cf2sfile_open_some1: |
41 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk> |
129 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk> |
42 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'" |
130 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'" |
43 apply (frule vd_cons, frule vt_grant_os, frule noroot_events, rule ext) |
131 apply (frule vd_cons, frule vt_grant_os, frule noroot_events, rule ext) |
58 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_dir s f'\<rbrakk> |
146 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_dir s f'\<rbrakk> |
59 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' False = cf2sfile s f' False" |
147 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' False = cf2sfile s f' False" |
60 apply (frule vd_cons, drule is_dir_in_current) |
148 apply (frule vd_cons, drule is_dir_in_current) |
61 by (simp add:cf2sfile_open_some1) |
149 by (simp add:cf2sfile_open_some1) |
62 |
150 |
63 lemma cf2sfile_open_some: |
151 lemma cf2sfile_open_some4: |
64 "valid (Open p f flag fd (Some inum) # s) \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f True = ( |
152 "valid (Open p f flag fd (Some inum) # s) \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f True = ( |
65 case (parent f) of |
153 case (parent f) of |
66 Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd (Some inum) # s) (O_file f), sectxt_of_obj s (O_dir pf), |
154 Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd (Some inum) # s) (O_file f), sectxt_of_obj s (O_dir pf), |
67 get_parentfs_ctxts s pf) of |
155 get_parentfs_ctxts s pf) of |
68 (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs) |
156 (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs) |
70 | None \<Rightarrow> None)" |
158 | None \<Rightarrow> None)" |
71 apply (frule vd_cons, frule vt_grant_os, frule noroot_events) |
159 apply (frule vd_cons, frule vt_grant_os, frule noroot_events) |
72 apply (case_tac f, simp) |
160 apply (case_tac f, simp) |
73 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
161 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
74 get_parentfs_ctxts_simps) |
162 get_parentfs_ctxts_simps) |
75 apply (rule impI) |
163 apply (rule impI, (erule conjE)+) |
76 thm not_deleted_imp_exists |
164 apply (drule not_deleted_init_file, simp+) |
77 apply (auto split:if_splits option.splits dest!:current_has_sec' |
165 apply (simp add:is_file_in_current) |
78 simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
166 done |
79 get_parentfs_ctxts_simps) |
167 |
80 |
168 lemma cf2sfile_open_some5: |
81 |
169 "valid (Open p f flag fd (Some inum) # s) \<Longrightarrow> |
|
170 cf2sfile (Open p f flag fd (Some inum) # s) f False = cf2sfile s f False" |
|
171 apply (frule vd_cons, frule vt_grant_os, frule noroot_events) |
|
172 apply (case_tac f, simp) |
|
173 apply (auto simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
|
174 get_parentfs_ctxts_simps split:option.splits) |
|
175 done |
82 |
176 |
83 lemma cf2sfile_open: |
177 lemma cf2sfile_open: |
84 "valid (Open p f flag fd opt # s) \<Longrightarrow> cf2sfile (Open p f flag fd opt # s) = (\<lambda> f' b. |
178 "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk> |
|
179 \<Longrightarrow> cf2sfile (Open p f flag fd opt # s) f' b = ( |
85 if (opt = None) then cf2sfile s f' b |
180 if (opt = None) then cf2sfile s f' b |
86 else if (f' = f \<and> b = True) |
181 else if (f' = f \<and> b) |
87 then (case (parent f) of |
182 then (case (parent f) of |
88 Some pf \<Rightarrow> (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), |
183 Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd opt # s) (O_file f), sectxt_of_obj s (O_dir pf), |
89 get_parentfs_ctxts s pf) of |
184 get_parentfs_ctxts s pf) of |
90 (Some sec, Some psec, Some asecs) \<Rightarrow> |
185 (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs) |
91 Some (if (\<not> deleted (O_file f) s \<and> f \<in> init_files) |
|
92 then Init f else Created, sec, Some psec, set asecs) |
|
93 | _ \<Rightarrow> None) |
186 | _ \<Rightarrow> None) |
94 | None \<Rightarrow> None) |
187 | None \<Rightarrow> None) |
95 else cf2sfile s f' b)" |
188 else cf2sfile s f' b)" |
96 apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext) |
189 apply (case_tac opt) |
97 apply (auto split:if_splits option.splits |
190 apply (simp add:cf2sfile_open_none) |
98 simp:sectxt_of_obj_simps) |
191 apply (case_tac "f = f'") |
|
192 apply (auto simp:cf2sfile_open_some1 cf2sfile_open_some4 cf2sfile_open_some5 current_files_simps) |
|
193 done |
|
194 |
|
195 lemma cf2sfile_mkdir1: |
|
196 "\<lbrakk>valid (Mkdir p f i # s); f' \<in> current_files s\<rbrakk> |
|
197 \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'" |
|
198 apply (frule vd_cons, frule vt_grant_os, frule noroot_events, rule ext) |
|
199 apply (case_tac "f = f'", simp) |
|
200 apply (induct f', simp add:sroot_only, simp) |
|
201 apply (frule parentf_in_current', simp+) |
|
202 apply clarsimp |
|
203 apply (case_tac "f = f'", simp+) |
|
204 apply (simp (no_asm_simp) add:cf2sfile_def) |
|
205 apply (auto simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
|
206 get_parentfs_ctxts_simps split:if_splits option.splits) |
|
207 done |
|
208 |
|
209 lemma cf2sfile_mkdir2: |
|
210 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_file s f'\<rbrakk> |
|
211 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' True = cf2sfile s f' True" |
|
212 apply (frule vd_cons, drule is_file_in_current) |
|
213 by (simp add:cf2sfile_open_some1) |
|
214 |
|
215 lemma cf2sfile_mkdir3: |
|
216 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_dir s f'\<rbrakk> |
|
217 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' False = cf2sfile s f' False" |
|
218 apply (frule vd_cons, drule is_dir_in_current) |
|
219 by (simp add:cf2sfile_open_some1) |
|
220 |
|
221 |
|
222 lemma cf2sfile_mkdir: |
|
223 "valid (Mkdir p f i # s) |
|
224 \<Longrightarrow> cf2sfile (Mkdir p f i # s) = (\<lambda> f' b. |
|
225 if (f' = f \<and> \<not> b) |
|
226 then (case (parent f) of |
|
227 Some pf \<Rightarrow> (case (sectxt_of_obj (Mkdir p f i # s) (O_dir f), sectxt_of_obj s (O_dir pf), |
|
228 get_parentfs_ctxts s pf) of |
|
229 (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs) |
|
230 | _ \<Rightarrow> None) |
|
231 | None \<Rightarrow> None) |
|
232 else cf2sfile s f' b)" |
|
233 apply (frule vd_cons, frule vt_grant_os) |
|
234 apply (rule ext, rule ext) |
|
235 |
|
236 apply (auto simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
|
237 get_parentfs_ctxts_simps split:if_splits option.splits) |
|
238 |
|
239 |
|
240 |
|
241 |
|
242 |
|
243 |
99 |
244 |
100 |
245 |
101 |
246 |
102 |
247 |
103 |
248 |