Conception et analyse de rétroactions basées sur des canaux auxiliaires pour la découverte de vulnérabilités
Le fuzzing est une technique de test dynamique permettant la découverte de vulnérabilités de manière très efficace. Des centaines voire milliers de vulnérabilités sont ainsi détectées (et réparées) chaque année dans les logiciels que nous utilisons. Lorsque que l'on essaye de transposer l'approche fuzzing sur des systèmes embarqués on se retrouve confronté à plusieurs problèmes : le code source n'est pas toujours disponible, très peu d'informations sont disponibles sur le comportement du système à l'exécution et enfin il est difficile de détecter si un bug est apparu. Le laboratoire LTSO développe depuis plusieurs années des techniques à l'état de l'art dans l'analyse des canaux auxiliaires, notamment le rayonnement électromagnétique produit par les systèmes pendant leur fonctionnement. Ces mesures permettent d'inférer des informations (donnée, code exécuté) sur le comportement du système de manière non-intrusive. L'objectif de cette thèse est donc de déterminer si ces mesures side-channel permettent d'améliorer le processus de fuzzing sur les systèmes embarqués. L'utilisation de cette nouvelle source d'information ouvre également la porte à la découverte de nouvelle classes de vulnérabilités, comme les vulnérabilités micro-architecturales.
La thèse aura lieu au CEA Grenoble, au sein de l'institut du LETI, dans une équipe de recherche dédiée à l'étude et au développement de solutions pour la sécurité des systèmes électroniques présents et futurs (http://www.leti-cea.fr/cea-tech/leti/Pages/recherche-appliquee/infrastructures-de-recherche/plateforme-cybersecurite.aspx).
Amélioration de la sécurité des capteurs d'images, l'IA au service du tatouage numérique fragile et robuste
Ce sujet de thèse vise à améliorer la sécurité des capteurs d'images à travers l’exploration approfondie des récentes techniques d'apprentissage profond appliquées au tatouage numérique. Ce procédé de stéganographie consiste à dissimuler un message invisible dans un contenu image sans en altérer le rendu ; message pouvant être récupéré à l’aide d’un autre procédé dit d’extraction. Dans le contexte des chaînes algorithmiques de rendu d'images intégrées aux capteurs, cette étude vise à relever le défi double consistant à assurer un tatouage numérique à la fois résistant contre des attaques intentionnelles visant à briser le marquage (tatouage robuste) tout en maintenant une grande sensibilité aux altérations (tatouage fragile). L'objectif de cette approche duale est non seulement d'améliorer la sécurité des données capteur, mais ouvre de nouvelles perspectives en termes d'authentification, de détection de manipulation ou de contrefaçon, combinées à la vérification de l'intégrité des données. Ce sujet balayera des domaines allant de la conception d’algorithmes de rendu d'images utilisant des modèles d'apprentissage profond utilisant des mécanismes d'attention, aux subtilités de l'incorporation simultanée de plusieurs clés/filigranes, répondant ainsi à l'exigence de caractéristiques à la fois robustes et fragiles.
Ce sujet constitue donc une opportunité pour les candidats manifestant un intérêt pour l'apprentissage profond, le traitement d'images et de la stéganographie/cryptographie. Il offre non seulement un champ de recherche académique large pour des contributions scientifiques significatives, mais également un potentiel de résultats concrets pour de futurs transferts technologiques. En pratique, le travail consistera à trouver des solutions algorithmiques innovantes ayant pour but d’améliorer les performances du tatouage, solutions conçues pour faire face aux attaques les plus avancées à l’état de l’art et basées sur l'apprentissage profond, tout en s’assurant la préservation d’une haute qualité du rendu d'image.
Preuve d'équivalence fonctionnelle de codes binaires pour la sécurisation des programmes embarqués
La thèse se place dans le contexte de la cyber-sécurité des systèmes
embarqués et des objets connectés, plus particulièrement de leur
sécurisation contre les attaques physiques (attaques par canal
auxiliaire et attaques par injection de fautes).
Le CEA List développe une chaîne de compilation basée sur LLVM,
COGITO, pour l'application automatisée de contre-mesures contre les
attaques physiques. Deux éléments sont cruciaux pour renforcer la
confiance dans la robustesse des contre-mesures appliqués dans les
programmes binaires compilés :
1. la preuve de robustesse des contre-mesures mises en œuvre,
2. la preuve que l'ajout de contre-mesures au programme cible n'en
modifie pas la fonctionnalité.
Cette thèse ciblera le deuxième point : pouvoir apporter des garanties
formelles sur la conformité fonctionnelle d'un programme sécurisé.
Notre approche visera à prouver l'équivalence fonctionnelle du
programme sécurisé à un autre programme de référence, par exemple le même programme mais dépourvu de contre-mesures. Nous
utiliserons BINSEC (https://binsec.github.io), une plate-forme
open-source d'analyse de code binaire développée au CEA List
s'appuyant sur l'état de l'art en matière d'analyse de code binaire et
de méthodes formelles.
La thèse se déroulera sur le centre de Saclay du CEA List (NanoInnov), dans l'équipe de développement de BINSEC.
Plusieurs séjours sur le centre de Grenoble seront prévus pour assurer une étroite
collaboration avec l'équipe de développement de COGITO.
Combinaison de sur et sous-approximations pour l'analyse de programmes bas-niveau
Parce que l'analyse de programme est un problème indécidable, les analyses statiques se divisent en 2 catégories:
- Les analyses sound, qui calculent une surapproximation de tous les comportements du programme, et permettent de vérifier l'absence d'erreur.
- Les analyses complete, qui calculent une sous-approximation des comportements possibles du programme, et permettent de trouver des erreurs.
Le but de la thèse est d'étudier cette combinaison de ces techniques pour l'analyse statique de programmes bas-niveau, en particulier des exécutables binaires, en ciblant notamment les analyses de la mémoires et du flot de contrôle, qui sont les informations capitales pour comprendre les comportements possibles d'un binaire.
[POPL'23]: SSA Translation is an Abstract Interpretation, M. Lemerre (Distinguished paper award)
[VMCAI'22]: Lightweight Shape Analysis Based on Physical Types, O. Nicole, M. Lemerre, X. Rival
[RTAS'21]: No Crash, No Exploit: Automated Verification of Embedded Kernels, O. Nicole, M. Lemerre, S. Bardin, X. Rival (best paper award)
[LPAR'18] Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing B. Farinier, S. Bardin, R. David, M. Lemerre
Guidage astucieux des outils de géneration de tests
Le fuzzing est une technique de génération de tests automatisée. Il consiste en une exécution répétée d'un programme avec des entrées générées automatiquement, afin de déclencher des plantages, symptômes de bugs sous-jacents au niveau du code, qui peuvent ensuite être corrigés. Un défi majeur dans ce domaine consiste à passer d’une exploration indistincte du fonctionnement des programmes à un guidage astucieux vers la découverte de bugs importants. Profitant de l’expertise de notre équipe et de nos travaux antérieurs, l'objectif de la thèse est de proposer, mettre en œuvre et évaluer des moyens pour relever ce défi, en tirant avantage de mécanismes de guidage plus fins.
Tests basés sur des scénarios pour les systèmes automatisés : améliorer la sécurité et la fiabilité conformément aux réglementations et aux normes
Cette recherche vise à étudier l'efficacité des tests basés sur des scénarios en tant qu'approche complète et robuste pour évaluer les performances des Systèmes Automatisés (SA) tout en améliorant leur sécurité et leur fiabilité par rapport aux réglementations et aux normes.
L'objectif principal de cette thèse sera d'étudier les avantages des tests basés sur des scénarios pour les systèmes automatisés et leur conformité aux réglementations et aux normes. Les sous-objectifs suivants seront poursuivis :
- Effectuer une étude de la littérature et des pratiques sur les méthodologies de test des SA, en mettant l'accent sur les défis uniques posés par les algorithmes complexes de prise de décision des SA et l'interaction avec l'environnement dynamique.
- Développer un framework de test basé sur des scénarios pour l'identification, la génération, la sélection et l'exécution systématiques de scénarios réalistes et divers, pour les SA
- Analyser les lacunes ou les domaines de non-conformité concernant les concepts et exigences clés décrits dans les réglementations et les normes et examiner leur applicabilité, leurs implications et leurs améliorations pour les tests basés sur des scénarios.
- Effectuer une évaluation du framework proposé à travers différentes applications réelles et quasi réalistes (divers types, différents niveaux d'automatisation et divers scénarios réels) pour évaluer l'applicabilité et les avantages de la méthodologie.
Les résultats et les recommandations de cette recherche guideront in fine les fabricants, les régulateurs et les parties prenantes dans le développement et la validation de SA conformes au cadre réglementaire, favorisant le déploiement sûr et responsable des systèmes automatisés à l'avenir.