{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T20:54:12Z","timestamp":1781816052799,"version":"3.54.5"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T00:00:00Z","timestamp":1747094400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"The Ministry of Human Resource Development, Government of India (SPARC\u00a0P#701), IIT Bhubaneswar Seed Grant","award":["SP093"],"award-info":[{"award-number":["SP093"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2025,5,31]]},"abstract":"<jats:p>Wearable and implantable medical devices (IMDs) are increasingly deployed to diagnose, monitor, and provide therapy for critical medical conditions. Such medical devices are safety-critical cyber-physical systems (CPSs). These systems support wireless features introducing potential security vulnerabilities. Although these devices undergo rigorous safety certification processes, runtime security attacks are inevitable. Based on published literature, IMDs such as pacemakers and insulin infusion systems can be remotely controlled to inject deadly electric shocks and excess insulin, posing a threat to a patient\u2019s life. While prior works based on formal methods have been proposed to detect potential attack vectors using different forms of static analysis, these have limitations in preventing attacks at runtime.<\/jats:p>\n          <jats:p>This article discusses a formal framework for detecting cyber-physical attacks on a pacemaker by monitoring its security policies at runtime. We propose a wearable device that senses the electrocardiogram (ECG) and photoplethysmogram (PPG) of the body to detect attacks in a pacemaker. To facilitate the design of this device, we map the security policies of a pacemaker w.r.t. ECG and PPG, paving the way for designing formal verification monitors for pacemakers for the first time using multiple physiological signals. The proposed monitoring framework allows the synthesis of parallel monitors from a given set of desired security policies, where all the monitors execute concurrently and generate an alarm to the user in the case of policy violation. Our implementation and the performance evaluation results demonstrate the technical feasibility of designing such a wearable device for attack detection in pacemakers. This device is separate from the pacemaker, ensuring no need for re-certification of pacemakers. Our approach is amenable to the application of security patches when new attack vectors are detected, making the approach ideal for runtime monitoring of medical CPSs.<\/jats:p>","DOI":"10.1145\/3638286","type":"journal-article","created":{"date-parts":[[2024,1,6]],"date-time":"2024-01-06T14:16:09Z","timestamp":1704550569000},"page":"1-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Securing Pacemakers Using Runtime Monitors over Physiological Signals"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5469-7032","authenticated-orcid":false,"given":"Abhinandan","family":"Panda","sequence":"first","affiliation":[{"name":"Indian Institute of Technology Bhubaneswar, Bhubaneswar, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7779-8231","authenticated-orcid":false,"given":"Srinivas","family":"Pinisetty","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Bhubaneswar, Bhubaneswar, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9654-5678","authenticated-orcid":false,"given":"Partha","family":"Roop","sequence":"additional","affiliation":[{"name":"University of Auckland, Auckland, New Zealand"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,5,13]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"issue":"6","key":"e_1_3_3_3_2","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/s10877-007-9097-5","article-title":"The relationship between the photoplethysmographic waveform and systemic vascular resistance","volume":"21","author":"Awad Aymen A.","year":"2007","unstructured":"Aymen A. Awad, Ala S. Haddadin, Hossam Tantawy, Tarek M. Badr, Robert G. Stout, David G. Silverman, and Kirk H. Shelley. 2007. The relationship between the photoplethysmographic waveform and systemic vascular resistance. J. Clin. Monitor. Comput. 21, 6 (2007), 365\u2013372.","journal-title":"J. Clin. Monitor. Comput."},{"issue":"11","key":"e_1_3_3_4_2","doi-asserted-by":"crossref","first-page":"1284","DOI":"10.1016\/j.jacc.2018.01.023","article-title":"Cybersecurity for cardiac implantable electronic devices: What should you know?","volume":"71","author":"Baranchuk Adrian","year":"2018","unstructured":"Adrian Baranchuk, Marwan M. Refaat, Kristen K. Patton, Mina K. Chung, Kousik Krishnan, Valentina Kutyifa, Gaurav Upadhyay, John D. Fisher, Dhanunjaya R. Lakkireddy, American College of Cardiology, et\u00a0al. 2018. Cybersecurity for cardiac implantable electronic devices: What should you know? J. Am. College Cardiol. 71, 11 (2018), 1284\u20131288.","journal-title":"J. Am. College Cardiol."},{"key":"e_1_3_3_5_2","volume-title":"Cardiac Pacemakers Step by Step: An Illustrated Guide","author":"Barold S. Serge","year":"2008","unstructured":"S. Serge Barold, Roland X. Stroobandt, and Alfons F. Sinnaeve. 2008. Cardiac Pacemakers Step by Step: An Illustrated Guide. John Wiley & Sons."},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/2000799.2000800"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1126\/science.347.6221.499"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.2174\/157340312801215782"},{"key":"e_1_3_3_9_2","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1007\/978-3-642-04694-0_4","volume-title":"International Workshop on Runtime Verification","author":"Falcone Ylies","year":"2009","unstructured":"Ylies Falcone, Jean-Claude Fernandez, and Laurent Mounier. 2009. Runtime verification of safety-progress properties. In International Workshop on Runtime Verification. Springer, 40\u201359."},{"key":"e_1_3_3_10_2","unstructured":"U.S. Food and Drug Administration. 2016. Postmarket Management of Cybersecurity in Medical Devices. Technical Report. Guidance for Industry and Food and Drug Administration Staff. Retrieved january 5 2023 from https:\/\/www.fda.gov\/downloads\/medicaldevices\/deviceregulationandguidance\/guidancedocuments\/ucm482022.pdf"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1161\/01.CIR.101.23.e215"},{"key":"e_1_3_3_12_2","first-page":"2","volume-title":"Proceedings of the ACM Association for Computing Machinery\u2019s Special Interest Group on Data Communications Conference (SIGCOMM\u201911)","author":"Gollakota Shyamnath","year":"2011","unstructured":"Shyamnath Gollakota, Haitham Hassanieh, Benjamin Ransford, Dina Katabi, and Kevin Fu. 2011. They can hear your heartbeats: Non-invasive security for implantable medical devices. In Proceedings of the ACM Association for Computing Machinery\u2019s Special Interest Group on Data Communications Conference (SIGCOMM\u201911). 2\u201313."},{"key":"e_1_3_3_13_2","first-page":"1125","volume-title":"Proceedings of the IEEE International Conference on Computer Communications (INFOCOM\u201911)","author":"Gollakota Shyamnath","year":"2011","unstructured":"Shyamnath Gollakota and Dina Katabi. 2011. Physical layer wireless security made fast and channel independent. In Proceedings of the IEEE International Conference on Computer Communications (INFOCOM\u201911). IEEE, 1125\u20131133."},{"key":"e_1_3_3_14_2","first-page":"129","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy (SP\u201908)","author":"Halperin Daniel","year":"2008","unstructured":"Daniel Halperin, Thomas S. Heydt-Benjamin, Benjamin Ransford, Shane S. Clark, Benessa Defend, Will Morgan, Kevin Fu, Tadayoshi Kohno, and William H. Maisel. 2008. Pacemakers and implantable cardiac defibrillators: Software radio attacks and zero-power defenses. In Proceedings of the IEEE Symposium on Security and Privacy (SP\u201908). IEEE, 129\u2013142."},{"key":"e_1_3_3_15_2","first-page":"7","volume-title":"Proceedings of the International Conference on Innovations in Information Technology (IIT\u201918)","author":"Hamadaqa Emad","year":"2018","unstructured":"Emad Hamadaqa, Ahmad Abadleh, Ayoub Mars, and Wael Adi. 2018. Highly secured implantable medical devices. In Proceedings of the International Conference on Innovations in Information Technology (IIT\u201918). IEEE, 7\u201312."},{"issue":"3","key":"e_1_3_3_16_2","doi-asserted-by":"crossref","first-page":"404","DOI":"10.7763\/IJCEE.2012.V4.522","article-title":"Study and analysis of ecg signal using matlab &labview as effective tools","volume":"4","author":"Islam M. K.","year":"2012","unstructured":"M. K. Islam, G. Tangim, T. Ahammad, MRH Khondokar, et\u00a0al. 2012. Study and analysis of ecg signal using matlab &labview as effective tools. Int. J. Comput. Electr. Eng. 4, 3 (2012), 404.","journal-title":"Int. J. Comput. Electr. Eng."},{"key":"e_1_3_3_17_2","first-page":"188","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Jiang Zhihao","year":"2012","unstructured":"Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur, and Rahul Mangharam. 2012. Modeling and verification of a dual chamber implantable pacemaker. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 188\u2013203."},{"key":"e_1_3_3_18_2","article-title":"Pacemaker hack can deliver deadly 830-volt jolt","volume":"17","author":"Kirk Jeremy","year":"2012","unstructured":"Jeremy Kirk. 2012. Pacemaker hack can deliver deadly 830-volt jolt. Computerworld 17 (2012).","journal-title":"Computerworld"},{"key":"e_1_3_3_19_2","first-page":"150","volume-title":"Proceedings of the IEEE 13th International Conference on E-health Networking, Applications and Services","author":"Li Chunxiao","year":"2011","unstructured":"Chunxiao Li, Anand Raghunathan, and Niraj K. Jha. 2011. Hijacking an insulin pump: Security attacks and defenses for a diabetes therapy system. In Proceedings of the IEEE 13th International Conference on E-health Networking, Applications and Services. IEEE, 150\u2013156."},{"key":"e_1_3_3_20_2","volume-title":"Cyber-physical Attacks: A Growing Invisible Threat","author":"Loukas George","year":"2015","unstructured":"George Loukas. 2015. Cyber-physical Attacks: A Growing Invisible Threat. Butterworth-Heinemann."},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.3758\/s13428-020-01516-y"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/2991079.2991094"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/TBME.2015.2441951"},{"key":"e_1_3_3_24_2","series-title":"LNCS","first-page":"494","volume-title":"International Conference on Formal Engineering Methods","volume":"7635","author":"Blech Jan Olaf","year":"2012","unstructured":"Jan Olaf Blech, Yli\u00e8s Falcone, and Klaus Becker. 2012. Towards certified runtime verification. In International Conference on Formal Engineering Methods(LNCS, Vol. 7635). Springer, 494\u2013509."},{"key":"e_1_3_3_25_2","unstructured":"Abhinandan Panda Srinivas Pinisetty and Partha Roop. 2022. Runtime monitoring and statistical approaches for correlation analysis of ECG and PPG. Retrieved from https:\/\/arxiv.org\/abs\/2202.00559"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3487212.3487342"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3412841.3442139"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3359986.3361200"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/TBME.2016.2613124"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2017.06.060"},{"key":"e_1_3_3_31_2","first-page":"1","volume-title":"Proceedings of the 16th ACM\/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE\u201918)","author":"Pinisetty Srinivas","year":"2018","unstructured":"Srinivas Pinisetty, Partha S. Roop, Vidula Sawant, and Gerardo Schneider. 2018. Security of pacemakers using runtime verification. In Proceedings of the 16th ACM\/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE\u201918). IEEE, 1\u201311."},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3092282.3092291"},{"key":"e_1_3_3_33_2","doi-asserted-by":"crossref","unstructured":"Laurie Pycroft and Tipu Z. Aziz. 2018. Security of implantable medical devices with wireless connections: The dangers of cyber-attacks. Expert Review of Medical Devices 15 6 (2018) 403\u2013406.","DOI":"10.1080\/17434440.2018.1483235"},{"key":"e_1_3_3_34_2","volume-title":"Black Hat Conference Presentation Slides","volume":"2011","author":"Radcliffe Jerome","year":"2011","unstructured":"Jerome Radcliffe. 2011. Hacking medical devices for fun and insulin: Breaking the human SCADA system. In Black Hat Conference Presentation Slides, Vol. 2011."},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/1653662.1653712"},{"issue":"6","key":"e_1_3_3_36_2","doi-asserted-by":"crossref","first-page":"1229","DOI":"10.12785\/ijcds\/0906020","article-title":"Cyber-attacks on medical implants: A case study of Cardiac Pacemaker vulnerability","volume":"9","author":"Rehman Muhammad Muneeb Ur","year":"2020","unstructured":"Muhammad Muneeb Ur Rehman, Hafiz Zia Ur Rehman, and Zeashan Hameed Khan. 2020. Cyber-attacks on medical implants: A case study of Cardiac Pacemaker vulnerability. Int. J. Comput. Digit. Syst. 9, 6 (2020), 1229\u20131235.","journal-title":"Int. J. Comput. Digit. Syst."},{"key":"e_1_3_3_37_2","article-title":"J&J Warned insulin pump vulnerable to cyber hacking","author":"Rockoff J. D.","year":"2016","unstructured":"J. D. Rockoff. 2016. J&J Warned insulin pump vulnerable to cyber hacking. Wall Street Journal (2016). Retrieved July 2023 from https:\/\/www.wsj.com\/articles\/j-j-warns-insulin-pump-vulnerable-to-cyber-hacking-1475610989","journal-title":"Wall Street Journal"},{"key":"e_1_3_3_38_2","first-page":"1099","volume-title":"Proceedings of the ACM SIGSAC Conference on Computer & Communications Security","author":"Rostami Masoud","year":"2013","unstructured":"Masoud Rostami, Ari Juels, and Farinaz Koushanfar. 2013. Heart-to-heart (H2H) authentication for implanted medical devices. In Proceedings of the ACM SIGSAC Conference on Computer & Communications Security. 1099\u20131112."},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/2667218"},{"key":"e_1_3_3_40_2","volume-title":"Proceedings of the 1st Workshop on Intrusion Detection and Network Monitoring (ID 99)","author":"Sekar R.","year":"1999","unstructured":"R. Sekar and Thomas Bowen. 1999. On preventing intrusions by process behavior monitoring. In Proceedings of the 1st Workshop on Intrusion Detection and Network Monitoring (ID 99)."},{"key":"e_1_3_3_41_2","article-title":"A formal verification methodology for DDD mode pacemaker control programs","volume":"2015","author":"Shuja Sana","year":"2015","unstructured":"Sana Shuja, Sudarshan K. Srinivasan, Shaista Jabeen, and Dharmakeerthi Nawarathna. 2015. A formal verification methodology for DDD mode pacemaker control programs. J. Electr. Comput. Eng. 2015 (2015).","journal-title":"J. Electr. Comput. Eng."},{"key":"e_1_3_3_42_2","first-page":"164","volume-title":"Proceeding of the International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation on Runtime Verification (RV-CuBES\u201917)","author":"Signoles Julien","year":"2017","unstructured":"Julien Signoles, Nikolai Kosmatov, and Kostyantyn Vorobyov. 2017. E-ACSL, a runtime verification tool for safety and security of c programs (tool paper). In Proceeding of the International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation on Runtime Verification (RV-CuBES\u201917). 164\u2013173."},{"issue":"10","key":"e_1_3_3_43_2","doi-asserted-by":"crossref","first-page":"2721","DOI":"10.1109\/TBME.2020.2969719","article-title":"Real-time quality assessment of long-term ECG signals recorded by wearables in free-living conditions","volume":"67","author":"Smital Lukas","year":"2020","unstructured":"Lukas Smital, Clifton R. Haider, Martin Vitek, Pavel Leinveber, Pavel Jurak, Andrea Nemcova, Radovan Smisek, Lucie Marsanova, Ivo Provaznik, Christopher L. Felton, et\u00a0al. 2020. Real-time quality assessment of long-term ECG signals recorded by wearables in free-living conditions. IEEE Trans. Biomed. Eng. 67, 10 (2020), 2721\u20132734.","journal-title":"IEEE Trans. Biomed. Eng."},{"key":"e_1_3_3_44_2","unstructured":"D. Takahashi. 2011. Insulin Pump Hacker Says Vendor Medtronic Is Ignoring Security Risk. Retrieved from https:\/\/venturebeat.com\/2011\/08\/25\/insulin-pump-hacker-says-vendor-medtronic-is-ignoring-security-risk\/."},{"issue":"01","key":"e_1_3_3_45_2","first-page":"1","article-title":"A survey of hardware trojan taxonomy and detection","author":"Tehranipoor Mohammad","year":"2016","unstructured":"Mohammad Tehranipoor and Farinaz Koushanfar. 2016. A survey of hardware trojan taxonomy and detection. IEEE Des. Test Comput. 01 (2016), 1\u20131.","journal-title":"IEEE Des. Test Comput."},{"key":"e_1_3_3_46_2","first-page":"23","volume-title":"Proceedings of the 4th International Conference on Secure Software Integration and Reliability Improvement","author":"Tuan Luu Anh","year":"2010","unstructured":"Luu Anh Tuan, Man Chun Zheng, and Quan Thanh Tho. 2010. Modeling and verification of safety critical systems: A case study on pacemaker. In Proceedings of the 4th International Conference on Secure Software Integration and Reliability Improvement. IEEE, 23\u201332."},{"key":"e_1_3_3_47_2","unstructured":"UPPAAL DBM Library. 2020. The Library Used to Manipulate DBMs in UPPAAL. Retrieved June 18 2020 from http:\/\/people.cs.aau.dk\/adavid\/UDBM\/"},{"key":"e_1_3_3_48_2","article-title":"Patients put at risk by computer viruses","author":"Weaver Christopher","year":"2013","unstructured":"Christopher Weaver. 2013. Patients put at risk by computer viruses. The Wall Street Journal (2013). Retrieved December 2023 from https:\/\/www.wsj.com\/articles\/SB10001424127887324188604578543162744943762\/","journal-title":"The Wall Street Journal"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/TBCAS.2013.2245664"},{"key":"e_1_3_3_50_2","doi-asserted-by":"crossref","unstructured":"Qiang Zhu Xin Tian Chau-Wai Wong and Min Wu. 2021. Learning your heart actions from pulse: ECG waveform reconstruction from PPG. IEEE Internet of Things Journal 8 23 (2021) 16734\u201316748.","DOI":"10.1109\/JIOT.2021.3097946"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3638286","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3638286","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:53:35Z","timestamp":1750287215000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3638286"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,13]]},"references-count":49,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,5,31]]}},"alternative-id":["10.1145\/3638286"],"URL":"https:\/\/doi.org\/10.1145\/3638286","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,5,13]]},"assertion":[{"value":"2023-02-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-11-26","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-05-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}