Secure-by-construction Cyber-physical Systems

Security-related attacks are increasingly becoming pervasive in safety-critical cyber-physical systems (CPS) such as implantable and wearable medical devices, autonomous vehicles, smart communities, and smart infrastructure. Security vulnerabilities related to information leaks in CPS are extremely difficult to discover and mitigate as the interaction between the embedded control software and the physical environment exposes numerous attack surfaces for malicious exploitation. An important class of security properties is called opacity. Opacity is a confidentiality 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).

In HyConSys lab, we are working on efficient and decidable approaches for the formal verification and synthesis of opacity properties for complex CPS using abstraction-based techniques.

The following are some of the problems we are interested to study:

• Analysis of (approximate) opacity for (stochastic) cyber-physical systems

• Compositional verification and synthesis of opacity for (stochastic) interconnected systems

Active lab members

The following lab members are actively working on this topic:

• Siyuan Liu

• Majid Zamani

Related publications

The following publications are related to this active topic:

• X. Yin and M. Zamani. On approximate opacity of cyber-physical systems. Submitted for publication.

• K. Zhang, X. Yin, and M. Zamani. Opacity of nondeterministic transition systems: A (bi)simulation relation approach. IEEE Transactions on Automatic Control, accepted.

• J. Hou, X. Yin, S. Li, and M. Zamani. Abstraction-based synthesis of opacity-enforcing controllers using alternating simulation relations. The 58th IEEE Conference on Decision and Control (CDC), December 2019, to appear.