Modelling and Verification for Secure and Performant cPS – MoVe4SPS
A Digital Twin Approach for Studying Security-Performance Tradeoffs for Critical Cyber-Physical Systems
We propose to address security and performance aspects and their interrelationship in the lifecycle of cyber-physical systems using digital twins capable of handling security and performance aspects and containing explicit security countermeasures. The design is checked against its security and performance requirements and deployed relying on automated runtime monitors to detect security or performance issues. Identified problems are then fed back to update the digital twin model.
Reconcile security measures with safety and performance, with a special focus on critical infrastructures. We decided on a digital/analog twin and digital thread approach and a smart grid use case.
System security is a critical concern across all stages of a system's lifecycle, from development to operation. During development, engineering trade-offs often prioritize performance, functionality, or cost over achieving an ideal security infrastructure. As a result, many systems enter operation with vulnerabilities or imperfect protections. Addressing these gaps necessitates robust mechanisms during operation, including run time monitoring and anomaly detection, to detect and mitigate emerging security threats effectively. Ideally, these mechanisms should be foreseen throughout the design process, from the earliest phases onwards. Cyber-physical systems (CPS) are integrations of computational and physical processes, where embedded systems monitor and control physical components in real time. However, bridging the gap between development and operation poses significant challenges. Security vulnerabilities are often a byproduct of incomplete or siloed information transfer between these phases. Furthermore, addressing novel security issues requires navigating trade-offs between correctness, efficiency and security. Over-prioritizing one aspect can negatively affect others, for example, enforcing overly strict security measures may degrade system performance. To address this, we propose to leverage Digital Twin and Digital Thread technologies. Digital Twins, as virtual representations of physical systems, enable real-time monitoring, simulation, and analysis. Digital Threads extend this concept by providing a connected data flow that spans the entire system lifecycle, linking data from development, production, and operational phases. Together, these technologies can offer an integrated foundation for runtime monitoring and anomaly detection, particularly in addressing system security. We thus explore the application of Digital Twin and Digital Thread technologies to enhance security in cyber-physical systems. Our contribution includes the following novelties: - Security/Performance-Focused Application of Digital Twin and Digital Thread: We present a novel framework that prioritizes system security while guaranteeing performance, linking development-phase insights with operational monitoring for run time anomaly detection. This focused use of these technologies goes beyond their traditional roles in maintenance and performance optimization. - Application to a Smart Grid Use Case: We demonstrate the framework in the context of a smart grid and Electrical Vehicles (EV) charging application, a critical infrastructure with unique security challenges such as distributed control, real-time constraints, and 5G wireless inter-connectivity. This tailored application provides a practical example of addressing such challenges.
We give a short description of the overall method as shown in [2].
Initially in the design process, SysMD combines SysMLv2 with a constraint propagation solver and symbolic methods. This permits to model uncertainties by ranges, and to propagate them through different kind of structure and behavior. As a result, for system level quantities that occur in the MBSE (Model Based System Engineering) models, consistent, symbolically encoded ranges and sequences of ranges of feasible values in space and time can be obtained. Those can be used during operation as an indicator for anomalies like security breaches.
TTool is a free and open-source toolkit. Based on UML/SysML diagrams, it integrates simulation and formal verification at the push of a button. It includes methods dedicated to the design of embedded systems. TTool has been extended with features to enable digital/analog co-simulation (TTool-AMS). We thus conceive a virtual prototype which allows simulations on cycle/bit accurate level. Traces of performance results form both parts of the simulation are collected and analyzed; the results are the fed back into the higher/system-level models.
Timaeus-Net is an extended version of WoPANets tool for analyzing and verifying the worst-case performance of real-time networks, particularly in CPS domain. It is a decision-support tool based on Network Calculus, a formal and scalable timing analysis approach, destined to analyze the worst-case performance of large-scale real-time communication networks, such in smart grid for which real-time constraints need to be guaranteed.
Averest is a framework for the model-based design of reactive systems that supports the modeling, specification, simulation, compilation, formal verification, and synthesis of hardware and software for reactive embedded systems. It contains compilers for synchronous languages, a simulator for the latter, support for formal verification with temporal and other logics, and various transformations for the hardware and software synthesis of reactive embedded systems which also covers pure hardware circuits and pure software systems.
The strength of Lip6 is to perform full-system simulation efficiently. Developing a methodology for efficient cycle-bit-precise co-simulation between the virtual platform and the wireless network is the starting point our contribution. We combine dist-gem5 and the NS-3 network simulator. For large-scale simulations, we have access to the Lip6 computing clusters.
Wrt. the proposal, new tools have been integrated (SysMD), existing tools are developed further (TTool is currently extended with NS-3 modeling, Averest enriched with secure memory section handling). Some tools have been replaced by more recent developments :
WoPANets has been replaced by TimaeusNet, which is not free of charge, but ISAE works on an open version. SoCLib , which does not support a protocol stack, was replaced by Gem-5 to better interface with network simulators.
The precise case study was fixed early, april 2024.
Hagen Heermann, PhD student at RPTU-CS, supervised by C. Grimm and partially financed (18 months) by the project RPTU-CS, finished his thesis entitled "A Link Between Anomaly Detection and Runtime Verification" in october 2025. His work [1], compares and combines an AADD and hybrid automata based approach named H-classifier.
Marvin Häuser and Klaus Schneider published [4] and implemented a fully-featured prototype for the rustc compiler frontend (the compiler backend and OS changes are work-in-progress). The joint guarantees from changes to type checking, trait solving, and restrictive secret primitive type APIs allow proving select security properties (e.g., consant-time programming, relaxed noninterference) at compile time while maintaining almost all of Rust’s expressiveness. The prototype’s paper is currently being reviewed at ACM CCS 2026 and recently proceeded to round 2.
The following publications issued from the project until now:
[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.
So far, we organized three in-person project meetings/workshops, in Paris april 2024 and march 2025, Toulouse in february 2026, and regular visio conferences, first every two weeks, since this year monthly. The next in-person meeting is projected in november either in Sophia-Antipolis or in Kaiserslautern, when we hope to welcome back Christoph Grimm and Alan Birchler de Allende.
The project also organized a full-day workshop at CPS/IoT Week (Irvine, California, USA, May 6, 2025) organized by Johannes Koch (RPTU/CS) and Daniela Genius (Lip6), focused on model-based system engineering, with a keynote by Petri Solanti, Siemens, and proceedings published by ACM in the following document : (https://dl.acm.org/doi/proceedings/10.1145/3735948).
Several other papers have been submitted/are currently under review.
We have to point out that for the above mentioned reasons (timely start but financing shortened by half for the german partners, delay in Lip6’s PhD thesis, gap period for ISAE’s PhD student, serious health problems of some participants) not all partners are at the same state of advancement. We however found solutions to organize our collaboration accordingly, owing a lot to partners internal and external to the project volunteering additional work.
An outstanding feature is thus that the project attracted quite a number of researchers not directly financed by ANR MoVe4SPS and incited them to contribute on their own (Marvin Häuser, PhD student with RPTU-ES, on secure memory sections and compilation, Marina Dehez-Clementi from ISAE on cyber security and network modeling, Bastien Sultan, PostDoc at Télécom Paris, with Lip6 on formalization of block replication and complex communication schemes in TTool-AVATAR).
Two Master 2 internships took place in spring/summer 2024 and spring/summer 2025, respectively, leading to two complementary Phd theses by Alan Birchler de Allende (TP/ISAE) and Malou Rayon-Richter.
TP recentlty recruited a PostDoctoral researcher (Dr. Aissam Belghiat).
Malou Rayon-Richter will continue to develop his hybrid simulation approach for CPS, with embedded and networking aspects in mind. For simulation, he will combine dist-gem5 and NS-3 based simulation. We will also take up the TTool-AMS extension (Cortez-Porto/Genius/Apvrille SoSym 2021) which will evolve to support larger-scale digital/analog co-simulation and transfer results on improved methods on synchronization and causality and integrate the feedback of information from simulation with the virtual prototype.
Future work by ISAE will focus on identifying which parameters should be encrypted and which may remain unencrypted, based on their respective contributions to the overall security of the system. Following the development and evaluation of his simulation platform and the acquisition of preliminary results concerning the optimization of the performance–security trade-off, a research visit to Sophia Antipolis Lab would enable Alan to assess and validate his findings in a real-world 5G network environment.
Future work by RPTU-CPS is currently ensured by Moritz Herzog; a new PhD student and will focus on the evolution of the digital/analog twin model.
Regarding the security work on rustc by RPTU-ES, besides completing the prototype in the compiler backend and OS areas, future research includes basic information flow tracking for LLVM, separate code generation for, e.g., crypto code (relaxing compiler optimizations, applying mitigations like SLH and retpolines only locally), and integrating the rustc prototype with Averest as part of its software synthesis capabilities. Due to the security guarantees of the changes to Rust and rustc, as well as Rust’s focus on low-level and zero-cost abstractions, we expect significant alignment with the project’s goals.
Cyber-physical systems (CPS) are gaining a steadily increasing share of critical ecosystems and infrastructures. CPS can also be found inside autonomous vehicles, aircraft, health care equipment, the smart grid, and smart factories. Components of CPS combine analog parts such as sensors and actuators with digital control and networked software systems.
The design of these systems requires the integration of a high number of system components from many different disciplines.
Security and performance are of crucial importance, in the complete development-operation continuum.
Tightly entangled, security and performance are not always compatible.
Our objective is to define an adequate methodology to model and verify CPS with security requirements, considering trade-offs
between performance, security, development and runtime.
Project coordination
Daniela Genius (LIP6)
The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.
Partnership
LIP6 LIP6
DISC Département d'Ingénierie des Systèmes Complexes
LTCI Laboratoire Traitement et Communication de l'Information
Help of the ANR 516,628 euros
Beginning and duration of the scientific project:
February 2024
- 36 Months
