77
+ − 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