Skip to content

Latest commit

 

History

History
47 lines (33 loc) · 1.36 KB

README.md

File metadata and controls

47 lines (33 loc) · 1.36 KB
Raw

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 for the ARM architecture, run in directory l4v/:

L4V_ARCH=ARM ./run_tests 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.