Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base

Authors

  • Narjes Jomaa University of Lille
  • Paolo Torrini University of Lille
  • David Nowak University of Lille & CNRS
  • Gilles Grimaud University of Lille
  • Samuel Hym University of Lille

DOI:

https://doi.org/10.14279/tuj.eceasst.76.1080

Abstract

The development of provably secure OS kernels represents a fundamental step in the creation of safe and secure systems. To this aim, we propose the notion of protokernel and an implementation — the Pip protokernel — as a separation kernel whose trusted computing base is reduced to its bare bones, essentially providing separation of tasks in memory, on top of which non-influence can be proved. This proof-oriented design allows us to formally prove separation properties on a concrete executable model very close to its automatically extracted C implementation. Our design is shown to be realistic as it can execute isolated instances of a realtime embedded system that has moreover been modified to isolate its own processes through the Pip services.

Downloads

Published

2019-05-14