(*<*)theory Paperimports 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 autoconsts DUMMY::'aabbreviation "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 simplemma osgrant6: "\<lbrakk>p \<in> current_procs \<tau>; u \<in> init_users\<rbrakk> \<Longrightarrow> os_grant \<tau> (ChangeOwner p u)"by simplemma osgrant10: (* modified by chunhan *) "\<lbrakk>p \<in> current_procs \<tau>; p' \<notin> current_procs \<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 simplemma 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 simplemma 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 simplemma rcgrant7: "\<lbrakk>is_current_role s p r; r' \<in> comproles r\<rbrakk> \<Longrightarrow> rc_grant s (ChangeRole p r')"by simplemma 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_allapply(case_tac e)apply(simp_all)donelemma 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)donedefinition 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_defby(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 functions 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 (* HERE ????? chunhan *) \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 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 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 starting 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 ID 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 is 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 proviso 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]%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.*}(*<*)endend(*>*)(* 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.*}*)