Formal Methods for the Security of Medical Devices1
Srinivas Pinisetty, Nathan T. Allen, Hammond A. Pearce, Mark L. Trew, Manoj Singh Gaur, Partha S. Roop · 2022
Cyber-physical (CP) attacks, originate in cyber space but damage physical infrastructure, and are a significant recent research focus. Such attacks have affected many CP systems such as smart grids, intelligent transportation systems and medical devices. In this chapter we consider techniques for the detection and mitigation of CP attacks on medical devices. It is obvious that such attacks have immense safety implications. Our work is based on formal methods, a class of mathematically-founded techniques for the specification and verification of safety-critical systems. A cardiac pacemaker is our motivating medical device and we describe its interaction with the heart. We then provide an overview of formal methods with particular emphasis on run-time based approaches, which are ideal for the design of security monitors. Subsequently, we discuss in detail two recent approaches developed in our group for attack detection and mitigation. This chapter is a comprehensive overview of run-time based formal approaches for the attack detection and mitigation of medical devices.