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