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