Sensor attacks on Cyber-Physical Systems (CPS) can cause substantial damage in the physical world, which motivates two major threads of defense works including attack detection and attack recovery. The former aims to identify whether any sensors are compromised while the latter seeks to restore a system to safety once an attack is detected. Although either thread has drawn many efforts, how to coordinate the detection and recovery has been barely studied. Overlooking the coordination, existing works may result in ineffective and even failed defense. For example, if a detector raises an alarm too late, there may not be enough time for a system to recover but reach the unsafe region anyway, even though the detection result is accurate. By contrast, raising an alarm earlier allows more time for recovery, but may come with more false positives and thus unnecessarily trigger the recovery. To fill this gap, we aim to co-design attack detection and recovery, and propose a novel recovery-guaranteed sensor attack detection framework. The framework dynamically adjusts the detection sensitivity and authenticates state estimates at run time to guarantee timely and safe recovery once an attack is detected. The detection will always reserve sufficient time for the recovery while minimizing unnecessary activation of recovery. We conduct extensive simulations and real-world testbed experiments to show the efficiency of our solution.

We present REGLO, a novel methodology for repairing pretrained neural networks to satisfy global robustness and individual fairness properties. A neural network is said to be globally robust with respect to a given input region if and only if all the input points in the region are locally robust. This notion of global robustness also captures the notion of individual fairness as a special case. We prove that any counterexample to a global robustness property must exhibit a corresponding large gradient. For ReLU networks, this result allows us to efficiently identify the linear regions that violate a given global robustness property. By formulating and solving a suitable robust convex optimization problem, REGLO then computes a minimal weight change that will provably repair these violating linear regions.

Reaching a target safely and quickly is a control goal pursued by various applications, such as post-disaster rescue robots and industrial shipment. However, it is hard to formally guarantee safety and time-optimality under unknown dynamics via model-free controller synthesis algorithms. As a response, we propose a model-free reinforcement learning (RL) algorithm that synthesize a controller to reach a predefined target set of states with a probabilistic guarantee of time optimality, i.e., the actual reaching time is bounded close to the shortest time possible with high probability, and the bound becomes tighter when more training data is sampled. Our algorithm leverages a reward function that based on signal temporal logic (STL) robustness to reward fast reaching. With this reward function, we prove that Probably Approximately Correct (PAC) optimality in the state-value function implies PAC optimality in reach time. Then, we build our algorithm by extending Deplayed Gaussian Process Q learning (DGPQ) algorithm with a safety margin to protect the controlled agent. Consequently, our algorithm guarantees safety and a PAC bound in recovery time. Experiments show our method can achieve $\mathbf{9 7. 7 \%}$ success rate to reach the target with in the maximum time tolerance and outperform baselines.

Cyber-physical systems tightly integrate computational resources with physical processes through sensing and actuating, widely penetrating various safety-critical domains, such as autonomous driving, medical monitoring, and industrial control. Unfortunately, they are susceptible to assorted attacks that can result in injuries or physical damage soon after the system is compromised. Consequently, we require mechanisms that swiftly recover their physical states, redirecting a compromised system to desired states to mitigate hazardous situations that can result from attacks. However, existing recovery studies have overlooked stochastic uncertainties that can be unbounded, making a recovery infeasible or invalidating safety and real-time guarantees. This paper presents a novel recovery approach that achieves the highest probability of steering the physical states of systems with stochastic uncertainties to a target set rapidly or within a given time. Further, we prove that our method is sound, complete, fast, and has low computational complexity if the target set can be expressed as a strip. Finally, we demonstrate the practicality of our solution through the implementation in multiple use cases encompassing both linear and nonlinear dynamics, including robotic vehicles, drones, and vehicles in high-fidelity simulators.

Meeting deadlines is a fundamental requirement of cyber-physical systems (CPS) in real-time applications to consolidate their reliability and effectiveness in executing timecritical tasks. Recent research have focused on applying reinforcement learning to synthesize controllers for real-time systems, particularly in terms of achieving fast reach-avoid. However, achieving fast behavior does not necessarily equate to meeting deadlines. Sometimes reinforcement learning agents are trying to maximize the total reward by exploiting the reward function, and thus performing unwanted behavior, known as reward hacking. Therefore, depending on the deadlines, it is possible to have fast controllers that miss the deadlines and slow controllers that meet the deadlines. To address the misalignment between fast and meeting deadlines, we investigate the relationship between as soon as possible (ASAP) and deadline-safe. Additionally, we formulate the problem into a new Markov decision process R-MDP including time to avoid non-Markovian rewards when considering deadlines. Furthermore, we have designed new reward functions that encourage the agent to meet the deadlines. Moreover, we evaluate our method on various benchmarks. The experiment results show the effectiveness of our method in ensuring deadline compliance without compromising safety.

Neural networks (NNs) playing the role of controllers have demonstrated impressive empirical performance on challenging control problems. However, the potential adoption of NN controllers in real-life applications has been significantly impeded by the growing concerns over the safety of these NN-controlled systems (NNCSs). In this work, we present POLAR-Express, an efficient and precise formal reachability analysis tool for verifying the safety of NNCSs. POLAR-Express uses Taylor model (TM) arithmetic to propagate TMs layer-by-layer across an NN to compute an overapproximation of the NN. It can be applied to analyze any feedforward NNs with continuous activation functions, such as ReLU, Sigmoid, and Tanh activation functions that cover the common benchmarks for NNCS reachability analysis. Compared with its earlier prototype POLAR, we develop a novel approach in POLAR-Express to propagate TMs more efficiently and precisely across ReLU activation functions, and provide parallel computation support for TM propagation, thus significantly improving the efficiency and scalability. Across the comparison with six other state-of-the-art tools on a diverse set of common benchmarks, POLAR-Express achieves the best verification efficiency and tightness in the reachable set analysis. POLAR-Express is publicly available athttps://github.com/ChaoHuang2018/POLAR_Tool.

Cyber-physical systems (CPSs) leverage computations to operate physical objects in real-world environments, and increasingly more CPS-based applications have been designed for life-critical applications. Therefore, any vulnerability in such a system can lead to severe consequences if exploited by adversaries. In this paper, we present a data predictive recovery system to safeguard the CPS from sensor attacks, assuming that we can identify compromised sensors from data. Our recovery system guarantees that the CPS will never encounter unsafe states and will smoothly recover to a target set within a conservative deadline. It also guarantees that the CPS will remain within the target set for a specified period. Major highlights of our paper include (i) the recovery procedure works on nonlinear systems, (ii) the method leverages uncorrupted sensors to relieve uncertainty accumulation, and (iii) an extensive set of experiments on various nonlinear benchmarks that demonstrate our framework’s performance and efficiency.

The increasing autonomy and connectivity in cyber-physical systems (CPS) come with new security vulnerabilities that are easily exploitable by malicious attackers to spoof a system to perform dangerous actions. While the vast majority of existing works focus on attack prevention and detection, the key question is “what to do after detecting an attack?”. This problem attracts fairly rare attention though its significance is emphasized by the need to mitigate or even eliminate attack impacts on a system. In this article, we study this attack response problem and propose novel real-time recovery for securing CPS. First, this work’s core component is a recovery control calculator using a Linear-Quadratic Regulator (LQR) with timing and safety constraints. This component can smoothly steer back a physical system under control to a target state set before a safe deadline and maintain the system state in the set once it is driven to it. We further propose an Alternating Direction Method of Multipliers (ADMM) based algorithm that can fast solve the LQR-based recovery problem. Second, supporting components for the attack recovery computation include a checkpointer, a state reconstructor, and a deadline estimator. To realize these components respectively, we propose (i) a sliding-window-based checkpointing protocol that governs sufficient trustworthy data, (ii) a state reconstruction approach that uses the checkpointed data to estimate the current system state, and (iii) a reachability-based approach to conservatively estimate a safe deadline. Finally, we implement our approach and demonstrate its effectiveness in dealing with totally 15 experimental scenarios which are designed based on 5 CPS simulators and 3 types of sensor attacks.

Learning-enabled components have been widely deployed in autonomous systems. However, due to the weak interpretability and the prohibitively high complexity of large-scale machine learning models such as neural networks, reliability has been a crucial concern for safety-critical autonomous systems. This work proposes an online monitor called Reach-Flow for fault prevention of waypoint-following tasks for self-driving cars. It mainly consists of two components: (a) an online verification tool which conservatively checks the safety of the system behavior in the near future, and (b) a fallback controller which steers the system back to a desired state when the system is potentially unsafe. We implement ReachFlow in a self-driving racing car governed by a reinforcement learning-based controller. We demonstrate the effectiveness by rigorously verifying a safe waypoint-following control and providing a fallback control for an unsafe situation in which a large deviation from the planned path is predicted.

Attack detection and recovery are fundamental elements for the operation of safe and resilient cyber-physical systems. Most of the literature focuses on attack-detection, while leaving attack-recovery as an open problem. In this paper, we propose novel attack-recovery control for securing cyber-physical systems. Our recovery control consists of new concepts required for a safe response to attacks, which includes the removal of poisoned data, the estimation of the current state, a prediction of the reachable states, and the online design of a new controller to recover the system. The synthesis of such recovery controllers for cyber-physical systems has barely investigated so far. To fill this void, we present a formal method-based approach to online compute a recovery control sequence that steers a system under an ongoing sensor attack from the current state to a target state such that no unsafe state is reachable on the way. The method solves a reach-avoid problem on a Linear Time-Invariant (LTI) model with the consideration of an error bound ε ≥ 0. The obtained recovery control is guaranteed to work on the original system if the behavioral difference between the LTI model and the system's plant dynamics is not larger than ε. Since a recovery control should be obtained and applied at the runtime of the system, in order to keep its computational time cost as low as possible, our approach firstly builds a linear programming restriction with the accordingly constrained safety and target specifications for the given reach-avoid problem, and then uses a linear programming solver to find a solution. To demonstrate the effectiveness of our method, we provide (a) the comparison to the previous work over 5 system models under 3 sensor attack scenarios: modification, delay, and reply; (b) a scalability analysis based on a scalable model to evaluate the performance of our method on large-scale systems.

In this article, we present a layer-wise refinement method for neural network output range analysis. While approaches such as nonlinear programming (NLP) can directly model the high nonlinearity brought by neural networks in output range analysis, they are known to be difficult to solve in general. We propose to use a convex polygonal relaxation (overapproximation) of the activation functions to cope with the nonlinearity. This allows us to encode the relaxed problem into a mixedinteger linear program (MILP), and control the tightness of the relaxation by adjusting the number of segments in the polygon. Starting with a segment number of 1 for each neuron, which coincides with a linear programming (LP) relaxation, our approach selects neurons layer by layer to iteratively refine this relaxation. To tackle the increase of the number of integer variables with tighter refinement, we bridge the propagation-based method and the programming-based method by dividing and sliding the layerwise constraints. Specifically, given a sliding number s, for the neurons in layer l, we only encode the constraints of the layers between l - s and l. We show that our overall framework is sound and provides a valid overapproximation. Experiments on deep neural networks demonstrate significant improvement on output range analysis precision using our approach compared to the state-of-the-art.

We present an approach for the synthesis and verification of neural network controllers for closed loop dynamical systems, modelled as an ordinary differential equation. Feedforward neural networks are ubiquitous when it comes to approximating functions, especially in the machine learning literature. The proposed verification technique tries to construct an over-approximation of the system trajectories using a combination of tools, such as, Sherlock and Flow*. In addition to computing reach sets, we incorporate counter examples or bad traces into the synthesis phase of the controller as well. We go back and forth between verification and counter example generation until the system outputs a fully verified controller, or the training fails to terminate in a neural network which is compliant with the desired specifications. We demonstrate the effectiveness of our approach over a suite of benchmarks ranging from 2 to 17 variables.

We present an approach to construct reachable set overapproximations for continuous-time dynamical systems controlled using neural network feedback systems. Feedforward deep neural networks are now widely used as a means for learning control laws through techniques such as reinforcement learning and data-driven predictive control. However, the learning algorithms for these networks do not guarantee correctness properties on the resulting closed-loop systems. Our approach seeks to construct overapproximate reachable sets by integrating a Taylor model-based flowpipe construction scheme for continuous differential equations with an approach that replaces the neural network feedback law for a small subset of inputs by a polynomial mapping. We generate the polynomial mapping using regression from input-output samples. To ensure soundness, we rigorously quantify the gap between the output of the network and that of the polynomial model. We demonstrate the effectiveness of our approach over a suite of benchmark examples ranging from 2 to 17 state variables, comparing our approach with alternative ideas based on range analysis.

Neural networks are widely used in many applications ranging from classification to control. While these networks are composed of simple arithmetic operations, they are challenging to formally verify for properties such as reachability due to the presence of nonlinear activation functions. In this paper, we make the observation that Lipschitz continuity of a neural network not only can play a major role in the construction of reachable sets for neural-network controlled systems but also can be systematically controlled during training of the neural network. We build on this observation to develop a novel verification-aware knowledge distillation framework that transfers the knowledge of a trained network to a new and easier-to-verify network. Experimental results show that our method can substantially improve reachability analysis of neural-network controlled systems for several state-of-the-art tools.

Applying neural networks as controllers in dynamical systems has shown great promises. However, it is critical yet challenging to verify the safety of such control systems with neural-network controllers in the loop. Previous methods for verifying neural network controlled systems are limited to a few specific activation functions. In this work, we propose a new reachability analysis approach based on Bernstein polynomials that can verify neural-network controlled systems with a more general form of activation functions, i.e., as long as they ensure that the neural networks are Lipschitz continuous. Specifically, we consider abstracting feedforward neural networks with Bernstein polynomials for a small subset of inputs. To quantify the error introduced by abstraction, we provide both theoretical error bound estimation based on the theory of Bernstein polynomials and more practical sampling based error bound estimation, following a tight Lipschitz constant estimation approach based on forward reachability analysis. Compared with previous methods, our approach addresses a much broader set of neural networks, including heterogeneous neural networks that contain multiple types of activation functions. Experiment results on a variety of benchmarks show the effectiveness of our approach.

The predictive monitoring problem asks whether a deployed system is likely to fail over the next T seconds under some environmental conditions. This problem is of the utmost importance for cyber-physical systems, and has inspired real-time architectures capable of adapting to such failures upon forewarning. In this paper, we present a linear model-predictive scheme for the real-time monitoring of linear systems governed by time-triggered controllers and time-varying disturbances. The scheme uses a combination of offline (advance) and online computations to decide if a given plant model has entered a state from which no matter what control is applied, the disturbance has a strategy to drive the system to an unsafe region. Our approach is independent of the control strategy used: this allows us to deal with plants that are controlled using model-predictive control techniques or even opaque machine-learning based control algorithms that are hard to reason with using existing reachable set estimation algorithms. Our online computation reuses the symbolic reachable sets computed offline. The real-time monitor instantiates the reachable set with a concrete state estimate, and repeatedly performs emptiness checks with respect to a safety property. We classify the various alarms raised by our approach in terms of what they imply about the system as a whole. We implement our real-time monitoring approach over numerous linear system benchmarks and show that the computation can be performed rapidly in practice. Furthermore, we also examine the alarms reported by our approach and show how some of the alarms can be used to improve the controller.

We propose techniques to construct abstractions for nonlinear dynamics in terms of relations expressed in linear arithmetic. Such relations are useful for translating the closed loop verification problem of control software with continuous-time, nonlinear plant models into discrete and linear models that can be handled by efficient software verification approaches for discrete-time systems. We construct relations using Taylor model based flowpipe construction and the systematic composition of relational abstractions for smaller components. We focus on developing efficient schemes for the special case of composing abstractions for linear and nonlinear components. We implement our ideas using a relational abstraction system, using the resulting abstraction inside the verification tool NuXMV, which implements numerous SAT/SMT solver-based verification techniques for discrete systems. Finally, we evaluate the application of relational abstractions for verifying properties of time triggered controllers, comparing with the Flow* tool. We conclude that relational abstractions are a promising approach towards nonlinear hybrid system verification, capable of proving properties that are beyond the reach of tools such as Flow*. At the same time, we highlight the need for improvements to existing linear arithmetic SAT/SMT solvers to better support reasoning with large relational abstractions.

We introduce an approach to conservatively abstract a nonlinear continuous system by a hybrid automaton whose continuous dynamics are given by a decomposition of the original dynamics. The decomposed dynamics is in the form of a set of lower-dimensional ODEs with time-varying uncertainties whose ranges are defined by the hybridization domains. We propose several techniques in the paper to effectively compute abstractions and flowpipe overapproximations. First, a novel method is given to reduce the overestimation accumulation in a Taylor model flowpipe construction scheme. Then we present our decomposition method, as well as the framework of on-the-fly hybridization. A combination of the two techniques allows us to handle much larger, nonlinear systems with comparatively large initial sets. Our prototype implementation is compared with existing reachability tools for offline and online flowpipe construction on challenging benchmarks of dimensions ranging from 7 to 30. Our code has successfully passed the artifact evaluation.

We propose an approach for computing under- as well as over-approximations for the reachable sets of continuous systems which are defined by non-linear Ordinary Differential Equations (ODEs). Given a compact and connected initial set of states, described by a system of polynomial inequalities, we compute under-approximations of the set of states reachable over time. Our approach is based on a simple yet elegant technique to obtain an accurate Taylor model over-approximation for a backward flowmap based on well-known techniques to over-approximate the forward map. Next, we show that this over-approximation can be used to yield both over- and under-approximations for the forward reachable sets. Based on the result, we are able to conclude "may" as well as "must" reachability to prove properties or conclude the existence of counterexamples. A prototype of the approach is implemented and its performance is evaluated over a reasonable number of benchmarks.

This paper studies the effect of parameter variation on the behavior of analog circuits at the transistor (netlist) level. It is well known that variation in key circuit parameters can often adversely impact the correctness and performance of analog circuits during fabrication. An important problem lies in characterizing a safe subset of the parameter space for which the circuit can be guaranteed to satisfy the design specification. Due to the sheer size and complexity of analog circuits, a formal approach to the problem remains out of reach, especially at the transistor level. Therefore, we present a statistical model inference approach that exploits recent advances in statistical verification techniques. Our approach uses extensive circuit simulations to infer polynomials that approximate the behavior of a circuit. A procedure inspired by statistical model checking is then introduced to produce “statistically sound” models that extend the polynomial approximation. The resulting model can be viewed as a statistically guaranteed over-approximation of the circuit behavior. The proposed technique is demonstrated with two case studies in which it identifies subsets of parameters that satisfy the design specifications.

We propose an approach for verifying non-linear hybrid systems using higher-order Taylor models that are a combination of bounded degree polynomials over the initial conditions and time, bloated by an interval. Taylor models are an effective means for computing rigorous bounds on the complex time trajectories of non-linear differential equations. As a result, Taylor models have been successfully used to verify properties of non-linear continuous systems. However, the handling of discrete (controller) transitions remains a challenging problem. In this paper, we provide techniques for handling the effect of discrete transitions on Taylor model flow pipe construction. We explore various solutions based on two ideas: domain contraction and range over-approximation. Instead of explicitly computing the intersection of a Taylor model with a guard set, domain contraction makes the domain of a Taylor model smaller by cutting away parts for which the intersection is empty. It is complemented by range over-approximation that translates Taylor models into commonly used representations such as template polyhedra or zonotopes, on which intersections with guard sets have been previously studied. We provide an implementation of the techniques described in the paper and evaluate the various design choices over a set of challenging benchmarks.