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安全的工作主要集中在攻击的实际可行性上（例如，如何使用无线电发射器重新配置设备），从而导致简单，易于检测的攻击（例如暂停治疗）。这让我们不禁要问，是否可以衍生出更复杂的攻击，例如，更隐蔽或更适合目标患者的攻击。我们的目标是调查医疗cps安全中这些和其他以前未探索的维度。在MCPS-VeriSec中，我们建议开发一个框架来提供经过验证的防御机制，以防止对medcps的隐形攻击，特别是传感器欺骗攻击。我们将采用基于模型的方法来系统地探索攻击空间和安全威胁。特别是，我们将重点关注以下方向：-帕累托最优攻击和防御。在攻击的有效性（游戏邦注：即它在多大程度上破坏了预期的治疗）和隐蔽性（游戏邦注：即它有多难以被发现）之间存在着一种自然的权衡。MCPS-VeriSec将自动合成帕累托最优攻击（即，上述权衡是最优的）和相应的防御。这可以看作是一个多目标（MO）双人游戏，我们将通过引入生成对抗网络的一种新的MO变体来解决这个问题。——防御机制。我们将考虑两种协同防御，分别用于检测和减轻恶意信号干扰。-经过验证的防御。我们建议采用形式验证来验证防御的安全概率，并利用验证结果对防御进行再培训和增强。特别地，我们将引入第一个概率验证方法来支持因果效应的推理，我们将使用它来精确地评估在无攻击条件下防御的有效性。——个性化。我们将通过将有关受害者的生理状态和医疗设备的信息纳入用于合成的medCPS模型，得出个性化的攻击和防御。利用我们基于模型的方法，我们将探索一系列对手的能力，从白盒攻击（使用关于受害者的完整和准确信息的模型合成）到黑盒攻击（使用代理或不确定的模型）。我们将把我们的方法应用于两种最流行的医疗cps：用于心律失常治疗的icd（植入式心律转复除颤器）和用于胰岛素治疗的人工胰腺控制算法。对于每个案例研究，我们将比较传统（非机器学习）设备控制器与基于机器学习的设备控制器的对抗性攻击的鲁棒性。MCPS-VeriSec将是第一个在医疗领域调查帕累托攻击、受害者个性化、机器学习漏洞和正式验证防御的公司，从而针对即将到来的一代联网和支持机器学习的医疗设备。该项目产生的新型合成和验证方法不仅与医疗应用高度相关，而且与基于模型的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