Towards Run-Time Verification of Adaptive Security for IoT in eHealth

This paper integrates run-time verification enablers in the feedback adaptation loop of the ASSET adaptive security framework for Internet of Things (IoT) in the eHealth settings and instantiates the resulting framework with Colored Petri Nets. The run-time enablers make machine-readable formal models of a system state and context available at run-time. In addition, they make requirements that define the objectives of verification available at run-time as formal specifications and enable dynamic context monitoring and adaptation. Run-time adaptive behavior that deviates from the normal mode of operation of the system represents a major threat to the sustainability of critical eHealth services. Therefore, the integration of run-time enablers into the ASSET adaptive framework could lead to a sustainable security framework for IoT in eHealth.