Synthesizing Stealthy Reprogramming Attacks on Cardiac Devices

TL;DR

This paper introduces a formal, optimization-based method to synthesize stealthy and effective reprogramming attacks on Implantable Cardioverter Defibrillators, aiming to disrupt therapy while remaining undetected.

Contribution

It presents the first systematic approach to generate ICD reprogramming attacks that balance effectiveness and stealthiness using multi-objective optimization and formal methods.

Findings

Successfully derives optimal attack parameters along the Pareto front.

Demonstrates attack effectiveness on synthetic cardiac signals.

Generalizes to unseen patient signals, indicating robustness.

Abstract

An Implantable Cardioverter Defibrillator (ICD) is a medical device used for the detection of potentially fatal cardiac arrhythmia and their treatment through the delivery of electrical shocks intended to restore normal heart rhythm. An ICD reprogramming attack seeks to alter the device's parameters to induce unnecessary shocks and, even more egregious, prevent required therapy. In this paper, we present a formal approach for the synthesis of ICD reprogramming attacks that are both effective, i.e., lead to fundamental changes in the required therapy, and stealthy, i.e., involve minimal changes to the nominal ICD parameters. We focus on the discrimination algorithm underlying Boston Scientific devices (one of the principal ICD manufacturers) and formulate the synthesis problem as one of multi-objective optimization. Our solution technique is based on an Optimization Modulo Theories encoding of the problem and allows us to derive device parameters that are optimal with respect to the effectiveness-stealthiness tradeoff (i.e., lie along the corresponding Pareto front). To the best of our knowledge, our work is the first to derive systematic ICD reprogramming attacks designed to maximize therapy disruption while minimizing detection. To evaluate our technique, we employ an extensive dataset of synthetic EGMs (cardiac signals), each generated with a prescribed arrhythmia, allowing us to synthesize attacks tailored to the victim's cardiac condition. Our approach readily generalizes to unseen signals, representing the unknown EGM of the victim patient.