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