(*<*)

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\<^sup>s") and

  tainted_s ("tainted\<^sup>s") and

  all_sobjs ("reachable\<^sup>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.