(*<*)
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: (* 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 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 has been designed and proved correct 
  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 *)
text {*
  \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.

*}





(*<*)
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.

*}
*)