Contrats HW/SW pour l’analyse de robustesse aux fautes de processeurs open-source

Cette thèse se concentre sur la cybersécurité des systèmes embarqués, en particulier sur la vulnérabilité des processeurs et des programmes face aux attaques par injection de fautes. Ces attaques perturbent le fonctionnement normal des systèmes, permettant aux attaquants d'exploiter des failles pour accéder à des informations sensibles. Bien que des méthodes formelles aient été développées pour analyser la robustesse des systèmes, elles se limitent souvent à des analyses séparées du matériel et des logiciels, négligeant l'interaction entre les deux.

Le travail proposé vise à formaliser des contrats entre le matériel et le logiciel (HW/SW) spécifiquement pour l'analyse de sécurité contre les injections de fautes. En s'appuyant sur une approche de partitionnement matériel, cette recherche cherche à atténuer les problèmes de scalabilité liés à la complexité des modèles de microarchitecture. Les résultats attendus incluent le développement de techniques et d'outils permettant une vérification efficace de la sécurité des systèmes embarqués, ainsi que la création de contrats qui faciliteront l'évaluation de la conformité des implémentations matérielles et logicielles. Cette approche pourrait également réduire le temps de mise sur le marché des systèmes sécurisés.

Constructions à sécurité CCA pour le FHE

Le chiffrement homomorphe (FHE) est un corpus de techniques cryptographiques permettant le calcul directement sur les chiffrés. Depuis ses débuts, il y a une quinzaine d’années, le FHE a fait l’objet de nombreuses recherches en vue d’améliorer son efficacité calculatoire. Toutefois, sur le plan de la sécurité, le FHE pose encore de nombreuses questions. En particulier, tous les FHE utilisés en pratique (BFV, BGV, CKKS et TFHE) n’atteignent que le niveau de sécurité CPA (qui permet essentiellement de se prémunir contre des adversaires dit passifs).

Ces dernières années, plusieurs travaux ont donc étudié la sécurité du FHE dans le régime au-delà de CPA et introduit de nouvelles notions de sécurité (CPAD, FuncCPA, vCCA, vCCAD, …). Ces travaux ont conduit à de nouvelles attaques, de nouvelles constructions et, globalement, une meilleure compréhension de la sécurité du FHE dans ce régime.

Concernant la sécurité CCA, des travaux très récents (2024) ont défini de nouvelles notions strictement plus forte que CCA1 et ont démontré qu’elles pouvaient en théorie être atteintes par des schémas FHE exacts ou approchés. Avec ces avancées comme point de départ, la présente thèse visera à concevoir de nouveau schémas cryptographiques pratiques offrant à la fois de la malléabilité et des propriétés de sécurité CCA, au moins pour des applications spécifiques.

Exploration d’approches non supervisés pour modéliser l’environnement à partir de données RADAR

Les technologies RADAR ont gagné en intérêt ces dernières années, notamment avec l'émergence des radars MIMO et des "Imaging Radars 4D". Cette nouvelle génération RADAR offre des opportunités mais aussi des défis pour le développement d'algorithmes de perception. Les algorithmes traditionnels comme la FFT, le CFAR et le DOA sont efficaces pour la détection de cibles en mouvement, mais les nuages de points générés sont encore trop épars pour une modélisation d'environnement précise. C’est une problématique cruciale pour les véhicules autonomes et la robotique.
Cette thèse propose d'explorer des techniques de Machine Learning non-supervisé pour améliorer la modélisation d'environnement à partir de données RADAR. L'objectif est de produire un modèle d'environnement plus riche, avec une meilleure densité et description de la scène, tout en maîtrisant le coût calculatoire pour une exploitation en temps réel. La thèse abordera les questions du type de données RADAR sont les plus adaptés en entrée des algorithmes ainsi que pour représenter l’environnement. Le candidat devra explorer des solutions algorithmiques non-supervisées et rechercher les optimisations de calcul pouvoir rendre ces solutions compatibles avec le temps réel.
Ces solutions devront à terme être conçues pour être embarquées au plus proche du capteur, afin d'être exécutées sur des cibles contraintes.

Conception et développement d’algorithmes asynchrones pour la résolution de l’équation du transport des neutrons sur des architectures massivement parallèles et hétérogènes

Cette proposition de thèse s’inscrit dans le cadre de la résolution numérique d’équations aux dérivées partielles par le biais d’une discrétisation des variables. Elle s’intéresse, dans un formalisme d’éléments finis, à travailler sur la conception d’algorithmes au travers de modèles de programmation parallèle et asynchrone pour la résolution de ces équations.
Le cadre industriel applicatif est la résolution de l’équation de Boltzmann appliquée au transport des neutrons dans le cœur d’un réacteur nucléaire. Dans ce contexte, beaucoup de codes modernes de simulations’appuient sur une discrétisation par éléments finis (plus précisément, un schéma Galerkin discontinu décentré amont) pour des maillages cartésiens ou hexagonaux du domaine spatial. L’intérêt de ce travail de thèse prolonge des travaux précédents pour explorer leur extension dans un cadre d’architecture distribuée qui n’ont pas été abordé jusque-là dans notre contexte. Il s’agira de coupler des stratégies algorithmiques et numériques pour la résolution du problème à un modèle de programmation qui expose du parallélisme asynchrone.
Ce sujet s’inscrit dans le cadre de la simulation numérique des réacteurs nucléaires. Ces simulations multiphysiques coûteuses requièrent le calcul du transport des neutrons en cinétique qui peuvent être associées à des transitoires de puissance violents. La stratégie de recherche adopté pour cette thèse permettra de gagner en coût de calcul, et alliée à un modèle massivement parallèle, peut définir les contours d’un solveur neutronique efficace pour ces problèmes multiphysiques.
Un travail réussi dans le cadre de cette thèse permettra à l’étudiant de prétendre à un poste de recherche en simulation et analyse numérique de problèmes physiques complexes, par-delà la seule physique des réacteurs nucléaires.

Sécurisation cryptographique d’enclaves de processeurs RISC-V avec CHERI

CHERI (Capability Hardware Enhanced RISC Instructions) est une solution permettant de sécuriser le processeur contre les fuites spatiales et temporelles de mémoire en transformant tout pointeur en capacité définissant de façon claire les bornes d’accès aux données ou instructions adressées.
Dans cette thèse, nous proposons sur un processeur d’applications RISC-V d’enrichir CHERI et ses possibilités d’intégrité de flot de contrôle avec une protection des instructions allant jusqu’à leur exécution contre tout type de modifications. Dans un second temps, sur la base d’un chiffrement authentifié de la mémoire, nous étudierons la possibilité avec CHERI de définir des enclaves sécurisées permettant une isolation cryptographique entre processus. Le processeur sera modifié pour que chaque processus soit chiffré avec sa propre clé et puisse avoir un cycle de vie sûr. L’ensemble des clés devra être protégé efficacement dans le matériel.

Transformer de vision multimodale efficace pour système embarqué

La thèse proposée se concentre sur l'optimisation des transformers multimodaux de vision (ViT) pour la segmentation panoptique d'objets, en explorant deux axes principaux. Il s'agit d'abord de développer un pipeline de fusion polyvalent pour intégrer des données multimodales (RGB, IR, profondeur, événements, nuages de points), en exploitant les relations d'alignement inter-modales. Ensuite, une approche combinant le pruning et la quantification à précision mixte sera étudiée. L'objectif global est de concevoir des modèles ViT multimodaux légers, adaptés aux contraintes des systèmes embarqués, tout en optimisant leurs performances et en réduisant la complexité computationnelle.

Combinaison de sous et surapproximations de la memoire pour l'analyse de code bas-niveau

Le théorème de Rice énonçant qu'on ne peut pas avoir de méthode qui sache automatiquement dire si une propriété sur un programme est vraie ou non a conduit à séparer les outils de vérification en deux groupes: les outils sound fonctionnant par sur-approximation, comme l'interprétation abstraite, sont capables de prouver automatiquement que certaines propriétés sont vraies, mais ne savent parfois pas conclure et produisent des alarmes; à l'inverse, les outils complete fonctionnant par sous-approximation, comme l'exécution symbolique, savent produire des contre-exemples, mais pas démontrer si une propriété est vraie.

*Le but général de la thèse est d'étudier la combinaison entre méthodes sound et complete d'analyse de programme, et en particulier l'analyse statique par interprétation abstraite et la génération de formules sous-approximée par exécution symbolique*.

Nous nous intéresserons particulièrement à la combinaison d'abstractions sur et sous-approximantes, en particulier pour la mémoire. Les applications envisagées en priorité concernent les analyses de code au niveau binaire, telles que réalisées par la combinaison des plateformes d'analyse BINSEC et CODEX, pour pouvoir trouver des failles de securite automatiquement ou demontrer leur absence.

Génération assistée de noyaux de calculs complexes en mécanique du solide

Les lois de comportement utilisées dans les simulations numériques décrivent les caractéristiques physiques des matériaux simulés. À mesure que notre compréhension de ces matériaux évolue, la complexité de ces lois augmente.L'intégration de ces lois constitue une étape critique pour la performance et la robustesse des calculs scientifiques. De ce fait, cette étape peut conduire à des développements intrusifs et complexes dans le code.

De nombreuses plateformes numériques telles que FEniCS, FireDrake, FreeFEM, Comsol, proposent des techniques de génération de code à la volée (JIT, pour Just In Time) pour gérer différentes physiques. Cette approche JIT réduit considérablement les temps de mise en oeuvre de nouvelles simulations, offrant ainsi une grande versatilité à l'utilisateur. De plus, elle permet une optimisation spécifique aux cas traités et facilite le portage sur diverses architectures (CPU ou GPU). Enfin, cette approche permet de masquer les détails d'implémentation: une évolution de ces derniers est invisible pour l'utilisateur et est absorbée par la couche de génération de code.

Cependant, ces techniques sont généralement limitées aux étapes d'assemblage des systèmes linéaires à résoudre et n'incluent pas l'étape cruciale d'intégration des lois de comportement.

S'inspirant de l'expérience réussie du projet open-source mgis.fenics [1], cette thèse vise à développer une solution de génération de code à la volée dédiée au code de mécanique des structures de nouvelle génération Manta [2] développé par le CEA. L'objectif est de permettre un couplage fort avec les lois de comportement générées par MFront [3], améliorant ainsi la flexibilité, les performances et la robustesse des simulations numériques.

Le doctorant bénéficiera d'un encadrement de la part des développeurs des codes MFront et Manta (CEA), ainsi que des développeurs du code A-Set (collaboration entre Mines-Paris Tech, Onera, et Safran). Cette collaboration au sein d'une équipe multidisciplinaire offrira un environnement stimulant et enrichissant pour le candidat.

De plus, le travail de thèse sera valorisé par la possibilité de participer à des conférences et de publier des articles dans des revues scientifiques à comité de lecture, offrant une visibilité nationale et internationale aux résultats de la thèse.

Le doctorat se déroulera au CEA Cadarache, dans le sud est de la France, au sein du département d'études des combustibles nucléaires de l'institut IRESNE [4]. Le laboratoire d'accueil est le LMPC dont le rôle est de contribuer au développement des composants physiques de la plateforme numérique PLEIADES [5], co-développée par le CEA et EDF.

[1] https://thelfer.github.io/mgis/web/mgis_fenics.html
[2] MANTA : un code HPC généraliste pour la simulation de problèmes complexes en mécanique. https://hal.science/hal-03688160
[3] https://thelfer.github.io/tfel/web/index.html
[4] https://www.cea.fr/energies/iresne/Pages/Accueil.aspx
[5] PLEIADES: A numerical framework dedicated to the multiphysics and multiscale nuclear fuel behavior simulation https://www.sciencedirect.com/science/article/pii/S0306454924002408

Révolutionner l'intervention en milieux complexes : L'IA et les Jumeaux numériques en synergie pour des solutions innovantes et efficaces.

Contexte scientifique
L’exploitation d’équipements complexes, notamment dans le secteur nucléaire, repose sur l’accès rapide et sécurisé à des données hétérogènes. Les avancées en IA générative, combinées aux Jumeaux Numériques (JN), offrent des solutions innovantes pour améliorer les interactions humain-système. Cependant, l’intégration de ces technologies dans des environnements critiques nécessite des approches adaptées pour garantir intuitivité, sécurité et efficacité.
Travail proposé
Cette thèse propose de développer une architecture d’IA générative enrichie par des données métiers et accessible via la réalité mixte, permettant à un opérateur de boite à gants de poser des questions en langage naturel. Les travaux incluent :
1. Une revue de l’état de l’art sur la génération augmentée (RAG), les technologies ASR/TTS et les JN.
2. Le développement et l’intégration d’un chatbot pour l’exploitation nucléaire.
3. L’évaluation des interactions humain-IA et la définition de métriques d’efficacité et d’adoption.
Résultats attendus
Le projet vise à améliorer la sécurité et la productivité grâce à une interaction optimisée et à proposer des guidelines pour l’adoption de ces systèmes dans des environnements critiques.

Optimisations matérielles pour une IA générative efficace avec les réseaux Mamba

L'IA générative a le potentiel de transformer diverses industries. Cependant, les modèles actuels de pointe comme les transformers rencontrent des défis significatifs en termes d'efficacité computationnelle et de mémoire, notamment lorsqu'ils sont déployés sur des matériels à ressources limitées. Cette recherche de doctorat vise à résoudre ces problèmes en optimisant les réseaux Mamba pour des applications matérielles. Les réseaux Mamba offrent une alternative prometteuse en réduisant la complexité quadratique des mécanismes d'attention par des choix architecturaux innovants. En utilisant des techniques comme les motifs d'attention éparses et le partage efficace des paramètres, les réseaux Mamba peuvent générer des données de haute qualité avec des besoins en ressources beaucoup plus faibles. La recherche se concentrera sur la mise en œuvre d'optimisations matérielles pour améliorer l'efficacité des réseaux Mamba, les rendant adaptés aux applications en temps réel et aux dispositifs embarqués. Cela inclut l'optimisation des temps de formation et d'inférence, ainsi que l'exploration des accélérations matérielles potentielles. L'objectif est d'avancer le déploiement pratique de l'IA générative dans des domaines à ressources limitées, contribuant ainsi à son adoption plus large et à son impact.