Séminaire SoSySec

Sécurité des logiciels et des systèmes

Accueil     Présentation     Archives

David Nowak (CNRS & Univ. Lille)

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).