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' = 

   545      (if (p = p' \<and> fd = fd') then Some flags else flags_of_proc_fd \<tau> p' fd')"

   546 | "flags_of_proc_fd (CloseFd p fd # \<tau>) p' fd' = 

   547      (if (p = p' \<and> fd = fd') then None else flags_of_proc_fd \<tau> p' fd')"

   548 | "flags_of_proc_fd (CreateSock p af st fd ino # \<tau>) p' fd' = 

   549      (if (p = p' \<and> fd = fd') then None else flags_of_proc_fd \<tau> p' fd')"

   550 | "flags_of_proc_fd (Accept p fd addr lport' fd' ino # \<tau>) p' fd'' = 

   551      (if (p = p' \<and> fd' = fd'') then None else flags_of_proc_fd \<tau> p' fd'')"

   552 | "flags_of_proc_fd (Clone p p' fds # \<tau>) p'' fd = 

   553      (if (p' = p'' \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd else flags_of_proc_fd \<tau> p'' fd)"  

   554 | "flags_of_proc_fd (Execve p f fds # \<tau>) p' fd = 

   555      (if (p' = p \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd else flags_of_proc_fd \<tau> p' fd)"

   556 | "flags_of_proc_fd (Kill p\<^isub>1 p\<^isub>2 # \<tau>) p fd = 

   557      (if (p = p\<^isub>2) then None else flags_of_proc_fd \<tau> p fd)"

   558 | "flags_of_proc_fd (Exit p # \<tau>) p' fd' = 

   559      (if (p = p') then None else flags_of_proc_fd \<tau> p' fd')"

   560 | "flags_of_proc_fd (e # \<tau>) p fd = flags_of_proc_fd \<tau> p fd" 

   561 

   562 (* 

   563 fun file_at_writing_by:: "t_state \<Rightarrow> t_file \<Rightarrow> (t_process \<times> t_fd) set"

   564 where

   565   "file_at_writing_by [] f = init_file_at_writing_by f"  

   566 | "file_at_writing_by (Open p f flags fd (Some inum) # \<tau>) f' = (

   567      if (f' = f) 

   568      then ( if (is_write_flag flags) 

   569             then {(p, fd)}

   570             else {} )

   571      else file_at_writing_by \<tau> f'                              )"

   572 | "file_at_writing_by (Open p f flags fd None # \<tau>) f' = (

   573      if (f' = f \<and> is_write_flag flags) 

   574      then insert (p, fd) (file_at_writing_by \<tau> f) 

   575      else file_at_writing_by \<tau> f'                       )"

   576 | "file_at_writing_by (Mkdir p f inum # \<tau>) f' = 

   577      (if (f' = f) then {} else file_at_writing_by \<tau> f')"

   578 | "file_at_writing_by (LinkHard p f f' # \<tau>) f'' = 

   579      (if (f'' = f') then file_at_writing_by \<tau> f else file_at_writing_by \<tau> f'')"

   580 | "file_at_writing_by (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = (

   581      if (f\<^isub>3 \<preceq> f) then file_at_writing_by \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f)

   582      else file_at_writing_by \<tau> f               )"

   583 | "file_at_writing_by (CloseFd p fd # \<tau>) f = 

   584      (file_at_writing_by \<tau> f - {(p, fd)})"

   585 | "file_at_writing_by (Clone p p' fds shms # \<tau>) f = 

   586      (file_at_writing_by \<tau> f) \<union> {(p',fd)| fd. fd \<in> fds \<and> (p, fd) \<in> file_at_writing_by \<tau> f}"

   587 | "file_at_writing_by (Execve p f fds # \<tau>) f' = 

   588      (if (f' = f) then {} else file_at_writing_by \<tau> f')"

   589 | "file_at_writing_by (Exit p # \<tau>) f = 

   590      (file_at_writing_by \<tau> f - {(p, fd)| fd. (p, fd) \<in> file_at_writing_by \<tau> f})"

   591 | "file_at_writing_by (Kill p p' # \<tau>) f = 

   592      (file_at_writing_by \<tau> f - {(p', fd)| fd. (p', fd) \<in> file_at_writing_by \<tau> f})"

   593 | "file_at_writing_by (e # \<tau>) f            =  file_at_writing_by \<tau> f"

   594 *)

   595 

   596 definition current_users :: "t_state \<Rightarrow> user_t set"

   597 where

   598   "current_users \<tau> \<equiv> init_users"  

   599 

   600 fun update_with_shuthow :: "t_sock_state option \<Rightarrow> t_shutdown_how \<Rightarrow> t_sock_state option"

   601 where

   602   "update_with_shuthow (Some (SS_trans Trans_Recv)) SHUT_RD = Some (SS_trans Trans_No)"

   603 | "update_with_shuthow (Some (SS_trans Trans_RS))   SHUT_RD = Some (SS_trans Trans_Send)"

   604 | "update_with_shuthow (Some (SS_trans Trans_Send)) SHUT_RD = Some (SS_trans Trans_Send)"

   605 | "update_with_shuthow (Some (SS_trans Trans_No))   SHUT_RD = Some (SS_trans Trans_No)"

   606 | "update_with_shuthow (Some (SS_trans Trans_Recv)) SHUT_WR = Some (SS_trans Trans_Recv)"

   607 | "update_with_shuthow (Some (SS_trans Trans_RS))   SHUT_WR = Some (SS_trans Trans_Recv)"

   608 | "update_with_shuthow (Some (SS_trans Trans_Send)) SHUT_WR = Some (SS_trans Trans_No)"

   609 | "update_with_shuthow (Some (SS_trans Trans_No))   SHUT_WR = Some (SS_trans Trans_No)"

   610 | "update_with_shuthow (Some (SS_trans Trans_Recv)) SHUT_RDWR = Some (SS_trans Trans_No)"

   611 | "update_with_shuthow (Some (SS_trans Trans_RS))   SHUT_RDWR = Some (SS_trans Trans_No)"

   612 | "update_with_shuthow (Some (SS_trans Trans_Send)) SHUT_RDWR = Some (SS_trans Trans_No)"

   613 | "update_with_shuthow (Some (SS_trans Trans_No))   SHUT_RDWR = Some (SS_trans Trans_No)"

   614 | "update_with_shuthow opt1                         how       = None" 

   615 

   616 fun socket_state :: "t_state \<Rightarrow> t_socket \<Rightarrow> t_sock_state option"

   617 where

   618   "socket_state [] = init_socket_state"

   619 | "socket_state (CloseFd p fd # \<tau>) = 

   620      (socket_state \<tau>) ((p, fd):= None)"

   621 | "socket_state (CreateSock p af st fd ino # \<tau>) = 

   622      (socket_state \<tau>) ((p, fd) := Some SS_create)"

   623 | "socket_state (Bind p fd addr # \<tau>) = 

   624      (socket_state \<tau>) ((p, fd) := Some SS_bind)"

   625 | "socket_state (Connect p fd addr # \<tau>) = 

   626      (socket_state \<tau>) ((p, fd) := Some (SS_trans Trans_RS))"

   627 | "socket_state (Listen p fd # \<tau>) = 

   628      (socket_state \<tau>) ((p, fd) := Some SS_listen)"

   629 | "socket_state (Accept p fd addr lport' fd' ino # \<tau>) = 

   630      (socket_state \<tau>) ((p, fd') := Some (SS_trans Trans_RS))"

   631 | "socket_state (Shutdown p fd sh # \<tau>) = 

   632      (socket_state \<tau>) ((p, fd) := update_with_shuthow (socket_state \<tau> (p, fd)) sh)"

   633 | "socket_state (Clone p p' fds # \<tau>) = 

   634      (\<lambda> (p'', fd). if (p'' = p' \<and> fd \<in> fds) then socket_state \<tau> (p, fd) 

   635                    else if (p'' = p') then None

   636                    else socket_state \<tau> (p'', fd))" 

   637 | "socket_state (Execve p f fds # \<tau>) = 

   638      (\<lambda> (p', fd). if (p' = p \<and> fd \<in> fds) then socket_state \<tau> (p, fd) 

   639                   else if (p' = p) then None 

   640                   else socket_state \<tau> (p', fd))" 

   641 | "socket_state (Kill p\<^isub>1 p\<^isub>2 # \<tau>) = 

   642      (\<lambda> (p, fd). if (p = p\<^isub>2) then None else socket_state \<tau> (p, fd))"

   643 | "socket_state (Exit p # \<tau>) = 

   644      (\<lambda> (p', fd'). if (p = p') then None else socket_state \<tau> (p', fd'))"

   645 | "socket_state (e # \<tau>) = socket_state \<tau>"  

   646 

   647 definition socket_in_trans :: "t_state \<Rightarrow> t_socket \<Rightarrow> bool"

   648 where

   649   "socket_in_trans \<tau> s \<equiv> (case (socket_state \<tau> s) of

   650                             Some st \<Rightarrow> (case st of 

   651                                           SS_trans para \<Rightarrow> True

   652                                         | _             \<Rightarrow> False)

   653                           | _       \<Rightarrow> False)"

   654 

   655 definition socket_in_sending :: "t_state \<Rightarrow> t_socket \<Rightarrow> bool"

   656 where

   657   "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))"

   658 

   659 definition socket_in_recving :: "t_state \<Rightarrow> t_socket \<Rightarrow> bool"

   660 where

   661   "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))"

   662 

   663 

   664 (******* admissable check by the OS *******)

   665 fun os_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool"

   666 where

   667   "os_grant \<tau> (Open p f flags fd inumopt) = (

   668      case inumopt of

   669        Some ino \<Rightarrow>

   670     (p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and> 

   671      (\<exists> pf. parent f = Some pf \<and> is_dir \<tau> pf \<and> pf \<notin> files_hung_by_del \<tau>) \<and>

   672      is_creat_flag flags \<and> fd \<notin> (current_proc_fds \<tau> p) \<and> ino \<notin> (current_inode_nums \<tau>))

   673    |   None     \<Rightarrow>

   674     (p \<in> current_procs \<tau> \<and> \<not> is_creat_excl_flag flags \<and> is_file \<tau> f \<and>

   675      fd \<notin> (current_proc_fds \<tau> p))           )"

   676 (*(if (is_dir \<tau> f) then (is_dir_flag flags \<and> \<not> is_write_flag flags) else (\<not> is_dir_flag flags)),

   677   here open is not applied to directories, readdir is for that, but it is not security-related *)

   678 | "os_grant \<tau> (CloseFd p fd)                  = 

   679     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p)"

   680 | "os_grant \<tau> (UnLink p f)                    = 

   681     (p \<in> current_procs \<tau> \<and> is_file \<tau> f \<and> f \<notin> files_hung_by_del \<tau>)"

   682 | "os_grant \<tau> (Rmdir p f)                     = 

   683     (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 *)

   684 | "os_grant \<tau> (Mkdir p f ino)                 = 

   685     (p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and> 

   686      (\<exists> pf. parent f = Some pf \<and> is_dir \<tau> pf \<and> pf \<notin> files_hung_by_del \<tau>) \<and>

   687      ino \<notin> (current_inode_nums \<tau>))"

   688 | "os_grant \<tau> (LinkHard p f\<^isub>1 f\<^isub>2)              = 

   689     (p \<in> current_procs \<tau> \<and> is_file \<tau> f\<^isub>1 \<and> f\<^isub>2 \<notin> current_files \<tau> \<and> 

   690      (\<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>))"

   691 | "os_grant \<tau> (Truncate p f len)              = 

   692     (p \<in> current_procs \<tau> \<and> is_file \<tau> f)"

   693 (*

   694 | "os_grant \<tau> (FTruncate p fd len)            = 

   695     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> 

   696      (\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau> \<and> is_file \<tau> f) \<and> 

   697      (\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_write_flag flags))"

   698 *)

   699 | "os_grant \<tau> (ReadFile p fd)                 = 

   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> 

   702      (\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_read_flag flags))"

   703 | "os_grant \<tau> (WriteFile p fd)                = 

   704     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> 

   705      (\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau>) \<and> 

   706      (\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_write_flag flags))" 

   707 | "os_grant \<tau> (Execve p f fds)                = 

   708     (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 *)

   709 (*

   710 | "os_grant \<tau> (Rename p f\<^isub>2 f\<^isub>3)                = 

   711     (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>

   712      (\<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> 

   713              pf\<^isub>3 \<notin> files_hung_by_del \<tau>) )"

   714 *)

   715 | "os_grant \<tau> (CreateMsgq p q)                = 

   716     (p \<in> current_procs \<tau> \<and> q \<notin> (current_msgqs \<tau>))"

   717 | "os_grant \<tau> (SendMsg p q m)                 = 

   718     (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m \<notin> (set (msgs_of_queue \<tau> q)))"

   719 | "os_grant \<tau> (RecvMsg p q m)                 = 

   720     (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> [])"

   721 | "os_grant \<tau> (RemoveMsgq p q)                = 

   722     (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau>)"

   723 (*

   724 | "os_grant \<tau> (CreateShM p h)                 = 

   725     (p \<in> current_procs \<tau> \<and> h \<notin> (current_shms \<tau>))"

   726 | "os_grant \<tau> (Attach p h flag)               = 

   727     (p \<in> current_procs \<tau> \<and> h \<in> current_shms \<tau> \<and> \<not> (\<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h))"

   728 | "os_grant \<tau> (Detach p h)                    = 

   729     (p \<in> current_procs \<tau> \<and> h \<in> current_shms \<tau> \<and> (\<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h))"

   730 | "os_grant \<tau> (DeleteShM p h)                 = 

   731     (p \<in> current_procs \<tau> \<and> h \<in> current_shms \<tau>)"

   732 *)

   733 | "os_grant \<tau> (CreateSock p af st fd ino)     = 

   734     (p \<in> current_procs \<tau> \<and> af = AF_INET \<and> fd \<notin> (current_proc_fds \<tau> p) \<and> 

   735      ino \<notin> (current_inode_nums \<tau>))"

   736 | "os_grant \<tau> (Accept p fd addr port fd' ino) = 

   737     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and> 

   738      fd' \<notin> (current_proc_fds \<tau> p) \<and> socket_state \<tau> (p, fd) = Some SS_listen \<and> 

   739      is_tcp_sock \<tau> (p, fd) \<and> ino \<notin> (current_inode_nums \<tau>))"

   740 | "os_grant \<tau> (Bind p fd addr)                = 

   741     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and> 

   742      socket_state \<tau> (p, fd) = Some SS_create)" (* ?? !! (case addr of INET_ADDR ip port \<Rightarrow> ip \<in> local_ipaddrs)) *)

   743 | "os_grant \<tau> (Connect p fd addr)             = 

   744     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and> 

   745      socket_state \<tau> (p, fd) = Some SS_bind)"

   746 | "os_grant \<tau> (Listen p fd)                   = 

   747     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> is_tcp_sock \<tau> (p, fd) \<and>

   748      socket_state \<tau> (p, fd) = Some SS_bind)" (* Listen and Accept should only be used for TCP sever side *)

   749 | "os_grant \<tau> (SendSock p fd)                 = 

   750     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and> 

   751      socket_in_sending \<tau> (p, fd))"

   752 | "os_grant \<tau> (RecvSock p fd)                 = 

   753     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and> 

   754      socket_in_recving \<tau> (p, fd))"

   755 | "os_grant \<tau> (Shutdown p fd sh)              = 

   756     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and> 

   757      socket_in_trans \<tau> (p, fd))"

   758 (*

   759 | "os_grant \<tau> (ChangeOwner p u)               = (p \<in> current_procs \<tau> \<and> u \<in> current_users \<tau>)"

   760 *)

   761 | "os_grant \<tau> (Clone p p' fds)           = 

   762     (p \<in> current_procs \<tau> \<and> p' \<notin> (current_procs \<tau>) \<and> fds \<subseteq> proc_file_fds \<tau> p)" (*\<and> 

   763      (\<forall> h \<in> shms. \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h) current_proc_fds \<rightarrow> proc_file_fds *)

   764 | "os_grant \<tau> (Kill p\<^isub>1 p\<^isub>2)                    = 

   765     (p\<^isub>1 \<in> current_procs \<tau> \<and> p\<^isub>2 \<in> current_procs \<tau>)" (* a process can kill itself right? *)

   766 | "os_grant \<tau> (Exit p)                        = 

   767     (p \<in> current_procs \<tau>)"

   768 | "os_grant \<tau> (Ptrace p\<^isub>1 p\<^isub>2)                  = 

   769     (p\<^isub>1 \<in> current_procs \<tau> \<and> p\<^isub>2 \<in> current_procs \<tau>)" (* a process can trace itself right? *)

   770 

   771 fun alive :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"

   772 where

   773   "alive s (O_proc p)     = (p \<in> current_procs s)"

   774 | "alive s (O_file f)     = (is_file s f)"

   775 | "alive s (O_dir  f)     = (is_dir s f)"

   776 | "alive s (O_fd p fd)    = (fd \<in> current_proc_fds s p)"

   777 | "alive s (O_node n)     = (n \<in> init_nodes)"

   778 | "alive s (O_tcp_sock k) = (is_tcp_sock s k)"

   779 | "alive s (O_udp_sock k) = (is_udp_sock s k)"

   780 (*

   781 | "alive s (O_shm  h)     = (h \<in> current_shms s)"

   782 *)

   783 | "alive s (O_msgq q)     = (q \<in> current_msgqs s)"

   784 | "alive s (O_msg q m)    = (m \<in> set (msgs_of_queue s q) \<and> q \<in> current_msgqs s)"

   785 

   786 (* deleted objects should be "taintable" objects, objects like fd should not be in consideration *)

   787 (* actually, deleted should be renamed as "vanished", cause "exit/closefd" *)

   788 fun deleted :: "t_object \<Rightarrow> t_event list \<Rightarrow> bool"

   789 where

   790   "deleted obj [] = False"

   791 | "deleted obj (Kill p p' # s) = (obj = O_proc p' \<or> deleted obj s)"

   792 (*

   793 | "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> 

   794                                   (\<exists> fd. obj = O_tcp_sock (p', fd) \<and> is_tcp_sock s (p',fd)) \<or>

   795                                   (\<exists> fd. obj = O_udp_sock (p', fd) \<and> is_udp_sock s (p',fd)) \<or>

   796                                   deleted obj s)"

   797 | "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>

   798                                      (obj = O_udp_sock (p,fd) \<and> is_udp_sock s (p, fd)) \<or> 

   799                                      (\<exists> f. obj = O_file f \<and> proc_fd_of_file s f = {(p, fd)} \<and> 

   800                                            f \<in> files_hung_by_del s) \<or> deleted obj s)"

   801 | "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> 

   802                                        (\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd) \<and> fd \<notin> fds) \<or>

   803                                        (\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd) \<and> fd \<notin> fds) \<or>

   804                                        deleted obj s)"

   805 | "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> 

   806                                             deleted obj s)"

   807 *)

   808 | "deleted obj (CloseFd p fd # s) = ((\<exists> f. obj = O_file f \<and> proc_fd_of_file s f = {(p, fd)} \<and> 

   809                                       f \<in> files_hung_by_del s) \<or> deleted obj s)"

   810 | "deleted obj (UnLink p f # s) = ((proc_fd_of_file s f = {} \<and> obj = O_file f) \<or> deleted obj s)"

   811 | "deleted obj (Rmdir p f # s)  = ((obj = O_dir  f) \<or> deleted obj s)"

   812 (*

   813 | "deleted obj (Exit p # s) = ((obj = O_proc p) \<or> (\<exists> fd \<in> current_proc_fds s p. obj = O_fd p fd) \<or> 

   814                                (\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd)) \<or>

   815                                (\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd)) \<or> deleted obj s)"

   816 *)

   817 (*

   818 | "deleted obj (Rename p f f' # s)  = 

   819      (case obj of

   820         O_file f'' \<Rightarrow> f \<preceq> f'' \<or> deleted obj s

   821       | O_dir  f'' \<Rightarrow> f \<preceq> f'' \<or> deleted obj s

   822       | _ \<Rightarrow> deleted obj s)"

   823 *)

   824 | "deleted obj (RemoveMsgq p q # s) = (obj = O_msgq q \<or> deleted obj s)"

   825 (*

   826 | "deleted obj (DeleteShM p h # s) = (obj = O_shm h \<or> deleted obj s)"

   827 

   828 | "deleted obj (RecvMsg p q m # s)  = (obj = O_msg q m \<or> deleted obj s)"

   829 *)

   830 | "deleted obj (_ # s) = deleted obj s"

   831 

   832 (* actually, died should be renamed as "vanished", cause "exit/closefd" *)

   833 fun died :: "t_object \<Rightarrow> t_event list \<Rightarrow> bool"

   834 where

   835   "died obj [] = False"

   836 | "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> 

   837                                   (\<exists> fd. obj = O_tcp_sock (p', fd) \<and> is_tcp_sock s (p',fd)) \<or>

   838                                   (\<exists> fd. obj = O_udp_sock (p', fd) \<and> is_udp_sock s (p',fd)) \<or>

   839                                   died obj s)"

   840 | "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>

   841                                      (obj = O_udp_sock (p,fd) \<and> is_udp_sock s (p, fd)) \<or> 

   842                                      (\<exists> f. obj = O_file f \<and> proc_fd_of_file s f = {(p, fd)} \<and> 

   843                                            f \<in> files_hung_by_del s) \<or> died obj s)"

   844 | "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> 

   845                                        (\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd) \<and> fd \<notin> fds) \<or>

   846                                        (\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd) \<and> fd \<notin> fds) \<or>

   847                                        died obj s)"

   848 | "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> 

   849                                             died obj s)"

   850 | "died obj (UnLink p f # s) = ((proc_fd_of_file s f = {} \<and> obj = O_file f) \<or> died obj s)"

   851 | "died obj (Rmdir p f # s)  = ((obj = O_dir f) \<or> died obj s)"

   852 | "died obj (Exit p # s) = ((obj = O_proc p) \<or> (\<exists> fd \<in> current_proc_fds s p. obj = O_fd p fd) \<or> 

   853                                (\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd)) \<or>

   854                                (\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd)) \<or> died obj s)"

   855 (*

   856 | "died obj (Rename p f f' # s)  = 

   857      (case obj of

   858         O_file f'' \<Rightarrow> f \<preceq> f'' \<or> died obj s

   859       | O_dir  f'' \<Rightarrow> f \<preceq> f'' \<or> died obj s

   860       | _ \<Rightarrow> died obj s)"

   861 *)

   862 | "died obj (RemoveMsgq p q # s) = (obj = O_msgq q \<or> (\<exists> m. obj = O_msg q m ) \<or> died obj s)"

   863 (*

   864 | "died obj (DeleteShM p h # s) = (obj = O_shm h \<or> died obj s)"

   865 *)

   866 | "died obj (RecvMsg p q m # s)  = (obj = O_msg q m \<or> died obj s)"

   867 | "died obj (_ # s) = died obj s"

   868 

   869 end

   870 

   871 

   872 

   873 locale flask = init + 

   874  fixes

   875    (***************** Policy-specific Parameters *************)

   876       type_transition_rules :: "type_transition_rule_list_t"

   877   and allowed_rules :: "allowed_rule_list_t"

   878   and role_allowed_rules :: "role_allow_rule_list_t"

   879   and role_declaration_rules :: "role_declarations_list_t"

   880   and role_transition_rules:: "role_transition_rule_list_t"

   881   and constrains_rules :: "constrains_list_t"

   882 

   883   and init_type_of_obj :: "t_object \<rightharpoonup> type_t"

   884   and init_user_of_obj :: "t_object \<rightharpoonup> user_t"

   885   and init_role_of_proc :: "t_process \<rightharpoonup> role_t"

   886 

   887   assumes

   888    

   889       init_obj_has_type: "\<And> obj. init_alive obj \<Longrightarrow> \<exists> t. init_type_of_obj obj = Some t"

   890   and init_type_has_obj: "\<And> obj t. init_type_of_obj obj = Some t \<Longrightarrow> init_alive obj"

   891   and init_obj_has_user: "\<And> obj. init_alive obj \<Longrightarrow> \<exists> u. init_user_of_obj obj = Some u"

   892   and init_user_has_obj: "\<And> obj u. init_user_of_obj obj = Some u \<Longrightarrow> init_alive obj \<and> u \<in> init_users"

   893   and init_proc_has_role: "bidirect_in_init init_procs init_role_of_proc"

   894 

   895 begin

   896 

   897 (*********** policy-specified computations, not-event-related ************)

   898 

   899 (* security_transition_sid : type_transition_rules

   900  * It's a system-call offered by security-server? So access-control-checked too?

   901  * according to selinux, it deals only with execve and file-creation

   902  *  is_execve: if is the execve case

   903  *  is_file: if is the creation of file/dir

   904  *  change from is_execve to is_file, because the new message by default use

   905  *  the type of the sending process too. 

   906  *)

   907 

   908 definition type_transition :: "type_t \<Rightarrow> type_t \<Rightarrow> security_class_t \<Rightarrow> bool \<Rightarrow> type_t"

   909 where

   910   "type_transition st rt tc IS_file \<equiv> (

   911      case (lookup type_transition_rules 

   912              (\<lambda> (stp, rtp, tc', dt). patt_match stp st \<and> patt_match rtp rt \<and> tc = tc')) of

   913        None     \<Rightarrow> (if IS_file then rt else st)

   914      | Some (stp,rtp,tc',dt) \<Rightarrow> dt)"

   915 

   916 (* allowed_rule_list *)

   917 definition TE_allow :: "type_t \<Rightarrow> type_t \<Rightarrow> security_class_t \<Rightarrow> permission_t \<Rightarrow> bool"

   918 where

   919   "TE_allow st tt tc perm \<equiv> member allowed_rules

   920       (\<lambda> (stp, ttp, tc', pp). tc = tc' \<and> patt_match stp st \<and> patt_match_self ttp tt st \<and>

   921                               patt_match pp perm)"

   922 

   923 (* role_allow_rule_list_t *)

   924 definition role_transition :: "role_t \<Rightarrow> type_t \<Rightarrow> role_t option"

   925 where

   926   "role_transition r t \<equiv> 

   927      (case (lookup role_transition_rules (\<lambda> (pr, ft, nr). pr = r \<and> t = ft)) of

   928         None \<Rightarrow> None

   929       | Some (pr,ft,nr) \<Rightarrow> Some nr)"

   930 

   931 definition role_decl_check :: "role_t \<Rightarrow> type_t \<Rightarrow> bool"

   932 where

   933   "role_decl_check r t \<equiv> member role_declaration_rules (\<lambda> (role, types). r = role \<and> t \<in> types)"

   934 

   935 definition role_allow :: "role_t \<Rightarrow> role_t \<Rightarrow> bool"

   936 where

   937   "role_allow r nr \<equiv> member role_allowed_rules (\<lambda> (from, to). r \<in> from \<and> nr \<in> to)"

   938 

   939 (* here don't use lookup, because constrains should all be satisfied, 

   940  * while transitions always choose the "first" one 

   941  *)

   942 definition constrains_satisfied :: 

   943   "security_context_t \<Rightarrow> security_context_t \<Rightarrow> security_class_t \<Rightarrow> permission_t \<Rightarrow> bool"

   944 where

   945   "constrains_satisfied sctxt tctxt c p \<equiv> 

   946     (fold (\<lambda> (cset, pset, P) res. res \<and> (if (c \<in> cset \<and> p \<in> pset) 

   947                                             then P sctxt tctxt else True))

   948           constrains_rules True)"

   949 

   950 (* main interface for TE_allow check and constrains check *)

   951 fun permission_check:: 

   952   "security_context_t \<Rightarrow> security_context_t \<Rightarrow> security_class_t \<Rightarrow> permission_t \<Rightarrow> bool"

   953 where

   954   "permission_check (su,sr,st) (tu,tr,tt) c p =

   955     ((TE_allow st tt c p) \<and> (constrains_satisfied (su,sr,st) (tu,tr,tt) c p))"

   956 declare permission_check.simps [simp del]

   957 

   958 (* no changeowner ??? : by adding "relabel obj sectxt" event or "login" event? 

   959  * or this explanation: the running of the sever will not grant any login but running 

   960  * of the server-programs! 

   961  *)

   962 

   963 fun user_of_obj :: "t_state \<Rightarrow> t_object \<Rightarrow> user_t option"

   964 where 

   965   "user_of_obj [] = init_user_of_obj"

   966 | "user_of_obj (Clone p p' fds # s) = 

   967     (\<lambda> obj. case obj of 

   968               O_proc p'' \<Rightarrow> if (p'' = p') then user_of_obj s (O_proc p) else user_of_obj s obj

   969             | O_fd p'' fd  \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then user_of_obj s (O_fd p fd)

   970                               else if (p'' = p') then None

   971                                    else user_of_obj s obj

   972             | O_tcp_sock (p'',fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then user_of_obj s (O_tcp_sock (p, fd))

   973                                      else if (p'' = p') then None

   974                                           else user_of_obj s obj

   975             | O_udp_sock (p'',fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then user_of_obj s (O_udp_sock (p, fd))

   976                                      else if (p'' = p') then None

   977                                           else user_of_obj s obj 

   978             | _ \<Rightarrow> user_of_obj s obj)"

   979 | "user_of_obj (Open p f flags fd iopt # s) = 

   980     (case iopt of

   981        None \<Rightarrow> (user_of_obj s) ((O_fd p fd) := user_of_obj s (O_proc p))

   982      | _    \<Rightarrow> ((user_of_obj s) ((O_fd p fd) := user_of_obj s (O_proc p)))

   983                ((O_file f) := user_of_obj s (O_proc p)))"

   984 | "user_of_obj (Mkdir p f inum # s) =

   985     (user_of_obj s) ((O_dir f) := user_of_obj s (O_proc p))"

   986 | "user_of_obj (LinkHard p f f' # s) = 

   987     (user_of_obj s) ((O_file f') := user_of_obj s (O_proc p))"

   988 (*

   989 | "user_of_obj (Rename p f2 f3 # s) = 

   990     (\<lambda> obj. case obj of 

   991               O_file f \<Rightarrow> if (f3 \<preceq> f) then user_of_obj s (O_file (file_before_rename f2 f3 f))

   992                           else user_of_obj s obj

   993             | O_dir  f \<Rightarrow> if (f3 \<preceq> f) then user_of_obj s (O_dir (file_before_rename f2 f3 f))

   994                           else user_of_obj s obj

   995             | _        \<Rightarrow> user_of_obj s obj)"

   996 *)

   997 | "user_of_obj (CreateMsgq p q # s) = 

   998     (user_of_obj s) ((O_msgq q) := user_of_obj s (O_proc p))" 

   999 | "user_of_obj (SendMsg p q m # s) = 

  1000     (user_of_obj s) ((O_msg q m) := user_of_obj s (O_proc p))"

  1001 (*

  1002 | "user_of_obj (CreateShM p h # s) = 

  1003     (user_of_obj s) ((O_shm h) := user_of_obj s (O_proc p))"

  1004 *)

  1005 | "user_of_obj (CreateSock p af st fd inum # s) =  (\<lambda> obj. 

  1006      case obj of

  1007        O_fd p' fd' \<Rightarrow> if (p' = p \<and> fd' = fd) then user_of_obj s (O_proc p)

  1008                       else user_of_obj s obj

  1009      | O_tcp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = STREAM) then user_of_obj s (O_proc p)

  1010                                else user_of_obj s obj

  1011      | O_udp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = DGRAM) then user_of_obj s (O_proc p)

  1012                                else user_of_obj s obj

  1013      | _ \<Rightarrow> user_of_obj s obj )"

  1014 | "user_of_obj (Accept p fd addr port fd' inum # s) = (\<lambda> obj. 

  1015      case obj of

  1016        O_fd p' fd'' \<Rightarrow> if (p' = p \<and> fd'' = fd') then user_of_obj s (O_proc p)

  1017                       else user_of_obj s obj

  1018      | O_tcp_sock (p', fd'') \<Rightarrow> if (p' = p \<and> fd'' = fd') then user_of_obj s (O_proc p)

  1019                                else user_of_obj s obj

  1020      | _ \<Rightarrow> user_of_obj s obj )"

  1021 | "user_of_obj (_ # s) = user_of_obj s"

  1022 

  1023 fun type_of_obj :: "t_state \<Rightarrow> (t_object \<Rightarrow> type_t option)"

  1024 where

  1025   "type_of_obj [] = init_type_of_obj"

  1026 | "type_of_obj (Clone p p' fds # s) = (\<lambda> obj. 

  1027      case obj of 

  1028        O_proc p'' \<Rightarrow> if (p'' = p') then type_of_obj s (O_proc p) else type_of_obj s obj

  1029      | O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then type_of_obj s (O_fd p fd)

  1030                       else if (p'' = p') then None

  1031                            else type_of_obj s obj

  1032      | O_tcp_sock (p'', fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then type_of_obj s (O_tcp_sock (p, fd))

  1033                                else if (p'' = p') then None

  1034                                     else type_of_obj s obj

  1035      | O_udp_sock (p'', fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then type_of_obj s (O_udp_sock (p, fd))

  1036                                else if (p'' = p') then None

  1037                                     else type_of_obj s obj

  1038      | _ \<Rightarrow> type_of_obj s obj )"

  1039 | "type_of_obj (Execve p f fds # s) = (type_of_obj s) ((O_proc p) := 

  1040     (case (type_of_obj s (O_proc p), type_of_obj s (O_file f)) of 

  1041        (Some tp, Some tf) \<Rightarrow> Some (type_transition tp tf C_process False)

  1042      | _                  \<Rightarrow> None)                    )"

  1043 | "type_of_obj (Open p f flags fd (Some inum) # s) = ((type_of_obj s) ((O_file f) := 

  1044      (case (parent f) of 

  1045         Some pf \<Rightarrow> (case (type_of_obj s (O_proc p), type_of_obj s (O_dir pf)) of 

  1046                       (Some tp, Some tpf) \<Rightarrow> Some (type_transition tp tpf C_file True)

  1047                     | _ \<Rightarrow> None)

  1048       | _       \<Rightarrow> None)                              )) ((O_fd p fd) := 

  1049      type_of_obj s (O_proc p))"

  1050 | "type_of_obj (Open p f flags fd None # s) = (type_of_obj s) ((O_fd p fd) := 

  1051      type_of_obj s (O_proc p))"

  1052 | "type_of_obj (Mkdir p f inum # s) = (type_of_obj s) ((O_dir f) := 

  1053      (case (parent f) of 

  1054         Some pf \<Rightarrow> (case (type_of_obj s (O_proc p), type_of_obj s (O_dir pf)) of

  1055                      (Some tp, Some tpf) \<Rightarrow> Some (type_transition tp tpf C_dir True)

  1056                    | _ \<Rightarrow> None)

  1057      | _ \<Rightarrow> None)                                 )"

  1058 | "type_of_obj (LinkHard p f f' # s) = (type_of_obj s) ((O_file f') := 

  1059     (case (parent f') of 

  1060        Some pf \<Rightarrow> (case (type_of_obj s (O_proc p), type_of_obj s (O_dir pf)) of

  1061                     (Some tp, Some tpf) \<Rightarrow> Some (type_transition tp tpf C_file True)

  1062                   | _ \<Rightarrow> None)

  1063      | _ \<Rightarrow> None)                                      )"

  1064 (*

  1065 | "type_of_obj (Rename p f f' # s) = (\<lambda> obj. 

  1066       case obj of

  1067         O_file f'' \<Rightarrow> (if (f' \<preceq> f'') then type_of_obj s (O_file (file_before_rename f f' f''))

  1068                        else type_of_obj s (O_file f''))

  1069       | O_dir f'' \<Rightarrow> (if (f' \<preceq> f'') then type_of_obj s (O_file (file_before_rename f f' f''))

  1070                       else type_of_obj s (O_file f''))

  1071       | _ \<Rightarrow> type_of_obj s obj   )"

  1072 *)

  1073 | "type_of_obj (CreateMsgq p q # s) = (type_of_obj s) ((O_msgq q) := 

  1074      (case (type_of_obj s (O_proc p)) of 

  1075         Some tp \<Rightarrow> Some tp

  1076       | _       \<Rightarrow> None)                          )"

  1077 | "type_of_obj (SendMsg p q m # s) = (type_of_obj s) ((O_msg q m) := 

  1078      (case (type_of_obj s (O_proc p), type_of_obj s (O_msgq q)) of 

  1079         (Some tp, Some tq) \<Rightarrow> Some (type_transition tp tq C_msg False)

  1080       | _ \<Rightarrow> None)                               )"

  1081 (*

  1082 | "type_of_obj (CreateShM p h # s) = (type_of_obj s) ((O_shm h) := 

  1083      (case (type_of_obj s (O_proc p)) of 

  1084         Some tp \<Rightarrow> Some tp

  1085       | _       \<Rightarrow> None)                          )"

  1086 *)

  1087 | "type_of_obj (CreateSock p af st fd inum # s) = (\<lambda> obj. 

  1088      case obj of

  1089        O_fd p' fd' \<Rightarrow> if (p' = p \<and> fd' = fd) then type_of_obj s (O_proc p)

  1090                       else type_of_obj s obj

  1091      | O_tcp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = STREAM) then type_of_obj s (O_proc p)

  1092                                else type_of_obj s obj

  1093      | O_udp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = DGRAM) then type_of_obj s (O_proc p)

  1094                                else type_of_obj s obj

  1095      | _ \<Rightarrow> type_of_obj s obj )"

  1096 | "type_of_obj (Accept p fd addr port fd' inum # s) = (\<lambda> obj. 

  1097      case obj of

  1098        O_fd p' fd'' \<Rightarrow> if (p' = p \<and> fd'' = fd') then type_of_obj s (O_proc p)

  1099                       else type_of_obj s obj

  1100      | O_tcp_sock (p', fd'') \<Rightarrow> if (p' = p \<and> fd'' = fd') then type_of_obj s (O_proc p)

  1101                                else type_of_obj s obj

  1102      | _ \<Rightarrow> type_of_obj s obj )"

  1103 | "type_of_obj (_ # s) = type_of_obj s"

  1104 

  1105 fun role_of_proc :: "t_state \<Rightarrow> (t_process \<Rightarrow> role_t option)"

  1106 where

  1107   "role_of_proc [] = init_role_of_proc"

  1108 | "role_of_proc (Clone p p' fds # s) = 

  1109     (role_of_proc s) (p' := role_of_proc s p)"

  1110 | "role_of_proc (Execve p f fds # s) = (role_of_proc s) (p := 

  1111     (case (role_of_proc s p, type_of_obj s (O_file f)) of

  1112        (Some r, Some ft) \<Rightarrow> role_transition r ft

  1113      | _ \<Rightarrow> None)                       )"

  1114 | "role_of_proc (_ # s) = role_of_proc s"

  1115 

  1116 fun role_of_obj :: "t_state \<Rightarrow> t_object \<Rightarrow> role_t option"

  1117 where

  1118   "role_of_obj s (O_proc p) = role_of_proc s p"

  1119 | "role_of_obj s _          = Some R_object"  (* object_r *)

  1120 

  1121 definition sectxt_of_obj :: "t_state \<Rightarrow> t_object \<Rightarrow> security_context_t option"

  1122 where

  1123   "sectxt_of_obj s obj = (

  1124      case (user_of_obj s obj, role_of_obj s obj, type_of_obj s obj) of

  1125        (Some u, Some r, Some t) \<Rightarrow> Some (u, r, t)

  1126      | _                        \<Rightarrow> None)"

  1127 

  1128 fun init_role_of_obj :: "t_object \<Rightarrow> role_t option"

  1129 where

  1130   "init_role_of_obj (O_proc p) = init_role_of_proc p"

  1131 | "init_role_of_obj _          = Some R_object"

  1132 

  1133 definition init_sectxt_of_obj :: "t_object \<Rightarrow> security_context_t option"

  1134 where

  1135   "init_sectxt_of_obj obj \<equiv>