• Langue : Anglais, Français
• Discipline : Informatique et applications
• Identifiant : 2022ULILB038
• Type de thèse : Doctorat
• Date de soutenance : 14/12/2022

Résumé en langue originale

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.

Résumé traduit

This thesis invests the field of cybersecurity for small computer systems (embedded systems/connected objects/low-end devices, of type microcontroller) and more precisely aims to bring strong memory isolation guarantees for tasks executing on them.The heterogeneity and strong resource constraints (memory, computing power, energy) of constrained embedded systems require tailored solutions. The embedded software life cycle and the specific hardware platforms challenge us to reconsider the security schemes that leave open memory vulnerability issues, still prevailing today. Furthermore, the risk of vulnerability exploits elevates with the growing number of use cases (smart environments in general) implying increased complexity within these systems and with the burgeoning market of the Internet-of-Things (notably for remote update purposes). As a consequence, cyber attackers can take profit from these vulnerabilities to take remote control of these connected systems in a very scalable way.In this context, the thesis proposes to design a kernel for constrained objects that is able to bring strong memory isolation guarantees. It studies the blend of high flexibility and strong security for this class of devices with the aim of security-by-design without functional loss. The thesis presents two main contributions dealing with software attacks on memory.The first contribution is an Operating System (OS) kernel, named Pip-MPU, that offers a hardware-based isolation solution with a degree of flexibility outperforming current solutions. Pip-MPU is adapted from the Pip protokernel initially designed for high-end/general-purpose computers that are provided with more furnished and different hardware platforms than the ones of constrained objects. For that, the designed kernel is a complete refactoring of Pip and offers a security mechanism based on the Memory Protection Unit (MPU), a unit of the processor, which enables hardware-based access control on memory resources. Despite strong limitations due to the limited hardware platform, Pip-MPU is as flexible as its parent project Pip. With a code base size of less than 10 Kb and about 16% extra costs in terms of performance and energy consumption, Pip-MPU reduces the number of privileged operations by 99% and the attack surface of the accessible application memory by 98%.The second contribution is the demonstration of strong isolation guarantees by the use of formal methods. Several kernel services have been proved against isolation by the use of the Coq Proof Assistant. The proved properties are Pip's security properties that enforce a strict memory isolation security model. To our knowledge, no state-of-the-art solution offering MPU-based isolation has been proved before. We develop novel proof conduct techniques and propose new metrics to follow the proof effort and evaluate the hypotheses supporting the proofs.All the contributions developed in this thesis are made publicly available under open-source licences.