  Smart healthcare systems (SHSs) are providing fast and efficient disease
treatment leveraging wireless body sensor networks (WBSNs) and implantable
medical devices (IMDs)-based internet of medical things (IoMT). In addition,
IoMT-based SHSs are enabling automated medication, allowing communication among
myriad healthcare sensor devices. However, adversaries can launch various
attacks on the communication network and the hardware/firmware to introduce
false data or cause data unavailability to the automatic medication system
endangering the patient's life. In this paper, we propose SHChecker, a novel
threat analysis framework that integrates machine learning and formal analysis
capabilities to identify potential attacks and corresponding effects on an
IoMT-based SHS. Our framework can provide us with all potential attack vectors,
each representing a set of sensor measurements to be altered, for an SHS given
a specific set of attack attributes, allowing us to realize the system's
resiliency, thus the insight to enhance the robustness of the model. We
implement SHChecker on a synthetic and a real dataset, which affirms that our
framework can reveal potential attack vectors in an IoMT system. This is a
novel effort to formally analyze supervised and unsupervised machine learning
models for black-box SHS threat analysis.
