Formal robustness for Cyber-Physical Systems under Sensor Attacks 

Oct 29 11:30-12:30. WWH 335

Jian Xiang

Department of Software and Information Systems

Abstract:

Cyber-physical systems, such as autonomous vehicles, must defend against attacks that target sensor hardware. Analyzing system design can help system engineers understand how a compromised sensor could impact the system’s behavior; however, developing security guarantees, especially formal guarantees, for cyber-physical systems is difficult due to their combination of discrete dynamics, continuous dynamics, and nondeterminism. In this talk, we will introduce a series of our recent works in using formal methods for modeling and analyzing sensor attacks on cyber-physical systems. These works formalize and analyze a system’s robustness properties, which express whether a system’s safety property can be affected by sensor attacks. The talk will especially focus on quantitative safety, which measures the minimum distance of a system’s reachable states to the unsafe region. In particular, we will discuss (1) notions of quantitative safety, (2) notions of quantitative robustness, and (3) reasoning techniques for quantitative robustness. For the reasoning of robustness, we have developed a notion called simulation distance, which is defined based on the behavioral distances between the original system and the system with compromised sensors. The simulation distance helps characterize upper bounds of the safety loss caused by the sensor attacks. We have developed relational reasoning techniques to prove simulation distance. These formal notions and techniques have been applied to a few case studies in various CPS models.

Bio: 

Jian Xiang is an Assistant Professor in the Department of Software and Information Systems at UNC Charlotte’s College of Computing and Informatics. His primary research goal is to advance the state of the art in formal methods for the correctness and security of computer systems, particularly cyber-physical systems (CPSs), and to develop tools and techniques for building systems that are provably correct and secure. His broader research interests include formal verification, language-based security, information-flow analysis, and cyber-physical systems.