Neuro-Symbolic Perception for Estimation and Control

Modern cyber-physical systems (CPS) are increasingly neuro-symbolic. A typical CPS control pipeline consists of 1) neural networks (NNs), used to process raw high-dimensional data, such as camera images, and 2) downstream symbolic components, such as state estimation and control, that take the NNs' output in order to close the loop. However, there is a fundamental mismatch between the uncertainty on the NN outputs and the assumptions of the downstream components. NNs are known to be vulnerable to even minor input perturbations and distribution shifts that make it hard to characterize the properties of NN outputs. In turn, such robustness issues violate the symbolic tasks' assumptions and guarantees, thus compromising the overall system safety and predictability. We aim to develop neuro-symbolic calibration and training methods that repair the fundamental neuro-symbolic mismatch. The research would enable the application of powerful symbolic tasks (e.g., resilient state estimation and robust control) to modern perception-based CPS where the presence of NNs might otherwise violate the symbolic tasks' assumptions.

Assured Autonomy

The recent improvements in sensing, perception and control have enabled the development of autonomous systems in multiple safety-critical domains such as autonomous driving, unmanned rockets, drones, and medical devices. However, the neural networks used in these systems often fail in seeminlgy arbitrary ways, as is the case with adversarial examples. Such issues highlight the need to assure the safety of autonomous systems with leaning-enabled components (LECs) before they are deployed at scale. To achieve high assurance, I am exploring a collection of design-time and run-time techniques. At design time, my contribution is a verification technique for closed-loop systems with neural network components, as described next.

Verifying Safety of Autonomous Systems with Neural Network Components

The closed-loop verification problem we consider is illustrated in the figure on the right. We consider an autonomous system that operates in a known environment. The system has access to different measurerements of its state and the environment, which are then sent to a neural network (NN) controller that closes the loop. Given a hybrid system model of the plant's dynamics and measurement model, the goal is to verify that the system does not reach any unsafe states (e.g., a crash), when started from a given set of initial conditions. The main challenge in this problem is how to handle the NN since NN verification is NP-hard even for simple input/output properties. The key idea of our approach is that a NN with sigmoid activations can be transfrmed into an equivalent hybrid system. Specifically, since the sigmoid is the solution to a quadratic differential equation, each neuron can be mapped to a state and each layer can be mapped to a mode in a hybrid system. Finally, the NN's hybrid system can be composed with the plant's hybrid system, thereby casting the verification problem as a hybrid system reachability problem which can be solved by optimized tools (e.g., Flow*).

We implemented our approach in a tool called Verisig. We evaluated Verisig on a number of case studies: 1) a reinforcement learning benchmark called Mountain Car, 2) an unmanned aerial vehicle trying to reach a goal without colliding into obstacle, 3) a NN-controlled car that navigates a structured environment using LiDAR measurements. To validate the verification result, we also performed real experiments for the 3rd case study, in which the car can successfully navigate a hallway environment without colliding into walls. Note that this is an end-to-end NN controller that takes LiDAR measurements as input and produces control actions as output. A video with the experiments is shown on the right. Verisig can currently scale up to NNs with several hundred neurons per layer and roughly a dozen layers, i.e., NNs that are sufficiently large for a large number of applications, as suggested by the diversity of our case studies.

Security of Cyber-Physical Systems

The increasing autonomy and sophistication of modern CPS have led to multiple accidents in the last few years, caused not only by component failures but also by malicious attacks exploiting communication vulnerabilities, software bugs, etc. These accidents have exposed the need for a unifying theory for analyzing the safety of such systems even in the presence of faults and attacks. The main challenge for developing such techniques is that, due to the complexity of modern CPS, components might experience unexpected faults or attacks and behave in arbitrary ways. This means that no assumptions can be made about how or when components might fail.

Safety Detection Using Sensor Fusion

To address the above challenges, we make use of the fact that modern CPS have multiple redundant sensors that can be used to estimate the same state. For example, the LandShark robot (shown on the right) has five sensors that can be used to estimate its speed. Given this redundancy, the system can tolerate failures and attacks in some of its sensors, provided that it uses the remaining correct ones. In order to formalize this concept, we developed sensor fusion techniques for detecting when the systems is unsafe even in the presence of attacks and faults. While sensor fusion eliminates the need to assume how and when sensors might fail, it comes at a cost as well -- more than half of all sensors must operate correctly. This is a reasonable assumption because it is unlikely that these diverse sensors will fail or be attacked at the same time. Given this assumption, sensor fusion outputs a bounded set that is guaranteed to contain the true state and can be used to detect if the system is unsafe.

In addition to the initial approach, we explored ways of adding more information to sensor fusion in order to improve its output. In the first extension, we modified the algorithm by incorporating historical measurements and mapping them to the current time using system dynamics. We developed multiple approaches to using historical measurements and identified the best ones under different conditions. Regardless of the method used, using historical measurements always results in tighter bounds on the output of sensor fusion. In the second modification to the sensor fusion algorithm, we note that modern CPS are built in a time-triggered fashion such that each sensor transmits its measurement during a predefined time-slot, effectively creating a schedule of measurement transmissions. Since these systems usually use shared buses (e.g., a CAN bus) where each measurement is broadcast to all nodes, the attacker can examine all other measurements before sending the spoofed measurements. Thus, we analyzed the impact of different transmission schedules on the attacker's information and provided both theoretical and experimental results in favor of the Ascending schedule, the one that schedules most precise sensors first. A video illustrating the benefit of the Ascending schedule is shown on the right.

Sensor Attack Detection

In order to further improve the output of sensor fusion (and of other components using sensor data), we also developed techniques for sensor attack detection and identification. Similar to the sensor fusion framework, in this work we also use sensor redundancy so as to avoid making unrealistic assumptions about how and when faults/attacks might occur (in existing anomaly detection works, it is either assumed that the system has a known initial condition or that the attack/fault has a known effect). Since sensors often experience transient faults that are a normal part of system operation (e.g., GPS losing its connection in a tunnel), we introduced the notion of a transient fault model for each sensor and developed an approach for identifying such models from data. Given such transient fault models, we presented an attack detection method (based on pairwise inconsistencies between sensor measurements, as shown on the right) that only flags attacks and does not raise alarms due to transient faults. We evaluated our approach using real data from the LandShark that was retrospectively augmented with various attacks -- our approach was eventually able to detect all sensor attacks.

High-Assurance Medical Cyber-Physical Systems

The increasing sophistication of medical devices in modern operating rooms presents a great opportunity to develop medical CPS. In particular, it is now possible to obtain the patient's vital sign data (e.g., heart rate, blood pressure) in real time and build algorithms to analyze the patient's condition and provide decision support to clinicians. At the same time, there are multiple challenges when building such a system. If we consider the typical plant-controller loop in the medical CPS setting (shown on the right), there are challenges at each level: 1) it is difficult to develop high-fidelity physiological models, 2) measurements are often infrequent, invasive or missing, 3) there are very strict requirements on the performance of these systems due to their safety criticality, 4) it is important to ensure a smooth human-machine interaction.

Estimation of Blood Oxygen Content Using Context-Aware Filtering

As a first step towards the development of medical CPS, we focused on one of the most closely monitored vital signs, namely blood oxygen content. Estimating the blood oxygen content is a challenging problem because measurements are mostly available on the pulmonary side whereas the goal is to estimate a state on the blood side. Thus, we built a physiological model (illustrated on the right) mapping the available measurements to the state. Since this model contains multiple parameters that vary widely with patients (and cannot be identified due to insufficient data), we use additional information in the form of context, i.e., high-level representation of low-level measurement data. For example, a patient's oxygen saturation measurement is hard to use directly for estimation purposes but if the overall saturation is low, then we can conclude that the overall oxygen content is also low. We developed the context-aware filter in order to handle such context measurements in addition to standard continuous measurements. We applied our approach to data from the Children's Hospital of Philadelphia (CHOP) and were able to achieve about 20% improvement in performance over prior work.

Prediction of Critical Pulmonary Shunts in Infants

In addition to the estimation problem described above, also investigated the problem of detecting drops in blood oxygen content as caused by pulmonary shunts in infants. Pulmonary shunts occur frequently during lung surgery where the perioperative lung is not ventilated in order to be kept still for surgery. Such shunts are especially dangerous for infants who have underdeveloped lungs and may not receive enough oxygen through one lung. In order to detect when such a shunt might lead to a drop in the patient's oxygen content, we developed a parameterized physiological model, similar to the estimation setting, mapping the measurements to the system state. Unlike the estimation setting, the detection problem does not require estimating the model parameters -- we employ a parameter-invariant technique in order to provide guaranteed false alarm performance for each patient regardless of their specific physiology. We applied our approach to data from lung lobectomies at CHOP and achieved a detection rate of about 85% with a potentially life-saving early warning of 90 seconds on average. In addition, our approach achieved a near-constant false alarm rate of 0.95 false alarms per hour. An example case with good detection is shown on the right (shaded area denotes the beginning of the shunt).