Formal Threat Analysis of Machine Learning-Based Control Systems: A Study on Smart Healthcare Systems

Modern cyber-physical systems (CPSs) use the Internet of Things (IoT) to collect and exchange data efficiently, monitor device/sensor level interaction effectively, and adopt new standards effortlessly. Machine learning (ML) models are growingly used in the controllers of these IoT-enabled CPSs for pattern identification, state estimation, prediction, and anomaly detection. However, sophisticated adversaries can launch various attacks on the communication network and the hardware/firmware to introduce corrupted sensor measurements to manipulate the ML-based CPSs and create critical physical hazards. Hence, analyzing the threat space of a CPS is essential to understand the system's strength and identify the most vital resources to protect. However, existing studies have not proposed any verifiable solution for the threat analysis of ML-based CPSs. This paper presents a novel framework that uses efficient mechanisms to extract constraints from ML-based decision models and perform a formal threat analysis to identify potential false data injection (FDI) attack paths and corresponding effects on an IoT-enabled ML-based CPS. Our framework can provide us with all possible attack vectors, each representing a set of sensor measurements to be altered for a CPS given a specific set of attack attributes. The attack vectors enable us to assess the system's resiliency, thus providing insight to enhance the system's robustness. We consider an internet of medical things-enabled safety-critical CPS naming smart healthcare system (SHS) as the reference case. We validate our framework on a real SHS dataset, proving our framework's success in revealing feasible FDI attack paths. Our evaluation using synthetic and two real SHS datasets also affirms the tool's efficacy in the threat analysis of ML-based CPSs.