rc: comparison Paper.thy

equal deleted inserted replaced

-:64b14b35454e
+:2dab4bbb6684
 lemma osgrant6:
 "\<lbrakk>p \<in> current_procs \<tau>; u \<in> init_users\<rbrakk> \<Longrightarrow> os_grant \<tau> (ChangeOwner p u)"
 by simp
-lemma osgrant10:
+lemma osgrant10: (* modified by chunhan *)
-"\<lbrakk>p \<in> current_procs \<tau>; p' = new_proc \<tau>\<rbrakk> \<Longrightarrow> os_grant \<tau> (Clone p p')"
+"\<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;
 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,
+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
 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
+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}
 \noindent
 Clearly the operating system should only allow to clone a process @{text p} if the
 process is currently alive. The cloned process will get the process
 ID generated by the function @{term new_proc}. This process ID should
 not already exist. Therefore we define @{term new_proc} as
+(* HERE ????? chunhan *)
 \begin{isabelle}\ \ \ \ \ %%%
 \mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 @{term "new_proc s"} & @{text "\<equiv>"} & @{term "Max (current_procs s) + 1"}
 \end{tabular}}
 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
+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
 @{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
+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 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
+infinite.  For example starting from an
 initial state containing a process @{text p} and a file @{text pf},
 we can create files @{text "f\<^isub>1"}, @{text "f\<^isub>2"}, @{text "..."}
 via @{text "CreateFile"}-events. This can be pictured roughly as follows:
 \begin{center}
 "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
+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.
 \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
+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"]}
 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
+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
 end
 end
 (*>*)
 (*
 Central to RC-Model is the roles and types. We start with do formalisation on
 types first.
 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}
 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.
+*}
 *)

changeset 8	2dab4bbb6684
parent 3	4d25a9919688
child 10	569222a42cf5