Pearce H.Kuo M.M.Y.Roop P.S.Pinisetty S.2025-02-172019http://dx.doi.org/10.1145/3359986.3361200https://idr.iitbbs.ac.in/handle/2008/2578In recent years we have seen numerous proof-of-concept attacks on implantable medical devices such as pacemakers. Attackers aim to breach the strict operational constraints that these devices operate within, with the end-goal of compromising patient safety and health. Most efforts to prevent these kinds of attacks are informal, and focus on application- and system-level security-for instance, using encrypted communications and digital certificates for program verification. However, these approaches will struggle to prevent all classes of attacks. Runtime verification has been proposed as a formal methodology for monitoring the status of implantable medical devices. Here, if an attack is detected a warning is generated. This leaves open the risk that the attack can succeed before intervention can occur. In this paper, we propose a runtime-enforcement based approach for ensuring patient security. Custom hardware is constructed for individual patients to ensure a safe minimum quality of service at all times. To ensure correctness we formally verify the hardware using a model-checker. We present our approach through a pacemaker case study and demonstrate that it incurs minimal overhead in terms of execution time and power consumption. � 2019 Association for Computing Machinery.enCyber-Physical AttacksCyber-Physical Systems (CPS)Formal VerificationPacemakersRuntime EnforcementSecurityConference Paper