rc: comparison Paper.thy

equal deleted inserted replaced

-:baa2970a9687
+:a5f4dc4bbc5d
 (*<*)
 theory Paper
 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 *)
 notation (Rule output)
 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
+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
 includes a large number of interdependent concepts and very complex
 operations that determine roles and types. In our opinion it is
 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
+A state is determined
-by a list of events, called the \emph{trace}.  We need to define
+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:
 %initial state:
 @{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
+The first clause states that in the empty trace the processes are given by @{text "init_processes"}. The
-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"}.
 \begin{tabular}{@ {}c@ {}}
 \mbox{@{thm [mode=Axiom] valid.intros(1)}}\hspace{5mm}
 \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
 that the initial state contains some tainted
 objects (we call them @{term "seeds"}). Therefore in the initial state @{term "[]"}
 \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
+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
 infinite.  For example starting from an
 initial state containing a process @{text p} and a file @{text pf},
 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.
+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.
 It uses Paulson's inductive method for
 reasoning about sequences of events \cite{Paulson98}.

changeset 16	a5f4dc4bbc5d
parent 15	baa2970a9687
child 17	a87e2181d6b6