Opacity of Large-Scale Cyber-Physical Systems

• Applicant: Professor Dr. Majid Zamani
• Subject Area: Automation, Mechatronics, Control Systems, Intelligent Technical Systems, Robotics
• Term: since 2021
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 449086651

In the last decade, there has been a significant interest in the algorithmic verification of or correct-by-construction controller synthesis for cyber-physical systems (CPSs), in which software components interact tightly with physical systems. CPSs are increasingly performing safety-critical tasks in modern life where design fault or security vulnerability can be catastrophic. Autonomous vehicles, implantable medical devices, and smart and connected communities are some of the prominent examples that underscore privacy and safety-criticality of modern CPSs. In the past few years, safety concerns have received considerable attention in the design of CPSs, while security analysis is left as an afterthought for the later stages. One of the important security properties is called opacity. Roughly speaking, opacity is a confidentiality or privacy property in security analysis that characterizes whether or not some "secret" information about the system (e.g., defender) can be inferred by outside observers with potentially malicious intentions (e.g., intruders or attackers). Many of the CPS applications are safety-critical with some vulnerability to (cyber) attacks and opacity can provide some formal guaranties for the plausible deniability of the system's "secret" in the presence of a potentially malicious observer. This project aims at enlarging the applicability of formal methods for designing safe and secure CPSs. Recent theoretical advances due to, among others, the members of our team make this goal achievable.In particular, we propose algorithmic approaches to synthesize secure-by-construction controllers for CPSs. In this methodology, we assume the safety requirements for the system are described using a temporal logic (such as linear temporal logic) formula or using automata on infinite strings. Then, we construct a finite abstraction of the CPS such that opacity properties are preserved over the abstraction and a secure-by-construction controller designed on the finite abstraction can be refined into a secure-by-construction one on the original system. To mitigate the computational complexity involved in dealing with finite systems, we also propose compositional methodologies on formally verifying or enforcing opacity for large-scale interconnected CPSs by leveraging decomposition as a key tool to tackle the analysis or design complexity.

• DFG Programme: Research Grants
• International Connection: China
• Partner Organisation: National Natural Science Foundation of China
• Cooperation Partner: Professor Xiang Yin, Ph.D.