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