--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper.thy Fri Apr 12 10:43:11 2013 +0100
@@ -0,0 +1,1517 @@
+(*<*)
+theory Paper
+imports rc_theory final_theorems rc_theory os_rc
+begin
+
+(* THEOREMS *)
+
+
+notation (Rule output)
+ "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+syntax (Rule output)
+ "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+ "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
+ ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
+
+ "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+notation (Axiom output)
+ "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+
+notation (IfThen output)
+ "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThen output)
+ "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+ "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+notation (IfThenNoBox output)
+ "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThenNoBox output)
+ "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+ "_asm" :: "prop \<Rightarrow> asms" ("_")
+
+(* insert *)
+notation (latex)
+ "Set.empty" ("\<emptyset>")
+
+translations
+ "{x} \<union> A" <= "CONST insert x A"
+ "{x,y}" <= "{x} \<union> {y}"
+ "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
+ "{x}" <= "{x} \<union> \<emptyset>"
+
+lemma impeq:
+ "A = B \<Longrightarrow> (B \<Longrightarrow> A)"
+by auto
+
+
+
+
+consts DUMMY::'a
+
+abbreviation
+ "is_parent f pf \<equiv> (parent f = Some pf)"
+
+context tainting_s_sound begin
+
+notation (latex output)
+ source_dir ("anchor") and
+ SProc ("P_\<^bsup>_\<^esup>") and
+ SFile ("F_\<^bsup>_\<^esup>") and
+ SIPC ("I'(_')\<^bsup>_\<^esup>") and
+ READ ("Read") and
+ WRITE ("Write") and
+ EXECUTE ("Execute") and
+ CHANGE_OWNER ("ChangeOwner") and
+ CREATE ("Create") and
+ SEND ("Send") and
+ RECEIVE ("Receive") and
+ DELETE ("Delete") and
+ compatible ("permissions") and
+ comproles ("compatible") and
+ DUMMY ("\<^raw:\mbox{$\_$}>") and
+ Cons ("_::_" [78,77] 79) and
+ Proc ("") and
+ File ("") and
+ File_type ("") and
+ Proc_type ("") and
+ IPC ("") and
+ init_processes ("init'_procs") and
+ os_grant ("admissible") and
+ rc_grant ("granted") and
+ exists ("alive") and
+ default_fd_create_type ("default'_type") and
+ InheritParent_file_type ("InheritPatentType") and
+ NormalFile_type ("NormalFileType") and
+ deleted ("deleted _ _" [50, 100] 100) and
+ taintable_s ("taintable\<^isup>s") and
+ tainted_s ("tainted\<^isup>s") and
+ all_sobjs ("reachable\<^isup>s") and
+ init_obj2sobj ("\<lbrakk>_\<rbrakk>") and
+ erole_functor ("erole'_aux") --"I have a erole_functor and etype_aux to handle
+ efficient, but their name not same, so ..., but don't work"
+
+
+abbreviation
+ "is_process_type s p t \<equiv> (type_of_process s p = Some t)"
+
+abbreviation
+ "is_current_role s p r \<equiv> (currentrole s p = Some r)"
+
+abbreviation
+ "is_file_type s f t \<equiv> (etype_of_file s f = Some t)"
+
+lemma osgrant2:
+ "\<lbrakk>p \<in> current_procs \<tau>; f \<notin> current_files \<tau>; parent f = Some pf; pf \<in> current_files \<tau>\<rbrakk> \<Longrightarrow>
+ os_grant \<tau> (CreateFile p f)"
+by simp
+
+lemma osgrant6:
+ "\<lbrakk>p \<in> current_procs \<tau>; u \<in> init_users\<rbrakk> \<Longrightarrow> os_grant \<tau> (ChangeOwner p u)"
+by simp
+
+lemma osgrant10:
+ "\<lbrakk>p \<in> current_procs \<tau>; p' = new_proc \<tau>\<rbrakk> \<Longrightarrow> os_grant \<tau> (Clone p p')"
+by simp
+
+
+lemma rcgrant1:
+ "\<lbrakk>is_parent f pf; is_file_type s pf t; is_current_role s p r;
+ default_fd_create_type r = InheritParent_file_type;
+ (r, File_type t, WRITE) \<in> compatible\<rbrakk>
+ \<Longrightarrow> rc_grant s (CreateFile p f)"
+by simp
+
+lemma rcgrant1':
+ "\<lbrakk>is_parent f pf; is_file_type s pf t; is_current_role s p r;
+ default_fd_create_type r = NormalFile_type t';
+ (r, File_type t, WRITE) \<in> compatible;
+ (r, File_type t', CREATE) \<in> compatible\<rbrakk>
+ \<Longrightarrow> rc_grant s (CreateFile p f)"
+by simp
+
+lemma rcgrant4:
+ "\<lbrakk>is_current_role s p r; is_file_type s f t; (r, File_type t, EXECUTE) \<in> compatible\<rbrakk>
+ \<Longrightarrow> rc_grant s (Execute p f)"
+by simp
+
+lemma rcgrant7:
+ "\<lbrakk>is_current_role s p r; r' \<in> comproles r\<rbrakk> \<Longrightarrow> rc_grant s (ChangeRole p r')"
+by simp
+
+lemma rcgrant_CHO:
+"\<lbrakk>is_current_role s p r;
+ type_of_process s p = Some t;
+ (r, Proc_type t, CHANGE_OWNER) \<in> compatible\<rbrakk> \<Longrightarrow> rc_grant s (ChangeOwner p u)"
+by(simp)
+
+lemma pf_in_current_paper:
+ "\<lbrakk>is_parent f pf; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> pf \<in> current_files s"
+by (simp add:parent_file_in_current)
+
+lemma dels:
+ shows "deleted (Proc p') ((Kill p p')#s)"
+ and "deleted (File f) ((DeleteFile p f)#s)"
+ and "deleted (IPC i) ((DeleteIPC p i)#s)"
+ and "deleted obj s \<Longrightarrow> deleted obj (e#s)"
+apply simp_all
+apply(case_tac e)
+apply(simp_all)
+done
+
+lemma tainted_10:
+ "\<lbrakk>(File f) \<in> tainted s; valid (e # s); f \<in> current_files (e # s)\<rbrakk>
+ \<Longrightarrow> (File f) \<in> tainted (e # s)"
+apply(rule tainted.intros)
+apply(assumption)
+apply(assumption)
+apply(simp only: exists.simps)
+done
+
+definition
+ Init ("init _")
+where
+ "Init obj \<equiv> exists [] obj"
+
+lemma Init_rhs:
+ shows "Init (File f) = (f \<in> init_files)"
+ and "Init (Proc p) = (p \<in> init_processes)"
+ and "Init (IPC i) = (i \<in> init_ipcs)"
+unfolding Init_def
+by(simp_all)
+
+notation (latex output)
+ Init ("_ \<in> init")
+
+lemma af_init':
+ "\<lbrakk>f \<in> init_files; is_file_type [] f t\<rbrakk>
+ \<Longrightarrow> SFile (t, f) (Some f) \<in> all_sobjs"
+apply(rule af_init)
+apply(simp)
+by (simp add:etype_of_file_def)
+
+declare [[show_question_marks = false]]
+
+
+(*>*)
+
+section {* Introduction *}
+
+text {*
+ Role-based access control models are used in many operating systems
+ for enforcing security properties. The
+ \emph{Role-Compatibility Model} (RC-Model), introduced by Ott
+ \cite{ottrc,ottthesis}, is one such role-based access control
+ model. It defines \emph{roles}, which are associated with processes,
+ and defines \emph{types}, which are associated with system
+ resources, such as files and directories. The RC-Model also includes
+ types for interprocess communication, that is message queues,
+ sockets and shared memory. A policy in the RC-Model gives every user
+ a default role, and also specifies how roles can be
+ changed. Moreover, it specifies which types of resources a role has
+ permission to access, and also the \emph{mode} with which the role
+ can access the resources, for example read, write, send, receive and
+ so on.
+
+ The RC-Model is built on top of a collection of system calls
+ provided by the operating system, for instance system calls for
+ reading and writing files, cloning and killing of processes, and
+ sending and receiving messages. The purpose of the RC-Model is to
+ restrict access to these system calls and thereby enforce security
+ properties of the system. A problem with the RC-Model and role-based
+ access control models in general is that a system administrator has
+ to specify an appropriate access control policy. The difficulty with
+ this is that \emph{``what you specify is what you get but not
+ necessarily what you want''} \cite[Page 242]{Jha08}. To overcome
+ this difficulty, a system administrator needs some kind of sanity
+ check for whether an access control policy is really securing
+ resources. Existing works, for example \cite{sanity01,sanity02},
+ provide sanity checks for policies by specifying properties and
+ using model checking techniques to ensure a policy at hand satisfies
+ these properties. However, these checks only address the problem on
+ the level of policies---they can only check ``on the surface''
+ whether the policy reflects the intentions of the system
+ administrator---these checks are not justified by the actual
+ behaviour of the operating system. The main problem this paper addresses is to check
+ when a policy matches the intentions of a system administrator
+ \emph{and} given such a policy, the operating system actually
+ enforces this policy.
+
+ Our work is related to the preliminary work by Archer et al
+ \cite{Archer03} about the security model of SELinux.
+ They also give a dynamic model of system calls on which the access
+ controls are implemented. Their dynamic model is defined in terms of
+ IO automata and mechanised in the PVS theorem prover. For specifying
+ and reasoning about automata they use the TAME tool in PVS. Their work checks
+ well-formedness properties of access policies by type-checking
+ generated definitions in PVS. They can also ensure some ``\emph{simple
+ properties}'' (their terminology), for example whether a process
+ with a particular PID is present in every reachable state from
+ an initial state. They also consider ``\emph{deeper properties}'', for
+ example whether only a process with root-permissions
+ or one of its descendents ever gets permission to write to kernel
+ log files. They write that they can state such deeper
+ properties about access policies, but about checking such properties
+ they write that ``\emph{the feasibility of doing
+ so is currently an open question}'' \cite[Page 167]{Archer03}.
+ We improve upon their results by using our sound and complete
+ static policy check to make this feasible.
+
+ Our formal models and correctness proofs are mechanised in the
+ interactive theorem prover Isabelle/HOL. The mechanisation of the models is a
+ prerequisite for any correctness proof about the RC-Model, since it
+ includes a large number of interdependent concepts and very complex
+ operations that determine roles and types. In our opinion it is
+ futile to attempt to reason about them by just using ``pencil-and-paper''.
+ Following good experience in earlier mechanisation work
+ \cite{ZhangUrbanWu12}, we use Paulson's inductive method for
+ reasoning about sequences of events \cite{Paulson98}. For example
+ we model system calls as events and reason about an inductive
+ definition of valid traces, that is lists of events. Central to
+ this paper is a notion of a resource being \emph{tainted}, which for
+ example means it contains a virus or a back door. We use our model
+ of system calls in order to characterise how such a tainted object
+ can ``spread'' through the system. For a system administrator the
+ important question is whether such a tainted file, possibly
+ introduced by a user, can affect core system files and render the
+ whole system insecure, or whether it can be contained by the access
+ policy. Our results show that a corresponding check can be performed
+ statically by analysing the initial state of the system and the access policy.
+ \smallskip
+
+ \noindent
+ {\bf Contributions:}
+ We give a complete formalisation of the RC-Model in the interactive
+ theorem prover Isabelle/HOL. We also give a dynamic model of the
+ operating system by formalising all security related events that can
+ happen while the system is running. As far as we are aware, we are
+ the first ones who formally prove that if a policy in the RC-Model
+ satisfies an access property, then there is no sequence of events
+ (system calls) that can violate this access property. We also prove
+ the opposite: if a policy does not meet an access property, then
+ there is a sequence of events that will violate this property in our
+ model of the operating system. With these two results in place we
+ can show that a static policy check is sufficient in order to
+ guarantee the access properties before running the system. Again as
+ far as we know, no such check that is the operating
+ system behaviour has been designed before.
+
+
+ %Specified dynamic behaviour of the system;
+ %we specified a static AC model; designed a tainted relation for
+ %the system; proved that they coincide.
+ %In our paper ....
+
+*}
+
+section {* Preliminaries about the RC-Model *}
+
+
+text {*
+ The Role-Compatibility Model (RC-Model) is a role-based access
+ control model. It has been introduced by Ott \cite{ottrc} and is
+ used in running systems for example to secure Apache servers. It
+ provides a more fine-grained control over access permissions than
+ simple Unix-style access control models. This more fine-grained
+ control solves the problem of server processes running as root with
+ too many access permissions in order to accomplish a task at
+ hand. In the RC-Model, system administrators are able to restrict
+ what the role of server is allowed to do and in doing so reduce the
+ attack surface of a system.
+
+ Policies in the RC-Model talk about \emph{users}, \emph{roles},
+ \emph{types} and \emph{objects}. Objects are processes, files or
+ IPCs (interprocess communication objects---such as message queues,
+ sockets and shared memory). Objects are the resources of a system an
+ RC-policy can restrict access to. In what follows we use the letter
+ @{term u} to stand for users, @{text r} for roles, @{term p} for
+ processes, @{term f} for files and @{term i} for IPCs. We also
+ use @{text obj} as a generic variable for objects.
+ The RC-Model has the following eight kinds of access modes to objects:
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \begin{tabular}{@ {}l}
+ @{term READ}, @{term WRITE}, @{term EXECUTE}, @{term "CHANGE_OWNER"},
+ @{term CREATE}, @{term SEND}, @{term RECEIVE} and @{term DELETE}
+ \end{tabular}
+ \end{isabelle}
+
+ In the RC-Model, roles group users according to tasks they need to
+ accomplish. Users have a default role specified by the policy,
+ which is the role they start with whenever they log into the system.
+ A process contains the information about its owner (a user), its
+ role and its type, whereby a type in the RC-Model allows system
+ administrators to group resources according to a common criteria.
+ Such detailed information is needed in the RC-Model, for example, in
+ order to allow a process to change its ownership. For this the
+ RC-Model checks the role of the process and its type: if the access
+ control policy states that the role has @{term CHANGE_OWNER} access mode for
+ processes of that type, then the process is permitted to assume a
+ new owner.
+
+ Files in the RC-Model contain the information about their types. A
+ policy then specifies whether a process with a given role can access
+ a file under a certain access mode. Files, however, also
+ include in the RC-Model information about roles. This information is
+ used when a process is permitted to execute a file. By doing so it
+ might change its role. This is often used in the context of
+ web-servers when a cgi-script is uploaded and then executed by the
+ server. The resulting process should have much more restricted
+ access permissions. This kind of behaviour when executing a file can
+ be specified in an RC-policy in several ways: first, the role of the
+ process does not change when executing a file; second, the process
+ takes on the role specified with the file; or third, use the role of
+ the owner, who currently owns this process. The RC-Model also makes
+ assumptions on how types can change. For example for files and IPCs
+ the type can never change once they are created. But processes can
+ change their types according to the roles they have.
+
+ As can be seen, the information contained in a policy in the
+ RC-Model can be rather complex: Roles and types, for example, are
+ policy-dependent, meaning each policy needs to define a set of roles and a
+ set of types. Apart from recording for each role the information
+ which type of resource it can access and under which access-mode, it
+ also needs to include a role compatibility set. This set specifies how one
+ role can change into another role. Moreover it needs to include default
+ information for cases when new processes or files are created.
+ For example, when a process clones itself, the type of the new
+ process is determined as follows: the policy might specify a default
+ type whenever a process with a certain role is cloned, or the policy
+ might specify that the cloned process inherits the type of the
+ parent process.
+
+ Ott implemented the RC-Model on top of Linux, but only specified it
+ as a set of informal rules, partially given as logic formulas,
+ partially given as rules in ``English''. Unfortunately, some
+ presentations about the RC-Model give conflicting definitions for
+ some concepts---for example when defining the semantics of the special role
+ ``inherit parent''. In \cite{ottrc} it means inherit the initial role
+ of the parent directory, but in \cite{ottweb} it means inherit
+ the role of the parent process. In our formalisation we mainly follow the
+ version given in \cite{ottrc}. In the next section we give a mechanised
+ model of the system calls on which the RC-Model is implemented.
+*}
+
+
+
+section {* Dynamic Model of System Calls *}
+
+text {*
+ Central to the RC-Model are processes, since they initiate any action
+ involving resources and access control. We use natural numbers to stand for process IDs,
+ but do not model the fact that the number of processes in any practical
+ system is limited. Similarly, IPCs and users are represented by natural
+ numbers. The thirteen actions a process can perform are represented by
+ the following datatype of \emph{events}
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{
+ \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l@ {\hspace{3mm}}l@
+ {\hspace{1.5mm}}l@ {\hspace{3mm}}l@ {\hspace{1.5mm}}l@
+ {\hspace{3mm}}l@ {\hspace{1.5mm}}l}
+ event
+ & @{text "::="} & @{term "CreateFile p f"} & @{text "|"} & @{term "ReadFile p f"} & @{text "|"} & @{term "Send p i"} & @{text "|"} & @{term "Kill p p'"} \\
+ & @{text "|"} & @{term "WriteFile p f"} & @{text "|"} & @{term "Execute p f"} & @{text "|"} & @{term "Recv p i"}\\
+ & @{text "|"} & @{term "DeleteFile p f"} & @{text "|"} & @{term "Clone p p'"} & @{text "|"} & @{term "CreateIPC p i"} \\
+ & @{text "|"} & @{term "ChangeOwner p u"} & @{text "|"} & @{term "ChangeRole p r"} & @{text "|"} & @{term "DeleteIPC p i"}\\
+ \end{tabular}}
+ \end{isabelle}
+
+ \noindent
+ with the idea that for example in @{term Clone} a process @{term p} is cloned
+ and the new process has the ID @{term "p'"}; with @{term Kill} the
+ intention is that the process @{term p} kills another process with
+ ID @{term p'}. We will later give the definition what the role
+ @{term r} can stand for in the constructor @{term ChangeRole}
+ (namely \emph{normal roles} only). As is custom in Unix, there is no
+ difference between a directory and a file. The files @{term f} in
+ the definition above are simply lists of strings. For example, the
+ file @{text "/usr/bin/make"} is represented by the list @{text
+ "[make, bin, usr]"} and the @{text root}-directory is the @{text
+ Nil}-list. Following the presentation in \cite{ottrc}, our model of
+ IPCs is rather simple-minded: we only have events for creation and deletion Of IPCs,
+ as well as sending and receiving messages.
+
+ Events essentially transform one state of the system into
+ another. The system starts with an initial state determining which
+ processes, files and IPCs are active at the start of the system. We assume the
+ users of the system are fixed in the initial state; we also assume
+ that the policy does not change while the system is running. We have
+ three sets, namely
+ @{term init_processes},
+ @{term init_files} and
+ @{term init_ipcs}
+ specifying the processes, files and IPCs present in the initial state.
+ We will often use the abbreviation
+
+ \begin{center}
+ @{thm (lhs) Init_def} @{text "\<equiv>"}
+ @{thm (rhs) Init_rhs(1)[where f=obj]} @{text "\<or>"}
+ @{thm (rhs) Init_rhs(2)[where p=obj]} @{text "\<or>"}
+ @{thm (rhs) Init_rhs(3)[where i=obj]}
+ \end{center}
+
+ \noindent
+ There are some assumptions we make about the files present in the initial state: we always
+ require that the @{text "root"}-directory @{term "[]"} is part of the initial state
+ and for every file in the initial state (excluding @{term "[]"}) we require that its
+ parent is also part of the
+ initial state.
+ After the initial state, the next states are determined
+ by a list of events, called the \emph{trace}. We need to define
+ functions that allow us to make some observations about traces. One
+ such function is called @{term "current_procs"} and
+ calculates the set of ``alive'' processes in a state:
+
+ %initial state:
+ %We make assumptions about the initial state, they're:
+ %1. there exists a set of processes, files, IPCs and users already in the initial state,
+ %users are not changed in system's running, we regards users adding and deleting a
+ %administration task, not the issue for our policy checker;
+ %2. every object in the initial state have got already roles/types/owner ... information assigned;
+ %3. all the policy information are already preloaded in the initial state, including:
+ %a compatible type table, @{term compatible};
+ %a mapping function from a role to its compatible role set, @{term comproles};
+ %every role's default values is pre-set, e.g. default process create type and
+ %and default file/directory create type.
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+ @{thm (lhs) current_procs.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) current_procs.simps(1)}\\
+ @{thm (lhs) current_procs.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) current_procs.simps(2)}\\
+ @{thm (lhs) current_procs.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) current_procs.simps(3)}\\
+ @{term "current_procs (DUMMY#s)"} & @{text "\<equiv>"} & @{term "current_procs s"}
+ \end{tabular}}
+ \end{isabelle}
+
+ \noindent
+ The first clause states that in the empty trace, that is initial
+ state, the processes are given by @{text "init_processes"}. The
+ events for cloning a process, respectively killing a process, update this
+ set of processes appropriately. Otherwise the set of live
+ processes is unchanged. We have similar functions for alive files and
+ IPCs, called @{term "current_files"} and @{term "current_ipcs"}.
+
+ We can use these function in order to formally model which events are
+ \emph{admissible} by the operating system in each state. We show just three
+ rules that give the gist of this definition. First the rule for changing
+ an owner of a process:
+
+ \begin{center}
+ @{thm[mode=Rule] osgrant6}
+ \end{center}
+
+ \noindent
+ We require that the process @{text p} is alive in the state @{text s}
+ (first premise) and that the new owner is a user that existed in the initial state
+ (second premise).
+ Next the rule for creating a new file:
+
+ \begin{center}
+ @{thm[mode=Rule] osgrant2}
+ \end{center}
+
+ \noindent
+ It states that
+ a file @{text f} can be created by a process @{text p} being alive in the state @{text s},
+ the new file does not exist already in this state and there exists
+ a parent file @{text "pf"} for the new file. The parent file is just
+ the tail of the list representing @{text f}. % if it exists
+ %(@{text "Some"}-case) or @{text None} if it does not.
+ Finally, the rule for cloning a process:
+
+ \begin{center}
+ @{thm[mode=Rule] osgrant10}
+ \end{center}
+
+ \noindent
+ Clearly the operating system should only allow to clone a process @{text p} if the
+ process is currently alive. The cloned process will get the process
+ ID generated by the function @{term new_proc}. This process ID should
+ not already exist. Therefore we define @{term new_proc} as
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+ @{term "new_proc s"} & @{text "\<equiv>"} & @{term "Max (current_procs s) + 1"}
+ \end{tabular}}
+ \end{isabelle}
+
+ \noindent
+ namely the highest ID currently in existence increased by one. The
+ admissibility rules for the other events impose similar conditions.
+
+ However, the admissibility check by the operating system is only one
+ ``side'' of the constraints the RC-Model imposes. We also need to
+ model the constraints of the access policy. For this we introduce
+ separate @{text granted}-rules involving the sets @{text
+ permissions} and @{text "compatible r"}: the former contains triples
+ describing access control rules; the latter specifies for each role @{text r}
+ which roles are compatible with @{text r}. These sets are used in the
+ RC-Model when a process having a role @{text r} takes on a new role
+ @{text r'}. For example, a login-process might belong to root;
+ once the user logs in, however, the role of the process should change to
+ the user's default role. The corresponding @{text "granted"}-rule is
+ as follows
+
+ \begin{center}
+ @{thm[mode=Rule] rcgrant7}
+ \end{center}
+
+ \noindent
+ where we check whether the process @{text p} has currently role @{text r} and
+ whether the RC-policy states that @{text r'} is in the role compatibility
+ set of @{text r}.
+
+ The complication in the RC-Model arises from the
+ way how the current role of a process in a state @{text s} is
+ calculated---represented by the predicate @{term is_current_role} in our formalisation.
+ For defining this predicate we need to trace the role of a process from
+ the initial state to the current state. In the
+ initial state all processes have the role given by the function
+ @{term "init_current_role"}. If a @{term Clone} event happens then
+ the new process will inherit the role from the parent
+ process. Similarly, if a @{term ChangeRole} event happens, then
+ as seen in the rule above we just change the role accordingly. More interesting
+ is an @{term Execute} event in the RC-Model. For this event we have
+ to check the role attached to the file to be executed.
+ There are a number of cases: If the role of the file is a
+ \emph{normal} role, then the process will just take on this role
+ when executing the file (this is like the setuid mechanism in Unix). But
+ there are also four \emph{special} roles in the RC-Model:
+ @{term "InheritProcessRole"}, @{term "InheritUserRole"},
+ @{term "InheritParentRole"} and @{term
+ InheritUpMixed}. For example, if a file to be executed has
+ @{term "InheritProcessRole"} attached to it, then the process
+ that executes this file keeps its role regardless of the information
+ attached to the file. In this way programs can be can quarantined;
+ @{term "InheritUserRole"} can be used for login shells
+ to make sure they run with the user's default role.
+ The purpose of the other special roles is to determine the
+ role of a process according to the directory in which the
+ files are stored.
+
+ Having the notion of current role in place, we can define the
+ granted rule for the @{term Execute}-event: Suppose a process @{term
+ p} wants to execute a file @{text f}. The RC-Model first fetches the
+ role @{text r} of this process (in the current state @{text s}) and
+ the type @{text t} of the file. It then checks if the tuple @{term
+ "(r, t, EXECUTE)"} is part of the policy, that is in our
+ formalisation being an element in the set @{term compatible}. The
+ corresponding rule is as follows
+
+ \begin{center}
+ @{thm[mode=Rule] rcgrant4}
+ \end{center}
+
+ \noindent
+ The next @{text granted}-rule concerns the @{term CreateFile} event.
+ If this event occurs, then we have two rules in our RC-Model
+ depending on how the type of the created file is derived. If the type is inherited
+ from the parent directory @{text pf}, then the @{term granted}-rule is as follows:
+
+ \begin{center}
+ @{thm[mode=Rule] rcgrant1}
+ \end{center}
+
+ \noindent
+ We check whether @{term pf} is the parent file (directory) of @{text f} and check
+ whether the type of @{term pf} is @{term t}. We also need to fetch the
+ the role @{text r} of the process that seeks to get permission for creating
+ the file. If the default type of this role @{text r} states that the
+ type of the newly created file will be inherited from the parent file
+ type, then we only need to check that the policy states that @{text r}
+ has permission to write into the directory @{text pf}.
+
+ The situation is different if the default type of role @{text r} is
+ some \emph{normal} type, like text-file or executable. In such cases we want
+ that the process creates some predetermined type of files. Therefore in the
+ rule we have to check whether the role is allowed to create a file of that
+ type, and also check whether the role is allowed to write any new
+ file into the parent file (directory). The corresponding rule is
+ as follows.
+
+ \begin{center}
+ @{thm[mode=Rule] rcgrant1'}
+ \end{center}
+
+ \noindent
+ Interestingly, the type-information in the RC-model is also used for
+ processes, for example when they need to change their owner. For
+ this we have the rule
+
+ \begin{center}
+ @{thm[mode=Rule] rcgrant_CHO}
+ \end{center}
+
+ \noindent
+ whereby we have to obtain both the role and type of the process @{term p}, and then check
+ whether the policy allows a @{term ChangeOwner}-event for that role and type.
+
+ Overall we have 13 rules for the admissibility check by the operating system and
+ 14 rules for the granted check by the RC-Model.
+ They are used to characterise when an event @{text e} is \emph{valid} to
+ occur in a state @{text s}. This can be inductively defined as the set of valid
+ states.
+
+ \begin{center}
+ \begin{tabular}{@ {}c@ {}}
+ \mbox{@{thm [mode=Axiom] valid.intros(1)}}\hspace{5mm}
+ \mbox{@{thm [mode=Rule] valid.intros(2)}}
+ \end{tabular}
+ \end{center}
+
+ The novel notion we introduce in this paper is the @{text tainted}
+ relation. It characterises how a system can become infected when
+ a file in the system contains, for example, a virus. We assume
+ that the initial state contains some tainted
+ objects (we call them @{term "seeds"}). Therefore in the initial state @{term "[]"}
+ an object is tainted, if it is an element in @{text "seeds"}.
+
+ \begin{center}
+ \mbox{@{thm [mode=Rule] tainted.intros(1)}}
+ \end{center}
+
+ \noindent
+ Let us first assume such a tainted object is a file @{text f}.
+ If a process reads or executes a tainted file, then this process becomes
+ tainted (in the state where the corresponding event occurs).
+
+ \begin{center}
+ \mbox{@{thm [mode=Rule] tainted.intros(3)}}\hspace{3mm}
+ \mbox{@{thm [mode=Rule] tainted.intros(6)}}
+ \end{center}
+
+ \noindent
+ We have a similar rule for a tainted IPC, namely
+
+ \begin{center}
+ \mbox{@{thm [mode=Rule] tainted.intros(9)}}
+ \end{center}
+
+ \noindent
+ which means if we receive anything from a tainted IPC, then
+ the process becomes tainted. A process is also tainted
+ when it is a produced by a @{text Clone}-event.
+
+ \begin{center}
+ \mbox{@{thm [mode=Rule] tainted.intros(2)}}
+ \end{center}
+
+ \noindent
+ However, the tainting relationship must also work in the
+ ``other'' direction, meaning if a process is tainted, then
+ every file that is written or created will be tainted.
+ This is captured by the four rules:
+
+ \begin{center}
+ \begin{tabular}{c}
+ \mbox{@{thm [mode=Rule] tainted.intros(4)}} \hspace{3mm}
+ \mbox{@{thm [mode=Rule] tainted.intros(7)}} \medskip\\
+ \mbox{@{thm [mode=Rule] tainted.intros(5)}} \hspace{3mm}
+ \mbox{@{thm [mode=Rule] tainted.intros(8)}}
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ Finally, we have three rules that state whenever an object is tainted
+ in a state @{text s}, then it will be still tainted in the
+ next state @{term "e#s"}, provided the object is still \emph{alive}
+ in that state. We have such a rule for each kind of objects, for
+ example for files the rule is:
+
+ \begin{center}
+ \mbox{@{thm [mode=Rule] tainted_10}}
+ \end{center}
+
+ \noindent
+ Similarly for alive processes and IPCs (then respectively with premises
+ @{term "p \<in> current_procs (e#s)"} and @{term "i \<in> current_ipcs (e#s)"}).
+ When an object present in the initial state can be tainted in
+ \emph{some} state (system run), we say it is @{text "taintable"}:
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{\begin{tabular}{lcl}
+ @{thm (lhs) taintable_def} & @{text "\<equiv>"} & @{term "init obj"} @{text "\<and>"} @{thm (rhs) taintable_def}
+ \end{tabular}}
+ \end{isabelle}
+
+ Before we can describe our static check deciding when a file is taintable, we
+ need to describe the notions @{term deleted} and @{term undeletable}
+ for objects. The former characterises whether there is an event that deletes
+ these objects (files, processes or IPCs). For this we have the following
+ four rules:
+
+ \begin{center}
+ \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+ \begin{tabular}{c}
+ @{thm [mode=Axiom] dels(1)}\\[-2mm]
+ @{thm [mode=Axiom] dels(2)}\\[-2mm]
+ @{thm [mode=Axiom] dels(3)}
+ \end{tabular} &
+ @{thm [mode=Rule] dels(4)}
+ \end{tabular}
+ \end{center}
+
+
+ \noindent
+ Note that an object cannot be deleted in the initial state @{text
+ "[]"}. An object is then said to be @{text "undeletable"} provided
+ it did exist in the initial state and there does not exists a valid
+ state in which the object is deleted:
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
+ @{thm (lhs) undeletable_def} & @{text "\<equiv>"} & %%@{thm (rhs) undeletable_def}
+ @{term "init obj \<and> \<not>(\<exists> s. (valid s \<and> deleted obj s))"}
+ \end{tabular}}
+ \end{isabelle}
+
+ \noindent
+ The point of this definition is that our static taintable check will only be
+ complete for undeletable objects. But these are
+ the ones system administrators are typically interested in (for
+ example system files). It should be clear, however, that we cannot
+ hope for a meaningful check by just trying out all possible
+ valid states in our dynamic model. The reason is that there are
+ potentially infinitely many of them and therefore the search space would be
+ infinite. For example staring from an
+ initial state containing a process @{text p} and a file @{text pf},
+ we can create files @{text "f\<^isub>1"}, @{text "f\<^isub>2"}, @{text "..."}
+ via @{text "CreateFile"}-events. This can be pictured roughly as follows:
+
+ \begin{center}
+ \begin{tabular}[t]{c@ {\hspace{-8mm}}c@ {\hspace{-8mm}}c@ {\hspace{-8mm}}c@ {\hspace{-8mm}}cc}
+ \begin{tabular}[t]{c}
+ Initial state:\\
+ @{term "{p, pf}"}
+ \end{tabular} &
+ \begin{tabular}[t]{c}
+ \\
+ @{text "\<Longrightarrow>"}\\[2mm]
+ {\small@{term "CreateFile p (f\<^isub>1#pf)"}}
+ \end{tabular}
+ &
+ \begin{tabular}[t]{c}
+ \\
+ @{term "{p, pf, f\<^isub>1#pf}"}
+ \end{tabular}
+ &
+ \begin{tabular}[t]{c}
+ \\
+ @{text "\<Longrightarrow>"}\\[2mm]
+ {\small@{term "CreateFile p (f\<^isub>2#f\<^isub>1#pf)"}}
+ \end{tabular}
+ &
+ \begin{tabular}[t]{c}
+ \\
+ @{term "{p, pf, f\<^isub>1#pf, f\<^isub>2#f\<^isub>1#pf}"}
+ \end{tabular} &
+ \begin{tabular}[t]{c}
+ \\
+ @{text "..."}\\
+ \end{tabular}
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ Instead, the idea of our static check is to use
+ the policies of the RC-model for generating an answer, since they
+ provide always a finite ``description of the system''. As we
+ will see in the next section, this needs some care, however.
+*}
+
+section {* Our Static Check *}
+
+text {*
+ Assume there is a tainted file in the system and suppose we face the
+ problem of finding out whether this file can affect other files,
+ IPCs or processes? One idea is to work on the level of policies only, and
+ check which operations are permitted by the role and type of this
+ file. Then one builds the ``transitive closure'' of this information
+ and checks for example whether the role @{text root} has become
+ affected, in which case the whole system is compromised. This is indeed the solution investigated
+ in~\cite{guttman2005verifying} in the context of information flow
+ and SELinux.
+
+ Unfortunately, restricting the calculations to only use policies is
+ too simplistic for obtaining a check that is sound and complete---it
+ over-approximates the dynamic tainted relation defined in the previous
+ section. To see the problem consider
+ the case where the tainted file has, say, the type @{text bin}. If
+ the RC-policy contains a role @{text r} that can both read and write
+ @{text bin}-files, we would conclude that all @{text bin}-files can potentially
+ be tainted. That
+ is indeed the case, \emph{if} there is a process having this role @{text
+ r} running in the system. But if there is \emph{not}, then the
+ tainted file cannot ``spread''. A similar problem arises in case there
+ are two processes having the same role @{text r}, and this role is
+ restricted to read files only. Now if one of the processes is tainted, then
+ the simple check involving only policies would incorrectly infer
+ that all processes involving that role are tainted. But since the
+ policy for @{text r} is restricted to be read-only, there is in fact
+ no danger that both processes can become tainted.
+
+ The main idea of our sound and complete check is to find a ``middle'' ground between
+ the potentially infinite dynamic model and the too coarse
+ information contained in the RC-policies. Our solution is to
+ define a ``static'' version of the tainted relation, called @{term
+ "tainted_s"}, that records relatively precisely the information
+ about the initial state of the system (the one in which an object
+ might be a @{term seed} and therefore tainted). However,
+ we are less precise about the objects created in every subsequent
+ state. The result is that we can avoid the potential infinity of
+ the dynamic model.
+ For the @{term tainted_s}-relation we will consider the following
+ three kinds of \emph{items} recording the information we need about
+ processes, files and IPCs, respectively:
+
+ \begin{center}
+ \begin{tabular}{l@ {\hspace{5mm}}l}
+ & Recorded information:\smallskip\\
+ Processes: & @{term "SProc (r, dr, t, u) po"}\\
+ Files: & @{term "SFile (t, a) fo"}\\
+ IPCs: & @{term "SIPC (t) io"}
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ For a process we record its role @{text r}, its default role @{text dr} (used to determine
+ the role when executing a file or changing the owner of a process), its type @{text t}
+ and its owner @{text u}. For a file we record
+ just the type @{text t} and its @{term "source_dir"} @{text a} (we define this
+ notion shortly). For IPCs we only record its type @{text t}. Note the superscripts
+ @{text po}, @{text fo} and @{text io} in each item. They are optional arguments and depend on
+ whether the corresponding object is present in the initial state or not.
+ If it \emph{is}, then for processes and IPCs we will record @{term "Some(id)"},
+ where @{text id} is the natural number that uniquely identifies a process or IPC;
+ for files we just record their path @{term "Some(f)"}. If the object is
+ \emph{not} present in the initial state, that is newly created, then we just have
+ @{term None} as superscript.
+ Let us illustrate the different superscripts with the following example
+ where the initial state contains a process @{term p} and a file (directory)
+ @{term pf}. Then this
+ process creates a file via a @{term "CreateFile"}-event and after that reads
+ the created file via a @{term Read}-event:
+
+ \begin{center}
+ \begin{tabular}[t]{ccccc}
+ \begin{tabular}[t]{c}
+ Initial state:\\
+ @{term "{p, pf}"}
+ \end{tabular} &
+ \begin{tabular}[t]{c}
+ \\
+ @{text "\<Longrightarrow>"}\\
+ {\small@{term "CreateFile p (f#pf)"}}
+ \end{tabular}
+ &
+ \begin{tabular}[t]{c}
+ \\
+ @{term "{p, pf, f#pf}"}
+ \end{tabular}
+ &
+ \begin{tabular}[t]{c}
+ \\
+ @{text "\<Longrightarrow>"}\\
+ {\small@{term "ReadFile p (f#pf)"}}
+ \end{tabular}
+ &
+ \begin{tabular}[t]{c}
+ \\
+ @{term "{p, pf, f#pf}"}
+ \end{tabular}
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ For the two objects in the initial state our static check records
+ the information @{term "SProc (r, dr, t, u) (Some(p))"} and @{term
+ "SFile (t', a) (Some(pf))"} (assuming @{text "r"}, @{text t} and so
+ on are the corresponding roles, types etc). In both cases we have
+ the superscript @{text "Some(...)"} since they are objects present
+ in the initial state. For the file @{term "f#pf"} created by the
+ @{term "CreateFile"}-event, we record @{term "SFile (t', a')
+ (None)"}, since it is a newly created file. The @{text
+ "ReadFile"}-event does not change the set of objects, therefore no
+ new information needs to be recorded. The problem we are avoiding
+ with this setup of recording the precise information for the initial
+ state is where two processes have the same role and type
+ information, but only one is tainted in the initial state, but the
+ other is not. The recorded unique process IDs allows us to
+ distinguish between both processes. For all newly created objects,
+ on the other hand, we do not care. This is crucial, because
+ otherwise exploring all possible ``reachable'' objects can lead to
+ the potential infinity like in the dynamic model.
+
+ An @{term source_dir} for a file is the ``nearest'' directory that
+ is present in the initial state and has not been deleted in a state
+ @{text s}. Its definition is the recursive function
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{\begin{tabular}{lcl}
+ @{thm (lhs) source_dir.simps(1)} & @{text "\<equiv>"} \;\; &
+ @{text "if"} @{text "\<not> deleted [] s"} @{text "then"} @{term "Some []"} @{text "else"} @{term "None"}\\
+ @{thm (lhs) source_dir.simps(2)} & @{text "\<equiv>"} &
+ @{text "if"} @{term "(f#pf) \<in> init_files \<and> \<not>(deleted (File (f#pf)) s)"}\\
+ & & @{text "then"} @{term "Some (f#pf)"} @{text "else"} @{term "source_dir s pf"}\\
+ \end{tabular}}
+ \end{isabelle}
+
+ \noindent
+ generating an optional value.
+ The first clause states that the anchor of the @{text
+ root}-directory is always its own anchor unless it has been
+ deleted. If a file is present in the initial state and not deleted
+ in @{text s}, then it is also its own anchor, otherwise the anchor
+ will be the anchor of the parent directory. For example if we have
+ a directory @{text pf} in the initial state, then its anchor is @{text "Some pf"}
+ (assuming it is not deleted). If we create a new file in this directory,
+ say @{term "f#pf"}, then its anchor will also be @{text "Some pf"}.
+ The purpose of @{term source_dir} is to determine the
+ role information when a file is executed, because the role of the
+ corresponding process, according to the RC-model, is determined by the role information of the
+ anchor of the file to be executed.
+
+ There is one last problem we have to solve before we can give the
+ rules of our @{term "tainted_s"}-check. Suppose an RC-policy
+ includes the rule @{text "(r, foo, Write) \<in> permissions"}, that is
+ a process of role @{text "r"} is allowed to write files of type @{text "foo"}.
+ If there is a tainted process with this role, we would conclude that
+ also every file of that type can potentially become tainted. However, that
+ is not the case if the initial state does not contain any file
+ with type @{text foo} and the RC-policy does not allow the
+ creation of such files, that is does not contain an access rule
+ @{text "(r, foo, Create) \<in> permissions"}. In a sense the original
+ @{text "(r, foo, Write)"} is ``useless'' and should not contribute
+ to the relation characterising the objects that are tainted.
+ To exclude such ``useless'' access rules, we define
+ a relation @{term "all_sobjs"} restricting our search space
+ to only configurations that correspond to states in our dynamic model.
+ We first have a rule for reachable items of the form @{text "F(t, f)\<^bsup>Some f\<^esup>"}
+ where the file @{text f} with type @{text t} is present in
+ the initial state.
+
+ \begin{center}
+ @{thm [mode=Rule] af_init'}
+ \end{center}
+
+ \noindent
+ We have similar reachability rules for processes and IPCs that are part of the
+ initial state. Next is the reachability rule in case a file is created
+
+ \begin{center}
+ @{thm [mode=Rule] af_cfd[where sd=a and sf="fo" and sp="po" and fr="dr"]}
+ \end{center}
+
+ \noindent
+ where we require that we have a reachable parent directory, recorded
+ as @{text "F(t, a)\<^bsup>fo\<^esup>"}, and also a
+ process that can create the file, recorded as @{text "P(r, dr, pt,
+ u)\<^bsup>po\<^esup>"}. As can be seen, we also require that we have both @{text "(r, t,
+ Write)"} and \mbox{@{text "(r, t', Create)"}} in the @{text permissions} set
+ for this rule to apply. If we did \emph{not} impose this requirement
+ about the RC-policy, then there would be no way to create a file
+ with @{term "NormalFileType t'"} according to our ``dynamic'' model.
+ However in case we want to create a
+ file of type @{term InheritPatentType}, then we only need the access-rule
+ @{text "(r, t, Write)"}:
+
+ \begin{center}
+ @{thm [mode=Rule] af_cfd'[where sd=a and sf="fo" and sp="po" and fr="dr"]}
+ \end{center}
+
+ \noindent
+ We also have reachability rules for processes executing files, and
+ for changing their roles and owners, for example
+
+ \begin{center}
+ @{thm [mode=Rule] ap_crole[where sp="po" and fr="dr"]}
+ \end{center}
+
+ \noindent
+ which states that when we have a process with role @{text r}, and the role
+ @{text "r'"} is in the corresponding role-compatibility set, then also
+ a process with role @{text "r'"} is reachable.
+
+ The crucial difference between between the ``dynamic'' notion of validity
+ and the ``static'' notion of @{term "all_sobjs"}
+ is that there can be infinitely many valid states, but assuming the initial
+ state contains only finitely many objects, then also @{term "all_sobjs"} will
+ be finite. To see the difference, consider the infinite ``chain'' of events
+ just cloning a process @{text "p\<^isub>0"}:
+
+ \begin{center}
+ \begin{tabular}[t]{c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}cc}
+ \begin{tabular}[t]{c}
+ Initial state:\\
+ @{term "{p\<^isub>0}"}
+ \end{tabular} &
+ \begin{tabular}[t]{c}
+ \\
+ @{text "\<Longrightarrow>"}\\[2mm]
+ {\small@{term "Clone p\<^isub>0 p\<^isub>1"}}
+ \end{tabular}
+ &
+ \begin{tabular}[t]{c}
+ \\
+ @{term "{p\<^isub>0, p\<^isub>1}"}
+ \end{tabular}
+ &
+ \begin{tabular}[t]{c}
+ \\
+ @{text "\<Longrightarrow>"}\\[2mm]
+ {\small@{term "Clone p\<^isub>0 p\<^isub>2"}}
+ \end{tabular}
+ &
+ \begin{tabular}[t]{c}
+ \\
+ @{term "{p\<^isub>0, p\<^isub>1, p\<^isub>2}"}
+ \end{tabular} &
+ \begin{tabular}[t]{c}
+ \\
+ @{text "..."}\\
+ \end{tabular}
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ The corresponding reachable objects are
+
+ \begin{center}
+ \begin{tabular}[t]{cccc}
+ \begin{tabular}[t]{c}
+ @{text "{P(r, dr, t, u)\<^bsup>Some (p\<^isub>0)\<^esup>}"}
+ \end{tabular} &
+ \begin{tabular}[t]{c}
+ @{text "\<Longrightarrow>"}
+ \end{tabular}
+ &
+ \begin{tabular}[t]{c}
+ @{text "{P(r, dr, t, u)\<^bsup>Some (p\<^isub>0)\<^esup>, P(r, dr, t, u)\<^bsup>None\<^esup>}"}
+ \end{tabular}
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ where no further progress can be made because the information
+ recorded about @{text "p\<^isub>2"}, @{text "p\<^isub>3"} and so on is just the same
+ as for @{text "p\<^isub>1"}, namely @{text "P(r, dr, t, u)\<^bsup>None\<^esup>"}. Indeed we
+ can prove the lemma:
+
+ \begin{lemma}\label{finite}
+ If @{text "finite init"}, then @{term "finite all_sobjs"}.
+ \end{lemma}
+
+ \noindent
+ This fact of @{term all_sobjs} being finite enables us to design a
+ decidable tainted-check. For this we introduce inductive rules defining the
+ set @{term "tainted_s"}. Like in the ``dynamic'' version of tainted,
+ if an object is element of @{text seeds}, then it is @{term "tainted_s"}.
+
+ \begin{center}
+ @{thm [mode=Rule] ts_init}
+ \end{center}
+
+ \noindent
+ The function @{text "\<lbrakk>_\<rbrakk>"} extracts the static information from an object.
+ For example for a process it extracts the role, default role, type and
+ user; for a file the type and the anchor. If a process in tainted and creates
+ a file with a normal type @{text "t'"} then also the created file
+ is tainted. The corresponding rule is
+
+ \begin{center}
+ @{thm [mode=Rule] ts_cfd[where sd=a and sf="fo" and sp="po" and fr="dr"]}
+ \end{center}
+
+ \noindent
+ If a tainted process creates a file that inherits the type of the directory,
+ then the file will also be tainted:
+
+ \begin{center}
+ @{thm [mode=Rule] ts_cfd'[where sd=a and sf="fo" and sp="po" and fr="dr"]}
+ \end{center}
+
+ \noindent
+ If a tainted process changes its role, then also with this changed role
+ it will be tainted:
+
+ \begin{center}
+ @{thm [mode=Rule] ts_crole[where pt=t and sp="po" and fr="dr"]}
+ \end{center}
+
+ \noindent
+ Similarly when a process changes its owner. If a file is tainted, and
+ a process has read-permission to that type of files, then the
+ process becomes tainted. The corresponding rule is
+
+ \begin{center}
+ @{thm [mode=Rule] ts_read[where sd=a and sf="fo" and sp="po" and fr="dr"]}
+ \end{center}
+
+ \noindent
+ If a process is tainted and it has write-permission for files of type @{text t},
+ then these files will be tainted:
+
+ \begin{center}
+ @{thm [mode=Rule] ts_write[where sd=a and sf="fo" and sp="po" and fr="dr"]}
+ \end{center}
+
+ \noindent
+ We omit the remaining rules for executing a file, cloning a process and
+ rules involving IPCs, which are similar. A simple consequence of our definitions
+ is that every tainted object is also reachable:
+
+ \begin{lemma}
+ @{text "tainted\<^isup>s \<subseteq> reachable\<^isup>s"}
+ \end{lemma}
+
+ \noindent
+ which in turn means that the set of @{term "tainted_s"} items is finite by Lemma~\ref{finite}.
+
+ Returning to our original question about whether tainted objects can spread
+ in the system. To answer this question, we take these tainted objects as
+ seeds and calculate the set of items that are @{term "tainted_s"}. We proved this
+ set is finite and can be enumerated using the rules for @{term tainted_s}.
+ However, this set is about items, not about whether objects are tainted or not.
+ Assuming an item in @{term tainted_s} arises from an object present in the initial
+ state, we have recorded enough information to translate items back into objects
+ via the function @{text "|_|"}:
+
+ \begin{center}
+ \begin{tabular}{lcl}
+ @{text "|P(r, dr, t, u)\<^bsup>po\<^esup>|"} & @{text "\<equiv>"} & @{text po}\\
+ @{text "|F(t, a)\<^bsup>fo\<^esup>|"} & @{text "\<equiv>"} & @{text fo}\\
+ @{text "|I(t\<^bsup>\<^esup>)\<^bsup>io\<^esup>|"} & @{text "\<equiv>"} & @{text io}
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ Using this function, we can define when an object is @{term taintable_s} in terms of
+ an item being @{term tainted_s}, namely
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{\begin{tabular}{lcl}
+ @{thm (lhs) taintable_s_def} & @{text "\<equiv>"} & @{text "\<exists>item. item \<in> tainted\<^isup>s \<and> |item| = Some obj"}
+ \end{tabular}}
+ \end{isabelle}
+
+ \noindent
+ Note that @{term taintable_s} is only about objects that are present in
+ the initial state, because for all other items @{text "|_|"} returns @{text None}.
+
+
+ With these definitions in place, we can state our theorem about the soundness of our
+ static @{term taintable_s}-check for objects.
+
+ \begin{theorem}[Soundness]
+ @{thm [mode=IfThen] static_sound}
+ \end{theorem}
+
+ \noindent
+ The proof of this theorem generates for every object that is ``flagged'' as
+ @{term taintable_s} by our check, a sequence of events which shows how the
+ object can become tainted in the dynamic model. We can also state a completeness
+ theorem for our @{term taintable_s}-check.
+
+ \begin{theorem}[Completeness]
+ @{thm [mode=IfThen] static_complete}
+ \end{theorem}
+
+ \noindent
+ This completeness theorem however needs to be restricted to
+ undeletebale objects. The reason is that a tainted process can be
+ killed by another process, and after that can be ``recreated'' by a
+ cloning event from an untainted process---remember we have no control
+ over which process ID a process will be assigned with. Clearly, in
+ this case the cloned process should be considered untainted, and
+ indeed our dynamic tainted relation is defined in this way. The
+ problem is that a static test cannot know about a process being
+ killed and then recreated. Therefore the static test will not be
+ able to ``detect'' the difference. Therefore we solve this problem
+ by considering only objects that are present in the initial state
+ and cannot be deleted. By the latter we mean that the RC-policy
+ stipulates an object cannot be deleted (for example it has been created
+ by @{term root} in single-user mode, but in the everyday running
+ of the system the RC-policy forbids to delete an object belonging to
+ @{term root}). Like @{term "taintable_s"}, we also have a static check
+ for when a file is undeletable according to an RC-policy.
+
+ This restriction to undeletable objects might be seen as a great
+ weakness of our result, but in practice this seems to cover the
+ interesting scenarios encountered by system administrators. They
+ want to know whether a virus-infected file introduced by a user can
+ affect the core system files. Our test allows the system
+ administrator to find this out provided the RC-policy makes the core
+ system files undeletable. We assume that this provisio is already part
+ of best practice rule for running a system.
+
+ We envisage our test to be useful in two kind of situations: First, if
+ there was a break-in into a system, then, clearly, the system
+ administrator can find out whether the existing access policy was
+ strong enough to contain the break-in, or whether core system files
+ could have been affected. In the first case, the system
+ administrator can just plug the hole and forget about the break-in;
+ in the other case the system administrator is wise to completely
+ reinstall the system.
+ Second, the system administrator can proactively check whether an
+ RC-policy is strong enough to withstand serious break-ins. To do so
+ one has to identify the set of ``core'' system files that the policy
+ should protect and mark every possible entry point for an attacker
+ as tainted (they are the seeds of the @{term "tainted_s"} relation).
+ Then the test will reveal
+ whether the policy is strong enough or needs to be redesigned. For
+ this redesign, the sequence of events our check generates should be
+ informative.
+*}
+
+
+
+
+
+section {*Conclusion and Related Works*}
+
+
+text {*
+ We have presented the first completely formalised dynamic model of
+ the Role-Compa\-tibility Model. This is a framework, introduced by Ott
+ \cite{ottrc}, in which role-based access control policies
+ can be formulated and is used in practice, for example, for securing Apache
+ servers. Previously, the RC-Model was presented as a
+ collection of rules partly given in ``English'', partly given as formulas.
+ During the formalisation we uncovered an inconsistency in the
+ semantics of the special role @{term "InheritParentRole"} in
+ the existing works about the RC-Model \cite{ottrc,ottweb}. By proving
+ the soundness and completeness of our static @{term
+ "taintable_s"}-check, we have formally related the dynamic behaviour
+ of the operating system implementing access control and the static
+ behaviour of the access policies of the RC-Model. The
+ crucial idea in our static check is to record precisely the
+ information available about the initial state (in which some resources might be
+ tainted), but be less precise
+ about the subsequent states. The former fact essentially gives us
+ the soundness of our check, while the latter results in a finite
+ search space.
+
+ The two most closely related works are by Archer et al and by Guttman et al
+ \cite{Archer03,guttman2005verifying}. The first describes a
+ formalisation of the dynamic behaviour of SELinux carried out in the
+ theorem prover PVS. However, they cannot use their formalisation in
+ order to prove any ``deep'' properties about access control rules
+ \cite[Page 167]{Archer03}. The second analyses access control
+ policies in the context of information flow. Since this work
+ is completely on the level of policies, it does
+ not lead to a sound and complete check for files being taintable (a dynamic notion
+ defined in terms of operations performed by the operating system).
+ While our results concern the RC-Model, we expect that they
+ equally apply to the access control model of SELinux. In fact,
+ we expect that the formalisation is simpler for SELinux, since
+ its rules governing roles are much simpler than in the RC-Model.
+ The definition of our admissibility rules can be copied verbatim for SELinux;
+ we would need to modify our granted rules and slightly adapt our
+ static check. We leave this as future work.
+
+
+ Our formalisation is carried out in the Isabelle/HOL theorem prover.
+ It uses Paulson's inductive method for
+ reasoning about sequences of events \cite{Paulson98}.
+ We have approximately 1000 lines of code for definitions and 6000 lines of
+ code for proofs. Our formalisation is available from the
+ Mercurial repository at \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/rc/}.\\[-12mm]
+
+
+% 0. Not Policy-Analysis: cause even policy is analysed correct, there is still a gap between it and policy application to the real Access Control system. Hence here Our dynamic model is bridging this gap. Policy-Analysis "basic" based on "Information flow", but it is not enough: the static "write" right to a certain typed file do not mean a process having this right definitely can write the file, it has to pass a "particular" "Control Flow" to achieve the state of "There are this typed file and this righted process"!
+% 1. Both Dynamic and Statical analysis, and proved link between two \\
+% 2. Tainting Relation Formalisation \\
+% 3. Formalisation and Verification than Model Checking \\
+% 4. Universal Checker of Policy \\
+% 5. source of RC rules made more precise \\
+% 6. RC example of Webserver with CGIs (key notion: Program Based Roles) \\
+% 7. RBAC is more Policy-lever(with HUGE companies, many stablised num of roles but frequently varifying num of users); RC is more Program Base Roles, set for system with a lot of program based default value, once pre-setted, it will remains after running. which is key to policy checker.
+
+%The distinct feature of RC is to deal with program based roles, such as server behaviour.
+%This is in contrast to usual RSBAC models where roles are modeled around a hierachy, for
+%example in a company.
+
+
+%In a word, what the manager need is that given the
+%initial state of the system, a policy checker that make sure the under the policy
+%he made, this important file cannot: 1. be deleted; 2. be tainted.
+%Formally speaking, this policy-checker @{text "PC"} (a function that given the
+%initial state of system, a policy and an object, it tells whether this object
+%will be fully protected or not) should satisfy this criteria:
+
+% @{text "(PC init policy obj) \<and> (exists init obj) \<longrightarrow> \<not> taintable obj"}
+%If the @{text obj} exists in the initial-state, and @{text "PC"} justify the safety
+%of this object under @{text "policy"}, this object should not be @{text taintable}.
+%We call this criteria the \emph{completeness} of @{text "PC"}.
+%And there is the \emph{soundness} criteria of @{text "PC"} too, otherwise a "NO-to-ALL"
+%answer always satisfy the \emph{completeness}. \emph{soundness} formally is:
+% @{text "PC init policy obj \<longrightarrow> taintable obj"}
+
+%This policy-checker should satisfy other properties:
+% 1. fully statical, that means this policy-checker should not rely on the system
+%running information, like new created files/process, and most importantly the
+%trace of system running.
+% 2. decidable, that means this policy-checker should always terminate.
+
+
+% The purpose of an operating system is to provide a common
+% interface for accessing resources. This interface is typically
+% realised as a collection of system calls, for example for reading
+% and writing files, forking of processes, or sending and receiving
+% messages. Role based access control is one approach for
+% restricting access to such system calls: if a user has
+% suffient rights, then a system call can be performed.
+
+% a user might have
+% one or more roles and acces is granted if the role has sufficent
+% rights
+
+% static world...make predictions about accessing
+% files, do they translate into actual systems behaviour.
+
+
+*}
+
+
+(*<*)
+end
+
+end
+(*>*)
+
+(*
+
+ Central to RC-Model is the roles and types. We start with do formalisation on
+ types first.
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{
+ \begin{tabular}{r@ {\hspace{1mm}}l@ {\hspace{2mm}}l}
+ @{text t_client} & @{text "="} & @{text "Christian"} \\
+ & @{text "|"} & @{text "Chunhan"} \\
+ & @{text "|"} & @{text " ... "} \\
+ \end{tabular}}
+
+ \mbox{
+ \begin{tabular}{r@ {\hspace{1mm}}l@ {\hspace{2mm}}l@ {\hspace{2mm}}l}
+ @{text t_normal_file_type} & @{text "="} & @{text "WebServerLog_file"} & \\
+ & @{text "|"} & @{text "WebData_file"} & @{text t_client} \\
+ & @{text "|"} & @{text "CGI_file"} & @{text t_client} \\
+ & @{text "|"} & @{text "Private_file"} & @{text t_client}
+ \end{tabular}}
+
+ \mbox{
+ \begin{tabular} {r@ {\hspace{1mm}}l@ {\hspace{5mm}}l}
+ @{text t_rc_file_type}
+ & @{text "="} & @{term "InheritParent_file_type"} \\
+ & @{text "|"} & @{term "NormalFile_type t_normal_file_type"}
+ \end{tabular}}
+ \end{isabelle}
+
+ @{term "type_of_file"} function calculates the current type for the files:
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{\begin{tabular}{lcl}
+ @{thm (lhs) type_of_file.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) type_of_file.simps(1)}\\
+ @{thm (lhs) type_of_file.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) type_of_file.simps(2)}\\
+ @{term "type_of_file (DUMMY#s)"} & @{text "\<equiv>"} & @{term "type_of_file s"}
+ \end{tabular}}
+ \end{isabelle}
+
+ Note that this @{term "type_of_file"} is not the function @{term "etype_of_file"}
+ that we call in the grant check of RC-Model, @{term "rc_grant"}. The reason is
+ that file's type can be set to a special type of @{term "InheritParent_file_type"},
+ means that the ``efficient'' type of this file is the efficient type of its directory.
+ \mbox{\begin{tabular}{lcl}
+ @{thm (lhs) etype_aux.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) etype_aux.simps(1)}\\
+ @{thm (lhs) etype_aux.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) etype_aux.simps(2)}\smallskip\\
+ @{thm (lhs) etype_of_file_def} & @{text "\<equiv>"} & @{thm (rhs) etype_of_file_def}
+ \end{tabular}}
+ Here @{term etype_aux} is an auxiliary function which do recursion
+ on the pathname of files. By the way, in our proofs, we do proved
+ that functions like @{term "etype_of_file"} will always return
+ ``normal'' values.
+
+
+ We have similar observation functions calculating the current type for processes
+ and IPCs too, only diffence here is that there is no ``effcient'' type here for
+ processes and IPCs, all types that calculated by @{term "type_of_process"} and
+ @{term "type_of_ipc"} are alrealdy efficient types.
+
+*}
+
+text {*
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{
+ \begin{tabular}{r@ {\hspace{1mm}}l@ {\hspace{2mm}}l@ {\hspace{2mm}}l}
+ @{text t_normal_role} & @{text "="} & @{text "WebServer"} & \\
+ & @{text "|"} & @{text "WS_client"} & @{text t_client} \\
+ & @{text "|"} & @{text "UpLoader"} & @{text t_client} \\
+ & @{text "|"} & @{text "CGI "} & @{text t_client}
+ \end{tabular}}
+
+ \mbox{
+ \begin{tabular} {r@ {\hspace{1mm}}l@ {\hspace{2mm}}l@ {\hspace{5mm}}l}
+ @{text t_role}
+ & @{text "="} & @{term "InheritParentRole"} & ``for file's initial/forced role,
+ meaning using parent directory's
+ role instead'' \\
+ & @{text "|"} & @{term "UseForcedRole"} & ``for file's initial role'' \\
+ & @{text "|"} & @{term "InheritProcessRole"} & ``using process' current role''\\
+ & @{text "|"} & @{term "InheritUserRole"} & ``using owner's default role''\\
+ & @{text "|"} & ... & \\
+ & @{text "|"} & @{term "NormalRole t_normal_role"} & ``user-defined
+ policy roles"
+ \end{tabular}}
+ \end{isabelle}
+
+ @{text "t_normal roles"} are normally user-defined roles in the
+ policy, where @{text "WebServer"} is the role who plays for the
+ server, while @{text "WS_client"} is the role server plays for
+ certain client, so is for @{text "UpLoader"} role. @{text "CGI"} is
+ the role that client's programme scripts play.
+
+ @{term "currentrole"} function calculates the current role of process, here we
+ only show 3 cases of its definition, it responses to @{term "ChangeOwner"},
+ @{term "ChangeRole"} events too.
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{\begin{tabular}{lcl}
+ @{thm (lhs) currentrole.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) currentrole.simps(1)}\\
+ @{thm (lhs) currentrole.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) currentrole.simps(2)}\\
+ @{thm (lhs) currentrole.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) currentrole.simps(3)}
+ \end{tabular}}
+ \end{isabelle}
+
+ If the event trace is @{term "[]"}, means the
+ system state currently is the initial state, then @{term "init_currentrole"} will
+ do. @{term "Execute p f"} event is one complex case, when this event happens, process
+ @{term p}'s role will be changed according to the efficient initial role of the
+ executable file @{term f}, here ``efficient'' is like the file's type too.
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{\begin{tabular}{lcl}
+ @{thm (lhs) initialrole.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) initialrole.simps(1)}\\
+ @{thm (lhs) initialrole.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) initialrole.simps(2)}\\
+ @{thm (lhs) initialrole.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) initialrole.simps(3)}\medskip\\
+
+ @{thm (lhs) erole_functor.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) erole_functor.simps(1)}\\
+ @{thm (lhs) erole_functor.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) erole_functor.simps(2)}
+ \end{tabular}}
+ \end{isabelle}
+
+ If this efficient initial role is normal role, then RC-Model assigns
+ this role to the process after execution finished. Otherwise if this
+ efficient initial role is using special value @{term
+ "UseForcedRole"}, then the new role for the process is then
+ determinated by the efficient forced role of the executable file
+ @{term "forcedrole"}. When new process is created, this process'
+ role is assigned to its creator's role.
+*)
\ No newline at end of file