Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base - Jomaa, Narjes; Torrini, Paolo; Nowak, David; Grimaud, Gilles; Hym, Samuel (Electronic Communications of the EASST, 2019)
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.