--- /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
+