|David Nowak (CNRS & Univ. Lille)|
Date de l'exposé : 23 septembre 2016
Formal Proof of Dynamic Memory Isolation Based on MMU
For security and safety reasons, it is essential to ensure memory isolation between processes. The memory manager is thus a critical part of the kernel of an operating system. It is common for kernels to ensure memory isolation through a piece of hardware called memory management unit (MMU). However an MMU by itself does not provide memory isolation. It is only a tool the kernel can use to ensure this property.
In the first part of this presentation, we will show how a proof assistant such as Coq can be used to model a hardware architecture with an MMU, and an abstract model of a microkernel supporting preemptive scheduling and memory management.
In a second part we will show how we take into account the lessons learned from the preliminary study in the previous part to design and prove secure at the same time a minimal kernel called Pip (codename: Pépin).