diff -r b992684e9ff6 -r dcde836219bc rc_theory.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/rc_theory.thy	Fri Apr 12 10:43:11 2013 +0100
@@ -0,0 +1,990 @@
+theory rc_theory
+imports Main my_list_prefix
+begin
+
+
+(****************** rc policy (role, type, ... ) type definitions *****************)
+(*** normal: user-defined values for policy ***)
+(*** others: RC special values for RC internal control ***)
+ 
+datatype t_client = 
+  Client1
+| Client2
+
+datatype t_normal_role =  
+  WebServer 
+| WS     "t_client" 
+| UpLoad "t_client" 
+| CGI     "t_client"
+
+datatype t_role = 
+  InheritParentRole 
+| UseForcedRole 
+| InheritUpMixed 
+| InheritUserRole 
+| InheritProcessRole 
+| NormalRole "t_normal_role" 
+
+datatype t_normal_file_type = 
+  Root_file_type   (* special value, as 0 for root-file in the NordSec paper*)
+| WebServerLog_file
+| WebData_file      "t_client" 
+| CGI_P_file        "t_client" 
+| PrivateD_file     "t_client" 
+| Executable_file   (* basic protection of RC *)
+
+datatype t_rc_file_type = 
+  InheritParent_file_type          
+| NormalFile_type t_normal_file_type
+
+datatype t_normal_proc_type = 
+  WebServer_proc
+| CGI_P_proc "t_client"
+
+datatype t_rc_proc_type =
+  InheritParent_proc_type
+| NormalProc_type t_normal_proc_type
+| UseNewRoleType  
+
+datatype t_normal_ipc_type = 
+  WebIPC
+
+datatype t_normal_rc_type =
+  File_type t_normal_file_type
+| Proc_type t_normal_proc_type
+| IPC_type  t_normal_ipc_type
+
+
+
+(******* Operating System type definitions ********)
+
+type_synonym t_process = nat
+
+type_synonym t_user = nat
+
+type_synonym t_fname = string
+
+type_synonym t_file = "t_fname list" 
+
+type_synonym t_ipc = nat
+
+
+
+(****** Access Control related type definitions *********)
+
+datatype t_event =
+  ChangeOwner  "t_process" "t_user" 
+| Clone        "t_process" "t_process"
+| Execute      "t_process" "t_file" 
+| CreateFile   "t_process" "t_file" 
+| CreateIPC    "t_process" "t_ipc" 
+| ChangeRole   "t_process" "t_normal_role"    (* A process should change to normal role, which not specified in paper! *) 
+
+(* below are events added for tainting modelling *)
+| ReadFile     "t_process" "t_file" 
+| WriteFile    "t_process" "t_file"     
+| Send         "t_process" "t_ipc"
+| Recv         "t_process" "t_ipc"
+
+| Kill         "t_process" "t_process"
+| DeleteFile   "t_process" "t_file"
+| DeleteIPC    "t_process" "t_ipc"
+                                  
+type_synonym t_state = "t_event list"
+             
+datatype t_access_type =        (*changed by wch, original: "types access_type = nat" *)
+  READ    
+| WRITE   
+| EXECUTE 
+| CHANGE_OWNER
+| CREATE
+| SEND
+| RECEIVE
+
+| DELETE
+
+
+(****** Some global functions' definition *****)
+
+fun parent :: "'a list \<Rightarrow> ('a list) option"
+where
+   "parent []     = None"
+ | "parent (n#ns) = Some ns"
+
+definition some_in_set :: "'a set \<Rightarrow> 'a"
+where
+  "some_in_set S \<equiv> SOME x. x \<in> S"
+
+lemma nonempty_set_has_ele: "S \<noteq> {} \<Longrightarrow> \<exists> e. e \<in> S" by auto
+
+lemma some_in_set_prop: "S \<noteq> {} \<Longrightarrow> some_in_set S \<in> S"
+by (drule nonempty_set_has_ele, auto simp:some_in_set_def intro:someI)
+
+
+(*********** locale for RC+OS definitions **********)
+
+definition bidirect_in_init :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> bool"
+where
+  "bidirect_in_init S f \<equiv>  (\<forall> a. a \<in> S \<longrightarrow> (\<exists> b. f a = Some b)) \<and> 
+                           (\<forall> a b. f a = Some b \<longrightarrow> a \<in> S)" 
+
+locale init =
+  fixes 
+      init_files :: "t_file set"
+  and init_file_type :: "t_file \<rightharpoonup> t_normal_file_type"
+  and init_initialrole :: "t_file \<rightharpoonup> t_role"
+  and init_forcedrole :: "t_file \<rightharpoonup> t_role"
+  
+  and init_processes :: "t_process set "
+  and init_process_type :: "t_process \<rightharpoonup> t_normal_proc_type"
+  and init_currentrole :: "t_process \<rightharpoonup> t_normal_role"
+  and init_proc_forcedrole:: "t_process \<rightharpoonup> t_role"
+
+  and init_ipcs :: "t_ipc set"
+  and init_ipc_type:: "t_ipc \<rightharpoonup> t_normal_ipc_type"
+
+  and init_users :: "t_user set"
+  and init_owner :: "t_process \<rightharpoonup> t_user"
+  and defrole :: "t_user \<rightharpoonup> t_normal_role" (* defrole should return normalrole, which is not
+specified in NordSec paper *) 
+
+  and default_fd_create_type :: "t_normal_role \<Rightarrow> t_rc_file_type" (* this func should only
+return type for normal role, for RC special role, error ! NordSec paper*)
+  and default_ipc_create_type :: "t_normal_role \<Rightarrow> t_normal_ipc_type" (* like above, NordSec paper
+does not specify the domain is normal roles *)
+  and default_process_create_type :: "t_normal_role \<Rightarrow> t_rc_proc_type"
+  and default_process_execute_type :: "t_normal_role \<Rightarrow> t_rc_proc_type"
+  and default_process_chown_type :: "t_normal_role \<Rightarrow> t_rc_proc_type"
+
+  and comproles :: "t_normal_role \<Rightarrow> t_normal_role set" (* NordSec paper do not specify all roles
+here are normal *)
+
+  and compatible :: "(t_normal_role \<times> t_normal_rc_type \<times> t_access_type) set"  (* NordSec paper do not specify all roles and all types here are normal ! *)
+
+  assumes
+      parent_file_in_init: "\<And> f pf. \<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> pf \<in> init_files"
+  and root_in_filesystem:  "[] \<in> init_files"
+  and init_irole_has_file: "\<And> f r. init_initialrole f = Some r \<Longrightarrow> f \<in> init_files"
+  and init_frole_has_file: "\<And> f r. init_forcedrole f = Some r \<Longrightarrow> f \<in> init_files"
+  and init_ftype_has_file: "\<And> f t. init_file_type f = Some t \<Longrightarrow> f \<in> init_files"
+  and
+      init_proc_has_role:  "bidirect_in_init init_processes init_currentrole"
+  and init_proc_has_frole: "bidirect_in_init init_processes init_proc_forcedrole"
+  and init_proc_has_type:  "bidirect_in_init init_processes init_process_type"
+  and
+      init_ipc_has_type:   "bidirect_in_init init_ipcs init_ipc_type"
+  and
+      init_user_has_role:  "bidirect_in_init init_users defrole"
+  and init_proc_has_owner: "bidirect_in_init init_processes init_owner"
+  and init_owner_valid:    "\<And> p u. init_owner p = Some u \<Longrightarrow> u \<in> init_users"
+  and
+      init_finite: "finite init_files \<and> finite init_processes \<and> finite init_ipcs \<and> finite init_users"
+begin 
+
+(***** Operating System Listeners *****)
+
+fun current_files :: "t_state \<Rightarrow> t_file set"
+where
+  "current_files [] = init_files"
+| "current_files (CreateFile p f # s) = insert f (current_files s)"
+| "current_files (DeleteFile p f # s) = current_files s - {f}"
+| "current_files (_ # s) = current_files s"
+
+fun current_procs :: "t_state \<Rightarrow> t_process set"
+where
+  "current_procs [] = init_processes"
+| "current_procs (Clone p p' # s) = insert p' (current_procs s)"
+| "current_procs (Kill p p' # s) = current_procs s - {p'} "
+| "current_procs (_ # s) = current_procs s"
+
+fun current_ipcs :: "t_state \<Rightarrow> t_ipc set"
+where
+  "current_ipcs [] = init_ipcs" 
+| "current_ipcs (CreateIPC p i # s) = insert i (current_ipcs s)"
+| "current_ipcs (DeleteIPC p i # s) = current_ipcs s - {i}"
+| "current_ipcs (_ # s) = current_ipcs s"
+
+fun owner :: "t_state \<Rightarrow> t_process \<rightharpoonup> t_user"
+where
+  "owner [] = init_owner"
+| "owner (Clone p p' # \<tau>) = (owner \<tau>) (p' := owner \<tau> p)"
+| "owner (ChangeOwner p u # \<tau>) = (owner \<tau>) (p := Some u)"
+| "owner (_ # \<tau>) = owner \<tau>"
+
+(***** functions for rc internal *****)
+
+(*** Roles Functions ***)
+
+(* comments:
+We have fix init_initialrole already in locale, why need this function?
+ Cause, users may be lazy to specify every file in the initial state to some InheritParent as
+initialrole, they can just specify all the important files with special initial role, leaving
+all other None, it is init_file_initialrole's job to fill default value(InheritParent) for 
+other files. Accutally, this has the point of "Functional default settings" in the 2 section of
+the NordSec paper. 
+init_file_forcedrole, and init_file_type_aux are of the same meaning. 
+*)
+fun init_file_initialrole :: "t_file \<rightharpoonup> t_role"
+where
+  "init_file_initialrole [] = (case (init_initialrole []) of
+                            None   \<Rightarrow> Some UseForcedRole
+                          | Some r \<Rightarrow> Some r)"
+| "init_file_initialrole f  = (case (init_initialrole f) of
+                            None   \<Rightarrow> Some InheritParentRole
+                          | Some r \<Rightarrow> Some r)"
+
+fun initialrole :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_role)"  
+where
+  "initialrole [] = init_file_initialrole"
+| "initialrole (CreateFile p f # s) = (initialrole s) (f:= Some InheritParentRole)" 
+| "initialrole (_ # s) = initialrole s"
+
+fun erole_functor :: "(t_file \<rightharpoonup> t_role) \<Rightarrow> t_role \<Rightarrow> (t_file \<rightharpoonup> t_role)"
+where
+  "erole_functor rfunc r [] = (
+     if (rfunc [] = Some InheritParentRole) 
+     then Some r 
+     else rfunc [] )"                             
+| "erole_functor rfunc r (n#ns) = (
+     if (rfunc (n#ns) = Some InheritParentRole) 
+     then erole_functor rfunc r ns 
+     else rfunc (n#ns) )"
+
+definition effinitialrole :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_role)"
+where
+  "effinitialrole s \<equiv> erole_functor (initialrole s) UseForcedRole"
+
+fun init_file_forcedrole :: "t_file \<rightharpoonup> t_role"
+where
+  "init_file_forcedrole [] = ( case (init_forcedrole []) of
+                                 None   \<Rightarrow> Some InheritUpMixed
+                               | Some r \<Rightarrow> Some r )"
+| "init_file_forcedrole f  = ( case (init_forcedrole f) of 
+                                 None   \<Rightarrow> Some InheritParentRole
+                              |  Some r \<Rightarrow> Some r )"  
+
+fun forcedrole :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_role)"  
+where
+  "forcedrole [] = init_file_forcedrole"
+| "forcedrole (CreateFile p f # s) = (forcedrole s) (f:= Some InheritParentRole)" 
+| "forcedrole (_ # s) = forcedrole s" 
+
+definition effforcedrole :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_role)" 
+where
+  "effforcedrole s \<equiv> erole_functor (forcedrole s) InheritUpMixed"
+
+fun proc_forcedrole :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_role)" (* $6.7$ *) 
+where
+  "proc_forcedrole [] = init_proc_forcedrole"
+| "proc_forcedrole (Execute p f # s) = (proc_forcedrole s) (p := effforcedrole s f)"    
+| "proc_forcedrole (Clone p p' # s) = (proc_forcedrole s) (p' := proc_forcedrole s p)" 
+| "proc_forcedrole (e # s) = proc_forcedrole s"
+
+fun currentrole :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_normal_role)" 
+where 
+  "currentrole [] = init_currentrole"
+| "currentrole (Clone p p' # \<tau>) = (currentrole \<tau>) (p' := currentrole \<tau> p)" 
+| "currentrole (Execute p f # \<tau>) = (currentrole \<tau>) (p := 
+     case (effinitialrole \<tau> f) of 
+       Some ir \<Rightarrow> (case ir of 
+                     NormalRole r \<Rightarrow> Some r
+                   | UseForcedRole \<Rightarrow> (
+                       case (effforcedrole \<tau> f) of
+                         Some fr \<Rightarrow> (case fr of
+                                       NormalRole r \<Rightarrow> Some r
+                                     | InheritUserRole \<Rightarrow> (defrole \<circ>\<^sub>m (owner \<tau>)) p
+                                     | InheritProcessRole \<Rightarrow> currentrole \<tau> p
+                                     | InheritUpMixed \<Rightarrow> currentrole \<tau> p
+                                     | _ \<Rightarrow> None )
+                       | _ \<Rightarrow> None    )
+                   | _  \<Rightarrow> None )
+     | _ \<Rightarrow> None                                   )"       
+| "currentrole (ChangeOwner p u # \<tau>) = (currentrole \<tau>) (p := 
+     case (proc_forcedrole \<tau> p) of 
+       Some fr \<Rightarrow> (case fr of
+                     NormalRole r \<Rightarrow> Some r
+                   | InheritProcessRole \<Rightarrow> currentrole \<tau> p
+                   | InheritUserRole \<Rightarrow> defrole u
+                   | InheritUpMixed \<Rightarrow> defrole u
+                   | _ \<Rightarrow> None)
+     | _ \<Rightarrow> None                                       )"  
+| "currentrole (ChangeRole p r # \<tau>) = (currentrole \<tau>) (p := Some r)"
+| "currentrole (_ # \<tau>) = currentrole \<tau>"  
+
+(*** Types Functions ***)
+
+fun init_file_type_aux :: "t_file \<rightharpoonup> t_rc_file_type"
+where
+  "init_file_type_aux f = (if (f \<in> init_files)
+                         then (case (init_file_type f) of 
+                                 Some t \<Rightarrow> Some (NormalFile_type t)
+                               | _      \<Rightarrow> Some InheritParent_file_type)
+                         else None)"
+
+fun type_of_file :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_rc_file_type)" (* (6) *)
+where
+  "type_of_file [] = init_file_type_aux" 
+| "type_of_file (CreateFile p f # s) = (
+     case (currentrole s p) of
+       Some r \<Rightarrow> (type_of_file s) (f := Some (default_fd_create_type r))
+     | _      \<Rightarrow> (type_of_file s) (f := None))" 
+| "type_of_file (_ # s) = type_of_file s"  (* add by wch *)
+
+fun etype_aux:: "(t_file \<rightharpoonup> t_rc_file_type) \<Rightarrow> (t_file \<rightharpoonup> t_normal_file_type)"
+where
+  "etype_aux typf [] = (
+     case (typf []) of 
+       Some InheritParent_file_type \<Rightarrow> Some Root_file_type
+     | Some (NormalFile_type t) \<Rightarrow> Some t
+     | None \<Rightarrow> None )"        
+| "etype_aux typf (n#ns) = (
+     case (typf (n#ns)) of
+       Some InheritParent_file_type \<Rightarrow> etype_aux typf ns
+     | Some (NormalFile_type t) \<Rightarrow> Some t
+     | None \<Rightarrow> None )"  
+
+definition etype_of_file :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_normal_file_type)" 
+    (* etype is always normal *)
+where
+  "etype_of_file s \<equiv> etype_aux (type_of_file s)"              
+
+definition pct :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_rc_proc_type)"
+where
+  "pct s p \<equiv> (case (currentrole s p) of
+                Some r \<Rightarrow> Some (default_process_create_type r)
+              | _      \<Rightarrow> None)"
+
+definition pet :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_rc_proc_type)"
+where
+  "pet s p \<equiv> (case (currentrole s p) of
+                Some r \<Rightarrow> Some (default_process_execute_type r)
+              | _      \<Rightarrow> None)"
+
+definition pot :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_rc_proc_type)"
+where
+  "pot s p \<equiv> (case (currentrole s p) of
+                Some r \<Rightarrow> Some (default_process_chown_type r)
+              | _      \<Rightarrow> None)"
+
+fun type_of_process :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_normal_proc_type)" 
+where
+  "type_of_process [] = init_process_type"
+| "type_of_process (Clone p p' # \<tau>) = (type_of_process \<tau>) (p' := 
+     case (pct \<tau> p) of
+       Some InheritParent_proc_type \<Rightarrow> type_of_process \<tau> p
+     | Some (NormalProc_type tp)    \<Rightarrow> Some tp
+     | _                            \<Rightarrow> None               )" (*6.80*)
+| "type_of_process (Execute p f # \<tau>) = (type_of_process \<tau>) (p :=
+     case (pet \<tau> p) of
+       Some InheritParent_proc_type \<Rightarrow> type_of_process \<tau> p
+     | Some (NormalProc_type tp)    \<Rightarrow> Some tp
+     | _                            \<Rightarrow> None                )" (*6.82*)
+| "type_of_process (ChangeOwner p u # \<tau>) = (type_of_process \<tau>) (p :=
+     case (pot \<tau> p) of
+       Some InheritParent_proc_type \<Rightarrow> type_of_process \<tau> p
+     | Some UseNewRoleType          \<Rightarrow> (case (pct (ChangeOwner p u # \<tau>) p) of 
+                                          Some InheritParent_proc_type \<Rightarrow> type_of_process \<tau> p
+                                        | Some (NormalProc_type tp)    \<Rightarrow> Some tp
+                                        | _                            \<Rightarrow> None)
+     | Some (NormalProc_type tp)    \<Rightarrow> Some tp
+     | _                            \<Rightarrow> None                    )"   (* the UseNewRoleType case is refered with Nordsec paper 4 (11), and it is not right??! of just
+use "pct" *)
+| "type_of_process (_ # \<tau>) = type_of_process \<tau>" 
+
+fun type_of_ipc :: "t_state \<Rightarrow> (t_ipc \<rightharpoonup> t_normal_ipc_type)" (* (14) *)
+where
+  "type_of_ipc [] = init_ipc_type" 
+| "type_of_ipc (CreateIPC p i # s) = (type_of_ipc s) (i := 
+     case (currentrole s p) of
+       Some r \<Rightarrow> Some (default_ipc_create_type r)
+     | _      \<Rightarrow> None                                )"
+| "type_of_ipc (_ # s) = type_of_ipc s" (* add by wch *)
+
+(*** RC access control ***)
+fun rc_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool"
+where
+  "rc_grant \<tau> (CreateFile p f) = (
+     case (parent f) of
+       Some pf \<Rightarrow> (
+         case (currentrole \<tau> p, etype_of_file \<tau> pf) of
+           (Some r, Some t) \<Rightarrow> (
+              case (default_fd_create_type r) of
+                InheritParent_file_type \<Rightarrow> (r, File_type t, WRITE) \<in> compatible 
+              | NormalFile_type t' \<Rightarrow> (r, File_type t, WRITE) \<in> compatible \<and> (r, File_type t', CREATE) \<in> compatible
+                               )
+         | _               \<Rightarrow> False )
+     | _       \<Rightarrow> False                         )"  
+| "rc_grant \<tau> (ReadFile p f) = (
+     case (currentrole \<tau> p, etype_of_file \<tau> f) of
+        (Some r, Some t) \<Rightarrow> (r, File_type t, READ) \<in> compatible 
+     | _                \<Rightarrow> False                )"
+| "rc_grant \<tau> (WriteFile p f) = (
+     case (currentrole \<tau> p, etype_of_file \<tau> f) of
+       (Some r, Some t) \<Rightarrow> (r, File_type t, WRITE) \<in> compatible 
+     | _      \<Rightarrow> False                          )"
+| "rc_grant \<tau> (Execute p f) = (
+     case (currentrole \<tau> p, etype_of_file \<tau> f) of
+       (Some r, Some t) \<Rightarrow> (r, File_type t, EXECUTE) \<in> compatible
+     | _                \<Rightarrow> False               )"     
+| "rc_grant \<tau> (ChangeOwner p u) = (
+     case (currentrole \<tau> p, type_of_process \<tau> p) of
+       (Some r, Some t) \<Rightarrow> (r, Proc_type t, CHANGE_OWNER) \<in> compatible
+     | _      \<Rightarrow> False                         )" 
+| "rc_grant \<tau> (Clone p newproc) = (
+     case (currentrole \<tau> p, type_of_process \<tau> p) of
+       (Some r, Some t) \<Rightarrow> (r, Proc_type t, CREATE) \<in> compatible
+     | _      \<Rightarrow> False                         )" (* premiss of no limit to clone is removed to locale assumptions *)
+| "rc_grant \<tau> (ChangeRole p r) = (
+     case (currentrole \<tau> p) of
+       Some cr \<Rightarrow> r \<in> comproles cr
+     | _       \<Rightarrow> False                        )"
+| "rc_grant \<tau> (Send p i) = (
+     case (currentrole \<tau> p, type_of_ipc \<tau> i) of 
+       (Some r, Some t) \<Rightarrow> (r, IPC_type t, SEND) \<in> compatible
+     | _                \<Rightarrow> False               )"
+| "rc_grant \<tau> (Recv p i) = (
+     case (currentrole \<tau> p, type_of_ipc \<tau> i) of 
+       (Some r, Some t) \<Rightarrow> (r, IPC_type t, RECEIVE) \<in> compatible
+     | _                \<Rightarrow> False               )"
+| "rc_grant \<tau> (CreateIPC p i) = (
+     case (currentrole \<tau> p) of
+       Some r \<Rightarrow> (r, IPC_type (default_ipc_create_type r), CREATE) \<in> compatible
+     | _      \<Rightarrow> False                         )"
+| "rc_grant \<tau> (DeleteFile p f) = (
+     case (currentrole \<tau> p, etype_of_file \<tau> f) of 
+       (Some r, Some t) \<Rightarrow> (r, File_type t, DELETE) \<in> compatible
+     | _                \<Rightarrow> False               )"
+| "rc_grant \<tau> (DeleteIPC p i) = (
+     case (currentrole \<tau> p, type_of_ipc \<tau> i) of 
+       (Some r, Some t) \<Rightarrow> (r, IPC_type t, DELETE) \<in> compatible
+     | _                \<Rightarrow> False               )"
+| "rc_grant \<tau> (Kill p p') = (
+     case (currentrole \<tau> p, type_of_process \<tau> p') of 
+       (Some r, Some t) \<Rightarrow> (r, Proc_type t, DELETE) \<in> compatible
+     | _                \<Rightarrow> False               )"
+
+
+(**** OS' job: checking resources existence & grant new resource ****)
+
+definition next_nat :: "nat set \<Rightarrow> nat"
+where
+  "next_nat ps = (Max ps) + 1"
+
+definition new_proc :: "t_state \<Rightarrow> t_process"
+where 
+  "new_proc \<tau> = next_nat (current_procs \<tau>)"
+
+definition new_ipc :: "t_state \<Rightarrow> t_ipc"
+where
+  "new_ipc \<tau> = next_nat (current_ipcs \<tau>)"
+
+(* new file pathname is user-defined, so os just check if its unexistence *) 
+fun os_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool"
+where
+  "os_grant \<tau> (Execute p f)    = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)"
+| "os_grant \<tau> (CreateFile p f) = (p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and> (\<exists> pf. (parent f = Some pf) \<and> pf \<in> current_files \<tau>))"  (*cannot create disk, ?? or f = [] ??*)
+| "os_grant \<tau> (ChangeRole p r) = (p \<in> current_procs \<tau>)"
+| "os_grant \<tau> (ReadFile p f)   = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)"
+| "os_grant \<tau> (WriteFile p f)  = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)"
+| "os_grant \<tau> (ChangeOwner p u)= (p \<in> current_procs \<tau> \<and> u \<in> init_users)"
+| "os_grant \<tau> (CreateIPC p i)  = (p \<in> current_procs \<tau> \<and> i = new_ipc \<tau>)"
+| "os_grant \<tau> (Send p i)       = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)" 
+| "os_grant \<tau> (Recv p i)       = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)"
+| "os_grant \<tau> (Clone p p')     = (p \<in> current_procs \<tau> \<and> p' = new_proc \<tau>)"
+| "os_grant \<tau> (Kill p p')      = (p \<in> current_procs \<tau> \<and> p' \<in> current_procs \<tau>)" 
+| "os_grant \<tau> (DeleteFile p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> \<not> (\<exists>fn. fn # f \<in> current_files \<tau>))"
+| "os_grant \<tau> (DeleteIPC p i)  = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)" 
+
+(**** system valid state ****)
+
+inductive valid :: "t_state \<Rightarrow> bool"
+where
+  vs_nil:  "valid []"
+| vs_step: "\<lbrakk>valid s; os_grant s e; rc_grant s e\<rbrakk> \<Longrightarrow> valid (e # s)"
+
+end
+
+(*** more RC constrains of type system in formalisation ***)
+
+locale rc_basic = init +
+  assumes 
+      init_initialrole_valid: "\<And> f r. init_initialrole f = Some r \<Longrightarrow> r = InheritParentRole \<or> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)"   (* 6.10 *)
+  and init_forcedrole_valid:  "\<And> f r. init_forcedrole f = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritParentRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)"  (* 6.11 *)
+  and init_proc_forcedrole_valid: "\<And> p r. init_proc_forcedrole p = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)"  (* 6.7 *)
+  and default_fd_create_type_valid: "\<And> nr t. default_fd_create_type nr = t \<Longrightarrow> t = InheritParent_file_type \<or> (\<exists> nt. t = NormalFile_type nt)" (*6.16*)
+  and default_process_create_type_valid: "\<And> nr t. default_process_create_type nr = t \<Longrightarrow> t = InheritParent_proc_type \<or> (\<exists> nt. t = NormalProc_type nt)" (*6.18*)
+  and default_process_chown_type_valid: "\<And> nr t. default_process_chown_type nr = t \<Longrightarrow> t = InheritParent_proc_type \<or> t = UseNewRoleType \<or> (\<exists> nt. t = NormalProc_type nt)" (*6.19*)
+  and default_process_execute_type_valid: "\<And> nr t. default_process_execute_type nr = t \<Longrightarrow> t = InheritParent_proc_type \<or> (\<exists> nt. t = NormalProc_type nt)" (*6.20*)
+
+begin
+
+lemma init_file_initialrole_valid: "init_file_initialrole f = Some r \<Longrightarrow> r = InheritParentRole \<or> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)"
+apply (induct f)
+by (auto simp:init_file_initialrole.simps dest:init_initialrole_valid split:option.splits)
+
+lemma initialrole_valid: "initialrole \<tau> f = Some r \<Longrightarrow> r = InheritParentRole \<or> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)"   (* 6.10 *)
+apply (induct \<tau> arbitrary:f)  defer
+apply (case_tac a)
+apply (auto simp:initialrole.simps dest:init_file_initialrole_valid 
+            split:option.splits if_splits)
+done
+
+lemma effinitialrole_valid: "effinitialrole \<tau> f = Some r \<Longrightarrow> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)" 
+apply (induct f)
+apply (auto simp:effinitialrole_def dest:initialrole_valid split:option.splits if_splits)
+done
+
+lemma init_file_forcedrole_valid: 
+  "init_file_forcedrole f = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritParentRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)" 
+apply (induct f)
+by (auto simp:init_file_forcedrole.simps dest:init_forcedrole_valid split:option.splits)
+
+lemma forcedrole_valid: "forcedrole \<tau> f = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritParentRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)"  (* 6.10 *)
+apply (induct \<tau> arbitrary:f) defer 
+apply (case_tac a)
+apply (auto simp:forcedrole.simps dest:init_file_forcedrole_valid 
+           split:option.splits if_splits)
+done
+
+lemma effforcedrole_valid: "effforcedrole \<tau> f = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole  \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)"
+apply (induct f)
+apply (auto simp:effforcedrole_def dest:forcedrole_valid split:option.splits if_splits)
+done
+
+lemma proc_forcedrole_valid: "proc_forcedrole \<tau> p = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)"  (* 6.7 *)
+apply (induct \<tau> arbitrary:p) defer
+apply (case_tac a)
+apply (auto simp:proc_forcedrole.simps dest:init_proc_forcedrole_valid effforcedrole_valid 
+           split:option.splits if_splits)
+done
+
+lemma pct_valid: "pct \<tau> p = Some t \<Longrightarrow> t = InheritParent_proc_type \<or> (\<exists> nt. t = NormalProc_type nt)"
+by (auto simp:pct_def default_process_create_type_valid split:option.splits)
+  
+lemma pot_valid: "pot \<tau> p = Some t \<Longrightarrow> t = InheritParent_proc_type \<or> t = UseNewRoleType \<or> (\<exists> nt. t = NormalProc_type nt)" 
+by (auto simp:pot_def default_process_chown_type_valid split:option.splits)
+
+lemma pet_valid: "pet \<tau> p = Some t \<Longrightarrow> t = InheritParent_proc_type \<or> (\<exists> nt. t = NormalProc_type nt)" 
+by (simp add:pet_def default_process_execute_type_valid map_comp_def split:option.splits)
+
+end
+
+(******* Reachable/tainting related type definitions  ********)
+ 
+datatype t_object = 
+  Proc "t_process" 
+| File "t_file"
+| IPC  "t_ipc"
+
+fun object_in_init :: "t_object \<Rightarrow> t_file set \<Rightarrow> t_process set \<Rightarrow> t_ipc set \<Rightarrow> bool"
+where
+  "object_in_init (Proc p) init_files init_procs init_ipcs = (p \<in> init_procs)"
+| "object_in_init (File f) init_files init_procs init_ipcs = (f \<in> init_files)"
+| "object_in_init (IPC i) init_files init_procs init_ipcs = (i \<in> init_ipcs)"
+
+(*** locale for dynamic tainting ***)
+
+locale tainting = rc_basic + 
+
+fixes seeds :: "t_object set"
+
+assumes
+  seeds_in_init: "\<And> obj. obj \<in> seeds \<Longrightarrow> object_in_init obj init_files init_processes init_ipcs"
+begin
+
+lemma finite_seeds: "finite seeds"
+proof-
+  have "finite {obj. object_in_init obj init_files init_processes init_ipcs}"
+  proof-
+    have "finite {File f| f. f \<in> init_files}"
+      using init_finite by auto
+    moreover have "finite {Proc p| p. p \<in> init_processes}"
+      using init_finite by auto
+    moreover have "finite {IPC i| i. i \<in> init_ipcs}"
+      using init_finite by auto
+    ultimately have "finite ({File f| f. f \<in> init_files} \<union> {Proc p| p. p \<in> init_processes} \<union> {IPC i| i. i \<in> init_ipcs})"
+      by auto
+    thus ?thesis
+      apply (rule_tac B = "({File f| f. f \<in> init_files} \<union> {Proc p| p. p \<in> init_processes} \<union> {IPC i| i. i \<in> init_ipcs})" in finite_subset)
+      by (auto, case_tac x, simp+)
+  qed
+  with seeds_in_init
+  show ?thesis
+    by (rule_tac finite_subset, auto)
+qed
+
+fun exists :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"
+where
+  "exists s (File f) = (f \<in> current_files s)"
+| "exists s (Proc p) = (p \<in> current_procs s)"
+| "exists s (IPC  i) = (i \<in> current_ipcs  s)"
+
+inductive tainted :: "t_object \<Rightarrow> t_state \<Rightarrow> bool" ("_ \<in> tainted _" [100, 100] 100)
+where
+  t_init:  "obj \<in> seeds \<Longrightarrow> obj \<in> tainted []"
+| t_clone: "\<lbrakk>Proc p \<in> tainted s; valid (Clone p p' # s)\<rbrakk> \<Longrightarrow> Proc p' \<in> tainted (Clone p p' # s)"
+| t_exec:  "\<lbrakk>File f \<in> tainted s; valid (Execute p f # s)\<rbrakk> \<Longrightarrow> Proc p \<in> tainted (Execute p f # s)"
+| t_cfile: "\<lbrakk>Proc p \<in> tainted s; valid (CreateFile p f # s)\<rbrakk> \<Longrightarrow> File f \<in> tainted (CreateFile p f # s)"
+| t_cipc:  "\<lbrakk>Proc p \<in> tainted s; valid (CreateIPC p i # s)\<rbrakk> \<Longrightarrow> IPC i \<in> tainted (CreateIPC p i # s)"
+| t_read:  "\<lbrakk>File f \<in> tainted s; valid (ReadFile p f # s)\<rbrakk> \<Longrightarrow> Proc p \<in> tainted (ReadFile p f # s)"
+| t_write: "\<lbrakk>Proc p \<in> tainted s; valid (WriteFile p f # s)\<rbrakk> \<Longrightarrow> File f \<in> tainted (WriteFile p f # s)"
+| t_send:  "\<lbrakk>Proc p \<in> tainted s; valid (Send p i # s)\<rbrakk> \<Longrightarrow> IPC i \<in> tainted (Send p i # s)"
+| t_recv:  "\<lbrakk>IPC i \<in> tainted s; valid (Recv p i # s)\<rbrakk> \<Longrightarrow> Proc p \<in> tainted (Recv p i # s)"
+| t_remain:"\<lbrakk>obj \<in> tainted s; valid (e # s); exists (e # s) obj\<rbrakk> \<Longrightarrow> obj \<in> tainted (e # s)"
+
+definition taintable:: "t_object \<Rightarrow> bool"
+where
+  "taintable obj \<equiv> \<exists> s. obj \<in> tainted s"
+
+fun deleted :: "t_object \<Rightarrow> t_event list \<Rightarrow> bool"
+where
+  "deleted obj [] = False"
+| "deleted obj (Kill p p' # \<tau>) = ((obj = Proc p') \<or> deleted obj \<tau>)"
+| "deleted obj (DeleteFile p f # \<tau>) = ((obj = File f) \<or> deleted obj \<tau>)"
+| "deleted obj (DeleteIPC p i # \<tau>) = ((obj = IPC i) \<or> deleted obj \<tau>)"
+| "deleted obj (_ # \<tau>) = deleted obj \<tau>"
+
+definition undeletable :: "t_object \<Rightarrow> bool"
+where
+  "undeletable obj \<equiv> exists [] obj \<and> \<not> (\<exists> s. valid s \<and> deleted obj s)"
+
+fun no_del_event:: "t_event list \<Rightarrow> bool"
+where
+  "no_del_event [] = True"
+| "no_del_event (Kill p p' # \<tau>) = False"
+| "no_del_event (DeleteFile p f # \<tau>) = False"
+| "no_del_event (DeleteIPC p i # \<tau>) = False"
+| "no_del_event (_ # \<tau>) = no_del_event \<tau>"
+
+end
+
+
+(***** locale for statical world *****)
+
+type_synonym t_sprocess = "t_normal_role \<times> t_role \<times> t_normal_proc_type \<times> t_user"
+
+type_synonym t_sfile = "t_normal_file_type \<times> t_file"
+
+type_synonym t_sipc = "t_normal_ipc_type"
+
+datatype t_sobject =
+  SProc "t_sprocess" "t_process option"
+| SFile "t_sfile"    "t_file option"
+| SIPC  "t_sipc"     "t_ipc option"
+| Unknown
+
+locale tainting_s_complete = tainting
+
+begin 
+
+definition chown_role_aux:: "t_normal_role \<Rightarrow> t_role \<Rightarrow> t_user \<Rightarrow> t_normal_role option"
+where
+  "chown_role_aux cr fr u \<equiv> (
+     case fr of
+       NormalRole r \<Rightarrow> Some r
+     | InheritProcessRole \<Rightarrow> Some cr
+     | _ \<Rightarrow> defrole u       )"
+
+definition chown_type_aux:: "t_normal_role \<Rightarrow> t_normal_role \<Rightarrow> t_normal_proc_type \<Rightarrow> t_normal_proc_type"
+where
+  "chown_type_aux cr nr t \<equiv> (
+     case (default_process_chown_type cr) of
+       InheritParent_proc_type   \<Rightarrow> t
+     | UseNewRoleType            \<Rightarrow> (case (default_process_create_type nr) of 
+                                      InheritParent_proc_type \<Rightarrow> t
+                                     | NormalProc_type tp      \<Rightarrow> tp)
+     | NormalProc_type tp        \<Rightarrow> tp )"
+
+definition exec_type_aux :: "t_normal_role \<Rightarrow> t_normal_proc_type \<Rightarrow> t_normal_proc_type"
+where
+  "exec_type_aux cr t \<equiv> (case (default_process_execute_type cr) of 
+                           InheritParent_proc_type \<Rightarrow> t
+                         | NormalProc_type tp      \<Rightarrow>tp)"
+
+definition exec_role_aux :: "t_normal_role \<Rightarrow> t_file \<Rightarrow> t_user \<Rightarrow> t_normal_role option"
+where
+ "exec_role_aux cr sd u \<equiv> (
+    case (erole_functor init_file_initialrole UseForcedRole sd) of
+      Some ir \<Rightarrow> (case ir of 
+                     NormalRole r \<Rightarrow> Some r
+                   | UseForcedRole \<Rightarrow> (
+                       case (erole_functor init_file_forcedrole InheritUpMixed sd) of
+                         Some fr \<Rightarrow> (case fr of 
+                                       NormalRole r \<Rightarrow> Some r
+                                     | InheritUserRole \<Rightarrow> defrole u 
+                                     | _ \<Rightarrow> Some cr )
+                       | None    \<Rightarrow> None )     
+                   | _  \<Rightarrow> None )
+     | _ \<Rightarrow> None            )"       
+
+definition clone_type_aux :: "t_normal_role \<Rightarrow> t_normal_proc_type \<Rightarrow> t_normal_proc_type"
+where
+  "clone_type_aux r t \<equiv> (case (default_process_create_type r) of
+                           InheritParent_proc_type \<Rightarrow> t
+                         | NormalProc_type tp      \<Rightarrow> tp)"
+
+(* all the static objects that dynamic objects referring to *)
+(* they should all be in a finite set ? *)
+(* besides, they're no clone case for all_sobjs, we have no "SProc ... None" case, Clone p p', p' statically viewed as p too, so the many2many mapping becomes to many2one, which makes all succeeded*)
+inductive_set all_sobjs :: "t_sobject set"
+where
+  af_init:  "\<lbrakk>f \<in> init_files; etype_aux init_file_type_aux f = Some t\<rbrakk> \<Longrightarrow> SFile (t, f) (Some f) \<in> all_sobjs"
+| af_cfd:   "\<lbrakk>SFile (t, sd) sf \<in> all_sobjs; SProc (r, fr, pt, u) sp \<in> all_sobjs; default_fd_create_type r = NormalFile_type t'; (r, File_type t, WRITE) \<in> compatible; (r, File_type t', CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t', sd) None \<in> all_sobjs"
+| af_cfd':  "\<lbrakk>SFile (t, sd) sf \<in> all_sobjs; SProc (r, fr, pt, u) sp \<in> all_sobjs; default_fd_create_type r = InheritParent_file_type; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) None \<in> all_sobjs"
+
+| ai_init:  "init_ipc_type i = Some t \<Longrightarrow> SIPC t (Some i) \<in> all_sobjs"
+| ai_cipc:  "\<lbrakk>SProc (r, fr, pt, u) sp \<in> all_sobjs; (r, IPC_type (default_ipc_create_type r), CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC (default_ipc_create_type r) None \<in> all_sobjs"
+
+| ap_init:  "\<lbrakk>init_currentrole p = Some r; init_proc_forcedrole p = Some fr; init_process_type p = Some t; init_owner p = Some u\<rbrakk> \<Longrightarrow> SProc (r, fr, t, u) (Some p) \<in> all_sobjs"
+| ap_crole: "\<lbrakk>SProc (r, fr, t, u) sp \<in> all_sobjs; r' \<in> comproles r\<rbrakk> \<Longrightarrow> SProc (r', fr, t, u) sp \<in> all_sobjs"
+| ap_chown: "\<lbrakk>SProc (r, fr, t, u') sp \<in> all_sobjs; u \<in> init_users; chown_role_aux r fr u = Some nr; (r, Proc_type t, CHANGE_OWNER) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (nr, fr, chown_type_aux r nr t, u) sp \<in> all_sobjs"
+| ap_exec:  "\<lbrakk>SProc (r, fr, pt, u) sp \<in> all_sobjs; SFile (t, sd) sf \<in> all_sobjs; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> all_sobjs" 
+| ap_clone: "SProc (r, fr, pt, u) sp \<in> all_sobjs \<Longrightarrow> SProc (r, fr, clone_type_aux r pt, u) sp \<in> all_sobjs"
+
+fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject"
+where
+  "init_obj2sobj (File f) = (
+     case (etype_aux init_file_type_aux f) of
+       Some t \<Rightarrow> SFile (t, f) (Some f)
+     | _      \<Rightarrow> Unknown      )"
+| "init_obj2sobj (Proc p) = (
+     case (init_currentrole p, init_proc_forcedrole p, init_process_type p, init_owner p) of
+       (Some r, Some fr, Some t, Some u) \<Rightarrow> SProc (r, fr, t, u) (Some p)
+     | _  \<Rightarrow> Unknown          )"
+| "init_obj2sobj (IPC i) = (
+     case (init_ipc_type i) of 
+       Some t \<Rightarrow> SIPC t (Some i)
+     | _      \<Rightarrow> Unknown      )"
+
+inductive_set tainted_s :: "t_sobject set"
+where
+  ts_init: "obj \<in> seeds \<Longrightarrow> init_obj2sobj obj \<in> tainted_s"
+| ts_exec1: "\<lbrakk>SFile (t, sd) sf \<in> tainted_s; SProc (r, fr, pt, u) sp \<in> all_sobjs; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> tainted_s"
+| ts_exec2: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; SFile (t, sd) sf \<in> all_sobjs; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> tainted_s"
+| ts_cfd:  "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; SFile (t, sd) sf \<in> all_sobjs; default_fd_create_type r = NormalFile_type t'; (r, File_type t, WRITE) \<in> compatible; (r, File_type t', CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t', sd) None \<in> tainted_s"
+| ts_cfd': "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; SFile (t, sd) sf \<in> all_sobjs; default_fd_create_type r = InheritParent_file_type; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) None \<in> tainted_s"
+| ts_cipc: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; (r, IPC_type (default_ipc_create_type r), CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC (default_ipc_create_type r) None \<in> tainted_s"
+| ts_read: "\<lbrakk>SFile (t, sd) sf \<in> tainted_s; SProc (r, fr, pt, u) sp \<in> all_sobjs; (r, File_type t, READ) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (r, fr, pt, u) sp \<in> tainted_s"
+| ts_write: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; SFile (t, sd) sf \<in> all_sobjs; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) sf \<in> tainted_s"
+| ts_recv: "\<lbrakk>SIPC t si \<in> tainted_s; SProc (r, fr, pt, u) sp \<in> all_sobjs; (r, IPC_type t, RECEIVE) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (r, fr, pt, u) sp \<in> tainted_s"
+| ts_send: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; SIPC t si \<in> all_sobjs; (r, IPC_type t, SEND) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC t si \<in> tainted_s"
+| ts_crole: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; r' \<in> comproles r\<rbrakk> \<Longrightarrow> SProc (r', fr, pt, u) sp \<in> tainted_s"
+| ts_chown: "\<lbrakk>SProc (r, fr, t, u') sp \<in> tainted_s; u \<in> init_users; chown_role_aux r fr u = Some nr; (r, Proc_type t, CHANGE_OWNER) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (nr, fr, chown_type_aux r nr t, u) sp \<in> tainted_s"
+| ts_clone: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; (r, Proc_type pt, CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (r, fr, clone_type_aux r pt, u) sp \<in> tainted_s"
+
+(*** mapping function from dynamic 2 statical ****)
+
+fun source_dir:: "t_state \<Rightarrow> t_file \<Rightarrow> t_file option"
+where
+   "source_dir s []     = (if ([] \<in> init_files \<and> \<not> (deleted (File []) s)) 
+                           then Some [] 
+                           else None
+                          )"                                 
+ | "source_dir s (f#pf) = (if ((f#pf) \<in> init_files \<and> \<not> (deleted (File (f#pf)) s)) 
+                           then Some (f#pf)
+                           else source_dir s pf
+                          )"
+
+(* cf2sfile's properities should all be under condition: f is not deleted in \<tau>*)
+fun cf2sfile:: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option"
+where 
+  "cf2sfile s f = (case (etype_of_file s f, source_dir s f) of
+                     (Some t, Some sd) \<Rightarrow> Some (t, sd)
+                   | _                 \<Rightarrow> None)"
+
+fun cp2sproc:: "t_state \<Rightarrow> t_process \<Rightarrow> t_sprocess option"
+where
+  "cp2sproc s p = (case (currentrole s p, proc_forcedrole s p, type_of_process s p, owner s p) of
+                     (Some r, Some  fr, Some t, Some u) \<Rightarrow> Some (r, fr, t, u)
+                   | _                                  \<Rightarrow> None)"
+
+fun ci2sipc:: "t_state \<Rightarrow> t_ipc \<Rightarrow> t_sipc option"
+where
+  "ci2sipc s i = (type_of_ipc s i)"
+
+(*** in statical view, clone event is process to try different runs(different sprocess:role/type...),
+so statically these sprocesses should have the same source: the process in the initial state *********)
+fun source_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process option"
+where
+  "source_proc [] p = (if (p \<in> init_processes) then Some p else None)"
+| "source_proc (Clone p p' # s) p'' = (if (p'' = p') then source_proc s p else source_proc s p'')"
+| "source_proc (e # s) p = source_proc s p"
+
+fun obj2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject"
+where
+  "obj2sobj s (File f) = (
+     case (cf2sfile s f) of
+       Some sf \<Rightarrow> (if (f \<in> init_files \<and> (\<not> deleted (File f) s)) 
+                   then SFile sf (Some f)  
+                   else SFile sf None)
+     | _       \<Rightarrow> Unknown )"
+| "obj2sobj s (Proc p) = (
+     case (cp2sproc s p) of 
+       Some sp \<Rightarrow> SProc sp (source_proc s p)
+     | _       \<Rightarrow> Unknown )"
+| "obj2sobj s (IPC i) = (
+     case (ci2sipc s i) of 
+       Some si \<Rightarrow> (if (i \<in> init_ipcs \<and> (\<not> deleted (IPC i) s)) 
+                   then SIPC si (Some i) 
+                   else SIPC si None)
+     | _       \<Rightarrow> Unknown )"
+
+fun role_of_sproc :: "t_sprocess \<Rightarrow> t_normal_role"
+where
+  "role_of_sproc (r, fr, pt, u) = r"
+
+fun source_of_sobj :: "t_sobject \<Rightarrow> t_object option"
+where
+  "source_of_sobj (SFile sf tag) = (case tag of
+                                        Some f \<Rightarrow> Some (File f)
+                                      | _      \<Rightarrow> None)"
+| "source_of_sobj (SProc sp tag) = (case tag of
+                                        Some p \<Rightarrow> Some (Proc p)
+                                      | _      \<Rightarrow> None)"
+| "source_of_sobj (SIPC  si tag) = (case tag of
+                                        Some i \<Rightarrow> Some (IPC i)
+                                      | _      \<Rightarrow> None)"
+| "source_of_sobj Unknown        = None"
+
+definition taintable_s :: "t_object \<Rightarrow> bool"
+where
+  "taintable_s obj \<equiv> \<exists>sobj. sobj \<in> tainted_s \<and> source_of_sobj sobj = Some obj"
+
+(*
+definition file_deletable_s:: "t_file \<Rightarrow> bool"
+where 
+  "file_deletable_s f \<equiv> \<forall> t sd srf. (SFile (t,sd) srf \<in> all_sobjs \<and> f \<preceq> sd \<longrightarrow> (\<exists> sp srp. SProc sp srp \<in> all_sobjs \<and> (role_of_sproc sp, File_type t, DELETE) \<in> compatible))"
+*)
+(*
+definition file_deletable_s:: "t_file \<Rightarrow> bool"
+where 
+  "file_deletable_s sd \<equiv> \<forall> f. (f \<in> init_files \<and> sd \<preceq> f \<longrightarrow> (\<exists> t sp srp. SProc sp srp \<in> all_sobjs \<and> etype_of_file [] f = Some t \<and> (role_of_sproc sp, File_type t, DELETE) \<in> compatible))"*)
+
+definition file_deletable_s:: "t_file \<Rightarrow> bool"
+where 
+  "file_deletable_s f \<equiv> \<exists> t sp srp. SProc sp srp \<in> all_sobjs \<and> etype_of_file [] f = Some t \<and> (role_of_sproc sp, File_type t, DELETE) \<in> compatible"
+
+definition proc_deletable_s:: "t_process \<Rightarrow> bool"
+where
+  "proc_deletable_s p \<equiv> \<exists> r fr pt u sp' srp'. SProc (r,fr,pt,u) (Some p) \<in> all_sobjs \<and> SProc sp' srp' \<in> all_sobjs \<and> (role_of_sproc sp', Proc_type pt, DELETE) \<in> compatible"
+
+definition ipc_deletable_s:: "t_ipc \<Rightarrow> bool"
+where
+  "ipc_deletable_s i \<equiv> \<exists> t sp srp. SProc sp srp \<in> all_sobjs \<and> type_of_ipc [] i = Some t \<and> (role_of_sproc sp, IPC_type t, DELETE) \<in> compatible"
+
+fun deletable_s :: "t_object \<Rightarrow> bool"
+where
+  "deletable_s (Proc p) = (p \<in> init_processes \<and> proc_deletable_s p)"
+| "deletable_s (File f) = (f \<in> init_files     \<and> file_deletable_s f)"
+| "deletable_s (IPC  i) = (i \<in> init_ipcs      \<and> ipc_deletable_s  i)"
+
+definition undeletable_s:: "t_object \<Rightarrow> bool"
+where
+  "undeletable_s obj \<equiv> exists [] obj \<and> \<not> deletable_s obj"
+
+end
+
+locale tainting_s_sound = tainting_s_complete +
+
+assumes
+  clone_type_unchange: "\<And> r. default_process_create_type r = InheritParent_proc_type"
+(* this is for statically clone do not change anything ! ! so that, there're no rule for 
+clone in all_sobjs and tainted_s *)
+and clone_no_limit: "\<And> r t. (r, Proc_type t, CREATE) \<in> compatible"
+
+begin
+
+(* the all_sobjs': the soundness view of all_sobjs, just remove the clone case, cause
+in this locale, clone doesn't change any information of such a sprocess*)
+inductive_set all_sobjs' :: "t_sobject set"
+where
+  af'_init:  "\<lbrakk>f \<in> init_files; etype_aux init_file_type_aux f = Some t\<rbrakk> \<Longrightarrow> SFile (t, f) (Some f) \<in> all_sobjs'"
+| af'_cfd:   "\<lbrakk>SFile (t, sd) sf \<in> all_sobjs'; SProc (r, fr, pt, u) sp \<in> all_sobjs'; default_fd_create_type r = NormalFile_type t'; (r, File_type t, WRITE) \<in> compatible; (r, File_type t', CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t', sd) None \<in> all_sobjs'"
+| af'_cfd':  "\<lbrakk>SFile (t, sd) sf \<in> all_sobjs'; SProc (r, fr, pt, u) sp \<in> all_sobjs'; default_fd_create_type r = InheritParent_file_type; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) None \<in> all_sobjs'"
+
+| ai'_init:  "init_ipc_type i = Some t \<Longrightarrow> SIPC t (Some i) \<in> all_sobjs'"
+| ai'_cipc:  "\<lbrakk>SProc (r, fr, pt, u) sp \<in> all_sobjs'; (r, IPC_type (default_ipc_create_type r), CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC (default_ipc_create_type r) None \<in> all_sobjs'"
+
+| ap'_init:  "\<lbrakk>init_currentrole p = Some r; init_proc_forcedrole p = Some fr; init_process_type p = Some t; init_owner p = Some u\<rbrakk> \<Longrightarrow> SProc (r, fr, t, u) (Some p) \<in> all_sobjs'"
+| ap'_crole: "\<lbrakk>SProc (r, fr, t, u) sp \<in> all_sobjs'; r' \<in> comproles r\<rbrakk> \<Longrightarrow> SProc (r', fr, t, u) sp \<in> all_sobjs'"
+| ap'_chown: "\<lbrakk>SProc (r, fr, t, u') sp \<in> all_sobjs'; u \<in> init_users; chown_role_aux r fr u = Some nr; (r, Proc_type t, CHANGE_OWNER) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (nr, fr, chown_type_aux r nr t, u) sp \<in> all_sobjs'"
+| ap'_exec:  "\<lbrakk>SProc (r, fr, pt, u) sp \<in> all_sobjs'; SFile (t, sd) sf \<in> all_sobjs'; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> all_sobjs'" 
+
+(* the tainted_s': the soundness view of all_sobjs, just remove the clone case, cause
+in this locale, clone doesn't change any information of such a sprocess*)
+inductive_set tainted_s' :: "t_sobject set"
+where
+  ts'_init: "obj \<in> seeds \<Longrightarrow> init_obj2sobj obj \<in> tainted_s'"
+| ts'_exec1: "\<lbrakk>SFile (t, sd) sf \<in> tainted_s'; SProc (r, fr, pt, u) sp \<in> all_sobjs'; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> tainted_s'"
+| ts'_exec2: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; SFile (t, sd) sf \<in> all_sobjs'; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> tainted_s'"
+| ts'_cfd:  "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; SFile (t, sd) sf \<in> all_sobjs'; default_fd_create_type r = NormalFile_type t'; (r, File_type t, WRITE) \<in> compatible; (r, File_type t', CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t', sd) None \<in> tainted_s'"
+| ts'_cfd': "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; SFile (t, sd) sf \<in> all_sobjs'; default_fd_create_type r = InheritParent_file_type; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) None \<in> tainted_s'"
+| ts'_cipc: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; (r, IPC_type (default_ipc_create_type r), CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC (default_ipc_create_type r) None \<in> tainted_s'"
+| ts'_read: "\<lbrakk>SFile (t, sd) sf \<in> tainted_s'; SProc (r, fr, pt, u) sp \<in> all_sobjs'; (r, File_type t, READ) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (r, fr, pt, u) sp \<in> tainted_s'"
+| ts'_write: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; SFile (t, sd) sf \<in> all_sobjs'; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) sf \<in> tainted_s'"
+| ts'_recv: "\<lbrakk>SIPC t si \<in> tainted_s'; SProc (r, fr, pt, u) sp \<in> all_sobjs'; (r, IPC_type t, RECEIVE) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (r, fr, pt, u) sp \<in> tainted_s'"
+| ts'_send: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; SIPC t si \<in> all_sobjs'; (r, IPC_type t, SEND) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC t si \<in> tainted_s'"
+| ts'_crole: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; r' \<in> comproles r\<rbrakk> \<Longrightarrow> SProc (r', fr, pt, u) sp \<in> tainted_s'"
+| ts'_chown: "\<lbrakk>SProc (r, fr, t, u') sp \<in> tainted_s'; u \<in> init_users; chown_role_aux r fr u = Some nr; (r, Proc_type t, CHANGE_OWNER) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (nr, fr, chown_type_aux r nr t, u) sp \<in> tainted_s'"
+
+fun sobj_source_eq_obj :: "t_sobject \<Rightarrow> t_object \<Rightarrow> bool"
+where
+  "sobj_source_eq_obj (SFile sf None)      (File f) = True"
+| "sobj_source_eq_obj (SFile sf (Some f')) (File f) = (f' = f)"
+| "sobj_source_eq_obj (SProc sp None)      (Proc p) = True"
+| "sobj_source_eq_obj (SProc sp (Some p')) (Proc p) = (p' = p)"
+| "sobj_source_eq_obj (SIPC  si None)      (IPC  i) = True"
+| "sobj_source_eq_obj (SIPC  si (Some i')) (IPC  i) = (i' = i)"
+| "sobj_source_eq_obj _                    _        = False"
+
+fun not_both_sproc:: "t_sobject \<Rightarrow> t_sobject \<Rightarrow> bool"
+where
+  "not_both_sproc (SProc sp srp) (SProc sp' srp') = False"
+| "not_both_sproc _              _                = True"
+
+(*** definitions for init processes statical informations reservation ***)
+
+definition initp_intact :: "t_state => bool"
+where
+  "initp_intact s \<equiv> \<forall> p. p \<in> init_processes --> p \<in> current_procs s \<and> obj2sobj s (Proc p) = init_obj2sobj (Proc p)"
+
+definition initp_alter :: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
+where
+ "initp_alter s p \<equiv> \<exists> p'. p' \<in> current_procs s \<and> obj2sobj s (Proc p') = init_obj2sobj (Proc p)"
+
+definition initp_intact_butp :: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
+where
+  "initp_intact_butp s proc \<equiv>  (\<forall> p. p \<in> init_processes \<and> p \<noteq> proc \<longrightarrow> p \<in> current_procs s \<and> obj2sobj s (Proc p) = init_obj2sobj (Proc p)) \<and> initp_alter s proc"
+
+fun initp_intact_but :: "t_state \<Rightarrow> t_sobject \<Rightarrow> bool"
+where
+  "initp_intact_but s (SProc sp (Some p)) = initp_intact_butp s p"
+| "initp_intact_but s _                   = initp_intact s"
+
+(*** how to generating new valid pathname for examples of CreateFile ***)
+
+definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname set"
+where
+  "all_fname_under_dir d \<tau> = {fn. \<exists> f. fn # d = f \<and> f \<in> current_files \<tau>}"
+
+fun fname_all_a:: "nat \<Rightarrow> t_fname"
+where
+  "fname_all_a 0 = []" |
+  "fname_all_a (Suc n) = ''a''@(fname_all_a n)"
+
+definition fname_length_set :: "t_fname set \<Rightarrow> nat set"
+where
+  "fname_length_set fns = length`fns"
+
+definition next_fname:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname"
+where
+  "next_fname pf \<tau> = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf \<tau>))) + 1)"
+
+definition new_childf:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file"
+where
+  "new_childf pf \<tau> = next_fname pf \<tau> # pf"
+
+end 
+
+end
+