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