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