Preuve formelle d'isolation mémoire dynamique à base de MMU

National audienceL'isolation mémoire est une propriété fondamentale pour garantir la sécurité des systèmes exécutant plusieurs processus de différents niveaux de sensibilité au dessus d'un noyau de confiance s'exécutant avec le plus haut niveau de privilège (noyau monolithique, micro-noyau, hyperviseurs, etc.). En effet, afin de garantir la confidentialité et l'intégrité du noyau et des processus, il est nécessaire d'interdire les accès illégaux (c.-à-d. ne répondant pas à la politique de sécurité attendue du système) en lecture et en écriture des processus vers d'une part la mémoire des autres processus et d'autre part vers la mémoire du noyau. Dans cet article nous présentons une formalisation en Coq d'un système d'exploitation simplifié. Il comprend un ordonnanceur préemptif et un gestionnaire mémoire utilisé par le noyau et par les processus pour allouer dynamiquement des pages en s'appuyant sur une unité matérielle de gestion mémoire (MMU). La modélisation proposée utilise une logique de Hoare définie au dessus d'une monade d'état. Le travail exposé propose une définition de l'isolation entre les processus et produit la preuve d'isolation sur le système formalisé