Modeling and Verification for Secure and Performant Cyber-Physical Systems

• Applicants: Professor Dr. Christoph Grimm; Professor Dr. Klaus Schneider
• Subject Area: Computer Architecture, Embedded and Massively Parallel Systems ; Security and Dependability, Operating-, Communication- and Distributed Systems
• Term: since 2023
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 530118585

Cyber-physical systems (CPS) are becoming an increasingly important part of critical infrastructure. CPSs can be found in autonomous vehicles, aircrafts, healthcare devices, smart grids, and smart factories. In addition to functional requirements, CPS must also meet non-functional requirements such as real-time behavior with limited power consumption. Due to safety-critical applications, verification is often mandatory to avoid malfunctioning behavior with catastrophic consequences. CPSs are inherently open as they interact with other systems. In addition, CPS need to be updated (often) after deployment due to subsequent updates to their environment. The networked implementation of CPS adds another layer of difficulty, making cybersecurity even more difficult to manage, since communication between networked systems can be attacked at any time. Model-based design methods have proven successful for the design of both embedded and cyber-physical systems. Such a design starts with a hardware-independent model of the system that can be verified against its functional requirements. However, non-functional requirements such as performance, power consumption, and security cannot yet be addressed at this level, since these properties depend on the partitioning into networked components and the hardware/software partitioning of the latter. However, this initial model-based design is very useful for satisfying the non-functional requirements, since one can derive different correct system implementations from the correct model in a design space exploration. Static analysis and virtual prototypes are among the techniques we will rely on for this optimization phase. While correctness is usually our primary objective, the later implementation of new security mechanisms in updated versions of a CPS may affect its performance and real-time behavior. Therefore, we propose to address the security and performance aspects (and their interrelationship) in the CPS lifecycle using digital twins capable of addressing the security and performance aspects, where the digital twin contains explicit security countermeasures. This design is then verified against its security and performance requirements. The system is then deployed using automated monitoring techniques that rely on runtime monitors to detect security or performance problems at runtime. Detected problems are then fed back into the design models, which are subsequently updated, e.g. with new security countermeasures. We will evaluate and demonstrate the results with a smart grid management system from a previous EU project.

• DFG Programme: Research Grants
• International Connection: France
• Cooperation Partners: Professor Dr. Ludovic Apvrille; Professorin Dr. Daniela Genius; Professorin Dr. Ahlem Mifdaoui