Cyber-Physical Systems (CPSs), especially those involving autonomy, need guarantees of their safety. Runtime Enforcement (RE) is a lightweight method to formally ensure that some specified properties are satisfied over the executions of the system. Hence, there is recent interest in the RE of CPS. However, existing methods are not designed to tackle specifications suitable for the hybrid dynamics of CPS. With this in mind, we develop runtime enforcement of CPS using properties defined in Signal Temporal Logic (STL).

Wearable and implantable medical devices (IMDs) are increasingly deployed to diagnose, monitor, and provide therapy for critical medical conditions. Such medical devices are safety-critical cyber-physical systems (CPSs). These systems support wireless features introducing potential security vulnerabilities. Although these devices undergo rigorous safety certification processes, runtime security attacks are inevitable. Based on published literature, IMDs such as pacemakers and insulin infusion systems can be remotely controlled to inject deadly electric shocks and excess insulin, posing a threat to a patient’s life. While prior works based on formal methods have been proposed to detect potential attack vectors using different forms of static analysis, these have limitations in preventing attacks at runtime. This article discusses a formal framework for detecting cyber-physical attacks on a pacemaker by monitoring its security policies at runtime. We propose a wearable device that senses the electrocardiogram (ECG) and photoplethysmogram (PPG) of the body to detect attacks in a pacemaker. To facilitate the design of this device, we map the security policies of a pacemaker w.r.t. ECG and PPG, paving the way for designing formal verification monitors for pacemakers for the first time using multiple physiological signals. The proposed monitoring framework allows the synthesis of parallel monitors from a given set of desired security policies, where all the monitors execute concurrently and generate an alarm to the user in the case of policy violation. Our implementation and the performance evaluation results demonstrate the technical feasibility of designing such a wearable device for attack detection in pacemakers. This device is separate from the pacemaker, ensuring no need for re-certification of pacemakers. Our approach is amenable to the application of security patches when new attack vectors are detected, making the approach ideal for runtime monitoring of medical CPSs.

Runtime Enforcement (RE) is a monitoring technique aimed at correcting possibly incorrect executions w.r.t. a set of formal requirements (properties) of a system. In this paper, we consider enforcement monitoring of real-time properties. Thus, executions are modelled as timed words and specifications as timed automata. Moreover, we consider that the enforcer has the ability to delay events by storing or buffering them into its internal memory (and releasing them when the property is finally satisfied) and suppressing events when no delaying is appropriate. Practically, in an implementation, the internal memory of the enforcer is finite. In this paper, we propose a new RE paradigm for timed properties, where the memory of the enforcer is bounded/finite, to address practical applications with memory constraints and timed specifications. Bounding the memory presents a number of difficulties, e.g., how to accommodate a timed event into the memory when the memory is full, s.t., regardless of the course of action we choose to handle this situation, the behaviour of the bounded enforcer should not significantly differ from that of the unbounded enforcer. The problem of how to optimally discard events when the buffer is full is significantly more difficult in a timed environment where the progress of time affects the satisfaction or violation of a property. We define the bounded-memory RE problem for timed properties and develop a framework for regular timed properties specified as timed automata. The proposed framework is implemented in Python, and its performance is evaluated. From experiments, we discovered that the enforcer has a reasonable execution time overhead.

Spiking Neural Networks (SNNs) have found increasing utility in designing safety-critical Cyber-Physical Systems (CPSs) such as implantable medical devices, autonomous vehicles, and space robotics due to their capability to operate on information represented in temporal coding and exhibit various behavioural modalities. Thus, there has been recent interest in formally verifying their timing behaviours and providing soundness guarantees of their diverse characteristics. However, beyond the simplistic Leaky Integrate and Fire (LIF) model, which only mimics 3 spiking behaviours, there is a lack of unifying methodology in literature to verify complex dynamics of biological neurons exhibiting 20 spiking behaviours as demonstrated by the pioneering work of Izhikevich. There is also a complete lack of formulation for the verification of SNN-based systems. This paper bridges these gaps by proposing a model-based approach for designing SNN-based controllers in CPS. We propose sound structural transformations translating any spiking neuron into networks of Timed Automata (TA), model the complex Izhikevich neural model and formally verify all 20 timing behaviours it exhibits for the first time. We then present two case studies that were modelled as SNNs using our approach: the PID controller, and the Car-Following controller, and subsequently attempt static model checking and statistical verification of their generated TA models for safety guarantees.

Diabetes is a global health threat, and its prevalence is rising at an alarming rate. Diabetes is the cause of severe complications in vital organs of the body. So, diabetes must be detected early for timely treatment and to prevent the condition from escalating to severe consequences. Many AI and machine learning approaches have been proposed for the non-invasive continuous monitoring of diabetes. However, using such informal methods in healthcare monitoring raises concerns about reliability. Furthermore, deploying an AI-based solution to continuously monitor a person's health state on resource-constrained embedded devices is a concern. We overcome these shortcomings in this work by proposing a formal runtime monitoring system for the first time for diabetes detection using Electrocardiogram (ECG) sensing. We implement a data mining model from the ECG features to infer ECG policies and thereby synthesize a formal verification monitor based on the policies. Using a diabetes dataset, we evaluate the verification monitor's performance compared to other proposed models.

Distributed systems are rife with failures. Several resiliency patterns are used to improve the ability of these systems to tolerate faults and maintain functionality. The circuit breaker pattern is a popular resiliency pattern that is especially suitable for the case when the faults causing dependency failures take a variable amount of time to resolve. In this paper, we propose a modification to the traditional circuit breaker pattern. We also propose a gossip-based information dissemination protocol that enables the (modified) circuit breakers deployed on multiple client-service instances to take a concerted and more informed decision when a common dependency is facing persistent failures. We formally model the client-server systems that use traditional and the proposed distributed circuit breaker patterns in UPPAAL to analyze and compare their performance. The statistical model checking queries performed on the models show that, as compared to the traditional circuit breaker pattern, the distributed version results in fewer unsuccessful requests, that consume system/network resources, with practically the same total execution time under various availability conditions - only at the famously low cost of a robust gossip-based information dissemination protocol.

Automatic detection of cardiac arrhythmia is an important tool in the fight against cardiovascular diseases and their associated human impacts. Such detection needs to be both accurate and timely, in order to allow for interventions to be administered within short time frames. Traditionally, such approaches have used black box implementations which are not explainable and hence have limited use in terms of clinical interpretability. Additionally, these implementations may either require additional training between patients, or have processing times which make them unsuitable for real-time classification. To address this, we develop a set of formal Timed Automaton-based policies that capture three common arrhythmia, Premature Ventricular Contraction, Ventricular Tachycardia, and Atrial Fibrilation, in terms of Electrocardiogram (ECG) features. We synthesise Runtime Verification monitors for each of these policies, and run them alongside existing clinical ECG databases to evaluate their efficacy. This approach shows comparable results to existing black box work with accuracies ranging from 90 % to 96 % while still being both explainable and clinically interpretable.

Unmanned aerial drones are Cyber-Physical Systems (CPSs) with increasing availability, popularity, and capability. Although other aeronautical and safety-critical industries apply stringent regulations and design approaches, smaller drones tend to have much weaker and informal design requirements. Due to the strong open-source movement in this space, there are numerous opportunities for malicious actors to find weaknesses to attack drone systems, and in parallel develop their own rogue drones. These factors present a risk of damage to people and property in addition to compromise of integrity and availability. However, a formal framework for ethical hacking that combines attacker modelling and launching of attacks is lacking in the literature. To this end, we leverage runtime enforcement, combined with the idea of suspension from synchronous programming to develop the first such formal framework. The proposed framework enables the modelling of complex attack vectors on drones. To facilitate this, we propose a bespoke policy-based runtime enforcement framework called enforcer interchange (EI). It is capable of both individual intent/target-specific attacks as well as more sophisticated combinations of attacks, which it manages by enabling and disabling attack enforcers at runtime in a context-aware manner. To demonstrate our framework, we utilise a quadcopter drone simulator and record the changes in the drone's behaviour as it executes a range of missions under different attacks. Our approach provides a framework for testing drones' resilience and defenses against malicious attacks, as well as exploring the capabilities of rogue drones.

Wearable and implantable medical devices are being increasingly deployed for diagnosis, monitoring, and to provide therapy for critical medical conditions. Such medical devices are examples of safety-critical, cyber-physical systems. In this paper we focus on insulin infusion systems (IISs), which are used by diabetics to maintain safe blood glucose levels. These systems support wireless features introducing potential vulnerabilities. Although these devices go through rigorous safety certification processes, these are not able to mitigate security threats. Based on published literature, attackers can remotely command to inject an incorrect amount of insulin thereby posing threat to a patient's life. While prior work based on formal methods have been proposed to detect potential attack vectors using different forms of static analysis, these have limitations in preventing attacks at run-time. Also, as these devices are safety critical, it is not possible to apply security patches, when new types of attacks are detected, due to the need for recertification.

Cyber-physical systems (CPSs) are implemented in many industrial and embedded control applications. Where these systems are safety-critical, correct and safe behavior is of paramount importance. Malicious attacks on such CPSs can have far-reaching repercussions. For instance, if elements of a power grid behave erratically, physical damage and loss of life could occur. Currently, there is a trend toward increased complexity and connectivity of CPS. However, as this occurs, the potential attack vectors for these systems grow in number, increasing the risk that a given controller might become compromised. In this article, we examine how the dangers of compromised controllers can be mitigated. We propose a novel application of runtime enforcement that can secure the safety of real-world physical systems. Here, we synthesize enforcers to a new hardware architecture within programmable logic controller I/O modules to act as an effective line of defence between the cyber and the physical domains. Our enforcers prevent the physical damage that a compromised control system might be able to perform. To demonstrate the efficacy of our approach, we present several benchmarks, and show that the overhead for each system is extremely minimal.

NAND flash memory has become the de facto standard for several non-volatile storages used in commercial and mission-critical applications. The advanced operations supported by NAND flash memory contribute to device performance and also influence the design of some of the crucial mechanisms of the flash memory device controller. In this research, we consider a recent ONFI standard i.e. ONFI-3.2 and successfully model the NAND flash memory device with the advanced operations in addition to many basic operations in contrast to the existing research works. We encode all the properties obtained from the standard in LTL and proved those using symbolic model checking. Our modeling approach simplifies the state machines and reduces resource requirements while capturing the essential information needed to verify the requirement based properties.

In recent years we have seen numerous proof-of-concept attacks on implantable medical devices such as pacemakers. Attackers aim to breach the strict operational constraints that these devices operate within, with the end-goal of compromising patient safety and health. Most efforts to prevent these kinds of attacks are informal, and focus on application- and system-level security --- for instance, using encrypted communications and digital certificates for program verification. However, these approaches will struggle to prevent all classes of attacks. Runtime verification has been proposed as a formal methodology for monitoring the status of implantable medical devices. Here, if an attack is detected a warning is generated. This leaves open the risk that the attack can succeed before intervention can occur. In this paper, we propose a runtime-enforcement based approach for ensuring patient security. Custom hardware is constructed for individual patients to ensure a safe minimum quality of service at all times. To ensure correctness we formally verify the hardware using a model-checker. We present our approach through a pacemaker case study and demonstrate that it incurs minimal overhead in terms of execution time and power consumption.

The US Food and Drug Administration (FDA) recently recalled approximately 465,000 pacemakers that were vulnerable to hacking. It was reported that hackers could either pace the devices rapidly inducing arrhythmia or could drain the battery. Such actions would compromise the health and well being of the patient concerned. Considering this, techniques to ensure the security of implantable medical devices is an emerging area of research. To the best of our knowledge, existing techniques lack the formal rigour for ensuring the safety and security of such systems. While methods exist for formal verification of pacemaker software, these are not suitable to prevent security vulnerabilities. To this end we develop a run-time verification based approach. Our approach proposes a wearable device that non-invasively senses the familiar ECG signals in order to determine if a pacemaker has been compromised. We develop a set of timed policies to be monitored at run-time. We provide a methodology for the design of the wearable device and results demonstrate the technical feasibility of the developed concept.

Synchronous programming is a paradigm of choice for the design of safety-critical reactive systems. Runtime enforcement is a technique to ensure that the output of a black-box system satisfies some desired properties. This paper deals with the problem of runtime enforcement in the context of synchronous programs. We propose a framework where an enforcer monitors both the inputs and the outputs of a synchronous program and (minimally) edits erroneous inputs/outputs in order to guarantee that a given property holds. We define enforceability conditions, develop an online enforcement algorithm, and prove its correctness. We also report on an implementation of the algorithm on top of the KIELER framework for the SCCharts synchronous language. Experimental results show that enforcement has minimal execution time overhead, which decreases proportionally with larger benchmarks.

Many implantable medical devices, such as pacemakers, have been recalled due to failure of their embedded software. This motivates rethinking their design and certification processes. We propose, for the first time, an additional layer of safety by formalising the problem of run-time enforcement of implantable pacemakers. While recent work has formalised run-time enforcement of reactive systems, the proposed framework generalises existing work along the following directions: (1) we develop bi-directional enforcement, where the enforced policies depend not only on the status of the pacemaker (the controller) but also of the heart (the plant), thus formalising the run-time enforcement problem for cyber-physical systems (2) we express policies using a variant of discrete timed automata (DTA), which can cover all regular properties unlike earlier frameworks limited to safety properties, (3) we are able to ensure the timing safety of implantable devices through the proposed enforcement, and (4) we show that the DTA-based approach is efficient relative to its dense time variant while ensuring that the discretisation error is relatively small and bounded. The developed approach is validated through a prototype system implemented using the open source KIELER framework. The experiments show that the framework incurs minimal runtime overhead.