La conception d'un noyau orientée par sa preuve d'isolation mémoire

Abstract

La vérification des logiciels critiques tels que les noyaux des systèmes d'exploitation est une activité longue et complexe. Celle-ci nécessite une attention particulière dès les premières phases de conception. Le choix des fonctionnalités, la stratégie d'implémentation, le modèle du matériel à gérer, les propriétés à vérifier et l'approche de vérification sont tous à prendre en compte pendant le développement du noyau. Ce papier discute de la stratégie de co-design d'un noyau de système d'exploitation et de sa preuve. L'objectif visé est d'adapter le design du noyau pour réduire la complexité de la production de sa preuve tout en préservant son utilisabilité. La propriété étudiée dans ce papier est une propriété de sécurité, exprimée en terme d'isolation mémoire. L'étude présentée met notamment en évidence l'importance de l'interface d'accès au matériel. In fine c'est cette interface qui est axiomatisée pour construire la preuve du noyau.