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

MCPS-VeriSec：基于模型的医疗网络物理系统安全

• 批准号: EP/W014785/1
• 负责人: Nicola Paoletti
• 金额: $ 54.08万
• 依托单位: Royal Holloway University of London
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2022
• 资助国家: 英国
• 起止时间: 2022 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FW014785%2F1
• 关键词: MCPS; VeriSec; Model; based; Security

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.

需要通过植入式和可穿戴设备进行治疗的医疗状况在英国和全球范围内变得越来越普遍。例子包括用心脏装置治疗心律失常以及用人工胰腺系统调节糖尿病的血糖。此类设备经历了巨大的技术进步，演变成复杂的计算系统——我们称之为医疗网络物理系统（medCPS）——其中包括用于自动治疗交付的控制算法以及用于远程患者监控以及与智能设备和临床系统通信的互联网连接。 medCPS 的复杂性带来了广泛的攻击面，可能危及患者的安全。由于机器学习 (ML) 的快速采用来辅助治疗决策，这种情况变得更加严重，因为机器学习特别容易受到隐秘的对抗性输入的影响。先前关于 medCPS 安全性的工作主要集中在攻击的实际可行性（例如，如何使用无线电发射器重新配置设备），从而导致简单、易于检测的攻击（例如暂停治疗）。这让我们不禁要问，是否可以衍生出更复杂的攻击，例如更隐蔽或更适合目标患者的攻击。我们的目标是研究 medCPS 安全性中的这些以及其他先前未探索的维度。在 MCPS-VeriSec 中，我们建议开发一个框架，以提供经过验证的防御机制，防止针对 medCPS 的隐形攻击，特别是传感器欺骗攻击。我们将采用基于模型的方法来系统地探索攻击空间和安全威胁。我们将特别关注以下方向： - 帕累托最优攻击和防御。攻击有效性（即，它对预期治疗的破坏程度）和隐蔽性（检测的难度）之间存在自然的权衡。 MCPS-VeriSec 将能够自动合成帕累托最优攻击（即，所述权衡是最优的）和相应的防御。这可以被视为一个多目标（MO）两人游戏，我们将通过引入生成对抗网络的一种新颖的 MO 变体来解决这个问题。 - 防御机制。我们将考虑两种协调防御，旨在分别检测和减轻恶意信号扰动。-经过验证的防御。我们建议应用形式验证来证明防御的安全概率，使用验证结果来重新训练和增强防御。特别是，我们将引入同类中的第一个概率验证方法来支持因果效应的推理，我们将用它来精确评估防御措施的有效性。无攻击状态。 - 个性化。我们将通过将受害者的生理状态和医疗设备的信息纳入用于合成的 medCPS 模型中，得出个性化的攻击和防御。利用我们基于模型的方法，我们将探索一系列对手的能力，从白盒攻击（使用包含受害者完整准确信息的模型合成）到黑盒攻击（使用替代或不确定模型）。我们将把我们的方法应用于两种最流行的 medCPS：用于心律失常治疗的 ICD（植入式心脏复律除颤器）和用于治疗心律失常的人工胰腺控制算法。 胰岛素治疗。对于每个案例研究，我们都会将传统（非 ML）设备控制器与基于 ML 的设备控制器的对抗性攻击的鲁棒性进行比较。MCPS-VeriSec 将成为医疗领域中第一个研究 Pareto 攻击、受害者个性化、ML 漏洞和正式验证的防御措施的公司，从而瞄准即将到来的新一代联网且支持 ML 的医疗设备。该项目产生的新颖综合和验证方法不仅与医疗应用高度相关，而且与基于模型的 CPS 安全领域高度相关。

项目成果

Synthesizing Pareto-Optimal Signal-Injection Attacks on ICDs

综合 ICD 的帕累托最优信号注入攻击

• DOI: 10.1109/access.2022.3233010
• 发表时间: 2023
• 期刊: IEEE Access
• 影响因子: 3.9
• 作者: Krish, Veena;Paoletti, Nicola;Smolka, Scott A.;Rahmati, Amir
• 通讯作者: Rahmati, Amir