Biblio

With the advent of network connectivity and complex software applications, life-critical systems like medical devices are subject to a plethora of security risks and vulnerabilities. Security threats and attacks exploiting these vulnerabilities have been shown to compromise patient safety by hampering essential functionality. This necessitates incorporating security from the very design of software. Isolation of software functionality into different modes and switching between them based on risk assessment, while maintaining a fail-safe mode ensuring device's essential functionality is a compelling design. Formal modeling is an essential ingredient for verification of such a design. Hence, in this paper, we formally model a trustworthy multi-modal framework for life-critical systems security and in turn safety. We formalize a multiple mode based software design approach of operation with a fail-safe mode that maintains critical functionality. We ensure trustworthyness by formalizing a composite risk model incorporated into the design for run-time risk assessment and management.

Network-connected embedded systems grow on a large scale as a critical part of Internet of Things, and these systems are under the risk of increasing malware. Anomaly-based detection methods can detect malware in embedded systems effectively and provide the advantage of detecting zero-day exploits relative to signature-based detection methods, but existing approaches incur significant performance overheads and are susceptible to mimicry attacks. In this article, we present a formal runtime security model that defines the normal system behavior including execution sequence and execution timing. The anomaly detection method in this article utilizes on-chip hardware to non-intrusively monitor system execution through trace port of the processor and detect malicious activity at runtime. We further analyze the properties of the timing distribution for control flow events, and select subset of monitoring targets by three selection metrics to meet hardware constraint. The designed detection method is evaluated by a network-connected pacemaker benchmark prototyped in FPGA and simulated in SystemC, with several mimicry attacks implemented at different levels. The resulting detection rate and false positive rate considering constraints on the number of monitored events supported in the on-chip hardware demonstrate good performance of our approach.