The imminent danger of cyber-physical malware (CPM) is evident from attacks such as the power outage in Ukraine, or the hijacking of a Jeep Cherokee. The traditional notion of malware is too narrow, and the prevalent characterizations (virus, worm, Trojan horse, spyware etc.) are neither precise nor comprehensive enough to characterize cyber-physical malware (CPM). Detecting sophisticated CPM is like searching for a needle in the haystack without knowing what the needle looks like. The technical briefing shall congregate interdisciplinary knowledge to describe the fundamentals of CPM, the mathematical foundation for analyzing and verifying CPM, the current state-of-the-art, the challenges, and directions for future research. Employing real-world examples, we shall illustrate the challenges of analyzing and verifying CPM.

CPS security problems are often rooted in the complex CPS software. It is hard for the CPS community to understand intricacies of software analysis and verification. And for the software engineering community, the lack of adequate CPS knowledge is a major roadblock. This makes it important to demystify CPM, so that software engineers can model the CPM problems, establish the mathematical foundation, and advance the software analysis and verification techniques to effectively address the CPM problems.

The knowledge about CPM gained through this technical briefing will be useful to understand the need for new modeling, analysis, and verification techniques. The real-world CPM examples from the technical briefing will bring out limitations of the current software security techniques and the need for new research directions. The experiment-discover paradigm mingled through the briefing will be of interest to innovate education in ways that arouse student’s curiosity and creativity.

The briefing will be shaped from the perspective of crucial needs for modeling, analyzing, and verifying CPM. It will cover:

Modeling: The Confidentiality-Integrity-Availability (CIA) triad characterizes the impact of the malware but it is not meant to facilitate analysis or verification of software. Modeling research is needed to characterize the program artifacts that enact CPM.
Analysis: Complete automation and machine learning are emphasized in many current research approaches to analyze software for security. The technical briefing will illustrate the shortcomings of such techniques and reflect on the need for a new type of analysis to address CPM.
Verification: Given the complexity of CPM and the possibility of catastrophic consequences, we will discuss the need for transparent verification that enable a human to easily participate by crosschecking the tool results or completing the verification where automation falls short.