Synthesizing stealthy reprogramming attacks on cardiac devices

摘要: An Implantable Cardioverter Defibrillator (ICD) is a medical device used for the detection of potentially fatal cardiac arrhythmias and their treatment through delivery electrical shocks intended to restore normal heart rhythm. ICD reprogramming attack seeks alter device's parameters induce unnecessary therapy or prevent required therapy. In this paper, we present formal approach synthesis attacks that are both effective, i.e., lead fundamental changes in therapy, stealthy, hard detect. We focus on discrimination algorithm underlying Boston Scientific devices (one principal manufacturers) formulate problem as one multi-objective optimization. Our solution technique based an Optimization Modulo Theories encoding allows us derive optimal with respect effectiveness-stealthiness tradeoff. method can be tailored patient's current condition, readily generalizes new rhythms. To best our knowledge, work first systematic designed maximize disruption while minimizing detection.