(*<*)
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.
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 ``randomly'' generated by the operating system, but this process ID should
not already exist. The admissibility rules for the other events impose similar conditions.
However, the admissibility check by the operating system is only one
``side'' of the constraints the RC-Model imposes. We also need to
model the constraints of the access policy. For this we introduce
separate @{text granted}-rules involving the sets @{text
permissions} and @{text "compatible r"}: the former contains triples
describing access control rules; the latter specifies for each role @{text r}
which roles are compatible with @{text r}. These sets are used in the
RC-Model when a process having a role @{text r} takes on a new role
@{text r'}. For example, a login-process might belong to root;
once the user logs in, however, the role of the process should change to
the user's default role. The corresponding @{text "granted"}-rule is
as follows
\begin{center}
@{thm[mode=Rule] rcgrant7}
\end{center}
\noindent
where we check whether the process @{text p} has currently role @{text r} and
whether the RC-policy states that @{text r'} is in the role compatibility
set of @{text r}.
The complication in the RC-Model arises from the
way the current role of a process in a state @{text s} is
calculated---represented by the predicate @{term is_current_role} in our formalisation.
For defining this predicate we need to trace the role of a process from
the initial state to the current state. In the
initial state all processes have the role given by the function
@{term "init_current_role"}. If a @{term Clone} event happens then
the new process will inherit the role from the parent
process. Similarly, if a @{term ChangeRole} event happens, then
as seen in the rule above we just change the role accordingly. More interesting
is an @{term Execute} event in the RC-Model. For this event we have
to check the role attached to the file to be executed.
There are a number of cases: If the role of the file is a
\emph{normal} role, then the process will just take on this role
when executing the file (this is like the setuid mechanism in Unix). But
there are also four \emph{special} roles in the RC-Model:
@{term "InheritProcessRole"}, @{term "InheritUserRole"},
@{term "InheritParentRole"} and @{term
InheritUpMixed}. For example, if a file to be executed has
@{term "InheritProcessRole"} attached to it, then the process
that executes this file keeps its role regardless of the information
attached to the file. In this way programs can be can quarantined;
@{term "InheritUserRole"} can be used for login shells
to make sure they run with the user's default role.
The purpose of the other special roles is to determine the
role of a process according to the directory in which the
files are stored.
Having the notion of current role in place, we can define the
granted rule for the @{term Execute}-event: Suppose a process @{term
p} wants to execute a file @{text f}. The RC-Model first fetches the
role @{text r} of this process (in the current state @{text s}) and
the type @{text t} of the file. It then checks if the tuple @{term
"(r, t, EXECUTE)"} is part of the policy, that is in our
formalisation being an element in the set @{term compatible}. The
corresponding rule is as follows
\begin{center}
@{thm[mode=Rule] rcgrant4}
\end{center}
\noindent
The next @{text granted}-rule concerns the @{term CreateFile} event.
If this event occurs, then we have two rules in our RC-Model
depending on how the type of the created file is derived. If the type is inherited
from the parent directory @{text pf}, then the @{term granted}-rule is as follows:
\begin{center}
@{thm[mode=Rule] rcgrant1}
\end{center}
\noindent
We check whether @{term pf} is the parent file (directory) of @{text f} and check
whether the type of @{term pf} is @{term t}. We also need to fetch
the role @{text r} of the process that seeks to get permission for creating
the file. If the default type of this role @{text r} states that the
type of the newly created file will be inherited from the parent file
type, then we only need to check that the policy states that @{text r}
has permission to write into the directory @{text pf}.
The situation is different if the default type of role @{text r} is
some \emph{normal} type, like text-file or executable. In such cases we want
that the process creates some predetermined type of files. Therefore in the
rule we have to check whether the role is allowed to create a file of that
type, and also check whether the role is allowed to write any new
file into the parent file (directory). The corresponding rule is
as follows.
\begin{center}
@{thm[mode=Rule] rcgrant1'}
\end{center}
\noindent
Interestingly, the type-information in the RC-model is also used for
processes, for example when they need to change their owner. For
this we have the rule
\begin{center}
@{thm[mode=Rule] rcgrant_CHO}
\end{center}
\noindent
whereby we have to obtain both the role and type of the process @{term p}, and then check
whether the policy allows a @{term ChangeOwner}-event for that role and type.
Overall we have 13 rules for the admissibility check by the operating system and
14 rules for the granted check by the RC-Model.
They are used to characterise when an event @{text e} is \emph{valid} to
occur in a state @{text s}. This can be inductively defined as the set of valid
states.
\begin{center}
\begin{tabular}{@ {}c@ {}}
\mbox{@{thm [mode=Axiom] valid.intros(1)}}\hspace{5mm}
\mbox{@{thm [mode=Rule] valid.intros(2)}}
\end{tabular}
\end{center}
The novel notion we introduce in this paper is the @{text tainted}
relation. It characterises how a system can become infected when
a file in the system contains, for example, a virus. We assume
that the initial state contains some tainted
objects (we call them @{term "seeds"}). Therefore in the initial state @{term "[]"}
an object is tainted, if it is an element in @{text "seeds"}.
\begin{center}
\mbox{@{thm [mode=Rule] tainted.intros(1)}}
\end{center}
\noindent
Let us first assume such a tainted object is a file @{text f}.
If a process reads or executes a tainted file, then this process becomes
tainted (in the state where the corresponding event occurs).
\begin{center}
\mbox{@{thm [mode=Rule] tainted.intros(3)}}\hspace{3mm}
\mbox{@{thm [mode=Rule] tainted.intros(6)}}
\end{center}
\noindent
We have a similar rule for a tainted IPC, namely
\begin{center}
\mbox{@{thm [mode=Rule] tainted.intros(9)}}
\end{center}
\noindent
which means if we receive anything from a tainted IPC, then
the process becomes tainted. A process is also tainted
when it is a produced by a @{text Clone}-event.
\begin{center}
\mbox{@{thm [mode=Rule] tainted.intros(2)}}
\end{center}
\noindent
However, the tainting relationship must also work in the
``other'' direction, meaning if a process is tainted, then
every file that is written or created will be tainted.
This is captured by the four rules:
\begin{center}
\begin{tabular}{c}
\mbox{@{thm [mode=Rule] tainted.intros(4)}} \hspace{3mm}
\mbox{@{thm [mode=Rule] tainted.intros(7)}} \medskip\\
\mbox{@{thm [mode=Rule] tainted.intros(5)}} \hspace{3mm}
\mbox{@{thm [mode=Rule] tainted.intros(8)}}
\end{tabular}
\end{center}
\noindent
Finally, we have three rules that state whenever an object is tainted
in a state @{text s}, then it will be still tainted in the
next state @{term "e#s"}, provided the object is still \emph{alive}
in that state. We have such a rule for each kind of objects, for
example for files the rule is:
\begin{center}
\mbox{@{thm [mode=Rule] tainted_10}}
\end{center}
\noindent
Similarly for alive processes and IPCs (then respectively with premises
@{term "p \<in> current_procs (e#s)"} and @{term "i \<in> current_ipcs (e#s)"}).
When an object present in the initial state can be tainted in
\emph{some} state (system run), we say it is @{text "taintable"}:
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{lcl}
@{thm (lhs) taintable_def} & @{text "\<equiv>"} & @{term "init obj"} @{text "\<and>"} @{thm (rhs) taintable_def}
\end{tabular}}
\end{isabelle}
Before we can describe our static check deciding when a file is taintable, we
need to describe the notions @{term deleted} and @{term undeletable}
for objects. The former characterises whether there is an event that deletes
these objects (files, processes or IPCs). For this we have the following
four rules:
\begin{center}
\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
\begin{tabular}{c}
@{thm [mode=Axiom] dels(1)}\\[-2mm]
@{thm [mode=Axiom] dels(2)}\\[-2mm]
@{thm [mode=Axiom] dels(3)}
\end{tabular} &
@{thm [mode=Rule] dels(4)}
\end{tabular}
\end{center}
\noindent
Note that an object cannot be deleted in the initial state @{text
"[]"}. An object is then said to be @{text "undeletable"} provided
it did exist in the initial state and there does not exists a valid
state in which the object is deleted:
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
@{thm (lhs) undeletable_def} & @{text "\<equiv>"} & %%@{thm (rhs) undeletable_def}
@{term "init obj \<and> \<not>(\<exists> s. (valid s \<and> deleted obj s))"}
\end{tabular}}
\end{isabelle}
\noindent
The point of this definition is that our static taintable check will only be
complete for undeletable objects. But these are
the ones system administrators are typically interested in (for
example system files). It should be clear, however, that we cannot
hope for a meaningful check by just trying out all possible
valid states in our dynamic model. The reason is that there are
potentially infinitely many of them and therefore the search space would be
infinite. For example starting from an
initial state containing a process @{text p} and a file @{text pf},
we can create files @{text "f\<^sub>1"}, @{text "f\<^sub>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\<^sub>1#pf)"}}
\end{tabular}
&
\begin{tabular}[t]{c}
\\
@{term "{p, pf, f\<^sub>1#pf}"}
\end{tabular}
&
\begin{tabular}[t]{c}
\\
@{text "\<Longrightarrow>"}\\[2mm]
{\small@{term "CreateFile p (f\<^sub>2#f\<^sub>1#pf)"}}
\end{tabular}
&
\begin{tabular}[t]{c}
\\
@{term "{p, pf, f\<^sub>1#pf, f\<^sub>2#f\<^sub>1#pf}"}
\end{tabular} &
\begin{tabular}[t]{c}
\\
@{text "..."}\\
\end{tabular}
\end{tabular}
\end{center}
\noindent
Instead, the idea of our static check is to use
the policies of the RC-model for generating an answer, since they
provide always a finite ``description of the system''. As we
will see in the next section, this needs some care, however.
*}
section {* Our Static Check *}
text {*
Assume there is a tainted file in the system and suppose we face the
problem of finding out whether this file can affect other files,
IPCs or processes? One idea is to work on the level of policies only, and
check which operations are permitted by the role and type of this
file. Then one builds the ``transitive closure'' of this information
and checks for example whether the role @{text root} has become
affected, in which case the whole system is compromised. This is indeed the solution investigated
in~\cite{guttman2005verifying} in the context of information flow
and SELinux.
Unfortunately, restricting the calculations to only use policies is
too simplistic for obtaining a check that is sound and complete---it
over-approximates the dynamic tainted relation defined in the previous
section. To see the problem consider
the case where the tainted file has, say, the type @{text bin}. If
the RC-policy contains a role @{text r} that can both read and write
@{text bin}-files, we would conclude that all @{text bin}-files can potentially
be tainted. That
is indeed the case, \emph{if} there is a process having this role @{text
r} running in the system. But if there is \emph{not}, then the
tainted file cannot ``spread''. A similar problem arises in case there
are two processes having the same role @{text r}, and this role is
restricted to read files only. Now if one of the processes is tainted, then
the simple check involving only policies would incorrectly infer
that all processes involving that role are tainted. But since the
policy for @{text r} is restricted to be read-only, there is in fact
no danger that both processes can become tainted.
The main idea of our sound and complete check is to find a ``middle'' ground between
the potentially infinite dynamic model and the too coarse
information contained in the RC-policies. Our solution is to
define a ``static'' version of the tainted relation, called @{term
"tainted_s"}, that records relatively precisely the information
about the initial state of the system (the one in which an object
might be a @{term seed} and therefore tainted). However,
we are less precise about the objects created in every subsequent
state. The result is that we can avoid the potential infinity of
the dynamic model.
For the @{term tainted_s}-relation we will consider the following
three kinds of \emph{items} recording the information we need about
processes, files and IPCs, respectively:
\begin{center}
\begin{tabular}{l@ {\hspace{5mm}}l}
& Recorded information:\smallskip\\
Processes: & @{term "SProc (r, dr, t, u) po"}\\
Files: & @{term "SFile (t, a) fo"}\\
IPCs: & @{term "SIPC (t) io"}
\end{tabular}
\end{center}
\noindent
For a process we record its role @{text r}, its default role @{text dr} (used to determine
the role when executing a file or changing the owner of a process), its type @{text t}
and its owner @{text u}. For a file we record
just the type @{text t} and its @{term "source_dir"} @{text a} (we define this
notion shortly). For IPCs we only record its type @{text t}. Note the superscripts
@{text po}, @{text fo} and @{text io} in each item. They are optional arguments and depend on
whether the corresponding object is present in the initial state or not.
If it \emph{is}, then for processes and IPCs we will record @{term "Some(id)"},
where @{text id} is the natural number that uniquely identifies a process or IPC;
for files we just record their path @{term "Some(f)"}. If the object is
\emph{not} present in the initial state, that is newly created, then we just have
@{term None} as superscript.
Let us illustrate the different superscripts with the following example
where the initial state contains a process @{term p} and a file (directory)
@{term pf}. Then this
process creates a file via a @{term "CreateFile"}-event and after that reads
the created file via a @{term Read}-event:
\begin{center}
\begin{tabular}[t]{ccccc}
\begin{tabular}[t]{c}
Initial state:\\
@{term "{p, pf}"}
\end{tabular} &
\begin{tabular}[t]{c}
\\
@{text "\<Longrightarrow>"}\\
{\small@{term "CreateFile p (f#pf)"}}
\end{tabular}
&
\begin{tabular}[t]{c}
\\
@{term "{p, pf, f#pf}"}
\end{tabular}
&
\begin{tabular}[t]{c}
\\
@{text "\<Longrightarrow>"}\\
{\small@{term "ReadFile p (f#pf)"}}
\end{tabular}
&
\begin{tabular}[t]{c}
\\
@{term "{p, pf, f#pf}"}
\end{tabular}
\end{tabular}
\end{center}
\noindent
For the two objects in the initial state our static check records
the information @{term "SProc (r, dr, t, u) (Some(p))"} and @{term
"SFile (t', a) (Some(pf))"} (assuming @{text "r"}, @{text t} and so
on are the corresponding roles, types etc). In both cases we have
the superscript @{text "Some(...)"} since they are objects present
in the initial state. For the file @{term "f#pf"} created by the
@{term "CreateFile"}-event, we record @{term "SFile (t', a')
(None)"}, since it is a newly created file. The @{text
"ReadFile"}-event does not change the set of objects, therefore no
new information needs to be recorded. The problem we are avoiding
with this setup of recording the precise information for the initial
state is where two processes have the same role and type
information, but only one is tainted in the initial state, but the
other is not. The recorded unique process ID allows us to
distinguish between both processes. For all newly created objects,
on the other hand, we do not care. This is crucial, because
otherwise exploring all possible ``reachable'' objects can lead to
the potential infinity like in the dynamic model.
An @{term source_dir} for a file is the ``nearest'' directory that
is present in the initial state and has not been deleted in a state
@{text s}. Its definition is the recursive function
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{lcl}
@{thm (lhs) source_dir.simps(1)} & @{text "\<equiv>"} \;\; &
@{text "if"} @{text "\<not> deleted [] s"} @{text "then"} @{term "Some []"} @{text "else"} @{term "None"}\\
@{thm (lhs) source_dir.simps(2)} & @{text "\<equiv>"} &
@{text "if"} @{term "(f#pf) \<in> init_files \<and> \<not>(deleted (File (f#pf)) s)"}\\
& & @{text "then"} @{term "Some (f#pf)"} @{text "else"} @{term "source_dir s pf"}\\
\end{tabular}}
\end{isabelle}
\noindent
generating an optional value.
The first clause states that the anchor of the @{text
root}-directory is always its own anchor unless it has been
deleted. If a file is present in the initial state and not deleted
in @{text s}, then it is also its own anchor, otherwise the anchor
will be the anchor of the parent directory. For example if we have
a directory @{text pf} in the initial state, then its anchor is @{text "Some pf"}
(assuming it is not deleted). If we create a new file in this directory,
say @{term "f#pf"}, then its anchor will also be @{text "Some pf"}.
The purpose of @{term source_dir} is to determine the
role information when a file is executed, because the role of the
corresponding process, according to the RC-model, is determined by the role information of the
anchor of the file to be executed.
There is one last problem we have to solve before we can give the
rules of our @{term "tainted_s"}-check. Suppose an RC-policy
includes the rule @{text "(r, foo, Write) \<in> permissions"}, that is
a process of role @{text "r"} is allowed to write files of type @{text "foo"}.
If there is a tainted process with this role, we would conclude that
also every file of that type can potentially become tainted. However, that
is not the case if the initial state does not contain any file
with type @{text foo} and the RC-policy does not allow the
creation of such files, that is does not contain an access rule
@{text "(r, foo, Create) \<in> permissions"}. In a sense the original
@{text "(r, foo, Write)"} is ``useless'' and should not contribute
to the relation characterising the objects that are tainted.
To exclude such ``useless'' access rules, we define
a relation @{term "all_sobjs"} restricting our search space
to only configurations that correspond to states in our dynamic model.
We first have a rule for reachable items of the form @{text "F(t, f)\<^bsup>Some f\<^esup>"}
where the file @{text f} with type @{text t} is present in
the initial state.
\begin{center}
@{thm [mode=Rule] af_init'}
\end{center}
\noindent
We have similar reachability rules for processes and IPCs that are part of the
initial state. Next is the reachability rule in case a file is created
\begin{center}
@{thm [mode=Rule] af_cfd[where sd=a and sf="fo" and sp="po" and fr="dr"]}
\end{center}
\noindent
where we require that we have a reachable parent directory, recorded
as @{text "F(t, a)\<^bsup>fo\<^esup>"}, and also a
process that can create the file, recorded as @{text "P(r, dr, pt,
u)\<^bsup>po\<^esup>"}. As can be seen, we also require that we have both @{text "(r, t,
Write)"} and \mbox{@{text "(r, t', Create)"}} in the @{text permissions} set
for this rule to apply. If we did \emph{not} impose this requirement
about the RC-policy, then there would be no way to create a file
with @{term "NormalFileType t'"} according to our ``dynamic'' model.
However in case we want to create a
file of type @{term InheritPatentType}, then we only need the access-rule
@{text "(r, t, Write)"}:
\begin{center}
@{thm [mode=Rule] af_cfd'[where sd=a and sf="fo" and sp="po" and fr="dr"]}
\end{center}
\noindent
We also have reachability rules for processes executing files, and
for changing their roles and owners, for example
\begin{center}
@{thm [mode=Rule] ap_crole[where sp="po" and fr="dr"]}
\end{center}
\noindent
which states that when we have a process with role @{text r}, and the role
@{text "r'"} is in the corresponding role-compatibility set, then also
a process with role @{text "r'"} is reachable.
The crucial difference between between the ``dynamic'' notion of validity
and the ``static'' notion of @{term "all_sobjs"}
is that there can be infinitely many valid states, but assuming the initial
state contains only finitely many objects, then also @{term "all_sobjs"} will
be finite. To see the difference, consider the infinite ``chain'' of events
just cloning a process @{text "p\<^sub>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\<^sub>0}"}
\end{tabular} &
\begin{tabular}[t]{c}
\\
@{text "\<Longrightarrow>"}\\[2mm]
{\small@{term "Clone p\<^sub>0 p\<^sub>1"}}
\end{tabular}
&
\begin{tabular}[t]{c}
\\
@{term "{p\<^sub>0, p\<^sub>1}"}
\end{tabular}
&
\begin{tabular}[t]{c}
\\
@{text "\<Longrightarrow>"}\\[2mm]
{\small@{term "Clone p\<^sub>0 p\<^sub>2"}}
\end{tabular}
&
\begin{tabular}[t]{c}
\\
@{term "{p\<^sub>0, p\<^sub>1, p\<^sub>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\<^sub>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\<^sub>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\<^sub>2"}, @{text "p\<^sub>3"} and so on is just the same
as for @{text "p\<^sub>1"}, namely @{text "P(r, dr, t, u)\<^bsup>None\<^esup>"}. Indeed we
can prove the lemma:
\begin{lemma}\label{finite}
If @{text "finite init"}, then @{term "finite all_sobjs"}.
\end{lemma}
\noindent
This fact of @{term all_sobjs} being finite enables us to design a
decidable tainted-check. For this we introduce inductive rules defining the
set @{term "tainted_s"}. Like in the ``dynamic'' version of tainted,
if an object is element of @{text seeds}, then it is @{term "tainted_s"}.
\begin{center}
@{thm [mode=Rule] ts_init}
\end{center}
\noindent
The function @{text "\<lbrakk>_\<rbrakk>"} extracts the static information from an object.
For example for a process it extracts the role, default role, type and
user; for a file the type and the anchor. If a process is tainted and creates
a file with a normal type @{text "t'"} then also the created file
is tainted. The corresponding rule is
\begin{center}
@{thm [mode=Rule] ts_cfd[where sd=a and sf="fo" and sp="po" and fr="dr"]}
\end{center}
\noindent
If a tainted process creates a file that inherits the type of the directory,
then the file will also be tainted:
\begin{center}
@{thm [mode=Rule] ts_cfd'[where sd=a and sf="fo" and sp="po" and fr="dr"]}
\end{center}
\noindent
If a tainted process changes its role, then also with this changed role
it will be tainted:
\begin{center}
@{thm [mode=Rule] ts_crole[where pt=t and sp="po" and fr="dr"]}
\end{center}
\noindent
Similarly when a process changes its owner. If a file is tainted, and
a process has read-permission to that type of files, then the
process becomes tainted. The corresponding rule is
\begin{center}
@{thm [mode=Rule] ts_read[where sd=a and sf="fo" and sp="po" and fr="dr"]}
\end{center}
\noindent
If a process is tainted and it has write-permission for files of type @{text t},
then these files will be tainted:
\begin{center}
@{thm [mode=Rule] ts_write[where sd=a and sf="fo" and sp="po" and fr="dr"]}
\end{center}
\noindent
We omit the remaining rules for executing a file, cloning a process and
rules involving IPCs, which are similar. A simple consequence of our definitions
is that every tainted object is also reachable:
\begin{lemma}
@{text "tainted\<^sup>s \<subseteq> reachable\<^sup>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\<^sup>s \<and> |item| = Some obj"}
\end{tabular}}
\end{isabelle}
\noindent
Note that @{term taintable_s} is only about objects that are present in
the initial state, because for all other items @{text "|_|"} returns @{text None}.
With these definitions in place, we can state our theorem about the soundness of our
static @{term taintable_s}-check for objects.
\begin{theorem}[Soundness]
@{thm [mode=IfThen] static_sound}
\end{theorem}
\noindent
The proof of this theorem generates for every object that is ``flagged'' as
@{term taintable_s} by our check, a sequence of events which shows how the
object can become tainted in the dynamic model. We can also state a completeness
theorem for our @{term taintable_s}-check.
\begin{theorem}[Completeness]
@{thm [mode=IfThen] static_complete}
\end{theorem}
\noindent
This completeness theorem however needs to be restricted to
undeletebale objects. The reason is that a tainted process can be
killed by another process, and after that can be ``recreated'' by a
cloning event from an untainted process---remember we have no control
over which process ID a process will be assigned with. Clearly, in
this case the cloned process should be considered untainted, and
indeed our dynamic tainted relation is defined in this way. The
problem is that a static test cannot know about a process being
killed and then recreated. Therefore the static test will not be
able to ``detect'' the difference. Therefore we solve this problem
by considering only objects that are present in the initial state
and cannot be deleted. By the latter we mean that the RC-policy
stipulates an object cannot be deleted (for example it has been created
by @{term root} in single-user mode, but in the everyday running
of the system the RC-policy forbids to delete an object belonging to
@{term root}). Like @{term "taintable_s"}, we also have a static check
for when a file is undeletable according to an RC-policy.
This restriction to undeletable objects might be seen as a great
weakness of our result, but in practice this seems to cover the
interesting scenarios encountered by system administrators. They
want to know whether a virus-infected file introduced by a user can
affect the core system files. Our test allows the system
administrator to find this out provided the RC-policy makes the core
system files undeletable. We assume that this proviso is already part
of best practice rule for running a system.
We envisage our test to be useful in two kind of situations: First, if
there was a break-in into a system, then, clearly, the system
administrator can find out whether the existing access policy was
strong enough to contain the break-in, or whether core system files
could have been affected. In the first case, the system
administrator can just plug the hole and forget about the break-in;
in the other case the system administrator is wise to completely
reinstall the system.
Second, the system administrator can proactively check whether an
RC-policy is strong enough to withstand serious break-ins. To do so
one has to identify the set of ``core'' system files that the policy
should protect and mark every possible entry point for an attacker
as tainted (they are the seeds of the @{term "tainted_s"} relation).
Then the test will reveal
whether the policy is strong enough or needs to be redesigned. For
this redesign, the sequence of events our check generates should be
informative.
*}
section {*Conclusion and Related Works*}
text {*
We have presented the first completely formalised dynamic model of
the Role-Compa\-tibility Model. This is a framework, introduced by Ott
\cite{ottrc}, in which role-based access control policies
can be formulated and is used in practice, for example, for securing Apache
servers. Previously, the RC-Model was presented as a
collection of rules partly given in ``English'', partly given as formulas.
During the formalisation we uncovered an inconsistency in the
semantics of the special role @{term "InheritParentRole"} in
the existing works about the RC-Model \cite{ottrc,ottweb}. By proving
the soundness and completeness of our static @{term
"taintable_s"}-check, we have formally related the dynamic behaviour
of the operating system implementing access control and the static
behaviour of the access policies of the RC-Model. The
crucial idea in our static check is to record precisely the
information available about the initial state (in which some resources might be
tainted), but be less precise
about the subsequent states. The former fact essentially gives us
the soundness of our check, while the latter results in a finite
search space.
The two most closely related works are by Archer et al and by Guttman et al
\cite{Archer03,guttman2005verifying}. The first describes a
formalisation of the dynamic behaviour of SELinux carried out in the
theorem prover PVS. However, they cannot use their formalisation in
order to prove any ``deep'' properties about access control rules
\cite[Page 167]{Archer03}. The second analyses access control
policies in the context of information flow. Since this work
is completely on the level of policies, it does
not lead to a sound and complete check for files being taintable (a dynamic notion
defined in terms of operations performed by the operating system).
While our results concern the RC-Model, we expect that they
equally apply to the access control model of SELinux. In fact,
we expect that the formalisation is simpler for SELinux, since
its rules governing roles are much simpler than in the RC-Model.
The definition of our admissibility rules can be copied verbatim for SELinux;
we would need to modify our granted rules and slightly adapt our
static check. We leave this as future work.
Our formalisation is carried out in the Isabelle/HOL theorem prover.
It uses Paulson's inductive method for
reasoning about sequences of events \cite{Paulson98}.
We have approximately 1000 lines of code for definitions and 6000 lines of
code for proofs. Our formalisation is available from the
Mercurial repository at \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/rc/}.\\[-12mm]
%In a word, what the manager need is that given the
%initial state of the system, a policy checker that make sure the under the policy
%he made, this important file cannot: 1. be deleted; 2. be tainted.
%Formally speaking, this policy-checker @{text "PC"} (a function that given the
%initial state of system, a policy and an object, it tells whether this object
%will be fully protected or not) should satisfy this criteria:
% @{text "(PC init policy obj) \<and> (exists init obj) \<longrightarrow> \<not> taintable obj"}
%If the @{text obj} exists in the initial-state, and @{text "PC"} justify the safety
%of this object under @{text "policy"}, this object should not be @{text taintable}.
%We call this criteria the \emph{completeness} of @{text "PC"}.
%And there is the \emph{soundness} criteria of @{text "PC"} too, otherwise a "NO-to-ALL"
%answer always satisfy the \emph{completeness}. \emph{soundness} formally is:
% @{text "PC init policy obj \<longrightarrow> taintable obj"}
%This policy-checker should satisfy other properties:
% 1. fully statical, that means this policy-checker should not rely on the system
%running information, like new created files/process, and most importantly the
%trace of system running.
% 2. decidable, that means this policy-checker should always terminate.
*}
(*<*)
end
end
(*>*)
(*
Central to RC-Model is the roles and types. We start with do formalisation on
types first.
\begin{isabelle}\ \ \ \ \ %%%
\mbox{
\begin{tabular}{r@ {\hspace{1mm}}l@ {\hspace{2mm}}l}
@{text t_client} & @{text "="} & @{text "Christian"} \\
& @{text "|"} & @{text "Chunhan"} \\
& @{text "|"} & @{text " ... "} \\
\end{tabular}}
\mbox{
\begin{tabular}{r@ {\hspace{1mm}}l@ {\hspace{2mm}}l@ {\hspace{2mm}}l}
@{text t_normal_file_type} & @{text "="} & @{text "WebServerLog_file"} & \\
& @{text "|"} & @{text "WebData_file"} & @{text t_client} \\
& @{text "|"} & @{text "CGI_file"} & @{text t_client} \\
& @{text "|"} & @{text "Private_file"} & @{text t_client}
\end{tabular}}
\mbox{
\begin{tabular} {r@ {\hspace{1mm}}l@ {\hspace{5mm}}l}
@{text t_rc_file_type}
& @{text "="} & @{term "InheritParent_file_type"} \\
& @{text "|"} & @{term "NormalFile_type t_normal_file_type"}
\end{tabular}}
\end{isabelle}
@{term "type_of_file"} function calculates the current type for the files:
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{lcl}
@{thm (lhs) type_of_file.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) type_of_file.simps(1)}\\
@{thm (lhs) type_of_file.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) type_of_file.simps(2)}\\
@{term "type_of_file (DUMMY#s)"} & @{text "\<equiv>"} & @{term "type_of_file s"}
\end{tabular}}
\end{isabelle}
Note that this @{term "type_of_file"} is not the function @{term "etype_of_file"}
that we call in the grant check of RC-Model, @{term "rc_grant"}. The reason is
that file's type can be set to a special type of @{term "InheritParent_file_type"},
means that the ``efficient'' type of this file is the efficient type of its directory.
\mbox{\begin{tabular}{lcl}
@{thm (lhs) etype_aux.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) etype_aux.simps(1)}\\
@{thm (lhs) etype_aux.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) etype_aux.simps(2)}\smallskip\\
@{thm (lhs) etype_of_file_def} & @{text "\<equiv>"} & @{thm (rhs) etype_of_file_def}
\end{tabular}}
Here @{term etype_aux} is an auxiliary function which do recursion
on the pathname of files. By the way, in our proofs, we do proved
that functions like @{term "etype_of_file"} will always return
``normal'' values.
We have similar observation functions calculating the current type for processes
and IPCs too, only diffence here is that there is no ``effcient'' type here for
processes and IPCs, all types that calculated by @{term "type_of_process"} and
@{term "type_of_ipc"} are alrealdy efficient types.
*)
(*
text {*
\begin{isabelle}\ \ \ \ \ %%%
\mbox{
\begin{tabular}{r@ {\hspace{1mm}}l@ {\hspace{2mm}}l@ {\hspace{2mm}}l}
@{text t_normal_role} & @{text "="} & @{text "WebServer"} & \\
& @{text "|"} & @{text "WS_client"} & @{text t_client} \\
& @{text "|"} & @{text "UpLoader"} & @{text t_client} \\
& @{text "|"} & @{text "CGI "} & @{text t_client}
\end{tabular}}
\mbox{
\begin{tabular} {r@ {\hspace{1mm}}l@ {\hspace{2mm}}l@ {\hspace{5mm}}l}
@{text t_role}
& @{text "="} & @{term "InheritParentRole"} & ``for file's initial/forced role,
meaning using parent directory's
role instead'' \\
& @{text "|"} & @{term "UseForcedRole"} & ``for file's initial role'' \\
& @{text "|"} & @{term "InheritProcessRole"} & ``using process' current role''\\
& @{text "|"} & @{term "InheritUserRole"} & ``using owner's default role''\\
& @{text "|"} & ... & \\
& @{text "|"} & @{term "NormalRole t_normal_role"} & ``user-defined
policy roles"
\end{tabular}}
\end{isabelle}
@{text "t_normal roles"} are normally user-defined roles in the
policy, where @{text "WebServer"} is the role who plays for the
server, while @{text "WS_client"} is the role server plays for
certain client, so is for @{text "UpLoader"} role. @{text "CGI"} is
the role that client's programme scripts play.
@{term "currentrole"} function calculates the current role of process, here we
only show 3 cases of its definition, it responses to @{term "ChangeOwner"},
@{term "ChangeRole"} events too.
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{lcl}
@{thm (lhs) currentrole.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) currentrole.simps(1)}\\
@{thm (lhs) currentrole.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) currentrole.simps(2)}\\
@{thm (lhs) currentrole.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) currentrole.simps(3)}
\end{tabular}}
\end{isabelle}
If the event trace is @{term "[]"}, means the
system state currently is the initial state, then @{term "init_currentrole"} will
do. @{term "Execute p f"} event is one complex case, when this event happens, process
@{term p}'s role will be changed according to the efficient initial role of the
executable file @{term f}, here ``efficient'' is like the file's type too.
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{lcl}
@{thm (lhs) initialrole.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) initialrole.simps(1)}\\
@{thm (lhs) initialrole.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) initialrole.simps(2)}\\
@{thm (lhs) initialrole.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) initialrole.simps(3)}\medskip\\
@{thm (lhs) erole_functor.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) erole_functor.simps(1)}\\
@{thm (lhs) erole_functor.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) erole_functor.simps(2)}
\end{tabular}}
\end{isabelle}
If this efficient initial role is normal role, then RC-Model assigns
this role to the process after execution finished. Otherwise if this
efficient initial role is using special value @{term
"UseForcedRole"}, then the new role for the process is then
determinated by the efficient forced role of the executable file
@{term "forcedrole"}. When new process is created, this process'
role is assigned to its creator's role.
*}
HERE: chunhan
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.
*)