Checking and Enforcing Security Through Opacity in Healthcare Applications

摘要

The Internet of Things (IoT) is a paradigm that can tremen-dously revolutionize health care thus benefiting both hospitals, doc¬tors and patients. In this context, protecting the IoT in health care against interference, including service attacks and malwares, is challeng¬ing. Opacity is a confidentiality property capturing a system's ability to keep a subset of its behavior hidden from passive observers. In this work, we seek to introduce an IoT-based heart attack detection system, that could be life-saving for patients without risking their need for privacy through the verification and enforcement of opacity. Our main contribu¬tions are the use of a tool to verify opacity in three of its forms, so as to detect privacy leaks in our system. Furthermore, we develop an effi¬cient, Symbolic Observation Graph (SOG)-based algorithm for enforcing opacity.