MCPS-VeriSec: Model-based Security of Medical Cyber-Physical Systems

Medical conditions requiring treatment via implantable and wearable devices are becoming increasingly prevalent in the UK and worldwide. Examples include arrhythmia treatment with cardiac devices and glucose regulation in diabetes with artificial pancreas systems. Such devices have experienced dramatic technological advancements, evolving into complex computing systems - which we call medical cyber-physical systems (medCPSs) - that include control algorithms for automated therapy delivery as well as internet connectivity for remote patient monitoring and communication with smart devices and clinical systems.

The complexity of medCPSs introduces broad attack surfaces that can jeopardize patient safety. This is exacerbated by the rapid adoption of machine learning (ML) to aid therapy decisions, which are particularly susceptible to stealthy adversarial inputs.

Prior work on medCPS security has mainly focused on the practical feasibility of the attacks (e.g., how to use a radio transmitter to reconfigure the device), resulting in simple, easy to detect, attacks (such as suspending therapy). This leads us to ask whether more sophisticated attacks can be derived that, for instance, are stealthier or better tailored to the target patient. Our aim is to investigate these and other previously unexplored dimensions in medCPS security.

In MCPS-VeriSec we propose to develop a framework to provide verified defence mechanisms against stealthy attacks on medCPSs, sensor spoofing attacks specifically. We will take a model-based approach to enable systematic exploration of the attack space and safety threats. In particular, we will focus on the following directions:
- Pareto-optimal attacks and defences. There is a natural trade-off between attack effectiveness (i.e., how much it disrupts the intended therapy) and stealthiness (how hard it is to detect). MCPS-VeriSec will enable automated synthesis of Pareto-optimal attacks (i.e., for which said trade-off is optimal) and corresponding defences. This can be viewed as a multi-objective (MO) two-player game, which we will solve by introducing a novel MO variant of generative adversarial nets.
- Defense mechanisms. We will consider two coordinated defences, designed to respectively detect and mitigate malicious signal perturbations.
- Verified defences. We propose to apply formal verification to certify the safety probability of the defences, using the verification results to retrain and enhance the defences. In particular, we will introduce the first probabilistic verification method of its kind to support reasoning about causal effects, which we will use to precisely assess the effectiveness of the defences w.r.t. the no-attack condition.
- Personalization. We will derive personalized attacks and defences by incorporating information about the victim's physiological state and medical device into the medCPS model used for synthesis. Leveraging our model-based approach, we will explore a range of adversary capabilities, from white-box attacks (synthesized using models with full and accurate information about the victim) to black-box attacks (using surrogate or uncertain models).

We will apply our approach to two of the most prevalent medCPSs: ICDs (Implantable Cardioverter Defibrillators) for cardiac arrhythmia treatment and artificial pancreas control algorithms for insulin therapy. For each case study, we will compare the robustness to adversarial attacks of traditional (non-ML) device controllers against ML-based ones.

MCPS-VeriSec will be the first in the medical context to investigate Pareto attacks, victim personalization, ML vulnerabilities, and formally verified defenses, thereby targeting the soon-to-come generation of connected and ML-enabled medical devices. The novel synthesis and verification methods resulting from this project will be highly relevant not just for medical applications, but for the field of model-based CPS security in general.