Cas d'Assurance Dynamiques pour les Systèmes Autonomes Adaptatifs

Donner l'assurance que les systèmes autonomes fonctionneront de manière sûre et sécurisée est une condition préalable à leur déploiement dans des domaines d'application critiques en termes de mission et de sécurité. Généralement, les assurances sont fournies sous la forme de cas d'assurance, qui sont des arguments vérifiables et raisonnés démontrant qu'une revendication de haut niveau (concernant généralement la sécurité ou d'autres propriétés critiques) est satisfaite compte tenu d'un ensemble de preuves relatives au contexte, à la conception et à la mise en œuvre d'un système. L'élaboration de cas d'assurance est traditionnellement une activité analytique, réalisée hors ligne avant le déploiement du système, et sa validité repose sur des hypothèses/prédictions concernant le comportement du système (y compris ses interactions avec son environnement). Cependant, il a été avancé que cette approche n'est pas viable pour les systèmes autonomes qui apprennent et s'adaptent en cours de fonctionnement. Cette thèse abordera les limites des approches d'assurance existantes en proposant une nouvelle catégorie de techniques d'assurance de la sécurité fondées sur la sécurité qui évaluent et font évoluer en permanence le raisonnement de sécurité, en même temps que le système, afin de fournir une assurance de la sécurité tout au long de son cycle de vie. En d'autres termes, l'assurance de la sécurité sera fournie non seulement au cours du développement et du déploiement initiaux, mais aussi en cours d'exécution, sur la base de données opérationnelles.

Modélisation et simulation du comportement humain pour des jumeaux numériques centrés sur l'humain

Grâce à une représentation virtuelle synchronisée, les jumeaux numériques sont un moyen pour produire des analyses, prédictions et optimisations de systèmes du monde réel. Or certains de ces systèmes interagissent étroitement avec les humains de sorte que le rôle de ces derniers est déterminant dans le fonctionnement du système. C’est par exemple le cas dans des contextes comme l’industrie 5.0 ou la gestion du pilotage de systèmes critiques, où la qualité de la collaboration entre les humains et les machines dépendra de l’anticipation de leurs actions, interactions et décisions respectives. Ainsi, pour améliorer la précision des prédictions et étendre l’applicabilité dans divers domaines, il est nécessaire, en s’appuyant sur les connaissances issues des sciences humaines et sociales, de développer des jumeaux numériques qui prennent en compte la complexité et la richesse des comportements humains (processus décisionnels, interactions, émotions…). Ces modèles comportementaux pourront notamment s’appuyer sur l’apprentissage automatique, l’exploration de données, la modélisation basée sur des agents et l’ingénierie des connaissances. Après avoir identifié les modèles de comportements humains utiles, il s’agira d’étudier leur articulation conceptuelle et leur intégration technique avec les modèles des entités cyber-physiques dans le système de jumeau numérique. De plus, nous explorerons comment les services de jumeaux numériques sont impactés et peuvent être révisés pour prendre en compte ces aspects centrés sur l’humain. Enfin, nous évaluerons l’efficacité des jumeaux numériques centrés sur l’humain dans diverses applications en mettant en œuvre des expériences sur des cas réels représentatifs.
Ce travail de recherche ambitionne les contributions suivantes :
• Le développement d'une approche basée sur des modèles de comportement humain pour obtenir des jumeaux numériques centrés sur l'humain.
• Des connaissances nouvelles sur l'impact du comportement humain sur le contrôle d'un système et inversement.
• Des applications pratiques et des recommandations sur l’usage de jumeaux numériques centrés sur l'humain dans des scénarios du monde réel.
Cette thèse se déroulera à Grenoble.

Analyses statiques avancées basées sur les types pour la vérification de systèmes d'exploitations

Dans des travaux récents [RTAS 2021], nous avons démontré l'intérêt d'une analyse statique guidée
par un système de types dépendants avancé pour analyses des programmes systèmes bas-niveau, allant
jusqu'à pouvoir vérifier automatiquement l'absence d'escalade de privilège dans un noyau de système
d'exploitation embarqué comme conséquence de la type-safety du code du noyau. La gestion de la
mémoire est un problème particulièrement ardu lors de l'analyse de programmes systèmes, ou plus largement,
de programmes écrits en C, et l'analyse basée sur les types fournit une solution satisfaisante à
applicabilité large (par exemple, code de gestion de structures de données [VMCAI 2022], runtime de
langage dynamique, code applicatif orienté performance, etc.)

Le but de la thèse est d'étendre le applications qui peuvent être faites de l'utilisation d'une analyse
statique basée sur les types.

[RTAS’21] No Crash, No Exploit: Automated Verification of Embedded Kernels. O. Nicole, M. Lemerre,
S. Bardin, X. Rival (Best paper)
[VMCAI’22] Lightweight Shape Analysis based on Physical Types, O. Nicole, M. Lemerre, X. Rival
[POPL’23] SSA Translation Is an Abstract Interpretation, M. Lemerre (Distinguished paper).

Cadre formel pour la spécification et la vérification de flots de communication de processus distribués dans le Cloud

Les clouds sont constitués de serveurs interconnectés via internet, sur lesquels on peut implémenter des systèmes faisant usages d’applications et de bases de données déployées sur les serveurs. L’informatique basée sur les clouds gagne considérablement en popularité, y compris pour y déployer des systèmes critiques. De ce fait, disposer d’un cadre formel pour raisonner sur ce type de systèmes devient une nécessité. Une exigence sur un tel cadre est qu’ils permettent de raisonner sur les concepts manipulés dans un cloud, ce qui inclue naturellement la capacité à raisonner sur des systèmes distribués, composés de sous-systèmes déployés sur différentes machines et interagissant par passage de messages pour réaliser des services. Dans ce contexte, la facilité à raisonner sur les flots de communications est un élément central. L'objectif de cette thèse est de définir un cadre formel outillé dédié à la spécification et la vérification de systèmes déployés sur des clouds. Ce cadre capitalisera sur le cadre formel des "interactions". Les interactions sont des modèles dédiés à la spécification des flots de communications entre différents acteurs d'un système. Les travaux de thèse étudieront comment définir des opérateurs de structuration (enrichissement, composition) et de raffinement pour permettre de mettre en œuvre des processus de génie logiciel classique en se basant sur les interactions.

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.

Top