rc: comparison Paper.thy

equal deleted inserted replaced

-:a5f4dc4bbc5d
+:a87e2181d6b6
 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 work is also closely related to the work on \emph{grsecurity}, an
+The  work we report is also closely related to the work on \emph{grsecurity}, an
 access control system developed as a patch on top of Linux kernel \cite{gran12}.
 It installs a reference monitor to restrict access to system resources.
 They model a dynamic semantics of the operating system with four rules dealing with
 executing a file, setting a role and setting an UID as well as GID.
-These rules depend on an arbitrary but fixed access policy.
+These rules are parametrerised by an arbitrary but fixed access policy.
 Although, there are only four rules, their state-space is in general
-infinite, like in our work. They then give an abstracted semantics,
+infinite, like in our work. They therfore give an abstracted semantics,
 which gives them a finite state-space. For example the abstracted
 semantics dispenses with users and roles by introducing
 abstract users and abstract roles. They obtain a soundness result
 for their abstract semantics and under some weak assumptions
-also a completeness result. Comparing it to our work, we will have a much
+also a completeness result. Comparing this to our work, we will have a much
 more fine-grained model of the underlying operating system. We will
 also obtain a soundness result, but more importantly obtain
 also a completeness result. But since we have a much more fine-grained
-model it will depend on some stronger assumptions.  The abstract semantics
+model, it will depend on some stronger assumptions.  The abstract semantics
 in \cite{gran12} is used for model-checking policies according to
 whether, for example, information flow properties are ensured.
-Since there formalism consists of only a few rules, they can get away with
+Since their formalism consists of only a few rules, they can get away with
-`pencil-and-paper proofs', whereas reasoning about our more detailed
+``pencil-and-paper proofs'', whereas reasoning about our more detailed
-model containing substantially more rules needs the support of
+model containing substantially more rules really necessitates the support of
-a theorem prover.
+a theorem prover and completely formalised models.
 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
 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]
+Mercurial repository at \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/rc/}.\\[-12mm]\mbox{}
+%%\\[-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.
 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{

changeset 17	a87e2181d6b6
parent 16	a5f4dc4bbc5d
child 21	17ea9ad46257