|
1 theory Sectxt_prop |
|
2 imports Main Flask Flask_type Current_files_prop Current_sockets_prop Alive_prop |
|
3 begin |
|
4 |
|
5 context flask begin |
|
6 |
|
7 lemma alive_obj_has_type: |
|
8 assumes alive: "alive s obj" and vs: "valid s" |
|
9 shows "\<exists> t. type_of_obj s obj = Some t" |
|
10 using alive vs |
|
11 proof (induct s arbitrary:obj) |
|
12 case Nil |
|
13 thus ?case |
|
14 by (simp add:init_alive_prop[THEN sym] init_obj_has_type) |
|
15 next |
|
16 case (Cons e s) |
|
17 hence a2: "alive (e # s) obj" and a3: "valid (e # s)" by auto |
|
18 hence a4: "valid s" and a5: "os_grant s e" and a6: "grant s e" |
|
19 by (auto intro:vd_cons vt_grant_os vt_grant) |
|
20 hence a1: "\<And> obj. alive s obj \<Longrightarrow> \<exists>t. type_of_obj s obj = Some t" using Cons by auto |
|
21 have a1': "\<And> obj. type_of_obj s obj = None \<Longrightarrow> \<not> alive s obj" by (rule_tac notI, auto dest:a1) |
|
22 have p1: "\<And> p. p \<in> current_procs s \<Longrightarrow> \<exists> t. type_of_obj s (O_proc p) = Some t" by (auto intro:a1) |
|
23 have p2: "\<And> f. is_file s f \<Longrightarrow> \<exists> t. type_of_obj s (O_file f) = Some t" |
|
24 by (auto intro!:a1 simp:is_file_in_current) |
|
25 have p3: "\<And> f. is_dir s f \<Longrightarrow> \<exists> t. type_of_obj s (O_dir f) = Some t" |
|
26 by (auto intro!:a1 simp:is_dir_in_current) |
|
27 have p4: "\<And> sock. is_tcp_sock s sock \<Longrightarrow> \<exists> t. type_of_obj s (O_tcp_sock sock) = Some t" |
|
28 by (auto intro!:a1 simp:is_tcp_in_current) |
|
29 have p5: "\<And> sock. is_udp_sock s sock \<Longrightarrow> \<exists> t. type_of_obj s (O_udp_sock sock) = Some t" |
|
30 by (auto intro!:a1 simp:is_udp_in_current) |
|
31 have p6: "\<And> p fd. fd \<in> current_proc_fds s p \<Longrightarrow> \<exists> t. type_of_obj s (O_fd p fd) = Some t" |
|
32 by (auto intro:a1) |
|
33 have p7: "\<And> n. n \<in> init_nodes \<Longrightarrow> \<exists> t. type_of_obj s (O_node n) = Some t" by (auto intro:a1) |
|
34 (* |
|
35 have p8: "\<And> h. h \<in> current_shms s \<Longrightarrow> \<exists> t. type_of_obj s (O_shm h) = Some t" by (auto intro:a1) |
|
36 *) |
|
37 have p9: "\<And> q. q \<in> current_msgqs s \<Longrightarrow> \<exists> t. type_of_obj s (O_msgq q) = Some t" by (auto intro:a1) |
|
38 have p10: "\<And> q m. \<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s\<rbrakk> |
|
39 \<Longrightarrow> \<exists> t. type_of_obj s (O_msg q m) = Some t" by (auto intro:a1) |
|
40 show ?case using a5 a2 a4 a3 |
|
41 apply (case_tac e) |
|
42 apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits |
|
43 dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 (* p8 *) p9 p10 simp:alive_simps) |
|
44 apply (frule_tac p = nat1 in file_fds_subset_pfds) |
|
45 apply (rule a1, auto) |
|
46 done |
|
47 qed |
|
48 |
|
49 lemma alive_obj_has_user: |
|
50 assumes alive: "alive s obj" and vs: "valid s" |
|
51 shows "\<exists> t. user_of_obj s obj = Some t" |
|
52 using alive vs |
|
53 proof (induct s arbitrary:obj) |
|
54 case Nil |
|
55 thus ?case |
|
56 by (simp add:init_alive_prop[THEN sym] init_obj_has_user) |
|
57 next |
|
58 case (Cons e s) |
|
59 hence a2: "alive (e # s) obj" and a3: "valid (e # s)" by auto |
|
60 hence a4: "valid s" and a5: "os_grant s e" and a6: "grant s e" |
|
61 by (auto intro:vd_cons vt_grant_os vt_grant) |
|
62 hence a1: "\<And> obj. alive s obj \<Longrightarrow> \<exists>t. user_of_obj s obj = Some t" using Cons by auto |
|
63 have a1': "\<And> obj. user_of_obj s obj = None \<Longrightarrow> \<not> alive s obj" by (rule_tac notI, auto dest:a1) |
|
64 have p1: "\<And> p. p \<in> current_procs s \<Longrightarrow> \<exists> t. user_of_obj s (O_proc p) = Some t" by (auto intro:a1) |
|
65 have p2: "\<And> f. is_file s f \<Longrightarrow> \<exists> t. user_of_obj s (O_file f) = Some t" |
|
66 by (auto intro!:a1 simp:is_file_in_current) |
|
67 have p3: "\<And> f. is_dir s f \<Longrightarrow> \<exists> t. user_of_obj s (O_dir f) = Some t" |
|
68 by (auto intro!:a1 simp:is_dir_in_current) |
|
69 have p4: "\<And> sock. is_tcp_sock s sock \<Longrightarrow> \<exists> t. user_of_obj s (O_tcp_sock sock) = Some t" |
|
70 by (auto intro!:a1 simp:is_tcp_in_current) |
|
71 have p5: "\<And> sock. is_udp_sock s sock \<Longrightarrow> \<exists> t. user_of_obj s (O_udp_sock sock) = Some t" |
|
72 by (auto intro!:a1 simp:is_udp_in_current) |
|
73 have p6: "\<And> p fd. fd \<in> current_proc_fds s p \<Longrightarrow> \<exists> t. user_of_obj s (O_fd p fd) = Some t" |
|
74 by (auto intro:a1) |
|
75 have p7: "\<And> n. n \<in> init_nodes \<Longrightarrow> \<exists> t. user_of_obj s (O_node n) = Some t" by (auto intro:a1) |
|
76 (* |
|
77 have p8: "\<And> h. h \<in> current_shms s \<Longrightarrow> \<exists> t. user_of_obj s (O_shm h) = Some t" by (auto intro:a1) |
|
78 *) |
|
79 have p9: "\<And> q. q \<in> current_msgqs s \<Longrightarrow> \<exists> t. user_of_obj s (O_msgq q) = Some t" by (auto intro:a1) |
|
80 have p10: "\<And> q m. \<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s\<rbrakk> |
|
81 \<Longrightarrow> \<exists> t. user_of_obj s (O_msg q m) = Some t" by (auto intro:a1) |
|
82 show ?case using a5 a2 a4 a3 |
|
83 apply (case_tac e) |
|
84 apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits |
|
85 dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 (* p8 *) p9 p10 simp:alive_simps) |
|
86 apply (frule_tac p = nat1 in file_fds_subset_pfds) |
|
87 apply (rule a1, auto) |
|
88 done |
|
89 qed |
|
90 |
|
91 lemma alive_obj_has_type': "\<lbrakk>type_of_obj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj" |
|
92 by (rule_tac notI, auto dest:alive_obj_has_type) |
|
93 |
|
94 lemma current_proc_has_type: |
|
95 "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_proc p) = Some t" |
|
96 by (auto intro:alive_obj_has_type) |
|
97 |
|
98 lemma current_proc_has_type': |
|
99 "\<lbrakk>type_of_obj s (O_proc p) = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s" |
|
100 by (rule notI, auto dest:current_proc_has_type) |
|
101 |
|
102 lemma is_file_has_type: "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_file f) = Some t" |
|
103 by (auto intro:alive_obj_has_type simp:is_file_in_current) |
|
104 |
|
105 lemma is_file_has_type': "\<lbrakk>type_of_obj s (O_file f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_file s f" |
|
106 by (auto intro:notI dest:is_file_has_type) |
|
107 |
|
108 lemma is_dir_has_type: "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_dir f) = Some t" |
|
109 by (auto intro:alive_obj_has_type simp:is_dir_in_current) |
|
110 |
|
111 lemma is_dir_has_type': "\<lbrakk>type_of_obj s (O_dir f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_dir s f" |
|
112 by (auto intro:notI dest:is_dir_has_type) |
|
113 |
|
114 lemma is_tcp_has_type: "\<lbrakk>is_tcp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_tcp_sock sock) = Some t" |
|
115 by (auto intro:alive_obj_has_type simp:is_tcp_in_current) |
|
116 |
|
117 lemma is_tcp_has_type': "\<lbrakk>type_of_obj s (O_tcp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_tcp_sock s sock" |
|
118 by (auto intro:notI dest:is_tcp_has_type) |
|
119 |
|
120 lemma is_udp_has_type: "\<lbrakk>is_udp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_udp_sock sock) = Some t" |
|
121 by (auto intro:alive_obj_has_type simp:is_udp_in_current) |
|
122 |
|
123 lemma is_udp_has_type': "\<lbrakk>type_of_obj s (O_udp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_udp_sock s sock" |
|
124 by (auto intro:notI dest:is_udp_has_type) |
|
125 |
|
126 lemma current_fd_has_type: "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_fd p fd) = Some t" |
|
127 by (auto intro:alive_obj_has_type) |
|
128 |
|
129 lemma current_fd_has_type': "\<lbrakk>type_of_obj s (O_fd p fd) = None; valid s\<rbrakk> \<Longrightarrow> fd \<notin> current_proc_fds s p" |
|
130 by (auto intro:notI dest:current_fd_has_type) |
|
131 |
|
132 lemma init_node_has_type: "\<lbrakk>n \<in> init_nodes; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_node n) = Some t" |
|
133 by (auto intro: alive_obj_has_type) |
|
134 |
|
135 lemma init_node_has_type': "\<lbrakk>type_of_obj s (O_node n) = None; valid s\<rbrakk> \<Longrightarrow> n \<notin> init_nodes" |
|
136 by (auto intro:notI dest:init_node_has_type) |
|
137 |
|
138 (* |
|
139 lemma current_shm_has_type: "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_shm h) = Some t" |
|
140 by (auto intro:alive_obj_has_type) |
|
141 |
|
142 lemma current_shm_has_type': "\<lbrakk>type_of_obj s (O_shm h) = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s" |
|
143 by (auto intro:notI dest:current_shm_has_type) |
|
144 *) |
|
145 lemma current_msgq_has_type: "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_msgq q) = Some t" |
|
146 by (auto intro:alive_obj_has_type) |
|
147 |
|
148 lemma current_msgq_has_type': "\<lbrakk>type_of_obj s (O_msgq q) = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s" |
|
149 by (auto intro:notI dest:current_msgq_has_type) |
|
150 |
|
151 lemma current_msg_has_type: "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk> |
|
152 \<Longrightarrow> \<exists> t. type_of_obj s (O_msg q m) = Some t" |
|
153 by (auto intro:alive_obj_has_type) |
|
154 |
|
155 lemma current_msg_has_type': "\<lbrakk>type_of_obj s (O_msg q m) = None; valid s\<rbrakk> |
|
156 \<Longrightarrow> m \<notin> set (msgs_of_queue s q) \<or> q \<notin> current_msgqs s" |
|
157 by (auto dest!:current_msg_has_type) |
|
158 |
|
159 lemmas current_has_type = alive_obj_has_type current_proc_has_type is_file_has_type is_dir_has_type |
|
160 is_tcp_has_type is_udp_has_type current_fd_has_type init_node_has_type (* current_shm_has_type *) |
|
161 current_msgq_has_type current_msg_has_type |
|
162 |
|
163 lemmas current_has_type' = alive_obj_has_type' current_proc_has_type' is_file_has_type' is_dir_has_type' |
|
164 is_tcp_has_type' is_udp_has_type' current_fd_has_type' init_node_has_type' (* current_shm_has_type' *) |
|
165 current_msgq_has_type' current_msg_has_type' |
|
166 |
|
167 lemma alive_obj_has_user': "\<lbrakk>user_of_obj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj" |
|
168 by (rule_tac notI, auto dest:alive_obj_has_user) |
|
169 |
|
170 lemma current_proc_has_user: |
|
171 "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_proc p) = Some t" |
|
172 by (auto intro:alive_obj_has_user) |
|
173 |
|
174 lemma current_proc_has_user': |
|
175 "\<lbrakk>user_of_obj s (O_proc p) = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s" |
|
176 by (rule notI, auto dest:current_proc_has_user) |
|
177 |
|
178 lemma is_file_has_user: "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_file f) = Some t" |
|
179 by (auto intro:alive_obj_has_user simp:is_file_in_current) |
|
180 |
|
181 lemma is_file_has_user': "\<lbrakk>user_of_obj s (O_file f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_file s f" |
|
182 by (auto intro:notI dest:is_file_has_user) |
|
183 |
|
184 lemma is_dir_has_user: "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_dir f) = Some t" |
|
185 by (auto intro:alive_obj_has_user simp:is_dir_in_current) |
|
186 |
|
187 lemma is_dir_has_user': "\<lbrakk>user_of_obj s (O_dir f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_dir s f" |
|
188 by (auto intro:notI dest:is_dir_has_user) |
|
189 |
|
190 lemma is_tcp_has_user: "\<lbrakk>is_tcp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_tcp_sock sock) = Some t" |
|
191 by (auto intro:alive_obj_has_user simp:is_tcp_in_current) |
|
192 |
|
193 lemma is_tcp_has_user': "\<lbrakk>user_of_obj s (O_tcp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_tcp_sock s sock" |
|
194 by (auto intro:notI dest:is_tcp_has_user) |
|
195 |
|
196 lemma is_udp_has_user: "\<lbrakk>is_udp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_udp_sock sock) = Some t" |
|
197 by (auto intro:alive_obj_has_user simp:is_udp_in_current) |
|
198 |
|
199 lemma is_udp_has_user': "\<lbrakk>user_of_obj s (O_udp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_udp_sock s sock" |
|
200 by (auto intro:notI dest:is_udp_has_user) |
|
201 |
|
202 lemma current_fd_has_user: "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_fd p fd) = Some t" |
|
203 by (auto intro:alive_obj_has_user) |
|
204 |
|
205 lemma current_fd_has_user': "\<lbrakk>user_of_obj s (O_fd p fd) = None; valid s\<rbrakk> \<Longrightarrow> fd \<notin> current_proc_fds s p" |
|
206 by (auto intro:notI dest:current_fd_has_user) |
|
207 |
|
208 lemma init_node_has_user: "\<lbrakk>n \<in> init_nodes; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_node n) = Some t" |
|
209 by (auto intro: alive_obj_has_user) |
|
210 |
|
211 lemma init_node_has_user': "\<lbrakk>user_of_obj s (O_node n) = None; valid s\<rbrakk> \<Longrightarrow> n \<notin> init_nodes" |
|
212 by (auto intro:notI dest:init_node_has_user) |
|
213 |
|
214 (* |
|
215 lemma current_shm_has_user: "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_shm h) = Some t" |
|
216 by (auto intro:alive_obj_has_user) |
|
217 |
|
218 lemma current_shm_has_user': "\<lbrakk>user_of_obj s (O_shm h) = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s" |
|
219 by (auto intro:notI dest:current_shm_has_user) |
|
220 *) |
|
221 |
|
222 lemma current_msgq_has_user: "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_msgq q) = Some t" |
|
223 by (auto intro:alive_obj_has_user) |
|
224 |
|
225 lemma current_msgq_has_user': "\<lbrakk>user_of_obj s (O_msgq q) = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s" |
|
226 by (auto intro:notI dest:current_msgq_has_user) |
|
227 |
|
228 lemma current_msg_has_user: "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk> |
|
229 \<Longrightarrow> \<exists> t. user_of_obj s (O_msg q m) = Some t" |
|
230 by (auto intro:alive_obj_has_user) |
|
231 |
|
232 lemma current_msg_has_user': "\<lbrakk>user_of_obj s (O_msg q m) = None; valid s\<rbrakk> |
|
233 \<Longrightarrow> m \<notin> set (msgs_of_queue s q) \<or> q \<notin> current_msgqs s" |
|
234 by (auto dest!:current_msg_has_user) |
|
235 |
|
236 lemmas current_has_user = alive_obj_has_user current_proc_has_user is_file_has_user is_dir_has_user |
|
237 is_tcp_has_user is_udp_has_user current_fd_has_user init_node_has_user (* current_shm_has_user *) |
|
238 current_msgq_has_user current_msg_has_user |
|
239 |
|
240 lemmas current_has_user' = alive_obj_has_user' current_proc_has_user' is_file_has_user' is_dir_has_user' |
|
241 is_tcp_has_user' is_udp_has_user' current_fd_has_user' init_node_has_user' (* current_shm_has_user' *) |
|
242 current_msgq_has_user' current_msg_has_user' |
|
243 |
|
244 lemma current_proc_has_role: |
|
245 "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> r. role_of_proc s p = Some r" |
|
246 apply (induct s arbitrary:p, simp add:init_procrole_prop2) |
|
247 apply (frule vd_cons, frule vt_grant_os, frule vt_grant, case_tac a) |
|
248 apply (auto split:option.splits dest:current_has_type' simp:sectxt_of_obj_def) |
|
249 done |
|
250 |
|
251 lemma current_proc_has_role': |
|
252 "\<lbrakk>role_of_proc s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s" |
|
253 by (auto dest:current_proc_has_role) |
|
254 |
|
255 lemma alive_obj_has_role: |
|
256 "\<lbrakk>alive s obj; valid s\<rbrakk> \<Longrightarrow> \<exists> r. role_of_obj s obj = Some r" |
|
257 by (case_tac obj, auto intro:current_proc_has_role) |
|
258 |
|
259 lemma alive_obj_has_sec: |
|
260 "\<lbrakk>alive s obj; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s obj = Some sec" |
|
261 apply (frule alive_obj_has_type, simp) |
|
262 apply (frule alive_obj_has_role, simp) |
|
263 apply (frule alive_obj_has_user, simp) |
|
264 apply (auto split:option.splits simp:sectxt_of_obj_def) |
|
265 done |
|
266 |
|
267 lemma alive_obj_has_sec': |
|
268 "\<lbrakk>sectxt_of_obj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj" |
|
269 by (auto dest:alive_obj_has_sec) |
|
270 |
|
271 lemma alive_obj_has_sec'': |
|
272 "\<lbrakk>alive s obj; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s obj = Some (u,r,t)" |
|
273 by (auto dest:alive_obj_has_sec) |
|
274 |
|
275 lemma current_proc_has_sec: |
|
276 "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_proc p) = Some sec" |
|
277 by (rule alive_obj_has_sec, simp+) |
|
278 |
|
279 lemma current_proc_has_sec': |
|
280 "\<lbrakk>sectxt_of_obj s (O_proc p) = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s" |
|
281 by (rule notI, auto dest:current_proc_has_sec) |
|
282 |
|
283 lemma current_proc_has_sec'': |
|
284 "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_proc p) = Some (u,r,t)" |
|
285 by (drule current_proc_has_sec, auto) |
|
286 |
|
287 lemma is_file_has_sec: "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_file f) = Some sec" |
|
288 by (rule alive_obj_has_sec, simp_all add:is_file_in_current) |
|
289 |
|
290 lemma is_file_has_sec': "\<lbrakk>sectxt_of_obj s (O_file f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_file s f" |
|
291 by (auto intro:notI dest:is_file_has_sec) |
|
292 |
|
293 lemma is_file_has_sec'': "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_file f) = Some (u,r,t)" |
|
294 by (drule is_file_has_sec, auto) |
|
295 |
|
296 lemma is_dir_has_sec: "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_dir f) = Some sec" |
|
297 by (rule alive_obj_has_sec, simp_all add:is_dir_in_current) |
|
298 |
|
299 lemma is_dir_has_sec': "\<lbrakk>sectxt_of_obj s (O_dir f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_dir s f" |
|
300 by (auto intro:notI dest:is_dir_has_sec) |
|
301 |
|
302 lemma is_dir_has_sec'': "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_dir f) = Some (u,r,t)" |
|
303 by (drule is_dir_has_sec, auto) |
|
304 |
|
305 lemma is_tcp_has_sec: "\<lbrakk>is_tcp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_tcp_sock sock) = Some sec" |
|
306 by (rule alive_obj_has_sec, simp_all add:is_tcp_in_current) |
|
307 |
|
308 lemma is_tcp_has_sec': "\<lbrakk>sectxt_of_obj s (O_tcp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_tcp_sock s sock" |
|
309 by (auto intro:notI dest:is_tcp_has_sec) |
|
310 |
|
311 lemma is_tcp_has_sec'': "\<lbrakk>is_tcp_sock s sock; valid s\<rbrakk> |
|
312 \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_tcp_sock sock) = Some (u,r,t)" |
|
313 by (drule is_tcp_has_sec, simp_all add:is_tcp_in_current) |
|
314 |
|
315 lemma is_udp_has_sec: "\<lbrakk>is_udp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_udp_sock sock) = Some sec" |
|
316 by (rule alive_obj_has_sec, simp_all add:is_udp_in_current) |
|
317 |
|
318 lemma is_udp_has_sec': "\<lbrakk>sectxt_of_obj s (O_udp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_udp_sock s sock" |
|
319 by (auto intro:notI dest:is_udp_has_sec) |
|
320 |
|
321 lemma is_udp_has_sec'': "\<lbrakk>is_udp_sock s sock; valid s\<rbrakk> |
|
322 \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_udp_sock sock) = Some (u,r,t)" |
|
323 by (drule is_udp_has_sec, simp_all add:is_udp_in_current) |
|
324 |
|
325 lemma current_fd_has_sec: "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_fd p fd) = Some sec" |
|
326 by (rule alive_obj_has_sec, simp+) |
|
327 |
|
328 lemma current_fd_has_sec': "\<lbrakk>sectxt_of_obj s (O_fd p fd) = None; valid s\<rbrakk> \<Longrightarrow> fd \<notin> current_proc_fds s p" |
|
329 by (auto intro:notI dest:current_fd_has_sec) |
|
330 |
|
331 lemma current_fd_has_sec'': "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> |
|
332 \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_fd p fd) = Some (u, r, t)" |
|
333 by (drule current_fd_has_sec, simp+) |
|
334 |
|
335 lemma init_node_has_sec: "\<lbrakk>n \<in> init_nodes; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_node n) = Some sec" |
|
336 by (rule alive_obj_has_sec, simp+) |
|
337 |
|
338 lemma init_node_has_sec': "\<lbrakk>sectxt_of_obj s (O_node n) = None; valid s\<rbrakk> \<Longrightarrow> n \<notin> init_nodes" |
|
339 by (auto intro:notI dest:init_node_has_sec) |
|
340 |
|
341 lemma init_node_has_sec'': "\<lbrakk>n \<in> init_nodes; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_node n) = Some (u,r,t)" |
|
342 by (drule init_node_has_sec, simp+) |
|
343 |
|
344 (* |
|
345 lemma current_shm_has_sec: "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_shm h) = Some sec" |
|
346 by (rule alive_obj_has_sec, simp+) |
|
347 |
|
348 lemma current_shm_has_sec': "\<lbrakk>sectxt_of_obj s (O_shm h) = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s" |
|
349 by (auto intro:notI dest:current_shm_has_sec) |
|
350 |
|
351 lemma current_shm_has_sec'': "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_shm h) = Some (u,r,t)" |
|
352 by (drule current_shm_has_sec, simp+) |
|
353 *) |
|
354 |
|
355 lemma current_msgq_has_sec: "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_msgq q) = Some sec" |
|
356 by (rule alive_obj_has_sec, simp+) |
|
357 |
|
358 lemma current_msgq_has_sec': "\<lbrakk>sectxt_of_obj s (O_msgq q) = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s" |
|
359 by (auto intro:notI dest:current_msgq_has_sec) |
|
360 |
|
361 lemma current_msgq_has_sec'': "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> |
|
362 \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_msgq q) = Some (u,r,t)" |
|
363 by (drule current_msgq_has_sec, simp+) |
|
364 |
|
365 lemma current_msg_has_sec: "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk> |
|
366 \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_msg q m) = Some sec" |
|
367 by (rule alive_obj_has_sec, simp+) |
|
368 |
|
369 lemma current_msg_has_sec': "\<lbrakk>sectxt_of_obj s (O_msg q m) = None; valid s\<rbrakk> |
|
370 \<Longrightarrow> m \<notin> set (msgs_of_queue s q) \<or> q \<notin> current_msgqs s" |
|
371 by (auto dest!:current_msg_has_sec) |
|
372 |
|
373 lemma current_msg_has_sec'': "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk> |
|
374 \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_msg q m) = Some (u, r, t)" |
|
375 by (drule current_msg_has_sec, simp+) |
|
376 |
|
377 lemmas current_has_sec = alive_obj_has_sec current_proc_has_sec is_file_has_sec is_dir_has_sec |
|
378 is_tcp_has_sec is_udp_has_sec current_fd_has_sec init_node_has_sec (* current_shm_has_sec *) |
|
379 current_msgq_has_sec current_msg_has_sec |
|
380 |
|
381 lemmas current_has_sec' = alive_obj_has_sec' current_proc_has_sec' is_file_has_sec' is_dir_has_sec' |
|
382 is_tcp_has_sec' is_udp_has_sec' current_fd_has_sec' init_node_has_sec' (* current_shm_has_sec' *) |
|
383 current_msgq_has_sec' current_msg_has_sec' |
|
384 |
|
385 lemmas current_has_sec'' = alive_obj_has_sec'' current_proc_has_sec'' is_file_has_sec'' is_dir_has_sec'' |
|
386 is_tcp_has_sec'' is_udp_has_sec'' current_fd_has_sec'' init_node_has_sec'' (* current_shm_has_sec'' *) |
|
387 current_msgq_has_sec'' current_msg_has_sec'' |
|
388 |
|
389 (************ root sec remains ************) |
|
390 |
|
391 lemma root_type_remains: |
|
392 "valid s \<Longrightarrow> type_of_obj s (O_dir []) = init_type_of_obj (O_dir [])" |
|
393 apply (induct s) |
|
394 apply (simp) |
|
395 apply (frule vd_cons, frule vt_grant_os, case_tac a) prefer 6 |
|
396 by (case_tac option, auto) |
|
397 |
|
398 lemma root_user_remains: |
|
399 "valid s \<Longrightarrow> user_of_obj s (O_dir []) = init_user_of_obj (O_dir [])" |
|
400 apply (induct s) |
|
401 apply (simp) |
|
402 apply (frule vd_cons, frule vt_grant_os, case_tac a) prefer 6 |
|
403 by (case_tac option, auto) |
|
404 |
|
405 lemma root_has_type': |
|
406 "\<lbrakk>type_of_obj s (O_dir []) = None; valid s\<rbrakk> \<Longrightarrow> False" |
|
407 apply (drule alive_obj_has_type', simp) |
|
408 by (drule root_is_dir, simp) |
|
409 |
|
410 lemma root_has_user': |
|
411 "\<lbrakk>user_of_obj s (O_dir []) = None; valid s\<rbrakk> \<Longrightarrow> False" |
|
412 apply (drule alive_obj_has_user', simp) |
|
413 by (drule root_is_dir, simp) |
|
414 |
|
415 lemma root_has_init_type': |
|
416 "init_type_of_obj (O_dir []) = None \<Longrightarrow> False" |
|
417 using init_obj_has_type[where obj = "O_dir []"] root_is_init_dir |
|
418 by auto |
|
419 |
|
420 lemma root_has_init_user': |
|
421 "init_user_of_obj (O_dir []) = None \<Longrightarrow> False" |
|
422 using init_obj_has_user[where obj = "O_dir []"] root_is_init_dir |
|
423 by auto |
|
424 |
|
425 lemma root_sec_remains: |
|
426 "valid s \<Longrightarrow> sectxt_of_obj s (O_dir []) = init_sectxt_of_obj (O_dir [])" |
|
427 by (auto simp:root_user_remains root_type_remains sectxt_of_obj_def init_sectxt_of_obj_def |
|
428 split:option.splits) |
|
429 |
|
430 lemma root_sec_set: |
|
431 "\<exists> u t. sec_of_root = (u, R_object, t)" |
|
432 by (auto simp:sec_of_root_def split:option.splits |
|
433 dest!: root_has_init_type' root_has_init_user') |
|
434 |
|
435 lemma sec_of_root_set: |
|
436 "init_sectxt_of_obj (O_dir []) = Some sec_of_root" |
|
437 using root_has_init_type' root_has_init_user' |
|
438 apply (auto simp:init_sectxt_of_obj_def sec_of_root_def split:option.splits) |
|
439 done |
|
440 |
|
441 (*************** sectxt_of_obj simpset ****************) |
|
442 |
|
443 lemma sec_execve: |
|
444 "valid (Execve p f fds # s) \<Longrightarrow> sectxt_of_obj (Execve p f fds # s) = |
|
445 (sectxt_of_obj s) (O_proc p := ( |
|
446 case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_file f)) of |
|
447 (Some psec, Some fsec) \<Rightarrow> npctxt_execve psec fsec |
|
448 | _ \<Rightarrow> None))" |
|
449 apply (rule ext, frule vd_cons, frule vt_grant_os, frule vt_grant,case_tac x) |
|
450 apply (auto simp:sectxt_of_obj_def split:option.splits |
|
451 dest!:current_has_type' current_proc_has_role' current_has_user') |
|
452 done |
|
453 |
|
454 lemma sec_clone: |
|
455 "valid (Clone p p' fds # s) \<Longrightarrow> sectxt_of_obj (Clone p p' fds # s) = (\<lambda> obj. |
|
456 case obj of |
|
457 O_proc p'' \<Rightarrow> if (p'' = p') then sectxt_of_obj s (O_proc p) |
|
458 else sectxt_of_obj s obj |
|
459 | O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then sectxt_of_obj s (O_fd p fd) |
|
460 else if (p'' = p') then None |
|
461 else sectxt_of_obj s obj |
|
462 | O_tcp_sock (p'', fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then sectxt_of_obj s (O_tcp_sock (p, fd)) |
|
463 else if (p'' = p') then None |
|
464 else sectxt_of_obj s obj |
|
465 | O_udp_sock (p'', fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then sectxt_of_obj s (O_udp_sock (p, fd)) |
|
466 else if (p'' = p') then None |
|
467 else sectxt_of_obj s obj |
|
468 | _ \<Rightarrow> sectxt_of_obj s obj )" |
|
469 apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac obj) |
|
470 apply (auto simp:sectxt_of_obj_def split:option.splits if_splits |
|
471 dest!:current_has_type' current_proc_has_role' current_has_user') |
|
472 done |
|
473 |
|
474 lemma sec_open: |
|
475 "valid (Open p f flags fd opt # s) \<Longrightarrow> sectxt_of_obj (Open p f flags fd opt # s) = (\<lambda> obj. |
|
476 case obj of |
|
477 O_file f' \<Rightarrow> if (f' = f \<and> opt \<noteq> None) then |
|
478 (case (parent f) of |
|
479 None \<Rightarrow> None |
|
480 | Some pf \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of |
|
481 (Some psec, Some pfsec) \<Rightarrow> Some (fst psec, R_object, |
|
482 type_transition ((snd o snd) psec) ((snd o snd) pfsec) C_file True) |
|
483 | _ \<Rightarrow> None)) |
|
484 else sectxt_of_obj s obj |
|
485 | O_fd p' fd' \<Rightarrow> if (p' = p \<and> fd' = fd) then |
|
486 (case (sectxt_of_obj s (O_proc p)) of |
|
487 Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec) |
|
488 | _ \<Rightarrow> None) |
|
489 else sectxt_of_obj s obj |
|
490 | _ \<Rightarrow> sectxt_of_obj s obj)" |
|
491 apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac obj) |
|
492 apply (auto simp:sectxt_of_obj_def split:option.splits if_splits |
|
493 dest!:current_has_type' current_proc_has_role' current_has_user') |
|
494 done |
|
495 |
|
496 lemma sec_mkdir: |
|
497 "valid (Mkdir p f inum # s) \<Longrightarrow> sectxt_of_obj (Mkdir p f inum # s) = |
|
498 (sectxt_of_obj s) (O_dir f := |
|
499 (case parent f of |
|
500 None \<Rightarrow> None |
|
501 | Some pf \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of |
|
502 (Some psec, Some pfsec) \<Rightarrow> Some (fst psec, R_object, |
|
503 type_transition ((snd o snd) psec) ((snd o snd) pfsec) C_dir True) |
|
504 | _ \<Rightarrow> None)))" |
|
505 apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac x) |
|
506 apply (auto simp:sectxt_of_obj_def split:option.splits if_splits |
|
507 dest!:current_has_type' current_proc_has_role' current_has_user') |
|
508 done |
|
509 |
|
510 lemma sec_linkhard: |
|
511 "valid (LinkHard p f f' # s) \<Longrightarrow> sectxt_of_obj (LinkHard p f f' # s) = |
|
512 (sectxt_of_obj s) (O_file f' := |
|
513 (case parent f' of |
|
514 None \<Rightarrow> None |
|
515 | Some pf \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of |
|
516 (Some psec, Some pfsec) \<Rightarrow> Some (fst psec, R_object, |
|
517 type_transition ((snd o snd) psec) ((snd o snd) pfsec) C_file True) |
|
518 | _ \<Rightarrow> None)))" |
|
519 apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac x) |
|
520 apply (auto simp:sectxt_of_obj_def split:option.splits if_splits |
|
521 dest!:current_has_type' current_proc_has_role' current_has_user') |
|
522 done |
|
523 |
|
524 lemma sec_createmsgq: |
|
525 "valid (CreateMsgq p q # s) \<Longrightarrow> sectxt_of_obj (CreateMsgq p q # s) = (sectxt_of_obj s) (O_msgq q := |
|
526 (case (sectxt_of_obj s (O_proc p)) of |
|
527 Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec) |
|
528 | _ \<Rightarrow> None))" |
|
529 apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac x) |
|
530 apply (auto simp:sectxt_of_obj_def split:option.splits if_splits |
|
531 dest!:current_has_type' current_proc_has_role' current_has_user') |
|
532 done |
|
533 |
|
534 lemma sec_sendmsg: |
|
535 "valid (SendMsg p q m # s) \<Longrightarrow> sectxt_of_obj (SendMsg p q m # s) = (sectxt_of_obj s) (O_msg q m := |
|
536 (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_msgq q)) of |
|
537 (Some psec, Some qsec) \<Rightarrow> Some (fst psec, R_object, |
|
538 type_transition ((snd o snd) psec) ((snd o snd) qsec) C_msg False) |
|
539 | _ \<Rightarrow> None))" |
|
540 apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac x) |
|
541 apply (auto simp:sectxt_of_obj_def split:option.splits if_splits |
|
542 dest!:current_has_type' current_proc_has_role' current_has_user') |
|
543 done |
|
544 |
|
545 (* |
|
546 lemma sec_createshm: |
|
547 "valid (CreateShM p h # s) \<Longrightarrow> sectxt_of_obj (CreateShM p h # s) = (sectxt_of_obj s) (O_shm h := |
|
548 case (sectxt_of_obj s (O_proc p)) of |
|
549 Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec) |
|
550 | _ \<Rightarrow> None)" |
|
551 apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac x) |
|
552 apply (auto simp:sectxt_of_obj_def split:option.splits if_splits |
|
553 dest!:current_has_type' current_proc_has_role' current_has_user') |
|
554 done |
|
555 *) |
|
556 |
|
557 lemma sec_createsock: |
|
558 "valid (CreateSock p af st fd inum # s) \<Longrightarrow> sectxt_of_obj (CreateSock p af st fd inum # s) = (\<lambda> obj. |
|
559 case obj of |
|
560 O_fd p' fd' \<Rightarrow> if (p' = p \<and> fd' = fd) then |
|
561 (case (sectxt_of_obj s (O_proc p)) of |
|
562 Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec) |
|
563 | _ \<Rightarrow> None) |
|
564 else sectxt_of_obj s obj |
|
565 | O_tcp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = STREAM) then |
|
566 (case (sectxt_of_obj s (O_proc p)) of |
|
567 Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec) |
|
568 | _ \<Rightarrow> None) |
|
569 else sectxt_of_obj s obj |
|
570 | O_udp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = DGRAM) then |
|
571 (case (sectxt_of_obj s (O_proc p)) of |
|
572 Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec) |
|
573 | _ \<Rightarrow> None) |
|
574 else sectxt_of_obj s obj |
|
575 | _ \<Rightarrow> sectxt_of_obj s obj )" |
|
576 apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac obj) |
|
577 apply (auto simp:sectxt_of_obj_def split:option.splits if_splits |
|
578 dest!:current_has_type' current_proc_has_role' current_has_user') |
|
579 done |
|
580 |
|
581 lemma sec_accept: |
|
582 "valid (Accept p fd addr port fd' inum # s) \<Longrightarrow> sectxt_of_obj (Accept p fd addr port fd' inum # s) = (\<lambda> obj. |
|
583 case obj of |
|
584 O_fd p' fd'' \<Rightarrow> if (p' = p \<and> fd'' = fd') then |
|
585 (case (sectxt_of_obj s (O_proc p)) of |
|
586 Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec) |
|
587 | _ \<Rightarrow> None) |
|
588 else sectxt_of_obj s obj |
|
589 | O_tcp_sock (p', fd'') \<Rightarrow> if (p' = p \<and> fd'' = fd') then |
|
590 (case (sectxt_of_obj s (O_proc p)) of |
|
591 Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec) |
|
592 | _ \<Rightarrow> None) |
|
593 else sectxt_of_obj s obj |
|
594 | _ \<Rightarrow> sectxt_of_obj s obj )" |
|
595 apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac obj) |
|
596 apply (auto simp:sectxt_of_obj_def split:option.splits if_splits |
|
597 dest!:current_has_type' current_proc_has_role' current_has_user') |
|
598 done |
|
599 |
|
600 lemma sec_others : |
|
601 "\<lbrakk>valid (e # s); |
|
602 \<forall> p p' fds. e \<noteq> Clone p p' fds; |
|
603 \<forall> p f fds. e \<noteq> Execve p f fds; |
|
604 \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt; |
|
605 \<forall> p f inum. e \<noteq> Mkdir p f inum; |
|
606 \<forall> p f f'. e \<noteq> LinkHard p f f'; |
|
607 \<forall> p q. e \<noteq> CreateMsgq p q; |
|
608 \<forall> p q m. e \<noteq> SendMsg p q m; |
|
609 \<forall> p af st fd inum. e \<noteq> CreateSock p af st fd inum; |
|
610 \<forall> p fd addr port fd' inum. e \<noteq> Accept p fd addr port fd' inum |
|
611 \<rbrakk> \<Longrightarrow> sectxt_of_obj (e # s) = sectxt_of_obj s" (* |
|
612 \<forall> p h. e \<noteq> CreateShM p h;*) |
|
613 apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac e, case_tac[!] x) |
|
614 apply (auto simp:sectxt_of_obj_def split:option.splits if_splits |
|
615 dest!:current_has_type' current_proc_has_role' current_has_user') |
|
616 done |
|
617 |
|
618 lemma sec_kill: |
|
619 "valid (Kill p p' # s) \<Longrightarrow> sectxt_of_obj (Kill p p' # s) = sectxt_of_obj s" |
|
620 by (auto dest!:sec_others) |
|
621 |
|
622 lemma sec_ptrace: |
|
623 "valid (Ptrace p p' # s) \<Longrightarrow> sectxt_of_obj (Ptrace p p' # s) = sectxt_of_obj s" |
|
624 by (auto dest!:sec_others) |
|
625 |
|
626 lemma sec_exit: |
|
627 "valid (Exit p # s) \<Longrightarrow> sectxt_of_obj (Exit p # s) = sectxt_of_obj s" |
|
628 by (auto dest!:sec_others) |
|
629 |
|
630 lemma sec_readfile: |
|
631 "valid (ReadFile p fd # s) \<Longrightarrow> sectxt_of_obj (ReadFile p fd # s) = sectxt_of_obj s" |
|
632 by (auto dest!:sec_others) |
|
633 |
|
634 lemma sec_writefile: |
|
635 "valid (WriteFile p fd # s) \<Longrightarrow> sectxt_of_obj (WriteFile p fd # s) = sectxt_of_obj s" |
|
636 by (auto dest!:sec_others) |
|
637 |
|
638 lemma sec_closefd: |
|
639 "valid (CloseFd p fd # s) \<Longrightarrow> sectxt_of_obj (CloseFd p fd # s) = sectxt_of_obj s" |
|
640 by (auto dest!:sec_others) |
|
641 |
|
642 lemma sec_unlink: |
|
643 "valid (UnLink p f # s) \<Longrightarrow> sectxt_of_obj (UnLink p f # s) = sectxt_of_obj s" |
|
644 by (auto dest!:sec_others) |
|
645 |
|
646 lemma sec_Rmdir: |
|
647 "valid (Rmdir p f # s) \<Longrightarrow> sectxt_of_obj (Rmdir p f # s) = sectxt_of_obj s" |
|
648 by (auto dest!:sec_others) |
|
649 |
|
650 lemma sec_truncate: |
|
651 "valid (Truncate p f len # s) \<Longrightarrow> sectxt_of_obj (Truncate p f len # s) = sectxt_of_obj s" |
|
652 by (auto dest!:sec_others) |
|
653 |
|
654 lemma sec_recvmsg: |
|
655 "valid (RecvMsg p q m # s) \<Longrightarrow> sectxt_of_obj (RecvMsg p q m # s) = sectxt_of_obj s" |
|
656 by (auto dest!:sec_others) |
|
657 |
|
658 lemma sec_removemsgq: |
|
659 "valid (RemoveMsgq p q # s) \<Longrightarrow> sectxt_of_obj (RemoveMsgq p q # s) = sectxt_of_obj s" |
|
660 by (auto dest!:sec_others) |
|
661 |
|
662 (* |
|
663 lemma sec_attach: |
|
664 "valid (Attach p h flag # s) \<Longrightarrow> sectxt_of_obj (Attach p h flag # s) = sectxt_of_obj s" |
|
665 by (auto dest!:sec_others) |
|
666 |
|
667 lemma sec_detach: |
|
668 "valid (Detach p h # s) \<Longrightarrow> sectxt_of_obj (Detach p h # s) = sectxt_of_obj s" |
|
669 by (auto dest!:sec_others) |
|
670 |
|
671 lemma sec_deleteshm: |
|
672 "valid (DeleteShM p h # s) \<Longrightarrow> sectxt_of_obj (DeleteShM p h # s) = sectxt_of_obj s" |
|
673 by (auto dest!:sec_others) |
|
674 *) |
|
675 |
|
676 lemma sec_bind: |
|
677 "valid (Bind p fd addr # s) \<Longrightarrow> sectxt_of_obj (Bind p fd addr # s) = sectxt_of_obj s" |
|
678 by (auto dest!:sec_others) |
|
679 |
|
680 lemma sec_connect: |
|
681 "valid (Connect p fd addr # s) \<Longrightarrow> sectxt_of_obj (Connect p fd addr # s) = sectxt_of_obj s" |
|
682 by (auto dest!:sec_others) |
|
683 |
|
684 lemma sec_listen: |
|
685 "valid (Listen p fd # s) \<Longrightarrow> sectxt_of_obj (Listen p fd # s) = sectxt_of_obj s" |
|
686 by (auto dest!:sec_others) |
|
687 |
|
688 lemma sec_sendsock: |
|
689 "valid (SendSock p fd # s) \<Longrightarrow> sectxt_of_obj (SendSock p fd # s) = sectxt_of_obj s" |
|
690 by (auto dest!:sec_others) |
|
691 |
|
692 lemma sec_recvsock: |
|
693 "valid (RecvSock p fd # s) \<Longrightarrow> sectxt_of_obj (RecvSock p fd # s) = sectxt_of_obj s" |
|
694 by (auto dest!:sec_others) |
|
695 |
|
696 lemma sec_shutdown: |
|
697 "valid (Shutdown p fd how # s) \<Longrightarrow> sectxt_of_obj (Shutdown p fd how # s) = sectxt_of_obj s" |
|
698 by (auto dest!:sec_others) |
|
699 |
|
700 lemmas sectxt_of_obj_simps = sec_execve sec_open sec_mkdir sec_linkhard sec_createmsgq sec_sendmsg |
|
701 (* sec_createshm *) sec_createsock sec_accept sec_clone sec_kill sec_ptrace sec_exit sec_readfile |
|
702 sec_writefile sec_closefd sec_unlink sec_Rmdir sec_truncate sec_recvmsg sec_removemsgq |
|
703 (* sec_attach sec_detach sec_deleteshm *) sec_bind sec_connect sec_listen sec_sendsock |
|
704 sec_recvsock sec_shutdown |
|
705 (* init_sectxt_prop *) |
|
706 |
|
707 (**************** get_parentfs_ctxts simpset **************) |
|
708 |
|
709 lemma parentf_is_dir_prop1: "\<lbrakk>is_dir s (x # pf); valid s\<rbrakk> \<Longrightarrow> is_dir s pf" |
|
710 apply (rule_tac f = "x # pf" in parentf_is_dir) |
|
711 by (auto simp:is_dir_def current_files_def split:option.splits t_inode_tag.splits) |
|
712 |
|
713 lemma parentf_is_dir_prop2: "\<lbrakk>is_file s (x # pf); valid s\<rbrakk> \<Longrightarrow> is_dir s pf" |
|
714 apply (rule_tac f = "x # pf" in parentf_is_dir) |
|
715 by (auto simp:is_dir_def is_file_def current_files_def split:option.splits t_inode_tag.splits) |
|
716 |
|
717 lemma parentf_is_dir_prop3: "\<lbrakk>(x # pf) \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_dir s pf" |
|
718 apply (rule_tac f = "x # pf" in parentf_is_dir) |
|
719 by (auto simp:is_dir_def current_files_def split:option.splits t_inode_tag.splits) |
|
720 |
|
721 lemma get_pfs_secs_prop': |
|
722 "\<lbrakk>get_parentfs_ctxts s f = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_dir s f" |
|
723 apply (induct f) |
|
724 by (auto split:option.splits dest:current_has_sec' parentf_is_dir_prop1) |
|
725 |
|
726 lemma get_pfs_secs_prop: |
|
727 "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> asecs. get_parentfs_ctxts s f = Some asecs" |
|
728 using get_pfs_secs_prop' |
|
729 by (auto) |
|
730 |
|
731 lemma get_pfs_secs_open: |
|
732 "valid (Open p f flags fd opt # s) \<Longrightarrow> get_parentfs_ctxts (Open p f flags fd opt # s) = get_parentfs_ctxts s" |
|
733 apply (frule noroot_events, frule vd_cons, frule vt_grant_os) |
|
734 apply (rule ext, induct_tac x) |
|
735 by (auto split:option.splits simp:sectxt_of_obj_simps) |
|
736 |
|
737 lemma get_pfs_secs_other: |
|
738 "\<lbrakk>valid (e # s); \<forall> p f inum. e \<noteq> Mkdir p f inum\<rbrakk> |
|
739 \<Longrightarrow> get_parentfs_ctxts (e # s) = get_parentfs_ctxts s" |
|
740 apply (frule vd_cons, frule vt_grant_os, rule ext, induct_tac x) |
|
741 apply (case_tac [!] e) |
|
742 apply (auto split:option.splits if_splits simp:sectxt_of_obj_simps) |
|
743 done |
|
744 |
|
745 lemma get_pfs_secs_mkdir1: |
|
746 assumes mkdir: "valid (Mkdir p f inum # s)" and noteq: "is_dir s f'" |
|
747 shows "get_parentfs_ctxts (Mkdir p f inum # s) f' = get_parentfs_ctxts s f'" |
|
748 proof- |
|
749 from mkdir have vd: "valid s" and os: "os_grant s (Mkdir p f inum)" |
|
750 by (frule_tac vd_cons, simp, frule_tac vt_grant_os, simp) |
|
751 from mkdir have notroot: "f \<noteq> []" by (auto intro!:noroot_mkdir) |
|
752 show ?thesis using noteq |
|
753 proof (induct f') |
|
754 case Nil |
|
755 show ?case using notroot mkdir by (simp add:sectxt_of_obj_simps) |
|
756 next |
|
757 case (Cons a f') |
|
758 hence p1: "is_dir s f'" using vd by (simp add:parentf_is_dir_prop1) |
|
759 from Cons have p2: "is_dir s (a # f')" by simp |
|
760 from Cons p1 have p3: "get_parentfs_ctxts (Mkdir p f inum # s) f' = get_parentfs_ctxts s f'" by simp |
|
761 from p2 os have p4: "a # f' \<noteq> f" by (auto simp:is_dir_in_current) |
|
762 from p1 os have p5: "f' \<noteq> f" by (auto simp:is_dir_in_current) |
|
763 show ?case using mkdir vd os p4 p5 p1 |
|
764 by (auto simp:sectxt_of_obj_simps is_dir_simps p3 |
|
765 split:option.splits dest:current_has_sec' get_pfs_secs_prop') |
|
766 qed |
|
767 qed |
|
768 |
|
769 lemma get_pfs_secs_mkdir2: |
|
770 "valid (Mkdir p f inum # s) \<Longrightarrow> get_parentfs_ctxts (Mkdir p f inum # s) f = ( |
|
771 case f of |
|
772 [] \<Rightarrow> get_parentfs_ctxts s [] |
|
773 | x#pf \<Rightarrow> (case (get_parentfs_ctxts s pf, sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of |
|
774 (Some pfsecs, Some psec, Some pfsec) \<Rightarrow> Some ((fst psec, R_object, type_transition ((snd o snd) psec) ((snd o snd) pfsec) C_dir True) # pfsecs) |
|
775 | _ \<Rightarrow> None))" |
|
776 apply (frule vd_cons, frule vt_grant_os) |
|
777 apply (frule noroot_events, case_tac f) |
|
778 by (auto split:option.splits dest:current_has_sec' get_pfs_secs_prop' get_pfs_secs_mkdir1 |
|
779 simp:sectxt_of_obj_simps is_dir_simps) |
|
780 |
|
781 lemmas get_parentfs_ctxts_simps = get_pfs_secs_other get_pfs_secs_mkdir1 get_pfs_secs_mkdir2 |
|
782 |
|
783 end |
|
784 |
|
785 end |