An Abstract Take/Grant Security Model ===================================== l4v/spec/take-grant/ This directory contains the Isabelle sources of an abstract take-grant security model, studying some of the underlying concepts of seL4's protection mechanisms. Overview -------- * `System_S` contains the operations and state space of the model. * `Confine_S` shows authority confinement * `Islands_S` explicitly defines the concept of authority-isolated islands and authority confinement on this concept. * `Isolations_S` defines a notion of high-level information flow on take-grant authority and shows that islands stay isolated. * `Example` and `Example2` are two example systems in this model. Building -------- The corresponding Isabelle session is `TakeGrant`. To build, run in directory `l4v/spec`: make TakeGrant Remarks ------- * This specification is *not* connected with the seL4 code and does *not* completely describe seL4 behaviour. Instead, it is a more abstract study of the underlying concepts. * A previous, simpler version of this model has appeared in Dhammika Elkaduwe's PhD thesis. * A description of the extended, more recent model can be found in Andrew Boyton's PhD thesis.