
diff -r baa2970a9687 -r a5f4dc4bbc5d Paper.thy
--- a/Paper.thy	Fri Sep 06 14:55:53 2013 +0100
+++ b/Paper.thy	Fri Sep 20 12:14:39 2013 +0100
@@ -3,6 +3,51 @@
 imports rc_theory final_theorems rc_theory os_rc 
 begin
 
+(* Still to be done
+
+- ... which OSes exactly use RBAC? SELinux uses DTE which 
+  seems simpler than the RC-Model, but the authors never cite the 
+  DTE papers when mentioning SELinux.
+
+- Fred Spiessens' work on SCOLLAR
+
+- Related work: "Gran: Model Checking Grsecurity RBAC Policies" at CSF 2012 explores 
+  similar issues with policies (but does not provide formal proofs); in particular it 
+  defines a property similar to tainting, develops an abstraction for dynamic 
+  taintability, and report issues with role inheritance rules.
+
+[1] Mikhail I. Gofman, Ruiqi Luo, Ayla C. Solomon, Yingbin Zhang, Ping Yang,
+Scott D. Stoller: RBAC-PAT: A Policy Analysis Tool for Role Based Access
+Control. TACAS 2009:46--49.
+
+[2] Scott D. Stoller, Ping Yang, C. R. Ramakrishnan, Mikhail I. Gofman:
+Efficient policy analysis for administrative role based access control. ACM
+Conference on Computer and Communications Security 2007:445--455.
+
+[3] Arosha K. Bandara, Emil Lupu, Alessandra Russo: Using Event Calculus to
+Formalise Policy Specification and Analysis. POLICY 2003.
+
+Elisa Bertino, Barbara Catania, Elena Ferrari, and Paolo Perlasca. A logical framework for reasoning about access control models. ACM Trans. Inf. Syst. Secur, 6:71–127, 2003.
+
+J. Bryans. Reasoning about XACML policies using CSP. In Proceedings of the 2005 workshop on Secure web services, page 35. ACM, 2005.
+
+K. Fisler, S. Krishnamurthi, L.A. Meyerovich, and M.C. Tschantz. Verification and changeimpact analysis of access control policies. In Proceedings of the 27th international conference on Software engineering, pages 196–205. ACM New York, NY, USA, 2005.
+
+V. Kolovski, J. Hendler, and B. Parsia. Analyzing web access control policies. In Proceedings of the 16th international conference on World Wide Web, page 686. ACM, 2007.
+
+Joseph Y. Halpern and Vicky Weissman. Using first-order logic to reason about policies. ACM Trans. Inf. Syst. Secur., 11(4), 2008.
+
+Prathima Rao, Dan Lin, Elisa Bertino, Ninghui Li, Jorge Lobo: EXAM: An Environment for Access Control Policy Analysis and Management. POLICY 2008: 238-240
+
+Alessandro Armando, Enrico Giunchiglia, and Serena Elisa Ponta. Formal specification and automatic analysis of business processes under authorization constraints: an action-based approach. In Proceedings of the 6th International Conference on Trust, Privacy and Security in Digital Business (TrustBus’09), 2009.
+
+G. Ahn, Hongxin Hu, Joohyung Lee, and Yunsong Meng. Reasoning about XACML policy descriptions in answer set programming (preliminary report). In Proceedings of International Workshop on Nonmonotonic Reasoning (NMR), 2010.
+
+G. Ahn, Hongxin Hu, Joohyung Lee, and Yunsong Meng. Representing and reasoning about web access control policies. In Proc. 34th Annual IEEE Computer Software and Applications Conference (COMPSAC 2010), pages 137–146, 2010.
+
+*)
+
+
 (* THEOREMS *)
 
 
@@ -264,6 +309,30 @@
   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 
+  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.
+  Although, there are only four rules, their state-space is in general
+  infinite, like in our work. They then 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
+  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
+  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
+  `pencil-and-paper proofs', whereas reasoning about our more detailed 
+  model containing substantially more rules needs the support of
+  a theorem prover.
+
   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
@@ -464,8 +533,11 @@
   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
+  A state is determined
+  by a list of events, called the \emph{trace}.  The empty trace, or empty list, stands 
+  for the initial state. Given a trace $s$, we prepend an event to $s$ to stand for the state in which the
+  event just happened.  
+  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:
@@ -492,8 +564,7 @@
   \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 
+  The first clause states that in the empty trace 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 
@@ -656,7 +727,11 @@
   \mbox{@{thm [mode=Rule] valid.intros(2)}} 
   \end{tabular}
   \end{center}  
+*}
 
+section {* The Tainted Relation *}
+
+text {*
   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
@@ -767,7 +842,9 @@
   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
+  example system files).  
+
+  It should be clear 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
@@ -1304,7 +1381,10 @@
   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.
+  static check. We leave this as future work. Another direction
+  of future work could be to reason formally about confidentiality in 
+  access control models. This would, of course, need the explicit assumption 
+  about the absence of any covert channels in systems. 
 
 
   Our formalisation is carried out in the Isabelle/HOL theorem prover.




