Completion de code outillé et supportée par des patterns de conceptions
L'IA générative et les grands modèles de langage (LLM), tels que Copilot et ChatGPT, peuvent compléter le code basé sur des fragments initiaux écrits par un développeur. Ils sont intégrés dans des environnements de développement logiciel tels que le VS code. De nombreux articles analysent les avantages et les limites de ces approches pour la génération de code, le code produit est souvent correct et les résultats sont de mieux en mieux.
Cependant, une quantité étonnamment faible de travaux ont été effectuées dans le contexte des modèles logiciels (par exemple basés sur UML). Des articles ont conclu que si les performances des LLM actuels pour la modélisation logicielle sont encore limitées (contrairement à la génération de code), il est nécessaire (contrairement à la génération de code) d'adapter nos pratiques d'ingénierie basées sur des modèles à ces nouveaux assistants. et les intégrer dans les méthodes et outils MBSE.
L'intégration des design-patterns est une partie complémentaire de ce travail. Le terme pattern de conception a été adopté dans le domaine logiciel pour capturer une solution éprouvée pour un problème donné avec ses avantages et ses inconvénients. Un peu plus tard, le terme anti-pattern a été proposé pour identifier les modèles qui sont connus pour ne pas fonctionner ou qui présentent de graves inconvénients. Ainsi, lors de la proposition d'une complétion, l'assistant pourrait explicitement référencer un modèle de conception existant avec ses implications. La proposition d'achèvement peut être basée soit sur des fragments de modèle identifiés (y compris des exigences modélisées), soit sur une sélection de modèle explicite.
Cette thèse explorera l'état de l'art de la complétion de modèles avec l'IA et les modèles de pattern et le support des outils associés. Jusqu'à présent, peu de travaux sont disponibles sur la formalisation des patrons et leur utilisation dans les outils de modélisation. Elle proposera d'identifier l'intention des dévéloppeurs, à partir de modèles partiels. La tâche pourrait être basée sur des règles, mais devrait également explorer des approches d'apprentissage automatique. Mettre en œuvre une proposition de réalisation dans le cadre d'un outil de conception, notamment Papyrus SW designer. La solution sera évaluée.
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.
Estimation de l'incertitude d'un réseau de neurones profond sur des cibles embarquées
Au cours de la dernière décennie, les réseaux neuronaux profonds (DNN) sont devenus un choix populaire pour mettre en œuvre les composants basés sur de l'apprentissage (LEC) dans les systèmes automatisés grâce à leur efficacité dans le traitement d'entrées complexes et à leur puissant apprentissage de représentation qui surpasse les performances des méthodes traditionnelles. Malgré les progrès remarquables réalisés dans l'apprentissage des représentations, les réseaux neuronaux doivent également représenter la confiance dans leurs prédictions pour pouvoir être déployés dans des systèmes critiques en termes de sécurité. Les réseaux neuronaux bayésiens (BNN) offrent un cadre fondé sur des principes pour modéliser et capturer l'incertitude dans les LEC. Cependant, l'inférence exacte dans les BNN est difficile à calculer. Nous nous appuyons donc sur des techniques d'échantillonnage pour obtenir une approximation de la véritable postériorité des poids afin de calculer la distribution prédictive postérieure (inférence). À cet égard, des méthodes d'échantillonnage relativement simples mais coûteuses en calcul et en mémoire ont été proposées pour l'inférence bayésienne approximative afin de quantifier l'incertitude dans les DNN, par exemple le Monte-Carlo dropout ou les Deep Ensembles. L'estimation efficace de l'incertitude des DNN sur des plates-formes matérielles à ressources limitées reste un problème ouvert, limitant l'adoption dans les applications de systèmes hautement automatisés qui possèdent des budgets de calcul et de mémoire stricts, des contraintes de temps courtes et des exigences de sécurité. Cette thèse vise à développer de nouvelles méthodes et des optimisations matérielles pour une estimation efficace et fiable de l'incertitude dans les architectures DNN modernes déployées dans des plateformes matérielles avec des ressources de calcul limitées.
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.