1
+ − 1
theory Flask
+ − 2
imports Main Flask_type OS_type_def File_renaming
+ − 3
begin
+ − 4
+ − 5
(****** Policy-language-level rule match/auxiliary functions ******)
+ − 6
+ − 7
fun patt_match :: "'a patt \<Rightarrow> 'a \<Rightarrow> bool"
+ − 8
where
+ − 9
"patt_match (Single x) y = (x = y)"
+ − 10
| "patt_match (Set s) x = (x \<in> s)"
+ − 11
| "patt_match (Tilde s) x = (x \<notin> s)"
+ − 12
| "patt_match Asterisk x = True"
+ − 13
+ − 14
(* match a target with a patt, but including the SELF special
+ − 15
* patt_match_self patt target source
+ − 16
*)
+ − 17
fun patt_match_self :: "(type_t patt) target_with_self_t \<Rightarrow> type_t \<Rightarrow> type_t \<Rightarrow> bool"
+ − 18
where
+ − 19
"patt_match_self Self tt st = (tt = st)"
+ − 20
| "patt_match_self (Not_self (Single p)) tt st = (tt = p)"
+ − 21
| "patt_match_self (Not_self (Set p)) tt st = (tt \<in> p)"
+ − 22
| "patt_match_self (Not_self (Tilde p)) tt st = (tt \<notin> p)"
+ − 23
| "patt_match_self (Not_self Asterisk) tt st = True"
+ − 24
+ − 25
(* list lookup: find the first one *)
+ − 26
fun lookup :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a option"
+ − 27
where
+ − 28
"lookup [] P = None"
+ − 29
| "lookup (x # xs) P = (if (P x) then Some x else lookup xs P)"
+ − 30
+ − 31
(* list member: if exists an element satisfy predicate P *)
+ − 32
fun member :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+ − 33
where
+ − 34
"member [] P = False"
+ − 35
| "member (x # xs) P = (if (P x) then True else member xs P)"
+ − 36
+ − 37
(******* socket related aux functions ********)
+ − 38
fun is_remote_request :: "t_event \<Rightarrow> bool"
+ − 39
where
+ − 40
"is_remote_request (Accept p fd addr port fd' i) = True"
+ − 41
| "is_remote_request (Connect p fd addr) = True"
+ − 42
| "is_remote_request (SendSock p fd) = True"
+ − 43
| "is_remote_request (RecvSock p fd) = True"
+ − 44
| "is_remote_request e = False"
+ − 45
+ − 46
fun ip_of_addr:: "t_sock_addr \<Rightarrow> t_inet_addr"
+ − 47
where
+ − 48
"ip_of_addr (INET_ADDR saddr sport) = saddr"
+ − 49
+ − 50
fun port_of_addr:: "t_sock_addr \<Rightarrow> t_socket_port"
+ − 51
where
+ − 52
"port_of_addr (INET_ADDR saddr sport) = sport"
+ − 53
+ − 54
fun after_bind:: "t_sock_state option \<Rightarrow> bool"
+ − 55
where
+ − 56
"after_bind None = False"
+ − 57
| "after_bind (Some SS_create) = False"
+ − 58
| "after_bind _= True" (* after bind , it should have local addr *)
+ − 59
+ − 60
fun after_conacc:: "t_sock_state option \<Rightarrow> bool"
+ − 61
where
+ − 62
"after_conacc None = False"
+ − 63
| "after_conacc (Some SS_create) = False"
+ − 64
| "after_conacc (Some SS_bind) = False"
+ − 65
| "after_conacc (Some SS_listen) = False"
+ − 66
| "after_conacc _ = True" (* after connect or accept, it should have remote addr *)
+ − 67
+ − 68
(* inet_addr_compare addr1 addr2 \<equiv> addr1 \<le> addr2; but in \<le>'s def,there is a \<exists>, is not a function*)
+ − 69
fun subnet_addr :: "t_inet_addr \<Rightarrow> t_inet_addr \<Rightarrow> bool"
+ − 70
where
+ − 71
"subnet_addr [] addr = True"
+ − 72
| "subnet_addr (x#xs) [] = False"
+ − 73
| "subnet_addr (x#xs) (y#ys) = ((x = y) \<and> subnet_addr xs ys)"
+ − 74
+ − 75
definition port_in_range :: "t_socket_port \<Rightarrow> t_socket_port \<Rightarrow> t_socket_port \<Rightarrow> bool"
+ − 76
where
+ − 77
"port_in_range minp maxp p \<equiv> ((p < maxp \<or> p = maxp) \<and> (p > minp \<or> p = minp))"
+ − 78
+ − 79
(* initial value of initiate state constrains aux function *)
+ − 80
definition bidirect_in_init :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> bool"
+ − 81
where
+ − 82
"bidirect_in_init S f \<equiv> (\<forall> a. a \<in> S \<longrightarrow> (\<exists> b. f a = Some b)) \<and>
+ − 83
(\<forall> a b. f a = Some b \<longrightarrow> a \<in> S)"
+ − 84
+ − 85
fun is_file_itag :: "t_inode_tag \<Rightarrow> bool"
+ − 86
where
+ − 87
"is_file_itag Tag_FILE = True"
+ − 88
| "is_file_itag tag = False"
+ − 89
+ − 90
fun is_dir_itag :: "t_inode_tag \<Rightarrow> bool"
+ − 91
where
+ − 92
"is_dir_itag Tag_DIR = True"
+ − 93
| "is_dir_itag tag = False"
+ − 94
+ − 95
fun is_file_dir_itag :: "t_inode_tag \<Rightarrow> bool"
+ − 96
where
+ − 97
"is_file_dir_itag Tag_FILE = True"
+ − 98
| "is_file_dir_itag Tag_DIR = True"
+ − 99
| "is_file_dir_itag tag = False"
+ − 100
+ − 101
fun is_tcp_itag :: "t_inode_tag \<Rightarrow> bool"
+ − 102
where
+ − 103
"is_tcp_itag Tag_TCP_SOCK = True"
+ − 104
| "is_tcp_itag tag = False"
+ − 105
+ − 106
fun is_udp_itag :: "t_inode_tag \<Rightarrow> bool"
+ − 107
where
+ − 108
"is_udp_itag Tag_UDP_SOCK = True"
+ − 109
| "is_udp_itag tag = False"
+ − 110
+ − 111
fun is_sock_itag :: "t_inode_tag \<Rightarrow> bool"
+ − 112
where
+ − 113
"is_sock_itag Tag_TCP_SOCK = True"
+ − 114
| "is_sock_itag Tag_UDP_SOCK = True"
+ − 115
| "is_sock_itag tag = False"
+ − 116
+ − 117
+ − 118
locale init =
+ − 119
fixes
+ − 120
init_files :: "t_file set"
+ − 121
and init_procs :: "t_process set"
+ − 122
and init_nodes :: "t_node set"
+ − 123
and init_sockets :: "t_socket set"
+ − 124
and init_users :: "user_t set"
+ − 125
+ − 126
and init_file_of_proc_fd :: "t_process \<Rightarrow> t_fd \<rightharpoonup> t_file"
+ − 127
and init_fds_of_proc :: "t_process \<Rightarrow> t_fd set"
+ − 128
and init_oflags_of_proc_fd:: "t_process \<Rightarrow> t_fd \<rightharpoonup> t_open_flags"
+ − 129
and init_inum_of_file :: "t_file \<rightharpoonup> t_inode_num"
+ − 130
and init_inum_of_socket:: "t_socket \<rightharpoonup> t_inode_num"
+ − 131
and init_itag_of_inum:: "t_inode_num \<rightharpoonup> t_inode_tag"
+ − 132
and init_files_hung_by_del :: "t_file set"
+ − 133
(*
+ − 134
and init_file_at_writing_by:: "t_file \<Rightarrow> (t_process \<times> t_fd) set"
+ − 135
*)
+ − 136
and init_socket_state :: "t_socket \<rightharpoonup> t_sock_state"
+ − 137
+ − 138
and init_msgqs :: "t_msgq set"
+ − 139
and init_msgs_of_queue:: "t_msgq \<Rightarrow> t_msg list"
+ − 140
and init_shms :: "t_shm set"
+ − 141
and init_procs_of_shm :: "t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set"
+ − 142
+ − 143
assumes
+ − 144
parent_file_in_init: "\<And> f pf. \<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> pf \<in> init_files"
+ − 145
and root_is_dir: "\<exists> i. init_inum_of_file [] = Some i \<and> init_itag_of_inum i = Some Tag_DIR"
+ − 146
and init_file_has_inum: "\<And> f. f \<in> init_files \<Longrightarrow> \<exists> im. init_inum_of_file f = Some im"
+ − 147
and inof_has_file_tag: "\<And> f im. init_inum_of_file f = Some im \<Longrightarrow> f \<in> init_files \<and> (\<exists> tag. init_itag_of_inum im = Some tag \<and> is_file_dir_itag tag)"
+ − 148
and init_file_no_son: "\<And> f im. \<lbrakk>init_inum_of_file f = Some im; init_itag_of_inum im = Some Tag_FILE\<rbrakk> \<Longrightarrow> \<not> (\<exists> f' \<in> init_files. parent f' = Some f)"
+ − 149
and init_parentf_is_dir: "\<And> f pf im. \<lbrakk>parent f = Some pf; f \<in> init_files; init_inum_of_file pf = Some im\<rbrakk> \<Longrightarrow> init_itag_of_inum im = Some Tag_DIR"
+ − 150
+ − 151
and init_files_hung_valid: "\<And> f. f \<in> init_files_hung_by_del \<Longrightarrow> f \<in> init_files \<and> (\<exists> p fd. init_file_of_proc_fd p fd = Some f)"
+ − 152
and init_files_hung_valid': "\<And> f im. \<lbrakk>f \<in> init_files_hung_by_del; init_inum_of_file f = Some im\<rbrakk> \<Longrightarrow>
+ − 153
init_itag_of_inum im = Some Tag_FILE \<or> (init_itag_of_inum im = Some Tag_DIR \<and> \<not> (\<exists> f'. f' \<in> init_files \<and> f \<prec> f'))"
+ − 154
+ − 155
and init_procfds_valid: "\<And> p fd. fd \<in> init_fds_of_proc p \<Longrightarrow> p \<in> init_procs \<and> ((\<exists> f \<in> init_files. init_file_of_proc_fd p fd = Some f) \<or> (p, fd) \<in> init_sockets)"
+ − 156
and init_filefd_valid: "\<And> p fd f. init_file_of_proc_fd p fd = Some f \<Longrightarrow> fd \<in> init_fds_of_proc p \<and> (\<exists> im. init_inum_of_file f = Some im \<and> init_itag_of_inum im = Some Tag_FILE) \<and> p \<in> init_procs \<and> (\<exists> flags. init_oflags_of_proc_fd p fd = Some flags)"
+ − 157
and init_fileflag_valid: "\<And> p fd flags. init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> \<exists> f. init_file_of_proc_fd p fd = Some f"
+ − 158
+ − 159
and init_procs_has_shm: "\<And> p h flag. (p,flag) \<in> init_procs_of_shm h \<Longrightarrow> p \<in> init_procs \<and> h \<in> init_shms"
+ − 160
and init_msgs_distinct: "\<And> q. distinct (init_msgs_of_queue q)"
4
+ − 161
and init_msgs_valid: "\<And> m q. m \<in> set (init_msgs_of_queue q) \<Longrightarrow> q \<in> init_msgqs"
1
+ − 162
+ − 163
and init_socket_has_inode: "\<And> p fd. (p, fd) \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket (p, fd) = Some im \<and> p \<in> init_procs \<and> fd \<in> init_fds_of_proc p"
+ − 164
and inos_has_sock_tag: "\<And> s im. init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets \<and> (\<exists> tag. init_itag_of_inum im = Some tag \<and> is_sock_itag tag)"
+ − 165
(*
+ − 166
and init_netobj_has_state: "bidirect_in_init init_netobjs init_netobj_state"
+ − 167
and init_netobj_has_socktype:"bidirect_in_init init_netobjs init_netobj_socktype"
+ − 168
and init_netobj_has_laddr: "\<And> s. after_bind (init_netobj_state s) \<Longrightarrow> init_netobj_localaddr s \<noteq> None"
+ − 169
and init_netobj_has_raddr: "\<And> s. after_conacc (init_netobj_state s) \<Longrightarrow> init_netobj_remoteaddr s \<noteq> None"
+ − 170
*)
+ − 171
+ − 172
and init_finite_sets: "finite init_files \<and> finite init_procs \<and> (\<forall> p. finite (init_fds_of_proc p)) \<and> finite init_shms \<and> finite init_msgqs \<and> finite init_users"
+ − 173
+ − 174
begin
+ − 175
+ − 176
definition is_init_file:: "t_file \<Rightarrow> bool"
+ − 177
where
+ − 178
"is_init_file f \<equiv> (case (init_inum_of_file f) of
+ − 179
Some i \<Rightarrow> (case (init_itag_of_inum i) of
+ − 180
Some Tag_FILE \<Rightarrow> True
+ − 181
| _ \<Rightarrow> False)
+ − 182
| _ \<Rightarrow> False)"
+ − 183
+ − 184
definition is_init_dir:: "t_file \<Rightarrow> bool"
+ − 185
where
+ − 186
"is_init_dir f \<equiv> (case (init_inum_of_file f) of
+ − 187
Some i \<Rightarrow> (case (init_itag_of_inum i) of
+ − 188
Some Tag_DIR \<Rightarrow> True
+ − 189
| _ \<Rightarrow> False)
+ − 190
| _ \<Rightarrow> False)"
+ − 191
+ − 192
definition is_init_tcp_sock:: "t_socket \<Rightarrow> bool"
+ − 193
where
+ − 194
"is_init_tcp_sock s \<equiv> (case (init_inum_of_socket s) of
+ − 195
Some i \<Rightarrow> (case (init_itag_of_inum i) of
+ − 196
Some Tag_TCP_SOCK \<Rightarrow> True
+ − 197
| _ \<Rightarrow> False)
+ − 198
| _ \<Rightarrow> False)"
+ − 199
+ − 200
definition is_init_udp_sock:: "t_socket \<Rightarrow> bool"
+ − 201
where
+ − 202
"is_init_udp_sock s \<equiv> (case (init_inum_of_socket s) of
+ − 203
Some i \<Rightarrow> (case (init_itag_of_inum i) of
+ − 204
Some Tag_UDP_SOCK \<Rightarrow> True
+ − 205
| _ \<Rightarrow> False)
+ − 206
| _ \<Rightarrow> False)"
+ − 207
2
+ − 208
definition init_same_inode_files :: "t_file \<Rightarrow> t_file set"
+ − 209
where
+ − 210
"init_same_inode_files f \<equiv> {f'. init_inum_of_file f = init_inum_of_file f'}"
+ − 211
1
+ − 212
fun init_alive :: "t_object \<Rightarrow> bool"
+ − 213
where
+ − 214
"init_alive (O_proc p) = (p \<in> init_procs)"
+ − 215
| "init_alive (O_file f) = (is_init_file f)"
+ − 216
| "init_alive (O_dir f) = (is_init_dir f)"
+ − 217
| "init_alive (O_fd p fd) = (fd \<in> init_fds_of_proc p)"
+ − 218
| "init_alive (O_node n) = (n \<in> init_nodes)"
+ − 219
| "init_alive (O_tcp_sock k) = (is_init_tcp_sock k)"
+ − 220
| "init_alive (O_udp_sock k) = (is_init_udp_sock k)"
+ − 221
| "init_alive (O_shm h) = (h \<in> init_shms)"
+ − 222
| "init_alive (O_msgq q) = (q \<in> init_msgqs)"
+ − 223
| "init_alive (O_msg q m) = (m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs)"
+ − 224
+ − 225
+ − 226
(************ system listeners, event-related ***********)
+ − 227
+ − 228
fun file_of_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_file option"
+ − 229
where
+ − 230
"file_of_proc_fd [] p' fd' = (init_file_of_proc_fd p' fd')"
+ − 231
| "file_of_proc_fd (Open p f flags fd iopt # \<tau>) p' fd' =
+ − 232
(if (p' = p \<and> fd = fd') then Some f else file_of_proc_fd \<tau> p' fd')"
+ − 233
| "file_of_proc_fd (CloseFd p fd # \<tau>) p' fd' =
+ − 234
(if (p = p' \<and> fd = fd') then None else file_of_proc_fd \<tau> p' fd')"
+ − 235
(*deleted: if (f\<^isub>3 \<preceq> f\<^isub>1) then None else *)
+ − 236
(*
+ − 237
| "file_of_proc_fd (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) p' fd =
+ − 238
(case (file_of_proc_fd \<tau> p' fd) of
+ − 239
Some f\<^isub>1 \<Rightarrow> (if (f\<^isub>2 \<preceq> f\<^isub>1) then Some (file_after_rename f\<^isub>2 f\<^isub>3 f\<^isub>1)
+ − 240
else Some f\<^isub>1)
+ − 241
| None \<Rightarrow> None )"
+ − 242
*)
+ − 243
| "file_of_proc_fd (Execve p f fds # \<tau>) p' fd =
+ − 244
(if (p' = p \<and> fd \<in> fds) then file_of_proc_fd \<tau> p fd
+ − 245
else if (p' = p) then None
+ − 246
else file_of_proc_fd \<tau> p' fd) "
+ − 247
| "file_of_proc_fd (Clone p p' fds shms # \<tau>) p'' fd =
+ − 248
(if (p'' = p' \<and> fd \<in> fds) then file_of_proc_fd \<tau> p fd
+ − 249
else if (p'' = p') then None
+ − 250
else file_of_proc_fd \<tau> p'' fd)"
+ − 251
| "file_of_proc_fd (Kill p\<^isub> p\<^isub>' # \<tau>) p'' fd =
+ − 252
(if (p'' = p\<^isub>') then None else file_of_proc_fd \<tau> p'' fd)"
+ − 253
| "file_of_proc_fd (Exit p # \<tau>) p' fd =
+ − 254
(if (p = p') then None else file_of_proc_fd \<tau> p' fd)"
+ − 255
| "file_of_proc_fd (_ # \<tau>) p fd = file_of_proc_fd \<tau> p fd"
+ − 256
+ − 257
definition proc_fd_of_file :: "t_state \<Rightarrow> t_file \<Rightarrow> (t_process \<times> t_fd) set"
+ − 258
where
+ − 259
"proc_fd_of_file \<tau> f = {(p, fd) | p fd. file_of_proc_fd \<tau> p fd = Some f}"
+ − 260
+ − 261
+ − 262
(****** files and directories ******)
+ − 263
+ − 264
fun files_hung_by_del :: "t_state \<Rightarrow> t_file set"
+ − 265
where
+ − 266
"files_hung_by_del [] = init_files_hung_by_del"
+ − 267
| "files_hung_by_del (UnLink p f # \<tau>) = (
+ − 268
if (proc_fd_of_file \<tau> f = {}) then files_hung_by_del \<tau>
+ − 269
else insert f (files_hung_by_del \<tau>))"
+ − 270
(* | files_hung_by_del (Rmdir p f) is not need, for open can only apply to file not dir *)
+ − 271
| "files_hung_by_del (CloseFd p fd # \<tau>) = (
+ − 272
case (file_of_proc_fd \<tau> p fd) of
+ − 273
Some f \<Rightarrow> (if (proc_fd_of_file \<tau> f = {(p, fd)})
+ − 274
then files_hung_by_del \<tau> - {f}
+ − 275
else files_hung_by_del \<tau>)
+ − 276
| None \<Rightarrow> files_hung_by_del \<tau> )"
+ − 277
(*
+ − 278
| "files_hung_by_del (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) = {file_after_rename f\<^isub>2 f\<^isub>3 f\<^isub>1| f\<^isub>1. f\<^isub>1 \<in> files_hung_by_del \<tau>}" (* for rename(2) does not infect on fd of the file, see man -S 2 rename *)
+ − 279
*)
+ − 280
| "files_hung_by_del (e # \<tau>) = files_hung_by_del \<tau>"
+ − 281
declare files_hung_by_del.simps [simp del]
+ − 282
+ − 283
fun inum_of_file :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_inode_num)"
+ − 284
where
+ − 285
"inum_of_file [] = init_inum_of_file"
+ − 286
| "inum_of_file (Open p f flags fd (Some inum) # \<tau>) = (inum_of_file \<tau>) (f := Some inum)"
+ − 287
| "inum_of_file (CloseFd p fd # \<tau>) = (
+ − 288
case (file_of_proc_fd \<tau> p fd) of
+ − 289
Some f \<Rightarrow> ( if ((proc_fd_of_file \<tau> f = {(p, fd)}) \<and> (f \<in> files_hung_by_del \<tau>))
+ − 290
then (inum_of_file \<tau>) (f := None)
+ − 291
else inum_of_file \<tau> )
+ − 292
| _ \<Rightarrow> (inum_of_file \<tau>) )"
+ − 293
| "inum_of_file (UnLink p f # \<tau>) = (
+ − 294
if (proc_fd_of_file \<tau> f = {})
+ − 295
then (inum_of_file \<tau>) (f := None)
+ − 296
else inum_of_file \<tau> )"
+ − 297
| "inum_of_file (Rmdir p f # \<tau>) = (
+ − 298
if (proc_fd_of_file \<tau> f = {})
+ − 299
then (inum_of_file \<tau>) (f := None)
+ − 300
else inum_of_file \<tau> )"
+ − 301
| "inum_of_file (Mkdir p f ino # \<tau>) = (inum_of_file \<tau>) (f:= Some ino)"
+ − 302
| "inum_of_file (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) = (inum_of_file \<tau>) (f\<^isub>2 := inum_of_file \<tau> f\<^isub>1)"
+ − 303
(*
+ − 304
| "inum_of_file (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) = (\<lambda> f.
+ − 305
if (f\<^isub>2 \<preceq> f) then None
+ − 306
else if (f\<^isub>3 \<preceq> f) then inum_of_file \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f)
+ − 307
else inum_of_file \<tau> f )"
+ − 308
*)
+ − 309
| "inum_of_file (e # \<tau>) = inum_of_file \<tau>"
+ − 310
+ − 311
definition current_files :: "t_state \<Rightarrow> t_file set"
+ − 312
where
+ − 313
"current_files \<tau> = {f. \<exists> i. inum_of_file \<tau> f = Some i}"
+ − 314
+ − 315
definition has_same_inode :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file \<Rightarrow> bool"
+ − 316
where
+ − 317
"has_same_inode \<tau> fa fb =
+ − 318
(\<exists>i. inum_of_file \<tau> fa = Some i \<and> inum_of_file \<tau> fb = Some i)"
+ − 319
+ − 320
fun inum_of_socket :: "t_state \<Rightarrow> (t_socket \<rightharpoonup> t_inode_num)"
+ − 321
where
+ − 322
"inum_of_socket [] = init_inum_of_socket"
+ − 323
| "inum_of_socket (CloseFd p fd # \<tau>) =
+ − 324
(inum_of_socket \<tau>) ((p, fd):= None)"
+ − 325
| "inum_of_socket (CreateSock p af st fd ino # \<tau>) =
+ − 326
(inum_of_socket \<tau>) ((p, fd) := Some ino)"
+ − 327
| "inum_of_socket (Accept p fd addr lport' fd' ino # \<tau>) =
+ − 328
(inum_of_socket \<tau>) ((p, fd') := Some ino)"
+ − 329
| "inum_of_socket (Clone p p' fds shms # \<tau>) =
+ − 330
(\<lambda> (p'', fd). if (p'' = p' \<and> fd \<in> fds) then inum_of_socket \<tau> (p, fd)
+ − 331
else if (p'' = p') then None
+ − 332
else inum_of_socket \<tau> (p'',fd))"
+ − 333
| "inum_of_socket (Execve p f fds # \<tau>) =
+ − 334
(\<lambda> (p', fd). if (p' = p \<and> fd \<in> fds) then inum_of_socket \<tau> (p, fd)
+ − 335
else if (p' = p) then None
+ − 336
else inum_of_socket \<tau> (p', fd))"
+ − 337
| "inum_of_socket (Kill p\<^isub>1 p\<^isub>2 # \<tau>) =
+ − 338
(\<lambda> (p, fd). if (p = p\<^isub>2) then None else inum_of_socket \<tau> (p, fd) )"
+ − 339
| "inum_of_socket (Exit p # \<tau>) =
+ − 340
(\<lambda> (p', fd). if (p' = p) then None else inum_of_socket \<tau> (p', fd))"
+ − 341
| "inum_of_socket (_ # \<tau>) = inum_of_socket \<tau>"
+ − 342
+ − 343
definition current_sockets :: "t_state \<Rightarrow> t_socket set"
+ − 344
where
+ − 345
"current_sockets \<tau> = {s. \<exists> i. inum_of_socket \<tau> s = Some i}"
+ − 346
+ − 347
(* experimentary: for the delete obj's (file or socket) inode num, it is unnecessary for itag_of_inum to be NONE, cause this is the situation blocked by inum_of_file / inum_of_socket !!! *)
+ − 348
(* delete a file, just recycle its inode num, but not destroy its inode \<dots>, so it is irrelative to these events, like closeFd, Rmdir, UnLink \<dots>*)
+ − 349
fun itag_of_inum :: "t_state \<Rightarrow> (t_inode_num \<rightharpoonup> t_inode_tag)"
+ − 350
where
+ − 351
"itag_of_inum [] = init_itag_of_inum"
+ − 352
| "itag_of_inum (Open p f flags fd (Some ino) # \<tau>) = (itag_of_inum \<tau>) (ino := Some Tag_FILE)"
+ − 353
| "itag_of_inum (Mkdir p f ino # \<tau>) = (itag_of_inum \<tau>) (ino := Some Tag_DIR)"
+ − 354
| "itag_of_inum (CreateSock p af st fd ino # \<tau>) =
+ − 355
(case st of
+ − 356
STREAM \<Rightarrow> (itag_of_inum \<tau>) (ino := Some Tag_TCP_SOCK)
+ − 357
| DGRAM \<Rightarrow> (itag_of_inum \<tau>) (ino := Some Tag_UDP_SOCK) )"
+ − 358
| "itag_of_inum (Accept p fd addr lport' fd' ino # \<tau>) =
+ − 359
(itag_of_inum \<tau>) (ino := Some Tag_TCP_SOCK)"
+ − 360
| "itag_of_inum (_ # \<tau>) = itag_of_inum \<tau>" (* may be sth wrong with nettemp representing addr \<times> netdev in statical analysis ??? *)
+ − 361
+ − 362
definition is_file:: "t_state \<Rightarrow> t_file \<Rightarrow> bool"
+ − 363
where
+ − 364
"is_file \<tau> f \<equiv> (case (inum_of_file \<tau> f) of
+ − 365
Some i \<Rightarrow> (case (itag_of_inum \<tau> i) of
+ − 366
Some Tag_FILE \<Rightarrow> True
+ − 367
| _ \<Rightarrow> False)
+ − 368
| _ \<Rightarrow> False)"
+ − 369
+ − 370
definition is_dir:: "t_state \<Rightarrow> t_file \<Rightarrow> bool"
+ − 371
where
+ − 372
"is_dir \<tau> f \<equiv> (case (inum_of_file \<tau> f) of
+ − 373
Some i \<Rightarrow> (case (itag_of_inum \<tau> i) of
+ − 374
Some Tag_DIR \<Rightarrow> True
+ − 375
| _ \<Rightarrow> False)
+ − 376
| _ \<Rightarrow> False)"
+ − 377
+ − 378
definition dir_is_empty :: "t_state \<Rightarrow> t_file \<Rightarrow> bool"
+ − 379
where
+ − 380
"dir_is_empty \<tau> f \<equiv> is_dir \<tau> f \<and> \<not> (\<exists> f'. f' \<in> current_files \<tau> \<and> f \<prec> f')"
+ − 381
+ − 382
definition is_tcp_sock :: "t_state \<Rightarrow> t_socket \<Rightarrow> bool"
+ − 383
where
+ − 384
"is_tcp_sock \<tau> s \<equiv> (case (inum_of_socket \<tau> s) of
+ − 385
Some i \<Rightarrow> (case (itag_of_inum \<tau> i) of
+ − 386
Some Tag_TCP_SOCK \<Rightarrow> True
+ − 387
| _ \<Rightarrow> False)
+ − 388
| _ \<Rightarrow> False)"
+ − 389
+ − 390
definition is_udp_sock :: "t_state \<Rightarrow> t_socket \<Rightarrow> bool"
+ − 391
where
+ − 392
"is_udp_sock \<tau> s \<equiv> (case (inum_of_socket \<tau> s) of
+ − 393
Some i \<Rightarrow> (case (itag_of_inum \<tau> i) of
+ − 394
Some Tag_UDP_SOCK \<Rightarrow> True
+ − 395
| _ \<Rightarrow> False)
+ − 396
| _ \<Rightarrow> False)"
+ − 397
+ − 398
fun current_procs :: "t_state \<Rightarrow> t_process set"
+ − 399
where
+ − 400
"current_procs [] = init_procs"
+ − 401
| "current_procs (Clone p p' fds shms # \<tau>) = (insert p' (current_procs \<tau>))"
+ − 402
| "current_procs (Exit p # \<tau>) = (current_procs \<tau> - {p})"
+ − 403
| "current_procs (Kill p p' # \<tau>) = (current_procs \<tau> - {p'})"
+ − 404
| "current_procs (_ # \<tau>) = current_procs \<tau>"
+ − 405
+ − 406
fun current_proc_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set"
+ − 407
where
+ − 408
"current_proc_fds [] = init_fds_of_proc"
+ − 409
| "current_proc_fds (Open p f flags fd iopt # \<tau>) =
+ − 410
(current_proc_fds \<tau>) (p:= insert fd (current_proc_fds \<tau> p))"
+ − 411
| "current_proc_fds (CreateSock p sf st newfd newi # \<tau>) =
+ − 412
(current_proc_fds \<tau>) (p:= insert newfd (current_proc_fds \<tau> p))"
+ − 413
| "current_proc_fds (Accept p fd raddr port fd' ino # \<tau>) =
+ − 414
(current_proc_fds \<tau>) (p:= insert fd' (current_proc_fds \<tau> p))"
+ − 415
| "current_proc_fds (CloseFd p fd # \<tau>) =
+ − 416
(current_proc_fds \<tau>) (p:= (current_proc_fds \<tau> p) - {fd})"
+ − 417
| "current_proc_fds (Clone p p' fds shms # \<tau>) =
+ − 418
(current_proc_fds \<tau>) (p':= fds)"
+ − 419
| "current_proc_fds (Execve p f fds # \<tau>) =
+ − 420
(current_proc_fds \<tau>) (p:= fds)"
+ − 421
| "current_proc_fds (Exit p # \<tau>) = (current_proc_fds \<tau>) (p := {})"
+ − 422
| "current_proc_fds (Kill p p' # \<tau>) = (current_proc_fds \<tau>) (p' := {})"
+ − 423
| "current_proc_fds (_ # \<tau>) = current_proc_fds \<tau>"
+ − 424
+ − 425
fun current_shms :: "t_state \<Rightarrow> t_shm set"
+ − 426
where
+ − 427
"current_shms [] = init_shms"
+ − 428
| "current_shms (CreateShM p newshm # \<tau>) = insert newshm (current_shms \<tau>)"
+ − 429
| "current_shms (DeleteShM p s # \<tau>) = (current_shms \<tau>) - {s}"
+ − 430
| "current_shms (e # \<tau>) = current_shms \<tau> "
+ − 431
+ − 432
fun procs_of_shm :: "t_state \<Rightarrow> t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set"
+ − 433
where
+ − 434
"procs_of_shm [] = init_procs_of_shm"
+ − 435
| "procs_of_shm (CreateShM p h # \<tau>) =
+ − 436
(procs_of_shm \<tau>) (h := {})" (* creator may not be the sharer of the shm *)
+ − 437
| "procs_of_shm (Attach p h flag # \<tau>) =
+ − 438
(procs_of_shm \<tau>) (h := insert (p, flag) (procs_of_shm \<tau> h))"
+ − 439
| "procs_of_shm (Detach p h # \<tau>) =
+ − 440
(procs_of_shm \<tau>) (h := (procs_of_shm \<tau> h) - {(p,flag). \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h})"
+ − 441
| "procs_of_shm (DeleteShM p h # \<tau>) = (procs_of_shm \<tau>) (h := {})"
+ − 442
| "procs_of_shm (Clone p p' fds shms # \<tau>) =
+ − 443
(\<lambda> h. if (h \<in> shms)
+ − 444
then (procs_of_shm \<tau> h) \<union> {(p', flag). \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h}
+ − 445
else procs_of_shm \<tau> h)"
+ − 446
| "procs_of_shm (Execve p f fds # \<tau>) =
+ − 447
(\<lambda> h. procs_of_shm \<tau> h - {(p, flag). \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h})"
+ − 448
| "procs_of_shm (e # \<tau>) = procs_of_shm \<tau>"
+ − 449
+ − 450
definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
+ − 451
where
+ − 452
"info_flow_shm \<tau> from to \<equiv> (from = to) \<or> (\<exists> h \<in> current_shms \<tau>. \<exists> toflag.
+ − 453
(((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))"
+ − 454
+ − 455
fun current_msgqs :: "t_state \<Rightarrow> t_msg set"
+ − 456
where
+ − 457
"current_msgqs [] = init_msgqs"
+ − 458
| "current_msgqs (CreateMsgq p q # \<tau>) = insert q (current_msgqs \<tau>)"
+ − 459
| "current_msgqs (RemoveMsgq p q # \<tau>) = (current_msgqs \<tau>) - {q}"
+ − 460
| "current_msgqs (_ # \<tau>) = current_msgqs \<tau>"
+ − 461
+ − 462
fun msgs_of_queue :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list"
+ − 463
where
+ − 464
"msgs_of_queue [] = init_msgs_of_queue"
+ − 465
| "msgs_of_queue (CreateMsgq p q # \<tau>) = (msgs_of_queue \<tau>)(q := [])"
+ − 466
| "msgs_of_queue (SendMsg p q m # \<tau>) = (msgs_of_queue \<tau>)(q := msgs_of_queue \<tau> q @ [m])"
+ − 467
| "msgs_of_queue (RecvMsg p q m # \<tau>) = (msgs_of_queue \<tau>)(q := tl (msgs_of_queue \<tau> q))"
+ − 468
| "msgs_of_queue (RemoveMsgq p q # \<tau>) = (msgs_of_queue \<tau>)(q := [])"
+ − 469
| "msgs_of_queue (_ # \<tau>) = msgs_of_queue \<tau>"
+ − 470
+ − 471
definition current_file_inums :: "t_state \<Rightarrow> t_inode_num set"
+ − 472
where
+ − 473
"current_file_inums \<tau> \<equiv> {im. \<exists> f. inum_of_file \<tau> f = Some im}"
+ − 474
+ − 475
definition current_sock_inums :: "t_state \<Rightarrow> t_inode_num set"
+ − 476
where
+ − 477
"current_sock_inums \<tau> = {im. \<exists> s. inum_of_socket \<tau> s = Some im}"
+ − 478
+ − 479
definition current_inode_nums :: "t_state \<Rightarrow> nat set"
+ − 480
where
+ − 481
"current_inode_nums \<tau> = current_file_inums \<tau> \<union> current_sock_inums \<tau>"
+ − 482
2
+ − 483
definition same_inode_files :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file set"
+ − 484
where
+ − 485
"same_inode_files s f \<equiv> {f'. inum_of_file s f = inum_of_file s f'}"
+ − 486
1
+ − 487
fun flags_of_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_open_flags option"
+ − 488
where
+ − 489
"flags_of_proc_fd [] p fd = init_oflags_of_proc_fd p fd"
+ − 490
| "flags_of_proc_fd (Open p f flags fd iopt # \<tau>) p' fd' =
+ − 491
(if (p = p' \<and> fd = fd') then Some flags else flags_of_proc_fd \<tau> p' fd')"
+ − 492
| "flags_of_proc_fd (CloseFd p fd # \<tau>) p' fd' =
+ − 493
(if (p = p' \<and> fd = fd') then None else flags_of_proc_fd \<tau> p' fd')"
+ − 494
| "flags_of_proc_fd (CreateSock p af st fd ino # \<tau>) p' fd' =
+ − 495
(if (p = p' \<and> fd = fd') then None else flags_of_proc_fd \<tau> p' fd')"
+ − 496
| "flags_of_proc_fd (Accept p fd addr lport' fd' ino # \<tau>) p' fd'' =
+ − 497
(if (p = p' \<and> fd' = fd'') then None else flags_of_proc_fd \<tau> p' fd'')"
+ − 498
| "flags_of_proc_fd (Clone p p' fds shms # \<tau>) p'' fd =
+ − 499
(if (p' = p'' \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd else flags_of_proc_fd \<tau> p'' fd)"
+ − 500
| "flags_of_proc_fd (Execve p f fds # \<tau>) p' fd =
+ − 501
(if (p' = p \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd else flags_of_proc_fd \<tau> p' fd)"
+ − 502
| "flags_of_proc_fd (Kill p\<^isub>1 p\<^isub>2 # \<tau>) p fd =
+ − 503
(if (p = p\<^isub>2) then None else flags_of_proc_fd \<tau> p fd)"
+ − 504
| "flags_of_proc_fd (Exit p # \<tau>) p' fd' =
+ − 505
(if (p = p') then None else flags_of_proc_fd \<tau> p' fd')"
+ − 506
| "flags_of_proc_fd (e # \<tau>) p fd = flags_of_proc_fd \<tau> p fd"
+ − 507
+ − 508
(*
+ − 509
fun file_at_writing_by:: "t_state \<Rightarrow> t_file \<Rightarrow> (t_process \<times> t_fd) set"
+ − 510
where
+ − 511
"file_at_writing_by [] f = init_file_at_writing_by f"
+ − 512
| "file_at_writing_by (Open p f flags fd (Some inum) # \<tau>) f' = (
+ − 513
if (f' = f)
+ − 514
then ( if (is_write_flag flags)
+ − 515
then {(p, fd)}
+ − 516
else {} )
+ − 517
else file_at_writing_by \<tau> f' )"
+ − 518
| "file_at_writing_by (Open p f flags fd None # \<tau>) f' = (
+ − 519
if (f' = f \<and> is_write_flag flags)
+ − 520
then insert (p, fd) (file_at_writing_by \<tau> f)
+ − 521
else file_at_writing_by \<tau> f' )"
+ − 522
| "file_at_writing_by (Mkdir p f inum # \<tau>) f' =
+ − 523
(if (f' = f) then {} else file_at_writing_by \<tau> f')"
+ − 524
| "file_at_writing_by (LinkHard p f f' # \<tau>) f'' =
+ − 525
(if (f'' = f') then file_at_writing_by \<tau> f else file_at_writing_by \<tau> f'')"
+ − 526
| "file_at_writing_by (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = (
+ − 527
if (f\<^isub>3 \<preceq> f) then file_at_writing_by \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f)
+ − 528
else file_at_writing_by \<tau> f )"
+ − 529
| "file_at_writing_by (CloseFd p fd # \<tau>) f =
+ − 530
(file_at_writing_by \<tau> f - {(p, fd)})"
+ − 531
| "file_at_writing_by (Clone p p' fds shms # \<tau>) f =
+ − 532
(file_at_writing_by \<tau> f) \<union> {(p',fd)| fd. fd \<in> fds \<and> (p, fd) \<in> file_at_writing_by \<tau> f}"
+ − 533
| "file_at_writing_by (Execve p f fds # \<tau>) f' =
+ − 534
(if (f' = f) then {} else file_at_writing_by \<tau> f')"
+ − 535
| "file_at_writing_by (Exit p # \<tau>) f =
+ − 536
(file_at_writing_by \<tau> f - {(p, fd)| fd. (p, fd) \<in> file_at_writing_by \<tau> f})"
+ − 537
| "file_at_writing_by (Kill p p' # \<tau>) f =
+ − 538
(file_at_writing_by \<tau> f - {(p', fd)| fd. (p', fd) \<in> file_at_writing_by \<tau> f})"
+ − 539
| "file_at_writing_by (e # \<tau>) f = file_at_writing_by \<tau> f"
+ − 540
*)
+ − 541
+ − 542
definition current_users :: "t_state \<Rightarrow> user_t set"
+ − 543
where
+ − 544
"current_users \<tau> \<equiv> init_users"
+ − 545
+ − 546
fun update_with_shuthow :: "t_sock_state option \<Rightarrow> t_shutdown_how \<Rightarrow> t_sock_state option"
+ − 547
where
+ − 548
"update_with_shuthow (Some (SS_trans Trans_Recv)) SHUT_RD = Some (SS_trans Trans_No)"
+ − 549
| "update_with_shuthow (Some (SS_trans Trans_RS)) SHUT_RD = Some (SS_trans Trans_Send)"
+ − 550
| "update_with_shuthow (Some (SS_trans Trans_Send)) SHUT_RD = Some (SS_trans Trans_Send)"
+ − 551
| "update_with_shuthow (Some (SS_trans Trans_No)) SHUT_RD = Some (SS_trans Trans_No)"
+ − 552
| "update_with_shuthow (Some (SS_trans Trans_Recv)) SHUT_WR = Some (SS_trans Trans_Recv)"
+ − 553
| "update_with_shuthow (Some (SS_trans Trans_RS)) SHUT_WR = Some (SS_trans Trans_Recv)"
+ − 554
| "update_with_shuthow (Some (SS_trans Trans_Send)) SHUT_WR = Some (SS_trans Trans_No)"
+ − 555
| "update_with_shuthow (Some (SS_trans Trans_No)) SHUT_WR = Some (SS_trans Trans_No)"
+ − 556
| "update_with_shuthow (Some (SS_trans Trans_Recv)) SHUT_RDWR = Some (SS_trans Trans_No)"
+ − 557
| "update_with_shuthow (Some (SS_trans Trans_RS)) SHUT_RDWR = Some (SS_trans Trans_No)"
+ − 558
| "update_with_shuthow (Some (SS_trans Trans_Send)) SHUT_RDWR = Some (SS_trans Trans_No)"
+ − 559
| "update_with_shuthow (Some (SS_trans Trans_No)) SHUT_RDWR = Some (SS_trans Trans_No)"
+ − 560
| "update_with_shuthow opt1 how = None"
+ − 561
+ − 562
fun socket_state :: "t_state \<Rightarrow> t_socket \<Rightarrow> t_sock_state option"
+ − 563
where
+ − 564
"socket_state [] = init_socket_state"
+ − 565
| "socket_state (CloseFd p fd # \<tau>) =
+ − 566
(socket_state \<tau>) ((p, fd):= None)"
+ − 567
| "socket_state (CreateSock p af st fd ino # \<tau>) =
+ − 568
(socket_state \<tau>) ((p, fd) := Some SS_create)"
+ − 569
| "socket_state (Bind p fd addr # \<tau>) =
+ − 570
(socket_state \<tau>) ((p, fd) := Some SS_bind)"
+ − 571
| "socket_state (Connect p fd addr # \<tau>) =
+ − 572
(socket_state \<tau>) ((p, fd) := Some (SS_trans Trans_RS))"
+ − 573
| "socket_state (Listen p fd # \<tau>) =
+ − 574
(socket_state \<tau>) ((p, fd) := Some SS_listen)"
+ − 575
| "socket_state (Accept p fd addr lport' fd' ino # \<tau>) =
+ − 576
(socket_state \<tau>) ((p, fd') := Some (SS_trans Trans_RS))"
+ − 577
| "socket_state (Shutdown p fd sh # \<tau>) =
+ − 578
(socket_state \<tau>) ((p, fd) := update_with_shuthow (socket_state \<tau> (p, fd)) sh)"
+ − 579
| "socket_state (Clone p p' fds shms # \<tau>) =
+ − 580
(\<lambda> (p'', fd). if (p'' = p' \<and> fd \<in> fds) then socket_state \<tau> (p, fd)
+ − 581
else if (p'' = p') then None
+ − 582
else socket_state \<tau> (p'', fd))"
+ − 583
| "socket_state (Execve p f fds # \<tau>) =
+ − 584
(\<lambda> (p', fd). if (p' = p \<and> fd \<in> fds) then socket_state \<tau> (p, fd)
+ − 585
else if (p' = p) then None
+ − 586
else socket_state \<tau> (p', fd))"
+ − 587
| "socket_state (Kill p\<^isub>1 p\<^isub>2 # \<tau>) =
+ − 588
(\<lambda> (p, fd). if (p = p\<^isub>2) then None else socket_state \<tau> (p, fd))"
+ − 589
| "socket_state (Exit p # \<tau>) =
+ − 590
(\<lambda> (p', fd'). if (p = p') then None else socket_state \<tau> (p', fd'))"
+ − 591
| "socket_state (e # \<tau>) = socket_state \<tau>"
+ − 592
+ − 593
definition socket_in_trans :: "t_state \<Rightarrow> t_socket \<Rightarrow> bool"
+ − 594
where
+ − 595
"socket_in_trans \<tau> s \<equiv> (case (socket_state \<tau> s) of
+ − 596
Some st \<Rightarrow> (case st of
+ − 597
SS_trans para \<Rightarrow> True
+ − 598
| _ \<Rightarrow> False)
+ − 599
| _ \<Rightarrow> False)"
+ − 600
+ − 601
definition socket_in_sending :: "t_state \<Rightarrow> t_socket \<Rightarrow> bool"
+ − 602
where
+ − 603
"socket_in_sending \<tau> s \<equiv> (socket_state \<tau> s = Some (SS_trans Trans_Send)) \<or> (socket_state \<tau> s = Some (SS_trans Trans_RS))"
+ − 604
+ − 605
definition socket_in_recving :: "t_state \<Rightarrow> t_socket \<Rightarrow> bool"
+ − 606
where
+ − 607
"socket_in_recving \<tau> s \<equiv> (socket_state \<tau> s = Some (SS_trans Trans_Recv)) \<or> (socket_state \<tau> s = Some (SS_trans Trans_RS))"
+ − 608
+ − 609
+ − 610
(******* admissable check by the OS *******)
+ − 611
fun os_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool"
+ − 612
where
+ − 613
"os_grant \<tau> (Open p f flags fd inumopt) = (
+ − 614
case inumopt of
+ − 615
Some ino \<Rightarrow>
+ − 616
(p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and>
+ − 617
(\<exists> pf. parent f = Some pf \<and> pf \<in> current_files \<tau> \<and> is_dir \<tau> pf \<and> pf \<notin> files_hung_by_del \<tau>) \<and>
+ − 618
is_creat_flag flags \<and> fd \<notin> (current_proc_fds \<tau> p) \<and> ino \<notin> (current_inode_nums \<tau>))
+ − 619
| None \<Rightarrow>
+ − 620
(p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> \<not> is_creat_excl_flag flags \<and> is_file \<tau> f \<and>
+ − 621
fd \<notin> (current_proc_fds \<tau> p)) )"
+ − 622
(*(if (is_dir \<tau> f) then (is_dir_flag flags \<and> \<not> is_write_flag flags) else (\<not> is_dir_flag flags)),
+ − 623
here open is not applied to directories, readdir is for that, but it is not security-related *)
+ − 624
| "os_grant \<tau> (CloseFd p fd) =
+ − 625
(p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p)"
+ − 626
| "os_grant \<tau> (UnLink p f) =
+ − 627
(p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> is_file \<tau> f \<and> f \<notin> files_hung_by_del \<tau>)"
+ − 628
| "os_grant \<tau> (Rmdir p f) =
+ − 629
(p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> dir_is_empty \<tau> f \<and> f \<notin> files_hung_by_del \<tau> \<and> f \<noteq> [])" (* root file cannot be deleted *)
+ − 630
| "os_grant \<tau> (Mkdir p f ino) =
+ − 631
(p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and>
+ − 632
(\<exists> pf. parent f = Some pf \<and> pf \<in> current_files \<tau> \<and> is_dir \<tau> pf \<and> pf \<notin> files_hung_by_del \<tau>) \<and>
+ − 633
ino \<notin> (current_inode_nums \<tau>))"
+ − 634
| "os_grant \<tau> (LinkHard p f\<^isub>1 f\<^isub>2) =
+ − 635
(p \<in> current_procs \<tau> \<and> f\<^isub>1 \<in> current_files \<tau> \<and> f\<^isub>2 \<notin> current_files \<tau> \<and>
+ − 636
(\<exists> pf\<^isub>2. parent f\<^isub>2 = Some pf\<^isub>2 \<and> pf\<^isub>2 \<in> current_files \<tau> \<and> is_dir \<tau> pf\<^isub>2 \<and>
+ − 637
pf\<^isub>2 \<notin> files_hung_by_del \<tau>) \<and> is_file \<tau> f\<^isub>1)"
+ − 638
| "os_grant \<tau> (Truncate p f len) =
+ − 639
(p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> is_file \<tau> f)"
+ − 640
(*
+ − 641
| "os_grant \<tau> (FTruncate p fd len) =
+ − 642
(p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and>
+ − 643
(\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau> \<and> is_file \<tau> f) \<and>
+ − 644
(\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_write_flag flags))"
+ − 645
*)
+ − 646
| "os_grant \<tau> (ReadFile p fd) =
+ − 647
(p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and>
+ − 648
(\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau>) \<and>
+ − 649
(\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_read_flag flags))"
+ − 650
| "os_grant \<tau> (WriteFile p fd) =
+ − 651
(p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and>
+ − 652
(\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau>) \<and>
+ − 653
(\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_write_flag flags))"
+ − 654
| "os_grant \<tau> (Execve p f fds) =
+ − 655
(p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> is_file \<tau> f \<and> fds \<subseteq> current_proc_fds \<tau> p)" (* file_at_writing_by \<tau> f = {} *)
+ − 656
(*
+ − 657
| "os_grant \<tau> (Rename p f\<^isub>2 f\<^isub>3) =
+ − 658
(p \<in> current_procs \<tau> \<and> f\<^isub>2 \<in> current_files \<tau> \<and> \<not>(f\<^isub>2 \<preceq> f\<^isub>3) \<and> f\<^isub>3 \<notin> current_files \<tau> \<and>
+ − 659
(\<exists> pf\<^isub>3. parent f\<^isub>3 = Some pf\<^isub>3 \<and> pf\<^isub>3 \<in> current_files \<tau> \<and> is_dir \<tau> pf\<^isub>3 \<and>
+ − 660
pf\<^isub>3 \<notin> files_hung_by_del \<tau>) )"
+ − 661
*)
+ − 662
| "os_grant \<tau> (CreateMsgq p q) =
+ − 663
(p \<in> current_procs \<tau> \<and> q \<notin> (current_msgqs \<tau>))"
+ − 664
| "os_grant \<tau> (SendMsg p q m) =
+ − 665
(p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m \<notin> (set (msgs_of_queue \<tau> q)))"
+ − 666
| "os_grant \<tau> (RecvMsg p q m) =
+ − 667
(p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m = hd (msgs_of_queue \<tau> q))"
+ − 668
| "os_grant \<tau> (RemoveMsgq p q) =
+ − 669
(p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau>)"
+ − 670
| "os_grant \<tau> (CreateShM p h) =
+ − 671
(p \<in> current_procs \<tau> \<and> h \<notin> (current_shms \<tau>))"
+ − 672
| "os_grant \<tau> (Attach p h flag) =
+ − 673
(p \<in> current_procs \<tau> \<and> h \<in> current_shms \<tau> \<and> \<not> (\<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h))"
+ − 674
| "os_grant \<tau> (Detach p h) =
+ − 675
(p \<in> current_procs \<tau> \<and> h \<in> current_shms \<tau> \<and> (\<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h))"
+ − 676
| "os_grant \<tau> (DeleteShM p h) =
+ − 677
(p \<in> current_procs \<tau> \<and> h \<in> current_shms \<tau>)"
+ − 678
| "os_grant \<tau> (CreateSock p af st fd ino) =
+ − 679
(p \<in> current_procs \<tau> \<and> af = AF_INET \<and> fd \<notin> (current_proc_fds \<tau> p) \<and>
+ − 680
ino \<notin> (current_inode_nums \<tau>))"
+ − 681
| "os_grant \<tau> (Accept p fd addr port fd' ino) =
+ − 682
(p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and>
+ − 683
fd' \<notin> (current_proc_fds \<tau> p) \<and> socket_state \<tau> (p, fd) = Some SS_listen \<and>
+ − 684
is_tcp_sock \<tau> (p, fd) \<and> ino \<notin> (current_inode_nums \<tau>))"
+ − 685
| "os_grant \<tau> (Bind p fd addr) =
+ − 686
(p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and>
+ − 687
socket_state \<tau> (p, fd) = Some SS_create)" (* ?? !! (case addr of INET_ADDR ip port \<Rightarrow> ip \<in> local_ipaddrs)) *)
+ − 688
| "os_grant \<tau> (Connect p fd addr) =
+ − 689
(p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and>
+ − 690
socket_state \<tau> (p, fd) = Some SS_bind)"
+ − 691
| "os_grant \<tau> (Listen p fd) =
+ − 692
(p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and>
+ − 693
socket_state \<tau> (p, fd) = Some SS_bind \<and> is_tcp_sock \<tau> (p, fd))" (* Listen and Accept should only be used for TCP sever side *)
+ − 694
| "os_grant \<tau> (SendSock p fd) =
+ − 695
(p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and>
+ − 696
socket_in_sending \<tau> (p, fd))"
+ − 697
| "os_grant \<tau> (RecvSock p fd) =
+ − 698
(p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and>
+ − 699
socket_in_recving \<tau> (p, fd))"
+ − 700
| "os_grant \<tau> (Shutdown p fd sh) =
+ − 701
(p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and>
+ − 702
socket_in_trans \<tau> (p, fd))"
+ − 703
(*
+ − 704
| "os_grant \<tau> (ChangeOwner p u) = (p \<in> current_procs \<tau> \<and> u \<in> current_users \<tau>)"
+ − 705
*)
+ − 706
| "os_grant \<tau> (Clone p p' fds shms) =
+ − 707
(p \<in> current_procs \<tau> \<and> p' \<notin> (current_procs \<tau>) \<and> fds \<subseteq> current_proc_fds \<tau> p \<and>
+ − 708
(\<forall> h \<in> shms. \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h))"
+ − 709
| "os_grant \<tau> (Kill p\<^isub>1 p\<^isub>2) =
+ − 710
(p\<^isub>1 \<in> current_procs \<tau> \<and> p\<^isub>2 \<in> current_procs \<tau>)" (* a process can kill itself right? *)
+ − 711
| "os_grant \<tau> (Exit p) =
+ − 712
(p \<in> current_procs \<tau>)"
+ − 713
| "os_grant \<tau> (Ptrace p\<^isub>1 p\<^isub>2) =
+ − 714
(p\<^isub>1 \<in> current_procs \<tau> \<and> p\<^isub>2 \<in> current_procs \<tau>)" (* a process can trace itself right? *)
+ − 715
+ − 716
fun alive :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"
+ − 717
where
+ − 718
"alive s (O_proc p) = (p \<in> current_procs s)"
+ − 719
| "alive s (O_file f) = (f \<in> current_files s \<and> is_file s f)"
+ − 720
| "alive s (O_dir f) = (f \<in> current_files s \<and> is_dir s f)"
+ − 721
| "alive s (O_fd p fd) = (fd \<in> current_proc_fds s p)"
+ − 722
| "alive s (O_node n) = (n \<in> init_nodes)"
+ − 723
| "alive s (O_tcp_sock k) = (k \<in> current_sockets s \<and> is_tcp_sock s k)"
+ − 724
| "alive s (O_udp_sock k) = (k \<in> current_sockets s \<and> is_udp_sock s k)"
+ − 725
| "alive s (O_shm h) = (h \<in> current_shms s)"
+ − 726
| "alive s (O_msgq q) = (q \<in> current_msgqs s)"
+ − 727
| "alive s (O_msg q m) = (m \<in> set (msgs_of_queue s q) \<and> q \<in> current_msgqs s)"
+ − 728
+ − 729
(* deleted objects should be "taintable" objects, objects like fd should not be in consideration *)
+ − 730
(* actually, deleted should be renamed as "vanished", cause "exit/closefd" *)
+ − 731
fun deleted :: "t_object \<Rightarrow> t_event list \<Rightarrow> bool"
+ − 732
where
+ − 733
"deleted obj [] = False"
+ − 734
| "deleted obj (Kill p p' # s) = ((obj = O_proc p') \<or> (\<exists> fd \<in> current_proc_fds s p'. obj = O_fd p' fd) \<or>
+ − 735
(\<exists> fd. obj = O_tcp_sock (p', fd) \<and> is_tcp_sock s (p',fd)) \<or>
+ − 736
(\<exists> fd. obj = O_udp_sock (p', fd) \<and> is_udp_sock s (p',fd)) \<or>
+ − 737
deleted obj s)"
+ − 738
| "deleted obj (CloseFd p fd # s) = ((obj = O_fd p fd) \<or> (obj = O_tcp_sock (p,fd) \<and> is_tcp_sock s (p,fd)) \<or>
4
+ − 739
(obj = O_udp_sock (p,fd) \<and> is_udp_sock s (p, fd)) \<or>
+ − 740
(\<exists> f. obj = O_file f \<and> proc_fd_of_file s f = {(p, fd)} \<and>
+ − 741
f \<in> files_hung_by_del s) \<or> deleted obj s)"
1
+ − 742
| "deleted obj (Execve p f fds # s) = ((\<exists> fd \<in> current_proc_fds s p. obj = O_fd p fd \<and> fd \<notin> fds) \<or>
+ − 743
(\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd) \<and> fd \<notin> fds) \<or>
+ − 744
(\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd) \<and> fd \<notin> fds) \<or>
+ − 745
deleted obj s)"
4
+ − 746
| "deleted obj (Clone p p' fds shms # s) = ((\<exists> fd \<in> current_proc_fds s p. obj = O_fd p' fd \<and> fd \<notin> fds) \<or>
+ − 747
deleted obj s)"
1
+ − 748
| "deleted obj (UnLink p f # s) = ((obj = O_file f) \<or> deleted obj s)"
+ − 749
| "deleted obj (Rmdir p f # s) = ((obj = O_dir f) \<or> deleted obj s)"
+ − 750
| "deleted obj (Exit p # s) = ((obj = O_proc p) \<or> (\<exists> fd \<in> current_proc_fds s p. obj = O_fd p fd) \<or>
+ − 751
(\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd)) \<or>
+ − 752
(\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd)) \<or> deleted obj s)"
+ − 753
(*
+ − 754
| "deleted obj (Rename p f f' # s) =
+ − 755
(case obj of
+ − 756
O_file f'' \<Rightarrow> f \<preceq> f'' \<or> deleted obj s
+ − 757
| O_dir f'' \<Rightarrow> f \<preceq> f'' \<or> deleted obj s
+ − 758
| _ \<Rightarrow> deleted obj s)"
+ − 759
*)
+ − 760
| "deleted obj (RemoveMsgq p q # s) = (obj = O_msgq q \<or> (\<exists> m. obj = O_msg q m) \<or> deleted obj s)"
+ − 761
| "deleted obj (DeleteShM p h # s) = (obj = O_shm h \<or> deleted obj s)"
+ − 762
| "deleted obj (RecvMsg p q m # s) = (obj = O_msg q m \<or> deleted obj s)"
+ − 763
| "deleted obj (_ # s) = deleted obj s"
+ − 764
+ − 765
+ − 766
end
+ − 767
+ − 768
+ − 769
+ − 770
locale flask = init +
+ − 771
fixes
+ − 772
(***************** Policy-specific Parameters *************)
+ − 773
type_transition_rules :: "type_transition_rule_list_t"
+ − 774
and allowed_rules :: "allowed_rule_list_t"
+ − 775
and role_allowed_rules :: "role_allow_rule_list_t"
+ − 776
and role_declaration_rules :: "role_declarations_list_t"
+ − 777
and role_transition_rules:: "role_transition_rule_list_t"
+ − 778
and constrains_rules :: "constrains_list_t"
+ − 779
+ − 780
and init_type_of_obj :: "t_object \<rightharpoonup> type_t"
+ − 781
and init_user_of_obj :: "t_object \<rightharpoonup> user_t"
+ − 782
and init_role_of_proc :: "t_process \<rightharpoonup> role_t"
+ − 783
+ − 784
assumes
+ − 785
+ − 786
init_obj_has_type: "\<And> obj. init_alive obj \<Longrightarrow> \<exists> t. init_type_of_obj obj = Some t"
+ − 787
and init_type_has_obj: "\<And> obj t. init_type_of_obj obj = Some t \<Longrightarrow> init_alive obj"
+ − 788
and init_obj_has_user: "\<And> obj. init_alive obj \<Longrightarrow> \<exists> u. init_user_of_obj obj = Some u"
+ − 789
and init_user_has_obj: "\<And> obj u. init_user_of_obj obj = Some u \<Longrightarrow> init_alive obj \<and> u \<in> init_users"
+ − 790
and init_proc_has_role: "bidirect_in_init init_procs init_role_of_proc"
+ − 791
+ − 792
begin
+ − 793
+ − 794
(*********** policy-specified computations, not-event-related ************)
+ − 795
+ − 796
(* security_transition_sid : type_transition_rules
+ − 797
* It's a system-call offered by security-server? So access-control-checked too?
+ − 798
* according to selinux, it deals only with execve and file-creation
+ − 799
* is_execve: if is the execve case
+ − 800
* is_file: if is the creation of file/dir
+ − 801
* change from is_execve to is_file, because the new message by default use
+ − 802
* the type of the sending process too.
+ − 803
*)
+ − 804
+ − 805
definition type_transition :: "type_t \<Rightarrow> type_t \<Rightarrow> security_class_t \<Rightarrow> bool \<Rightarrow> type_t"
+ − 806
where
+ − 807
"type_transition st rt tc IS_file \<equiv> (
+ − 808
case (lookup type_transition_rules
+ − 809
(\<lambda> (stp, rtp, tc', dt). patt_match stp st \<and> patt_match rtp rt \<and> tc = tc')) of
+ − 810
None \<Rightarrow> (if IS_file then rt else st)
+ − 811
| Some (stp,rtp,tc',dt) \<Rightarrow> dt)"
+ − 812
+ − 813
(* allowed_rule_list *)
+ − 814
definition TE_allow :: "type_t \<Rightarrow> type_t \<Rightarrow> security_class_t \<Rightarrow> permission_t \<Rightarrow> bool"
+ − 815
where
+ − 816
"TE_allow st tt tc perm \<equiv> member allowed_rules
+ − 817
(\<lambda> (stp, ttp, tc', pp). tc = tc' \<and> patt_match stp st \<and> patt_match_self ttp tt st \<and>
+ − 818
patt_match pp perm)"
+ − 819
+ − 820
(* role_allow_rule_list_t *)
+ − 821
definition role_transition :: "role_t \<Rightarrow> type_t \<Rightarrow> role_t option"
+ − 822
where
+ − 823
"role_transition r t \<equiv>
+ − 824
(case (lookup role_transition_rules (\<lambda> (pr, ft, nr). pr = r \<and> t = ft)) of
+ − 825
None \<Rightarrow> None
+ − 826
| Some (pr,ft,nr) \<Rightarrow> Some nr)"
+ − 827
+ − 828
definition role_decl_check :: "role_t \<Rightarrow> type_t \<Rightarrow> bool"
+ − 829
where
+ − 830
"role_decl_check r t \<equiv> member role_declaration_rules (\<lambda> (role, types). r = role \<and> t \<in> types)"
+ − 831
+ − 832
definition role_allow :: "role_t \<Rightarrow> role_t \<Rightarrow> bool"
+ − 833
where
+ − 834
"role_allow r nr \<equiv> member role_allowed_rules (\<lambda> (from, to). r \<in> from \<and> nr \<in> to)"
+ − 835
+ − 836
(* here don't use lookup, because constrains should all be satisfied,
+ − 837
* while transitions always choose the "first" one
+ − 838
*)
+ − 839
definition constrains_satisfied ::
+ − 840
"security_context_t \<Rightarrow> security_context_t \<Rightarrow> security_class_t \<Rightarrow> permission_t \<Rightarrow> bool"
+ − 841
where
+ − 842
"constrains_satisfied sctxt tctxt c p \<equiv>
+ − 843
(fold (\<lambda> (cset, pset, P) res. res \<and> (if (c \<in> cset \<and> p \<in> pset)
+ − 844
then P sctxt tctxt else True))
+ − 845
constrains_rules True)"
+ − 846
+ − 847
(* main interface for TE_allow check and constrains check *)
+ − 848
fun permission_check::
+ − 849
"security_context_t \<Rightarrow> security_context_t \<Rightarrow> security_class_t \<Rightarrow> permission_t \<Rightarrow> bool"
+ − 850
where
+ − 851
"permission_check (su,sr,st) (tu,tr,tt) c p =
+ − 852
((TE_allow st tt c p) \<and> (constrains_satisfied (su,sr,st) (tu,tr,tt) c p))"
+ − 853
declare permission_check.simps [simp del]
+ − 854
+ − 855
(* no changeowner ??? : by adding "relabel obj sectxt" event or "login" event?
+ − 856
* or this explanation: the running of the sever will not grant any login but running
+ − 857
* of the server-programs!
+ − 858
*)
+ − 859
+ − 860
fun user_of_obj :: "t_state \<Rightarrow> t_object \<Rightarrow> user_t option"
+ − 861
where
+ − 862
"user_of_obj [] = init_user_of_obj"
+ − 863
| "user_of_obj (Clone p p' fds shms # s) =
+ − 864
(\<lambda> obj. case obj of
+ − 865
O_proc p'' \<Rightarrow> if (p'' = p') then user_of_obj s (O_proc p) else user_of_obj s obj
+ − 866
| O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then user_of_obj s (O_fd p fd)
+ − 867
else if (p'' = p') then None
+ − 868
else user_of_obj s obj
+ − 869
| O_tcp_sock (p'',fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then user_of_obj s (O_tcp_sock (p, fd))
+ − 870
else if (p'' = p') then None
+ − 871
else user_of_obj s obj
+ − 872
| O_udp_sock (p'',fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then user_of_obj s (O_udp_sock (p, fd))
+ − 873
else if (p'' = p') then None
+ − 874
else user_of_obj s obj
+ − 875
| _ \<Rightarrow> user_of_obj s obj)"
+ − 876
| "user_of_obj (Open p f flags fd iopt # s) =
+ − 877
(case iopt of
+ − 878
None \<Rightarrow> (user_of_obj s) ((O_fd p fd) := user_of_obj s (O_proc p))
+ − 879
| _ \<Rightarrow> ((user_of_obj s) ((O_fd p fd) := user_of_obj s (O_proc p)))
+ − 880
((O_file f) := user_of_obj s (O_proc p)))"
+ − 881
| "user_of_obj (Mkdir p f inum # s) =
+ − 882
(user_of_obj s) ((O_dir f) := user_of_obj s (O_proc p))"
+ − 883
| "user_of_obj (LinkHard p f f' # s) =
+ − 884
(user_of_obj s) ((O_file f') := user_of_obj s (O_proc p))"
+ − 885
(*
+ − 886
| "user_of_obj (Rename p f2 f3 # s) =
+ − 887
(\<lambda> obj. case obj of
+ − 888
O_file f \<Rightarrow> if (f3 \<preceq> f) then user_of_obj s (O_file (file_before_rename f2 f3 f))
+ − 889
else user_of_obj s obj
+ − 890
| O_dir f \<Rightarrow> if (f3 \<preceq> f) then user_of_obj s (O_dir (file_before_rename f2 f3 f))
+ − 891
else user_of_obj s obj
+ − 892
| _ \<Rightarrow> user_of_obj s obj)"
+ − 893
*)
+ − 894
| "user_of_obj (CreateMsgq p q # s) =
+ − 895
(user_of_obj s) ((O_msgq q) := user_of_obj s (O_proc p))"
+ − 896
| "user_of_obj (SendMsg p q m # s) =
+ − 897
(user_of_obj s) ((O_msg q m) := user_of_obj s (O_proc p))"
+ − 898
| "user_of_obj (CreateShM p h # s) =
+ − 899
(user_of_obj s) ((O_shm h) := user_of_obj s (O_proc p))"
+ − 900
| "user_of_obj (CreateSock p af st fd inum # s) = (\<lambda> obj.
+ − 901
case obj of
+ − 902
O_fd p' fd' \<Rightarrow> if (p' = p \<and> fd' = fd) then user_of_obj s (O_proc p)
+ − 903
else user_of_obj s obj
+ − 904
| O_tcp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = STREAM) then user_of_obj s (O_proc p)
+ − 905
else user_of_obj s obj
+ − 906
| O_udp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = DGRAM) then user_of_obj s (O_proc p)
+ − 907
else user_of_obj s obj
+ − 908
| _ \<Rightarrow> user_of_obj s obj )"
+ − 909
| "user_of_obj (Accept p fd addr port fd' inum # s) = (\<lambda> obj.
+ − 910
case obj of
+ − 911
O_fd p' fd'' \<Rightarrow> if (p' = p \<and> fd'' = fd') then user_of_obj s (O_proc p)
+ − 912
else user_of_obj s obj
+ − 913
| O_tcp_sock (p', fd'') \<Rightarrow> if (p' = p \<and> fd'' = fd') then user_of_obj s (O_proc p)
+ − 914
else user_of_obj s obj
+ − 915
| _ \<Rightarrow> user_of_obj s obj )"
+ − 916
| "user_of_obj (_ # s) = user_of_obj s"
+ − 917
+ − 918
fun type_of_obj :: "t_state \<Rightarrow> (t_object \<Rightarrow> type_t option)"
+ − 919
where
+ − 920
"type_of_obj [] = init_type_of_obj"
+ − 921
| "type_of_obj (Clone p p' fds shms # s) = (\<lambda> obj.
+ − 922
case obj of
+ − 923
O_proc p'' \<Rightarrow> if (p'' = p') then type_of_obj s (O_proc p) else type_of_obj s obj
+ − 924
| O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then type_of_obj s (O_fd p fd)
+ − 925
else if (p'' = p') then None
+ − 926
else type_of_obj s obj
+ − 927
| O_tcp_sock (p'', fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then type_of_obj s (O_tcp_sock (p, fd))
+ − 928
else if (p'' = p') then None
+ − 929
else type_of_obj s obj
+ − 930
| O_udp_sock (p'', fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then type_of_obj s (O_udp_sock (p, fd))
+ − 931
else if (p'' = p') then None
+ − 932
else type_of_obj s obj
+ − 933
| _ \<Rightarrow> type_of_obj s obj )"
+ − 934
| "type_of_obj (Execve p f fds # s) = (type_of_obj s) ((O_proc p) :=
+ − 935
(case (type_of_obj s (O_proc p), type_of_obj s (O_file f)) of
+ − 936
(Some tp, Some tf) \<Rightarrow> Some (type_transition tp tf C_process False)
+ − 937
| _ \<Rightarrow> None) )"
+ − 938
| "type_of_obj (Open p f flags fd (Some inum) # s) = ((type_of_obj s) ((O_file f) :=
+ − 939
(case (parent f) of
+ − 940
Some pf \<Rightarrow> (case (type_of_obj s (O_proc p), type_of_obj s (O_dir pf)) of
+ − 941
(Some tp, Some tpf) \<Rightarrow> Some (type_transition tp tpf C_file True)
+ − 942
| _ \<Rightarrow> None)
+ − 943
| _ \<Rightarrow> None) )) ((O_fd p fd) :=
+ − 944
type_of_obj s (O_proc p))"
+ − 945
| "type_of_obj (Open p f flags fd None # s) = (type_of_obj s) ((O_fd p fd) :=
+ − 946
type_of_obj s (O_proc p))"
+ − 947
| "type_of_obj (Mkdir p f inum # s) = (type_of_obj s) ((O_dir f) :=
+ − 948
(case (parent f) of
+ − 949
Some pf \<Rightarrow> (case (type_of_obj s (O_proc p), type_of_obj s (O_dir pf)) of
+ − 950
(Some tp, Some tpf) \<Rightarrow> Some (type_transition tp tpf C_dir True)
+ − 951
| _ \<Rightarrow> None)
+ − 952
| _ \<Rightarrow> None) )"
+ − 953
| "type_of_obj (LinkHard p f f' # s) = (type_of_obj s) ((O_file f') :=
+ − 954
(case (parent f') of
+ − 955
Some pf \<Rightarrow> (case (type_of_obj s (O_proc p), type_of_obj s (O_dir pf)) of
+ − 956
(Some tp, Some tpf) \<Rightarrow> Some (type_transition tp tpf C_file True)
+ − 957
| _ \<Rightarrow> None)
+ − 958
| _ \<Rightarrow> None) )"
+ − 959
(*
+ − 960
| "type_of_obj (Rename p f f' # s) = (\<lambda> obj.
+ − 961
case obj of
+ − 962
O_file f'' \<Rightarrow> (if (f' \<preceq> f'') then type_of_obj s (O_file (file_before_rename f f' f''))
+ − 963
else type_of_obj s (O_file f''))
+ − 964
| O_dir f'' \<Rightarrow> (if (f' \<preceq> f'') then type_of_obj s (O_file (file_before_rename f f' f''))
+ − 965
else type_of_obj s (O_file f''))
+ − 966
| _ \<Rightarrow> type_of_obj s obj )"
+ − 967
*)
+ − 968
| "type_of_obj (CreateMsgq p q # s) = (type_of_obj s) ((O_msgq q) :=
+ − 969
(case (type_of_obj s (O_proc p)) of
+ − 970
Some tp \<Rightarrow> Some tp
+ − 971
| _ \<Rightarrow> None) )"
+ − 972
| "type_of_obj (SendMsg p q m # s) = (type_of_obj s) ((O_msg q m) :=
+ − 973
(case (type_of_obj s (O_proc p), type_of_obj s (O_msgq q)) of
+ − 974
(Some tp, Some tq) \<Rightarrow> Some (type_transition tp tq C_msg False)
+ − 975
| _ \<Rightarrow> None) )"
+ − 976
| "type_of_obj (CreateShM p h # s) = (type_of_obj s) ((O_shm h) :=
+ − 977
(case (type_of_obj s (O_proc p)) of
+ − 978
Some tp \<Rightarrow> Some tp
+ − 979
| _ \<Rightarrow> None) )"
+ − 980
| "type_of_obj (CreateSock p af st fd inum # s) = (\<lambda> obj.
+ − 981
case obj of
+ − 982
O_fd p' fd' \<Rightarrow> if (p' = p \<and> fd' = fd) then type_of_obj s (O_proc p)
+ − 983
else type_of_obj s obj
+ − 984
| O_tcp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = STREAM) then type_of_obj s (O_proc p)
+ − 985
else type_of_obj s obj
+ − 986
| O_udp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = DGRAM) then type_of_obj s (O_proc p)
+ − 987
else type_of_obj s obj
+ − 988
| _ \<Rightarrow> type_of_obj s obj )"
+ − 989
| "type_of_obj (Accept p fd addr port fd' inum # s) = (\<lambda> obj.
+ − 990
case obj of
+ − 991
O_fd p' fd'' \<Rightarrow> if (p' = p \<and> fd'' = fd') then type_of_obj s (O_proc p)
+ − 992
else type_of_obj s obj
+ − 993
| O_tcp_sock (p', fd'') \<Rightarrow> if (p' = p \<and> fd'' = fd') then type_of_obj s (O_proc p)
+ − 994
else type_of_obj s obj
+ − 995
| _ \<Rightarrow> type_of_obj s obj )"
+ − 996
| "type_of_obj (_ # s) = type_of_obj s"
+ − 997
+ − 998
fun role_of_proc :: "t_state \<Rightarrow> (t_process \<Rightarrow> role_t option)"
+ − 999
where
+ − 1000
"role_of_proc [] = init_role_of_proc"
+ − 1001
| "role_of_proc (Clone p p' fds shms # s) =
+ − 1002
(role_of_proc s) (p' := role_of_proc s p)"
+ − 1003
| "role_of_proc (Execve p f fds # s) = (role_of_proc s) (p :=
+ − 1004
(case (role_of_proc s p, type_of_obj s (O_file f)) of
+ − 1005
(Some r, Some ft) \<Rightarrow> role_transition r ft
+ − 1006
| _ \<Rightarrow> None) )"
+ − 1007
| "role_of_proc (_ # s) = role_of_proc s"
+ − 1008
+ − 1009
fun role_of_obj :: "t_state \<Rightarrow> t_object \<Rightarrow> role_t option"
+ − 1010
where
+ − 1011
"role_of_obj s (O_proc p) = role_of_proc s p"
+ − 1012
| "role_of_obj s _ = Some R_object" (* object_r *)
+ − 1013
+ − 1014
definition sectxt_of_obj :: "t_state \<Rightarrow> t_object \<Rightarrow> security_context_t option"
+ − 1015
where
+ − 1016
"sectxt_of_obj s obj = (
+ − 1017
case (user_of_obj s obj, role_of_obj s obj, type_of_obj s obj) of
+ − 1018
(Some u, Some r, Some t) \<Rightarrow> Some (u, r, t)
+ − 1019
| _ \<Rightarrow> None)"
+ − 1020
+ − 1021
(******* flask granting ********
+ − 1022
* involves three kinds of rules:
+ − 1023
* 1. allow rule of types, allowed_rule_list_t, main
+ − 1024
* 2. allow rule of roles, role_allow_rule_list_t, mainly for execve call
+ − 1025
* 3. constrains, section 3.4.5, user-specifically defined.
+ − 1026
* Passed all these 3, then grant Yes, else No
+ − 1027
*)
+ − 1028
+ − 1029
definition search_check_allp :: "security_context_t \<Rightarrow> security_context_t set \<Rightarrow> bool"
+ − 1030
where
+ − 1031
"search_check_allp pctxt sectxts = (\<forall> sec \<in> sectxts. permission_check pctxt sec C_dir P_search)"
+ − 1032
+ − 1033
definition search_check_file :: "security_context_t \<Rightarrow> security_context_t \<Rightarrow> bool"
+ − 1034
where
+ − 1035
"search_check_file sctxt fctxt \<equiv> permission_check sctxt fctxt C_file P_search"
+ − 1036
+ − 1037
definition search_check_dir :: "security_context_t \<Rightarrow> security_context_t \<Rightarrow> bool"
+ − 1038
where
+ − 1039
"search_check_dir sctxt fctxt \<equiv> permission_check sctxt fctxt C_dir P_search"
+ − 1040
+ − 1041
fun get_parentfs_ctxts :: "t_state \<Rightarrow> t_file \<Rightarrow> (security_context_t list) option"
+ − 1042
where
+ − 1043
"get_parentfs_ctxts s [] =
+ − 1044
(case (sectxt_of_obj s (O_dir [])) of
+ − 1045
Some ctxt \<Rightarrow> Some [ctxt]
+ − 1046
| _ \<Rightarrow> None)"
+ − 1047
| "get_parentfs_ctxts s (f#pf) =
+ − 1048
(case (get_parentfs_ctxts s pf, sectxt_of_obj s (O_dir (f#pf))) of
+ − 1049
(Some ctxts, Some ctxt) \<Rightarrow> Some (ctxt#ctxts)
+ − 1050
| _ \<Rightarrow> None)"
+ − 1051
+ − 1052
fun search_check :: "t_state \<Rightarrow> security_context_t \<Rightarrow> t_file \<Rightarrow> bool"
+ − 1053
where
+ − 1054
"search_check s pctxt [] =
+ − 1055
(case (sectxt_of_obj s (O_dir [])) of
+ − 1056
Some fctxt \<Rightarrow> search_check_dir pctxt fctxt
+ − 1057
| _ \<Rightarrow> False)"
+ − 1058
| "search_check s pctxt (f#pf) =
+ − 1059
(if (is_file s (f#pf))
+ − 1060
then (case (sectxt_of_obj s (O_file (f#pf)), get_parentfs_ctxts s pf) of
+ − 1061
(Some fctxt, Some pfctxts) \<Rightarrow> (search_check_file pctxt fctxt \<and> search_check_allp pctxt (set pfctxts))
+ − 1062
| _ \<Rightarrow> False)
+ − 1063
else (case (sectxt_of_obj s (O_dir (f#pf)), get_parentfs_ctxts s pf) of
+ − 1064
(Some fctxt, Some pfctxts) \<Rightarrow> (search_check_dir pctxt fctxt \<and> search_check_allp pctxt (set pfctxts))
+ − 1065
| _ \<Rightarrow> False))"
+ − 1066
+ − 1067
(* this means we should prove every current fd has a security context! *)
+ − 1068
definition sectxts_of_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set \<Rightarrow> security_context_t set"
+ − 1069
where
+ − 1070
"sectxts_of_fds s p fds \<equiv> {ctxt. \<exists> fd \<in> fds. sectxt_of_obj s (O_fd p fd) = Some ctxt}"
+ − 1071
+ − 1072
definition inherit_fds_check :: "t_state \<Rightarrow> security_context_t \<Rightarrow> t_process \<Rightarrow> t_fd set \<Rightarrow> bool"
+ − 1073
where
+ − 1074
"inherit_fds_check s npsectxt p fds \<equiv>
+ − 1075
(\<forall> ctxt \<in> sectxts_of_fds s p fds. permission_check npsectxt ctxt C_fd P_inherit)"
+ − 1076
+ − 1077
fun npctxt_execve :: "security_context_t \<Rightarrow> security_context_t \<Rightarrow> security_context_t option"
+ − 1078
where
+ − 1079
"npctxt_execve (pu,pr,pt) (fu,fr,ft) =
+ − 1080
(case (role_transition pr ft) of
+ − 1081
Some nr \<Rightarrow> Some (pu, nr, type_transition pt ft C_process False)
+ − 1082
| _ \<Rightarrow> None)"
+ − 1083
+ − 1084
fun nfctxt_create :: "security_context_t \<Rightarrow> security_context_t \<Rightarrow> security_class_t \<Rightarrow> security_context_t"
+ − 1085
where
+ − 1086
"nfctxt_create (pu,pr,pt) (fu,fr,ft) cls = (pu, R_object, type_transition pt ft cls True)"
+ − 1087
+ − 1088
fun grant_execve ::
+ − 1089
"security_context_t \<Rightarrow> security_context_t \<Rightarrow> security_context_t \<Rightarrow> bool"
+ − 1090
where
+ − 1091
"grant_execve (up,rp,tp) (uf,rf,tf) (up',nr,nt) =
+ − 1092
(role_decl_check nr nt \<and> role_allow rp nr \<and>
+ − 1093
permission_check (up,rp,tp) (uf,rf,tf) C_file P_execute \<and>
+ − 1094
permission_check (up,nr,nt) (uf,rf,tf) C_file P_entrypoint \<and>
+ − 1095
permission_check (up,rp,tp) (up,nr,nt) C_process P_transition \<and>
+ − 1096
permission_check (up,nr,nt) (uf,rf,tf) C_process P_execute)"
+ − 1097
+ − 1098
definition sectxts_of_shms :: "t_state \<Rightarrow> t_shm set \<Rightarrow> security_context_t set"
+ − 1099
where
+ − 1100
"sectxts_of_shms s shms \<equiv> {ctxt. \<exists> h \<in> shms. sectxt_of_obj s (O_shm h) = Some ctxt}"
+ − 1101
+ − 1102
definition inherit_shms_check :: "t_state \<Rightarrow> security_context_t \<Rightarrow> t_shm set \<Rightarrow> bool"
+ − 1103
where
+ − 1104
"inherit_shms_check s npsectxt shms \<equiv>
+ − 1105
(\<forall> ctxt \<in> sectxts_of_shms s shms. permission_check npsectxt ctxt C_shm P_inherit)"
+ − 1106
+ − 1107
fun perm_of_mflag :: "t_open_must_flag \<Rightarrow> permission_t set"
+ − 1108
where
+ − 1109
"perm_of_mflag OF_RDONLY = {P_read}"
+ − 1110
| "perm_of_mflag OF_WRONLY = {P_write}"
+ − 1111
| "perm_of_mflag OF_RDWR = {P_read, P_write}"
+ − 1112
+ − 1113
definition perm_of_oflag :: "t_open_option_flag set \<Rightarrow> permission_t set"
+ − 1114
where
+ − 1115
"perm_of_oflag oflags \<equiv>
+ − 1116
(case (OF_APPEND \<in> oflags, OF_CREAT \<in> oflags) of
+ − 1117
(True, True) \<Rightarrow> {P_append, P_create}
+ − 1118
| (True, _ ) \<Rightarrow> {P_append}
+ − 1119
| (_ , True) \<Rightarrow> {P_create}
+ − 1120
| _ \<Rightarrow> {})"
+ − 1121
+ − 1122
definition perms_of_flags :: "t_open_flags \<Rightarrow> permission_t set"
+ − 1123
where
+ − 1124
"perms_of_flags flags \<equiv>
+ − 1125
(case flags of
+ − 1126
(mflag,oflags) \<Rightarrow> (perm_of_mflag mflag \<union> perm_of_oflag oflags))"
+ − 1127
+ − 1128
(*
+ − 1129
definition class_of_flags :: "t_open_flags \<Rightarrow> security_class_t"
+ − 1130
where
+ − 1131
"class_of_flags flags \<equiv>
+ − 1132
(case flags of
+ − 1133
(mflag, oflags) \<Rightarrow> if (OF_DIRECTORY \<in> oflags) then C_dir else C_file)"
+ − 1134
+ − 1135
definition obj_of_flags :: "t_open_flags \<Rightarrow> t_file \<Rightarrow> t_object"
+ − 1136
where
+ − 1137
"obj_of_flags flags f \<equiv>
+ − 1138
(case flags of
+ − 1139
(mflag, oflags) \<Rightarrow> if (OF_DIRECTORY \<in> oflags) then O_dir f else O_file f)"
+ − 1140
*)
+ − 1141
+ − 1142
definition oflags_check :: "t_open_flags \<Rightarrow> security_context_t \<Rightarrow> security_context_t \<Rightarrow> bool"
+ − 1143
where
+ − 1144
"oflags_check flags pctxt fctxt \<equiv>
+ − 1145
\<forall> perm \<in> (perms_of_flags flags). permission_check pctxt fctxt C_file perm"
+ − 1146
+ − 1147
fun grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool"
+ − 1148
where
+ − 1149
"grant s (Execve p f fds) =
+ − 1150
(case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_file f)) of
+ − 1151
(Some (up, rp, tp), Some (uf, rf, tf)) \<Rightarrow>
+ − 1152
(case (npctxt_execve (up,rp,tp) (uf,rf,tf)) of
+ − 1153
Some (pu,nr,nt) \<Rightarrow> (
+ − 1154
search_check s (up,rp,tp) f \<and>
+ − 1155
grant_execve (up,rp,tp) (uf,rf,tf) (up,nr,nt) \<and>
+ − 1156
inherit_fds_check s (up,nr,nt) p fds)
+ − 1157
| _ \<Rightarrow> False)
+ − 1158
| _ \<Rightarrow> False )"
+ − 1159
| "grant s (Clone p p' fds shms) =
+ − 1160
(case (sectxt_of_obj s (O_proc p)) of
+ − 1161
Some (up, rp, tp) \<Rightarrow>
+ − 1162
(permission_check (up,rp,tp) (up,rp,tp) C_process P_fork \<and>
+ − 1163
inherit_fds_check s (up,rp,tp) p fds \<and>
+ − 1164
inherit_shms_check s (up,rp,tp) shms)
+ − 1165
| _ \<Rightarrow> False )"
+ − 1166
| "grant s (Kill p p') =
+ − 1167
(case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_proc p')) of
+ − 1168
(Some (su,sr,st), Some (tu,tr,tt)) \<Rightarrow>
+ − 1169
permission_check (su,sr,st) (tu,tr,tt) C_process P_sigkill
+ − 1170
| _ \<Rightarrow> False)"
+ − 1171
| "grant s (Ptrace p p') =
+ − 1172
(case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_proc p')) of
+ − 1173
(Some (su,sr,st), Some (tu,tr,tt)) \<Rightarrow>
+ − 1174
permission_check (su,sr,st) (tu,tr,tt) C_process P_ptrace
+ − 1175
| _ \<Rightarrow> False)"
+ − 1176
| "grant s (Exit p) = True"
+ − 1177
| "grant s (Open p f flags fd None) =
+ − 1178
(case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_file f)) of
+ − 1179
(Some (pu,pr,pt), Some (fu,fr,ft)) \<Rightarrow>
+ − 1180
search_check s (pu,pr,pt) f \<and>
+ − 1181
oflags_check flags (pu,pr,pt) (fu,fr,ft) \<and>
+ − 1182
permission_check (pu,pr,pt) (pu,pr,pt) C_fd P_setattr
+ − 1183
| _ \<Rightarrow>False)"
+ − 1184
| "grant s (Open p f flags fd (Some inum)) =
+ − 1185
(case (parent f) of
+ − 1186
Some pf \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of
+ − 1187
(Some (pu,pr,pt), Some (pfu,pfr,pft)) \<Rightarrow>
+ − 1188
(search_check s (pu,pr,pt) pf \<and>
+ − 1189
oflags_check flags (pu,pr,pt) (nfctxt_create (pu,pr,pt) (pfu,pfr,pft) C_file) \<and>
+ − 1190
permission_check (pu,pr,pt) (pfu,pfr,pft) C_dir P_add_name \<and>
+ − 1191
permission_check (pu,pr,pt) (pu,pr,pt) C_fd P_setattr)
+ − 1192
| _ \<Rightarrow> False)
+ − 1193
| _ \<Rightarrow> False)"
+ − 1194
| "grant s (ReadFile p fd) =
+ − 1195
(case (file_of_proc_fd s p fd) of
+ − 1196
Some f \<Rightarrow>
+ − 1197
(case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_fd p fd),
+ − 1198
sectxt_of_obj s (O_file f)) of
+ − 1199
(Some (pu,pr,pt), Some (fdu,fdr,fdt), Some (fu,fr,ft)) \<Rightarrow>
+ − 1200
(permission_check (pu,pr,pt) (fdu,fdr,fdt) C_fd P_setattr \<and>
+ − 1201
permission_check (pu,pr,pt) (fu,fr,ft) C_file P_read)
+ − 1202
| _ \<Rightarrow> False)
+ − 1203
| _ \<Rightarrow> False)"
+ − 1204
| "grant s (WriteFile p fd) =
+ − 1205
(case (file_of_proc_fd s p fd) of
+ − 1206
Some f \<Rightarrow>
+ − 1207
(case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_fd p fd),
+ − 1208
sectxt_of_obj s (O_file f)) of
+ − 1209
(Some (pu,pr,pt), Some (fdu,fdr,fdt), Some (fu,fr,ft)) \<Rightarrow>
+ − 1210
(permission_check (pu,pr,pt) (fdu,fdr,fdt) C_fd P_setattr \<and>
+ − 1211
permission_check (pu,pr,pt) (fu,fr,ft) C_file P_write)
+ − 1212
| _ \<Rightarrow> False)
+ − 1213
| _ \<Rightarrow> False)"
+ − 1214
| "grant s (CloseFd p fd) = True"
+ − 1215
| "grant s (UnLink p f) =
+ − 1216
(case (parent f) of
+ − 1217
Some pf \<Rightarrow>
+ − 1218
(case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf),
+ − 1219
sectxt_of_obj s (O_file f)) of
+ − 1220
(Some (pu,pr,pt), Some (du,dr,dt), Some (fu,fr,ft)) \<Rightarrow>
+ − 1221
(search_check s (pu,pr,pt) f \<and>
+ − 1222
permission_check (pu,pr,pt) (fu,fr,ft) C_file P_unlink \<and>
+ − 1223
permission_check (pu,pr,pt) (du,dr,dt) C_dir P_remove_name)
+ − 1224
| _ \<Rightarrow> False)
+ − 1225
| _ \<Rightarrow> False)"
+ − 1226
| "grant s (Rmdir p f) =
+ − 1227
(case (parent f) of
+ − 1228
Some pf \<Rightarrow>
+ − 1229
(case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf),
+ − 1230
sectxt_of_obj s (O_dir f)) of
+ − 1231
(Some (pu,pr,pt), Some (du,dr,dt), Some (fu,fr,ft)) \<Rightarrow>
+ − 1232
(search_check s (pu,pr,pt) f \<and>
+ − 1233
permission_check (pu,pr,pt) (fu,fr,ft) C_dir P_rmdir \<and>
+ − 1234
permission_check (pu,pr,pt) (du,dr,dt) C_dir P_remove_name)
+ − 1235
| _ \<Rightarrow> False)
+ − 1236
| _ \<Rightarrow> False)"
+ − 1237
| "grant s (Mkdir p f inum) =
+ − 1238
(case (parent f) of
+ − 1239
Some pf \<Rightarrow>
+ − 1240
(case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of
+ − 1241
(Some (pu,pr,pt), Some (du,dr,dt)) \<Rightarrow>
+ − 1242
(search_check s (pu,pr,pt) f \<and>
+ − 1243
permission_check (pu,pr,pt) (nfctxt_create (pu,pr,pt) (du,dr,dt) C_dir) C_dir P_create \<and>
+ − 1244
permission_check (pu,pr,pt) (du,dr,dt) C_dir P_add_name)
+ − 1245
| _ \<Rightarrow> False)
+ − 1246
| _ \<Rightarrow> False)"
+ − 1247
| "grant s (LinkHard p f f') =
+ − 1248
(case (parent f') of
+ − 1249
Some pf \<Rightarrow>
+ − 1250
(case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf),
+ − 1251
sectxt_of_obj s (O_file f)) of
+ − 1252
(Some (pu,pr,pt), Some (du,dr,dt), Some (fu,fr,ft)) \<Rightarrow>
+ − 1253
(search_check s (pu,pr,pt) f \<and> search_check s (pu,pr,pt) pf \<and>
+ − 1254
permission_check (pu,pr,pt) (fu,fr,ft) C_file P_link \<and>
+ − 1255
permission_check (pu,pr,pt) (du,dr,dt) C_dir P_add_name)
+ − 1256
| _ \<Rightarrow> False)
+ − 1257
| _ \<Rightarrow> False)"
+ − 1258
| "grant s (Truncate p f len) =
+ − 1259
(case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_file f)) of
+ − 1260
(Some (pu,pr,pt), Some (fu,fr,ft)) \<Rightarrow>
+ − 1261
(search_check s (pu,pr,pt) f \<and>
+ − 1262
permission_check (pu,pr,pt) (fu,fr,ft) C_file P_setattr)
+ − 1263
| _ \<Rightarrow> False)"
+ − 1264
(*
+ − 1265
| "grant s (Rename p f f') =
+ − 1266
(case (parent f, parent f') of
+ − 1267
(Some pf, Some pf') \<Rightarrow>
+ − 1268
(case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf),
+ − 1269
sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf')) of
+ − 1270
(Some (pu,pr,pt), Some (pfu,pfr,pft), Some (fu,fr,ft),
+ − 1271
Some (pfu',pfr',pft')) \<Rightarrow>
+ − 1272
(search_check s (pu,pr,pt) f \<and>
+ − 1273
permission_check (pu,pr,pt) (pfu,pfr,pft) C_dir P_remove_name \<and>
+ − 1274
(if (is_file s f)
+ − 1275
then permission_check (pu,pr,pt) (fu,fr,ft) C_file P_rename
+ − 1276
else permission_check (pu,pr,pt) (fu,fr,ft) C_dir P_reparent) \<and>
+ − 1277
search_check s (pu,pr,pt) pf' \<and>
+ − 1278
permission_check (pu,pr,pt) (pfu',pfr',pft') C_dir P_add_name)
+ − 1279
| _ \<Rightarrow> False)
+ − 1280
| _ \<Rightarrow> False)"
+ − 1281
*)
+ − 1282
| "grant s (CreateMsgq p q) =
+ − 1283
(case (sectxt_of_obj s (O_proc p)) of
+ − 1284
Some (pu,pr,pt) \<Rightarrow>
+ − 1285
(permission_check (pu,pr,pt) (pu,pr,pt) C_msgq P_associate \<and>
+ − 1286
permission_check (pu,pr,pt) (pu,pr,pt) C_msgq P_create)
+ − 1287
| _ \<Rightarrow> False)"
+ − 1288
| "grant s (SendMsg p q m) =
+ − 1289
(case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_msgq q)) of
+ − 1290
(Some (pu,pr,pt), Some (qu,qr,qt)) \<Rightarrow>
+ − 1291
(permission_check (pu,pr,pt) (qu,qr,qt) C_msgq P_enqueue \<and>
+ − 1292
permission_check (pu,pr,pt) (qu,qr,qt) C_msgq P_write \<and>
+ − 1293
permission_check (pu,pr,pt) (pu,pr,pt) C_msg P_send)
+ − 1294
| _ \<Rightarrow> False)"
+ − 1295
| "grant s (RecvMsg p q m) =
+ − 1296
(case (sectxt_of_obj s (O_proc p),sectxt_of_obj s (O_msgq q),sectxt_of_obj s (O_msg q m)) of
+ − 1297
(Some (pu,pr,pt), Some (qu,qr,qt), Some (mu,mr,mt)) \<Rightarrow>
+ − 1298
permission_check (pu,pr,pt) (qu,qr,qt) C_msgq P_read \<and>
+ − 1299
permission_check (pu,pr,pt) (mu,mr,mt) C_msg P_receive
+ − 1300
| _ \<Rightarrow> False)"
+ − 1301
| "grant s (RemoveMsgq p q) =
+ − 1302
(case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_msgq q)) of
+ − 1303
(Some (pu,pr,pt), Some (qu,qr,qt)) \<Rightarrow>
+ − 1304
permission_check (pu,pr,pt) (qu,qr,qt) C_msgq P_destroy
+ − 1305
| _ \<Rightarrow> False)"
+ − 1306
| "grant s (CreateShM p h) =
+ − 1307
(case (sectxt_of_obj s (O_proc p)) of
+ − 1308
Some (pu,pr,pt) \<Rightarrow>
+ − 1309
(permission_check (pu,pr,pt) (pu,pr,pt) C_shm P_associate \<and>
+ − 1310
permission_check (pu,pr,pt) (pu,pr,pt) C_shm P_create)
+ − 1311
| _ \<Rightarrow> False)"
+ − 1312
| "grant s (Attach p h flag) =
+ − 1313
(case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_shm h)) of
+ − 1314
(Some (pu,pr,pt), Some (hu,hr,ht)) \<Rightarrow>
+ − 1315
if flag = SHM_RDONLY
+ − 1316
then permission_check (pu,pr,pt) (hu,hr,ht) C_shm P_read
+ − 1317
else permission_check (pu,pr,pt) (hu,hr,ht) C_shm P_read \<and>
+ − 1318
permission_check (pu,pr,pt) (hu,hr,ht) C_shm P_write
+ − 1319
| _ \<Rightarrow> False)"
+ − 1320
| "grant s (Detach p h) = True" (*?*)
+ − 1321
| "grant s (DeleteShM p h) =
+ − 1322
(case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_shm h)) of
+ − 1323
(Some (pu,pr,pt), Some (hu,hr,ht)) \<Rightarrow>
+ − 1324
permission_check (pu,pr,pt) (hu,hr,ht) C_shm P_destroy
+ − 1325
| _ \<Rightarrow> False)"
+ − 1326
+ − 1327
+ − 1328
| "grant s _ = False" (* socket event is currently not in consideration *)
+ − 1329
+ − 1330
inductive valid :: "t_state \<Rightarrow> bool"
+ − 1331
where
+ − 1332
"valid []"
+ − 1333
| "\<lbrakk>valid s; os_grant s e; grant s e\<rbrakk> \<Longrightarrow> valid (e # s)"
+ − 1334
+ − 1335
(* tobj: object that can be tainted *)
+ − 1336
fun tobj_in_init :: "t_object \<Rightarrow> bool"
+ − 1337
where
+ − 1338
"tobj_in_init (O_proc p) = (p \<in> init_procs)"
+ − 1339
| "tobj_in_init (O_file f) = (f \<in> init_files)"
+ − 1340
(* directory is not taintable
+ − 1341
| "tobj_in_init (O_dir f) = (f \<in> init_files)"
+ − 1342
*)
+ − 1343
| "tobj_in_init (O_node n) = (n \<in> init_nodes)"
+ − 1344
| "tobj_in_init (O_msg q m) = (member (init_msgs_of_queue q) ((op =) m))"
+ − 1345
| "tobj_in_init _ = False" (* other kind of obj cannot be tainted *)
+ − 1346
+ − 1347
(* no use
+ − 1348
fun no_del_event:: "t_event list \<Rightarrow> bool"
+ − 1349
where
+ − 1350
"no_del_event [] = True"
+ − 1351
| "no_del_event (Kill p p' # \<tau>) = False"
+ − 1352
| "no_del_event (CloseFd p fd # \<tau>) = False"
+ − 1353
| "no_del_event (UnLink p f # \<tau>) = False"
+ − 1354
| "no_del_event (Rmdir p f # \<tau>) = False"
+ − 1355
(*
+ − 1356
| "no_del_event (Rename p f f' # \<tau>) = False"
+ − 1357
*)
+ − 1358
| "no_del_event (RemoveMsgq p q # \<tau>) = False"
+ − 1359
| "no_del_event (RecvMsg p q m # \<tau>) = False"
+ − 1360
| "no_del_event (_ # \<tau>) = no_del_event \<tau>"
+ − 1361
*)
+ − 1362
+ − 1363
end
+ − 1364
+ − 1365
locale tainting = flask +
+ − 1366
+ − 1367
fixes seeds :: "t_object set"
+ − 1368
assumes
+ − 1369
seeds_in_init: "\<And> obj. obj \<in> seeds \<Longrightarrow> tobj_in_init obj"
+ − 1370
+ − 1371
begin
+ − 1372
+ − 1373
inductive tainted :: "t_object \<Rightarrow> t_state \<Rightarrow> bool" ("_ \<in> tainted _" [100, 100] 100)
+ − 1374
where
+ − 1375
t_init: "obj \<in> seeds \<Longrightarrow> obj \<in> tainted []"
+ − 1376
| t_clone: "\<lbrakk>O_proc p \<in> tainted s; valid (Clone p p' fds shms # s)\<rbrakk>
+ − 1377
\<Longrightarrow> O_proc p' \<in> tainted (Clone p p' fds shms # s)"
+ − 1378
| t_execve: "\<lbrakk>O_file f \<in> tainted s; valid (Execve p f fds # s)\<rbrakk>
+ − 1379
\<Longrightarrow> O_proc p \<in> tainted (Execve p f fds # s)"
+ − 1380
| t_ptrace: "\<lbrakk>O_proc p \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p' p''\<rbrakk>
+ − 1381
\<Longrightarrow> O_proc p'' \<in> tainted (Ptrace p p' # s)"
+ − 1382
| t_ptrace':"\<lbrakk>O_proc p' \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p p''\<rbrakk>
+ − 1383
\<Longrightarrow> O_proc p'' \<in> tainted (Ptrace p p' # s)"
+ − 1384
| t_cfile: "\<lbrakk>O_proc p \<in> tainted s; valid (Open p f flags fd (Some inum) # s)\<rbrakk>
+ − 1385
\<Longrightarrow> O_file f \<in> tainted (Open p f flags fd (Some inum) # s)"
+ − 1386
| t_read: "\<lbrakk>O_file f \<in> tainted s; valid (ReadFile p fd # s);
+ − 1387
file_of_proc_fd s p fd = Some f; info_flow_shm s p p'\<rbrakk>
+ − 1388
\<Longrightarrow> O_proc p' \<in> tainted (ReadFile p fd # s)"
+ − 1389
| t_write: "\<lbrakk>O_proc p \<in> tainted s; valid (WriteFile p fd # s);
+ − 1390
file_of_proc_fd s p fd = Some f; has_same_inode s f f'\<rbrakk>
+ − 1391
\<Longrightarrow> O_file f' \<in> tainted (WriteFile p fd # s)"
+ − 1392
(* directory is not tainted
+ − 1393
| t_mkdir: "\<lbrakk>O_proc p \<in> tainted s; valid (Mkdir p f inum # s)\<rbrakk>
+ − 1394
\<Longrightarrow> O_dir f \<in> tainted (Mkdir p f inum # s)"
+ − 1395
*)
+ − 1396
| t_link: "\<lbrakk>O_file f \<in> tainted s; valid (LinkHard p f f' # s)\<rbrakk>
+ − 1397
\<Longrightarrow> O_file f' \<in> tainted (LinkHard p f f' # s)"
+ − 1398
| t_trunc: "\<lbrakk>O_proc p \<in> tainted s; valid (Truncate p f len # s); len > 0; has_same_inode s f f'\<rbrakk>
+ − 1399
\<Longrightarrow> O_file f' \<in> tainted (Truncate p f len # s)"
+ − 1400
(*
+ − 1401
| t_rename: "\<lbrakk>O_file f'' \<in> tainted s; valid (Rename p f f' # s);f \<preceq> f''\<rbrakk>
+ − 1402
\<Longrightarrow> O_file (file_after_rename f f' f'') \<in> tainted (Rename p f f' # s)"
+ − 1403
| t_rename':"\<lbrakk>O_dir f'' \<in> tainted s; valid (Rename p f f' # s);f \<preceq> f''\<rbrakk>
+ − 1404
\<Longrightarrow> O_dir (file_after_rename f f' f'') \<in> tainted (Rename p f f' # s)"
+ − 1405
*)
+ − 1406
| t_sendmsg:"\<lbrakk>O_proc p \<in> tainted s; valid (SendMsg p q m # s)\<rbrakk>
+ − 1407
\<Longrightarrow> O_msg q m \<in> tainted (SendMsg p q m # s)"
+ − 1408
| t_recvmsg:"\<lbrakk>O_msg q m \<in> tainted s; valid (RecvMsg p q m # s); info_flow_shm s p p'\<rbrakk>
+ − 1409
\<Longrightarrow> O_proc p' \<in> tainted (RecvMsg p q m # s)"
+ − 1410
| t_remain: "\<lbrakk>obj \<in> tainted s; valid (e # s); alive (e # s) obj\<rbrakk>
+ − 1411
\<Longrightarrow> obj \<in> tainted (e # s)"
+ − 1412
+ − 1413
definition taintable:: "t_object \<Rightarrow> bool"
+ − 1414
where
+ − 1415
"taintable obj \<equiv> init_alive obj \<and> (\<exists> s. obj \<in> tainted s)"
+ − 1416
+ − 1417
definition undeletable :: "t_object \<Rightarrow> bool"
+ − 1418
where
+ − 1419
"undeletable obj \<equiv> init_alive obj \<and> \<not> (\<exists> s. valid s \<and> deleted obj s)"
+ − 1420
+ − 1421
end
+ − 1422
+ − 1423
end