Browsing by Author "Pinisetty S."

Now showing 1 - 3 of 3

On the Runtime Enforcement of Timed Properties
(2019) Falcone Y.; Pinisetty S.
Runtime enforcement refers to the theories, techniques, and tools for enforcing correct behavior of systems at runtime. We are interested in such behaviors described by specifications that feature timing constraints formalized in what is generally referred to as timed properties. This tutorial presents a gentle introduction to runtime enforcement (of timed properties). First, we present a taxonomy of the main principles and concepts involved in runtime enforcement. Then, we give a brief overview of a line of research on theoretical runtime enforcement where timed properties are described by timed automata and feature uncontrollable events. Then, we mention some tools capable of runtime enforcement, and we present the TiPEX tool dedicated to timed properties. Finally, we present some open challenges and avenues for future work. � 2019, Springer Nature Switzerland AG.
Securing implantable medical devices with runtime enforcement hardware
(2019) Pearce H.; Kuo M.M.Y.; Roop P.S.; Pinisetty S.
In 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.
Security of pacemakers using runtime verification
(2018) Pinisetty S.; Roop P.S.; Sawant V.; Schneider G.
The US Food and Drug Administration (FDA) recently recalled approximately 465,000 pacemakers that were vulnerable to hacking. It was reported that hackers could either pace the devices rapidly inducing arrhythmia or could drain the battery. Such actions would compromise the health and well being of the patient concerned. Considering this, techniques to ensure the security of implantable medical devices is an emerging area of research. To the best of our knowledge, existing techniques lack the formal rigour for ensuring the safety and security of such systems. While methods exist for formal verification of pacemaker software, these are not suitable to prevent security vulnerabilities. To this end we develop a run-time verification based approach. Our approach proposes a wearable device that non-invasively senses the familiar ECG signals in order to determine if a pacemaker has been compromised. We develop a set of timed policies to be monitored at run-time. We provide a methodology for the design of the wearable device and results demonstrate the technical feasibility of the developed concept. � 2018 IEEE.