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.

在英国和全球范围内，需要通过可植入和可穿戴设备进行治疗的医疗状况越来越普遍。例子包括对心脏器件的心律不齐治疗以及用人造胰腺系统的糖尿病中的葡萄糖调节。这样的设备经历了巨大的技术进步，不断发展为复杂的计算系统 - 我们称为医学网络物理系统（MEDCPSS），其中包括用于自动治疗交付的控制算法以及用于远程患者监测以及与智能设备和临床系统的远程患者监测和通信的Internet连接。 MEDCPS的复杂性引入了广泛的攻击表面，可能会危及患者的安全。通过迅速采用机器学习（ML）来帮助治疗决策，这加剧了这一点，这些决策特别容易受到隐秘的对抗性投入的影响。先前的MEDCPS安全性工作主要集中在攻击的实际可行性上（例如，如何使用无线电发射器重新配置设备），从而简单，易于检测到攻击（例如暂停治疗）。这导致我们询问是否可以提出更多复杂的攻击，例如，对目标患者的量身定制或更适合量身定制。我们的目的是研究MEDCPS安全性中这些和其他以前未开发的维度。在MCPS-Verisec中，我们建议开发一个框架，以提供验证的防御机制，以防止对MEDCPS的隐秘攻击，特定的传感器欺骗攻击。我们将采用一种基于模型的方法来实现对攻击空间和安全威胁的系统探索。特别是，我们将重点关注以下方向： - 帕累托最佳攻击和防御。攻击效率（即，它破坏了预期的治疗）和隐身性（检测到多么困难）之间存在自然的权衡。 MCPS-VERISEC将实现帕累托最佳攻击的自动合成（即，所述权衡是最佳的）和相应的防御能力。这可以看作是一种多目标（MO）两人游戏，我们将通过引入新颖的MO变体来解决生成对抗性网的新型MO。我们将考虑两个协调的防御，旨在分别检测和减轻恶意信号扰动。-经过验证的防御。我们建议使用验证结果进行验证和增强防御能力，以证明防御措施的安全概率。特别是，我们将介绍同类概率验证方法，以支持有关因果影响的推理，我们将用来精确评估防御能力的有效性W.R.T.无攻击条件。 - 个性化。我们将通过将有关受害者的生理状态和医疗设备的信息纳入用于合成的MEDCPS模型中，来得出个性化的攻击和防御。利用我们的基于模型的方法，我们将探索一系列对手能力，从白盒攻击（使用具有完整而准确的受害者信息的模型合成）到黑盒攻击（使用替代或不确定的模型）。胰岛素疗法。对于每个案例研究，我们将将鲁棒性与传统（非ML）设备控制器对基于ML的攻击进行比较。MCPS-VERISEC将是医学环境中第一个研究帕累托攻击，受害者个性化，ML漏洞，正式验证的防御和正式验证的防御措施，并针对即将连接的医疗服务和ML-LL-LL-able-ablem-able-ablem-able-ablem-able-able-ablem-able-ablem-able-ablem-able-ablem-able-ablem-able-ablem-able-able-able-able-able-able-apper ables的攻击。该项目产生的新型综合和验证方法不仅与医疗应用有关，而且对于一般的基于模型的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