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

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

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.