Towards secure and robust stateful deep learning systems with model-based analysis - Du, Xiaoning (Nanyang Technological University, 2020)
More and more we start to embrace the convenience and effectiveness of the rapidly advancing artificial intelligence (AI) technologies in our lives and different industries. Within this revolution, deep learning (DL), as one of the key innovation in AI, has made significant progress over the past decades. However, even the state-of-the-art DL systems are susceptible to minor adversarial perturbations, and suffer from quality, reliability and security problems, preventing the deployment of DL systems on safety- and security-critical applications. An early-stage assessment of DL systems is crucial in discovering defects and improving the overall product quality. Mature analysis processes and techniques have been established for traditional software, but it is highly non-trivial to directly apply them to DL systems. These challenges have motivated researchers to investigate testing, verification and adversarial sample detection of feed-forward neural networks, but little has been done on the recurrent neural network (RNN)-based stateful DL systems. In this thesis, we initiate the first major effort on the white-box RNN analysis using model-based approach to focus on the security and robustness properties and demonstrate the usefulness with applications on test case production, attack generation, and adversarial sample detection. To further protect the DL systems, we propose an efficient monitoring algorithm which could be potentially used to shield DL systems against adversarial samples at runtime, based on the RNN behaviors reflected by the abstract models. The first part of the thesis focuses on RNN model extraction and offline analysis on the security and robustness properties based on the models extracted. First, we model an RNN as an abstract state transition system, namely Discrete-Time Markov Chain (DTMC), to characterize its internal behaviors. We design an algorithm to automatically extract DTMC from a given RNN. Based on the abstract model, we design two trace similarity metrics and five coverage criteria which enable the quantitative analysis of RNNs. We further propose two algorithms powered by the quantitative measures for adversarial sample detection and coverage-guided test generation. We evaluate the framework, DeepStellar, on four RNN-based systems covering image classification and automated speech recognition. The results demonstrate that the abstract model is useful in capturing the internal behaviors of RNNs, and confirm that (1) the similarity metrics could effectively capture the differences between samples even with very small perturbations and (2) the coverage criteria are useful in revealing erroneous behaviors. Secondly, we model RNN as an input-aware probabilistic abstract state transition system, namely Markov Decision Process (MDP), and define robustness property over the MDP. Robustness depicts how vulnerable the RNN is under minor input perturbations, thus the input awareness is of great importance. We first profile and perturb training data to collect RNN internal state information. Based on this, we build a probabilistic model to compactly characterize the behaviors of the RNN, through abstraction. Furthermore, we propose a refinement algorithm to iteratively derive an abstract model that enables to accurately quantify the robustness of an RNN. We evaluate the effectiveness on an LSTM model and a GRU model trained separately with two popular natural language datasets. The results demonstrate that our refinement algorithm is more efficient in deriving an accurate model than the random strategy, and our approach enables quantitative robustness analysis, in rendering better efficiency, accuracy, and scalability than the state-of-the-art technique. The second part of the thesis incorporates runtime monitoring as the last line of defense to detect whether the system is under attack in real-time. Defects in DL systems are difficult to fix, even with samples revealing such defects at hand. Hence, runtime monitoring plays an important role here to guard the systems against the adversary. Based on the robustness analysis, we find that perturbations over the input elements where RNN presents weaker robustness can lead to attacks more easily. Alarms shall be raised if the RNN becomes unrobustness when dealing with samples. Here, we monitor how often the runtime RNN behavioral trace triggered by a sample visits unrobust states. Temporal logic is versatile to describe history-sensitive properties. Traditionally, the use of temporal logic is to capture the qualitative aspects of the monitored systems. Nevertheless, quantitative specification is required to describe security policies for the adversarial sample detection, as well as malware detection and intrusion detection in platforms like Android and automatons vehicle, where frequency of events is a vital feature of the malicious behavior. There exist some extensions of temporal logic to allow quantitative policy specification but the cost of the corresponding monitoring algorithms cannot achieve a time and space complexity that is completely independent of the trace length. To guarantee the expressiveness and efficiency at the same time, we develop a logic specification language, MTLcnt, and derive a complete and efficient runtime verification algorithm with trace-length independent performance. MTLcnt allows specification on the number of times some sub-policies are satisfied in the specified past time interval. With trace-length independence (TLI), the monitoring cost does not increase as the execution trace grows, which is crucial for monitoring on devices with restricted computation and storage resources, such as smartphones and embedded systems. Theoretically, we show that a broad class of policies, but not all policies, specified with MTLcnt can be monitored in a TLI way, and provide a concrete algorithm to do so. Experimentally, we implement a prototype and test our algorithm on detecting Android malware and anomaly traffic in autonomous vehicles. This thesis makes the first attempt to perform model-based analysis for RNNs with both offline and online techniques, with which we hope to open a new research direction for the white-box analysis of stateful DL systems.