Modélisation et Vérification pour CPS Sécurisés et Performants – MoVe4SPS
Une approche par jumeau numérique pour l'étude des compromis sécurité-performance des systèmes cyber physiques critiques
Nous proposons d'aborder les aspects de sécurité et de performance, et leur interrelation, au long du cycle de vie des systèmes cyberphysiques, grâce à des jumeaux numériques capables de gérer ces aspects et intégrant des contre-mesures de sécurité explicites. La conception est vérifiée au regard des exigences de sécurité et de performance, puis déployée, en s'appuyant sur des moniteurs d'exécution automatisés. Les problèmes identifiés sont ensuite intégrés au modèle de jumeau numérique.
Concilier les mesures de sécurité avec la sûreté et la performance, avec attention particulière aux infrastructures critiques. Nous avons opté pour une approche de jumeau et de fil numérique .
La sécurité des systèmes est une préoccupation majeure à toutes les étapes de leur cycle de vie, du développement à l'exploitation. Lors du développement, les choix d'ingénierie privilégient souvent la performance, la fonctionnalité ou le coût au détriment d'une infrastructure de sécurité idéale. De ce fait, de nombreux systèmes entrent en service avec des vulnérabilités ou des protections imparfaites. Combler ces lacunes exige des mécanismes robustes en exploitation, notamment la surveillance en temps réel et la détection d'anomalies, afin de détecter et d'atténuer efficacement les nouvelles menaces de sécurité. Idéalement, ces mécanismes devraient être prévus dès les premières phases de conception. Les systèmes cyberphysiques (CPS) intègrent des processus informatiques et physiques, où des systèmes embarqués surveillent et contrôlent des composants physiques en temps réel. Cependant, la transition entre le développement et l'exploitation représente un défi de taille. Les vulnérabilités de sécurité résultent souvent d'un transfert d'informations incomplet ou cloisonné entre ces phases. De plus, la résolution de nouveaux problèmes de sécurité nécessite de trouver un équilibre entre exactitude, efficacité et sécurité. Prioriser excessivement un aspect peut nuire aux autres ; par exemple, des mesures de sécurité trop strictes peuvent dégrader les performances du système. Pour remédier à cela, nous proposons d'exploiter les technologies de jumeau numérique et de fil numérique. Les jumeaux numériques, représentations virtuelles de systèmes physiques, permettent la surveillance, la simulation et l'analyse en temps réel. Les fils numériques étendent ce concept en fournissant un flux de données continu couvrant l'intégralité du cycle de vie du système, reliant les données des phases de développement, de production et d'exploitation. Nous explorons ainsi l'application des technologies de jumeau numérique et de fil numérique afin d'améliorer la sécurité des systèmes cyber-physiques. Notre contribution comprend les nouveautés suivantes : - Application des jumeaux numériques et des fils numériques axée sur la sécurité et la performance : Nous présentons un nouveau cadre qui privilégie la sécurité du système tout en garantissant la performance, en reliant les enseignements tirés de la phase de développement à la surveillance opérationnelle pour la détection d'anomalies en temps réel. Cette utilisation ciblée de ces technologies dépasse leurs rôles traditionnels dans la maintenance et l'optimisation des performances. - Application à un cas d'usage de réseau intelligent : Nous présentons le cadre dans le contexte d'un réseau intelligent et d'une application de recharge pour véhicules électriques (VE), une infrastructure critique confrontée à des défis de sécurité spécifiques tels que le contrôle distribué, les contraintes de temps réel et l'interconnexion sans fil 5G. Cette application sur mesure fournit un exemple concret de solution à ces défis.
Nous présentons une brève description de la méthode globale décrite dans [2].
Lors de la conception initiale, SysMD combine SysMLv2 avec un solveur de propagation de contraintes et des méthodes symboliques. Ceci permet de modéliser les incertitudes par intervalles et de les propager à travers différents types de structures et de comportements. Ainsi, pour les grandeurs système présentes dans les modèles MBSE (Ingénierie Système Basée sur les Modèles), on obtient des intervalles et des séquences d'intervalles de valeurs possibles cohérents et codés symboliquement dans l'espace et le temps. Ces intervalles peuvent être utilisés en fonctionnement comme indicateur d'anomalies telles que des failles de sécurité.
TTool est une boîte à outils libre et open source. Basée sur les diagrammes UML/SysML, elle intègre la simulation et la vérification formelle en un clic. TTool a été étendu pour permettre la co-simulation numérique/analogique (TTool-AMS). Nous concevons ainsi un prototype virtuel permettant des simulations précises au niveau du cycle/bit. Les traces des résultats de performance des deux parties de la simulation sont collectées et analysées ; les résultats sont ensuite réinjectés dans les modèles de niveau supérieur/système.
Timaeus-Net est une version étendue de WoPANets, conçu pour analyser et vérifier les performances dans le pire des cas des réseaux temps réel, notamment dans le domaine des CPS. Cet outil d'aide à la décision repose sur le calcul de réseau, approche d'analyse temporelle formelle et évolutive, destinée à analyser les performances dans le pire des cas des réseaux de communication temps réel à grande échelle, tels que les réseaux intelligents (smart grids) pour lesquels les contraintes temps réel doivent être garanties.
Averest est un framework de conception de systèmes réactifs basé sur des modèles. Il prend en charge la modélisation, la spécification, la simulation, la compilation, la vérification formelle et la synthèse matérielle et logicielle des systèmes embarqués réactifs. Il comprend des compilateurs pour les langages synchrones, un simulateur pour ces derniers, la prise en charge de la vérification formelle avec des logiques temporelles et autres, ainsi que diverses transformations pour la synthèse matérielle et logicielle des systèmes embarqués réactifs, couvrant aussi bien les circuits matériels que les systèmes logiciels.
Le point fort de Lip6 est sa capacité à réaliser efficacement des simulations complètes de systèmes. Notre contribution repose sur le développement d'une méthodologie de co-simulation précise au cycle et au bit. Nous combinons dist-gem5 et le simulateur de réseau NS-3.
Concernant la proposition, de nouveaux outils ont été intégrés (SysMD), et les existants sont perfectionnés (TTool est actuellement étendu avec la modélisation NS-3, Averest enrichi d'une d'une gestion sécurisée des section mémoire.WoPANets a été remplacé par TimaeusNet, payante, mais l'ISAE développe une version libre).
L'étude de cas précise a été fixée dès avril 2024.
Hagen Heermann, doctorant à l'Université technique du Pacifique Nord (RPTU-CS), sous la direction de C. Grimm et bénéficiant d'un financement partiel (18 mois) du projet RPTU-CS, a soutenu sa thèse intitulée « Lien entre détection d'anomalies et vérification à l'exécution » en octobre 2025. Ses travaux [1] comparent et combinent une approche basée sur la détection d'anomalies et une approche hybride par automates, appelée H-classifier.
Marvin Häuser et Klaus Schneider ont publié [4] et implémenté un prototype complet pour le frontend du compilateur rustc (le backend du compilateur et les modifications du système d'exploitation sont en cours de développement). Les garanties conjointes issues des modifications apportées à la vérification des types, à la résolution des traits et aux API restrictives de types primitifs secrets permettent de prouver certaines propriétés de sécurité à la compilation, tout en préservant la quasi-totalité de l'expressivité de Rust. L'article décrivant le prototype est actuellement en cours d'évaluation à la conférence ACM CCS 2026 et a récemment franchi l'étape suivante.
Voici les publications issues de ce projet à ce jour :
[1] H. Heermann, C. Grimm. Bridging the Gap Between Anomaly Detection and Runtime Verification: H-Classifiers. 2025 Design Automation and Test in Europe, Mar 2025, Lyon, France. ⟨hal-05029242⟩
[2] H. Heermann, J. Koch, Ch. Grimm, D. Genius, L. Apvrille, Ah. Mifdaoui, K. Schneider : “Digital Twin and Digital Thread for System Security and Performance applied to an Electrical Vehicle Charging Use Case”, 2025 Forum on Specification & Design Languages (FDL), St. Goar, Germany, pp. 1-8, (IEEE) (2025)
[3] M. Rayon‑Richter, D. Genius : “Tool Support for Precise Assessment of Software Security/Performance Tradeoffs”, 2025 Work-in progress session, Forum on Specification & Design Languages (FDL), St. Goar, Germany, pp. 1-2, (IEEE), (ISBN: 979-8-3315-9379-7) (2025)
[4] M. Häuser, K. Schneider. Secret Types Require OS-Backed Secrecy Code Sections. 2025 Workshop on Modeling and Verification for Secure and Performant Cyber-Physical Systems (MoVe4SPS '25), Sep. 2025, Irvine, CA, USA.
[5] M. Rayon-Richter, D. Genius, L. Apvrille, Compromis entre sécurité et performance : étude cycle-précise, extended abstract and poster, colloque GDR SoC2, Marseille, juin 2026.
À ce jour, nous avons organisé 3 réunions/ateliers de projet en présentiel, à Paris en avril 2024 et mars 2025, et à Toulouse en février 2026, ainsi que des conférences Visio régulières, d'abord toutes les 2 semaines, puis mensuellement depuis cette année. La prochaine réunion en présentiel est prévue en novembre. Le projet a également organisé un workshop lors de la CPS/IoT Week (Irvine, Californie, États-Unis, 6 mai 2025), co-organisé par RPTU/CS et Lip6 et consacré à l'ingénierie système basée sur les modèles, avec une conférence inaugurale par Petri Solanti (Siemens) et actes publiées par ACM.
Il convient de préciser que, pour les raisons évoquées précédemment (démarrage en temps voulu mais financement réduit des partenaires allemands, retard dans la thèse de doctorat de Lip6, interruption de carrière pour le doctorant de l'ISAE, graves problèmes de santé de certains participants), tous les partenaires n'en sont pas au même stade d'avancement. Nous avons toutefois trouvé des solutions pour adapter notre collaboration, grâce notamment à l'implication de partenaires internes et externes au projet qui ont fourni un travail supplémentaire.
Un aspect remarquable du projet est qu'il a attiré de nombreux chercheurs non financés directement par l'ANR MoVe4SPS et les a incités à y contribuer (Marvin Häuser, doctorant à RPTU-ES), sur les sections de mémoire sécurisées et la compilation ; Marina Dehez-Clementi de l'ISAE, sur la cybersécurité et la modélisation des réseaux ; Bastien Sultan, post-doctorant à Télécom Paris, avec Lip6, sur la formalisation de la réplication par blocs et des schémas de communication complexes dans TTool-AVATAR).
Deux stages de Master 2 ont eu lieu respectivement au printemps/été 2024 et au printemps/été 2025, aboutissant à deux thèses de doctorat complémentaires, l'une d'Alan Birchler de Allende (TP/ISAE) et l'autre de Malou Rayon-Richter.
TP a récemment recruté un chercheur postdoctoral (Dr Aissam Belghiat).
Malou Rayon-Richter poursuivra son approche de simulation hybride pour les CPS, en tenant compte des aspects embarqués et du réseau. Il combinera les simulations basées sur dist-gem5 et NS-3. Nous intégrerons également l'extension TTool-AMS, qui évoluera pour prendre en charge la co-simulation numérique/analogique à plus grande échelle et transférer les résultats sur des méthodes améliorées de synchronisation et de causalité, et intégrer le retour d'information de la simulation au prototype virtuel.
Les travaux futurs de l'ISAE porteront sur l'identification des paramètres à chiffrer et de ceux pouvant rester non chiffrés, en fonction de leur contribution respective à la sécurité globale du système. Après le développement et l'évaluation de sa plateforme de simulation et l'acquisition de résultats préliminaires concernant l'optimisation du compromis performance-sécurité, un séjour de recherche au laboratoire Sophia Antipolis permettra à Alan d'évaluer et de valider ses conclusions dans un environnement de réseau 5G réel.
Les travaux futurs du RPTU-CPS sont actuellement assurés par Moritz Herzog, doctorant, et porteront sur l'évolution du modèle de jumeau numérique/analogique.
Concernant les travaux de sécurité sur rustc menés par le RPTU-ES, outre la finalisation du prototype au niveau du compilateur et du système d'exploitation, les recherches futures incluent le suivi des flux d'informations de base pour LLVM, la génération de code séparée pour, par exemple, le code cryptographique et l'intégration du prototype rustc avec Averest dans le cadre de ses fonctionnalités de synthèse logicielle.
Les systèmes cyber-physiques (CPS) sont en train de gagner une part croissante d'écosystèmes et d'infrastructures critiques. CPS sont également présents dans des véhicules autonomes, des avions, des équipements médicaux, et des réseaux électriques et usines intelligentes. Composants des CPS combinent parties analogiques tels que capteurs et actionneurs avec un contrôle numérique et des systèmes logiciels sur réseau. La conception de ces systèmes nécessite l'intégration d'un grand nombre de composants système de disciplines très diverses.
La sécurité et la performance sont d'importance cruciale dans le continuum développement-exécution. Étroitement imbriquées, elles ne sont pas toujours conciliables. Notre objectif est la définition d'une méthodologie adéquate de modélisation et vérification des CPS avec des contraintes de sécurité, prenant en compte les compromis entre performance, sécurité, développement et exécution.
Coordination du projet
Daniela Genius (LIP6)
L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.
Partenariat
LIP6 LIP6
DISC Département d'Ingénierie des Systèmes Complexes
LTCI Laboratoire Traitement et Communication de l'Information
Aide de l'ANR 516 628 euros
Début et durée du projet scientifique :
février 2024
- 36 Mois
