Cette thèse s’inscrit dans la thématique de la sécurité des petits systèmes informatiques (systèmes embarqués/objets connectés, de type microcontrôleur) et plus précisément vise à apporter des fortes garanties d’isolation mémoire pour les tâches qui s’y exécutent. L’hétérogénéité et les fortes contraintes en ressources (espace mémoire, puissance de calcul, énergie) nécessitent la mise en place de solutions sur mesure pour les systèmes embarqués contraints. Le cycle de vie des logiciels embarqués et les architectures matérielles spécifiques imposent de repenser la manière de mettre en oeuvre la sécurité qui, encore aujourd’hui, laisse ouvertes des problématiques de vulnérabilité mémoire. De plus, les risques d’exploitation de ces vulnérabilités grandissent avec l’émergence de nouveaux cas d’utilisation (environnements intelligents de manière générale) impliquant des systèmes de plus en plus complexes et l’explosion du nombre de systèmes connectés (notamment pour des besoins de mise à jour à distance). En conséquence, des cyber-attaquants peuvent tirer profit de telles vulnérabilités pour prendre le contrôle à distance de ces systèmes connectés de façon massive. Dans ce cadre, la thèse propose d’élaborer un noyau destiné aux petits objets qui soit capable d’apporter des garanties fortes d’isolation mémoire. Elle étudie l’association entre flexibilité élevée et forte sécurité au sein d’objets contraints pour une sécurité dès la conception sans perte fonctionnelle. Elle est constituée de deux contributions principales qui répondent aux attaques logicielles sur la mémoire. La première contribution est un noyau de système d’exploitation, appelé Pip-MPU, qui propose une solution d’isolation ancrée dans le matériel et offrant une flexibilité dépassant les solutions actuelles. Pip-MPU est adapté du protonoyau Pip initialement destiné à des ordinateurs généralistes dotés d’une plateforme matérielle plus fournie et différente de celle des objets contraints. Pour cela, le noyau conçu est une refonte totale de Pip et propose un mécanisme de sécurité basé sur la Memory Protection Unit (MPU), une unité du processeur, qui permet un contrôle d’accès matériel aux ressources. Malgré les fortes limitations imposées par la plateforme matérielle, Pip-MPU est aussi flexible que ce que permet la MMU en termes de sécurité. Du haut de ses 10 Ko de code et 16% de surcoût en termes de performances et de consommation d’énergie, Pip-MPU réduit le nombre d’opérations privilégiées exécutées de 99% et la surface d’attaque de la mémoire accessible depuis l’application de 98%. La deuxième contribution est l’obtention de garanties fortes de l’isolation par l’usage de méthodes formelles. Plusieurs services du noyau ont été formellement prouvés pour l’isolation à l’aide de l’assistant de preuve Coq. Les propriétés prouvées sont les propriétés de sécurité de Pip imposant son modèle de sécurité d’isolation stricte. A notre connaissance, aucun autre système de l’état de l’art proposant de l’isolation par MPU n’a été formellement prouvé auparavant. Nous développons des nouvelles techniques de conduite de preuve et proposons de nouvelles métriques permettant de suivre l’effort de preuve et d’évaluer les hypothèses soutenant les preuves. Toutes les contributions de la thèse sont en source ouverte.
Composition du jury proposé M. Gilles GRIMAUD Université de Lille Directeur de thèse M. Jean-Pierre TALPIN INRIA Rennes Rapporteur M. Didier DONSEZ Université Grenoble 1 Rapporteur Mme Chrystel GABER Orange Innovation Caen Examinatrice Mme Marie-Laure POTET ENSIMAG - Université Grenoble Alpes Examinatrice M. Julien SOPENA Sorbonne Université - LIP6 Examinateur Mme Patricia MOUY Laboratoire Sécurité du Logiciel - ANSSI Examinatrice M. Romain ROUVOY Université de Lille Examinateur M. Jean-Philippe WARY Orange Innovation Invité
Thesis of the team 2XS defended on 14/12/2022
français
English