ABSTRACT. The deployment of artificial intelligence (AI), particularly of systems that learn from data and experience, is rapidly expanding in our society. Verified artificial intelligence (AI) is the goal of designing AI-based systems that have strong, verified assurances of correctness with respect to mathematically-specified requirements. In this talk, I will consider Verified AI from a formal methods perspective. I will describe five challenges for achieving Verified AI, and five corresponding principles for addressing these challenges, with a special focus on run-time verification methods such as temporal logic falsification and run-time assurance. I will illustrate the ideas in the talk with examples and sample results from the domain of intelligent cyber-physical systems, with a particular focus on autonomous vehicles.

ABSTRACT. Detection and quantification of information leaks through timing side channels are important to guarantee confidentiality. Although static analysis remains the main approach for detecting timing side channels, it is computationally difficult for real-world applications. In addition, the detection techniques are restricted to ``yes'' or ``no'' answers. In practice, real-world applications may need to leak information about the secret. Therefore, quantification techniques are necessary to evaluate the resulting threats of information leaks. Since both problems are very difficult or impossible for static analysis techniques, we propose a dynamic analysis method. Our novel approach is to split the problem into two tasks. First, we learn a program's timing model as a neural network. Second, we analyze the neural network to quantify information leaks. As demonstrated in our experiments, both of these tasks are feasible in practice --- making the approach a significant improvement over the state-of-the-art side channel detectors and quantifiers. Our key technical contributions are (a) a neural network architecture that enables side channel discovery and (b) an MILP-based algorithm to estimate the side-channel strength. On a set of micro-benchmarks and real-world applications, we show that neural network models learn timing behaviors of programs with thousands of methods. We also show that neural networks with thousands of neurons can be efficiently analyzed to detect and quantify information leaks through timing side channels.

ABSTRACT. Neural State Classification (NSC) is a recently proposed method for runtime predictive monitoring of Hybrid Automata (HA) using deep neural networks (DNNs). NSC trains a DNN as an approximate reachability predictor that labels a given HA state x as positive if an unsafe state is reachable from x within a given time bound, and labels x as negative otherwise. NSC predictors have very high accuracy, yet are prone to prediction errors that can negatively impact reliability. To overcome this limitation, we present Neural Predictive Monitoring (NPM), a technique based on NSC and conformal prediction that complements the predictions with statistically sound estimates of uncertainty. This yields principled criteria for the rejection of predictions likely to be incorrect, without knowing the true reachability values. We also present an active learning method that significantly reduces both the NSC predictor's error rate and the percentage of rejected predictions. Our approach is highly efficient, with computation times on the order of milliseconds, and effective, managing in our experimental evaluation to successfully reject almost all incorrect predictions.

ABSTRACT. Predictive runtime verification estimates the probability of a future event by monitoring the executions of a system. In this paper we use Discrete-Time Markov Chain (DTMC) as predictive models that are trained from many execution samples demonstrating a rare event: an event that occurs with very low probability. More specifically we propose a method based on the grammar inference by which a DTMC is learned efficiently when the event is rare, i.e., with far fewer samples than normal sample distribution. We exploit the concept of importance sampling , and use a mixture of samples, generated from the original system distribution and distributions that are suitably modified to produce more failures. Using the likelihood ratios of the various samples, we ensure the final trained model is faithful to the original distribution. In this way we construct accurate predictive models with orders of magnitude fewer samples. We demonstrate the gains of our approach on a file transmission protocol case study from the literature, and highlight future directions.

ABSTRACT. We propose a predictive runtime monitoring approach for linear systems with stochastic disturbances. The goal of the monitor is to decide if there exists a possible sequence of control inputs over a given time horizon to ensure that a safety property is maintained with high probability. We derive an efficient algorithm for performing the predictive monitoring in real time, specifically for linear time invariant (LTI) systems driven by stochastic disturbances. The algorithm implicitly defines a control envelope set such that if the current control input to the system lies in this set, there exists a future strategy over a time horizon consisting of the next N steps to guarantee the safety property of interest. Thus, the proposed monitor is oblivious of the actual controller, and in this manner applicable even in the presence of complex control systems including highly adaptive controllers.

We apply our proposed approach to monitor whether a UAV will respect a "geofence" defined by a geographical region over which the vehicle may operate. To achieve this, we construct a data driven linear model of the UAVs dynamics, while carefully modeling the uncertainties due to wind, GPS errors and modeling errors as time varying disturbances. Using realistic data obtained from high fidelity simulators and flight tests, we demonstrate the advantages and drawbacks of the predictive monitoring approach.

ABSTRACT. Control Flow Integrity (CFI) is an effective defense approach against a variety of memory-based cyber attacks. Code instrumentation and high performance overhead are common issues when using software-based CFI. Although performance overhead can be mitigated by hardware-based CFI, existing hardware CFI techniques mostly rely on code instrumentation. We develop FastCFI, an FPGA based CFI system that can perform fine-grained and stateful checking without relying on code instrumentation. We also propose an automated Verilog generation technique that facilitates fast deployment of FastCFI. Experiments on popular benchmarks confirm that FastCFI can detect fine-grained CFI violations over unmodified binaries. The measurement results show an average of 0.36% performance overhead on SPEC 2006 benchmarks.

ABSTRACT. One important issue needed to be handled when applying runtime verification is the time overhead introduced by online monitors. According to how monitors are deployed with the system to be monitored, the overhead may come from execution of monitoring logic or asynchronous communication. In this paper, we present a method for deciding how to deploy runtime monitors with awareness of minimizing the overhead. We first propose a parametric model to estimate the overhead given the prior knowledge on the distribution of incoming events and the time cost of sending a message and executing monitoring logic. Then, we will discuss how to statically decide the boundary of synchronous and asynchronous monitors such that the lowest overhead can be obtained.