Concolic Testing for Deep Neural Networks

Introduction

Deep neural networks (DNNs) have been instrumental in solving a range of hard problems in AI, e.g., the ancient game of Go, image classification, and natural language processing. As a result, many potential applications are envisaged. However, major concerns have been raised about the suitability of this technique for safety- and security-critical systems, where faulty behaviour carries the risk of endangering human lives or financial damage. To address these concerns, a (safety or security) critical system comprising DNN-based components needs to be validated thoroughly.

The software industry relies on testing as a primary means to provide stakeholders with information about the quality of the software product or service under test . So far, there have been only few attempts to test DNNs systematically . These are either based on concrete execution, e.g., Monte Carlo tree search or gradient-based search , or symbolic execution in combination with solvers for linear arithmetic . Together with these test-input generation algorithms, several test coverage criteria have been presented, including neuron coverage , a criterion that is inspired by MC/DC , and criteria to capture particular neuron activation values to identify corner cases . None of these approaches implement concolic testing , which combines concrete execution and symbolic analysis to explore the execution paths of a program that are hard to cover by techniques such as random testing.

We hypothesise that concolic testing is particularly well-suited for DNNs. The input space of a DNN is usually high dimensional, which makes random testing difficult. For instance, a DNN for image classification takes tens of thousands of pixels as input. Moreover, owing to the widespread use of the ReLU activation function for hidden neurons, the number of “execution paths” in a DNN is simply too large to be completely covered by symbolic execution. Concolic testing can mitigate this complexity by directing the symbolic analysis to particular execution paths, through concretely evaluating given properties of the DNN.

In this paper, we present the first concolic testing method for DNNs. The method is parameterised using a set of coverage requirements, which we express using Quantified Linear Arithmetic over Rationals (QLAR). For a given set $\mathfrak{R}$ of coverage requirements, we incrementally generate a set of test inputs to improve coverage by alternating between concrete execution and symbolic analysis. Given an unsatisfied test requirement $r$, we identify a test input $t$ within our current test suite such that $t$ is close to satisfying $r$ according to an evaluation based on concrete execution. After that, symbolic analysis is applied to obtain a new test input $t^{\prime}$ that satisfies $r$. The test input $t^{\prime}$ is then added to the test suite. This process is iterated until we reach a satisfactory level of coverage.

Finally, the generated test suite is passed to a robustness oracle, which determines whether the test suite includes adversarial examples , i.e., pairs of test cases that disagree on their classification labels when close to each other with respect to a given distance metric. The lack of robustness has been viewed as a major weakness of DNNs, and the discovery of adversarial examples and the robustness problem are studied actively in several domains, including machine learning, automated verification, cyber security, and software testing.

Overall, the main contributions of this paper are threefold:

We develop the first concolic testing method for DNNs.

We evaluate the method with a broad range of test coverage requirements, including Lipschitz continuity and several structural coverage metrics . We show experimentally that our new algorithm supports this broad range of properties in a coherent way.

We implement the concolic testing method in the software tool DeepConcolic https://github.com/TrustAI/DeepConcolic. Experimental results show that DeepConcolic achieves high coverage and that it is able to discover a significant number of adversarial examples.

Related Work

We briefly review existing efforts for assessing the robustness of DNNs and the state of the art in concolic testing.

Current work on the robustness of DNNs can be categorised as offensive or defensive. Offensive approaches focus on heuristic search algorithms (mainly guided by the forward gradient or cost gradient of the DNN) to find adversarial examples that are as close as possible to a correctly classified input. On the other hand, the goal of defensive work is to increase the robustness of DNNs. There is an arms race between offensive and defensive techniques.

In this paper we focus on defensive methods. A promising approach is automated verification, which aims to provide robustness guarantees for DNNs. The main relevant techniques include a layer-by-layer exhaustive search , methods that use constraint solvers , global optimisation approaches and abstract interpretation to over-approximate a DNN’s behavior. Exhaustive search suffers from the state-space explosion problem, which can be alleviated by Monte Carlo tree search . Constraint-based approaches are limited to small DNNs with hundreds of neurons. Global optimisation improves over constraint-based approaches through its ability to work with large DNNs, but its capacity is sensitive to the number of input dimensions that need to be perturbed. The results of over-approximating analyses can be pessimistic because of false alarms.

The application of traditional testing techniques to DNNs is difficult, and work that attempts to do so is more recent, e.g., . Methods inspired by software testing methodologies typically employ coverage criteria to guide the generation of test cases; the resulting test suite is then searched for adversarial examples by querying an oracle. The coverage criteria considered include neuron coverage , which resembles traditional statement coverage. A set of criteria inspired by MD/DC coverage is used in ; Ma et al. present criteria that are designed to capture particular values of neuron activations. Tian et al. study the utility of neuron coverage for detecting adversarial examples in DNNs for the Udacity-Didi Self-Driving Car Challenge.

We now discuss algorithms for test input generation. Wicker et al. aim to cover the input space by exhaustive mutation testing that has theoretical guarantees, while in gradient-based search algorithms are applied to solve optimisation problems, and Sun et al. apply linear programming. None of these consider concolic testing and a general means for modeling test coverage requirements as we do in this paper.

2 Concolic Testing

By concretely executing the program with particular inputs, which includes random testing, a large number of inputs can be tested at low cost. However, without guidance, the generated test cases may be restricted to a subset of the execution paths of the program and the probability of exploring execution paths that contain bugs can be extremely low. In symbolic execution , an execution path is encoded symbolically. Modern constraint solvers can determine feasibility of the encoding effectively, although performance still degrades as the size of the symbolic representation increases. Concolic testing is an effective approach to automated test input generation. It is a hybrid software testing technique that alternates between concrete execution, i.e., testing on particular inputs, and symbolic execution, a classical technique that treats program variables as symbolic values .

Concolic testing has been applied routinely in software testing, and a wide range of tools is available, e.g., . It starts by executing the program with a concrete input. At the end of the concrete run, another execution path must be selected heuristically. This new execution path is then encoded symbolically and the resulting formula is solved by a constraint solver, to yield a new concrete input. The concrete execution and the symbolic analysis alternate until a desired level of structural coverage is reached.

The key factor that affects the performance of concolic testing is the heuristics used to select the next execution path. While there are simple approaches such as random search and depth-first search, more carefully designed heuristics can achieve better coverage . Automated generation of search heuristics for concolic testing is an active area of research .

3 Comparison with Related Work

We briefly summarise the similarities and differences between our concolic testing method, named DeepConcolic, and other existing coverage-driven DNN testing methods: DeepXplore , DeepTest , DeepCover , and DeepGauge . The details are presented in Table 1, where NC, SSC, and NBC are short for Neuron Coverage, SS Coverage, and Neuron Boundary Coverage, respectively. In addition to the concolic nature of DeepConcolic, we observe the following differences.

DeepConcolic is generic, and is able to take coverage requirements as input; the other methods are ad hoc, and are tailored to specific requirements.

DeepXplore requires a set of DNNs to explore multiple gradient directions. The other methods, including DeepConcolic, need a single DNN only.

In contrast to the other methods, DeepConcolic can achieve good coverage by starting from a single input; the other methods need a non-trivial set of inputs.

Until now, there is no conclusion on the best distance metric. DeepConcolic can be parameterized with a desired norm distance metric $||\cdot||$.

Moreover, DeepConcolic features a clean separation between the generation of test inputs and the test oracle. This is a good fit for traditional test case generation. The other methods use the oracle as part of their objectives to guide the generation of test inputs.

Deep Neural Networks

A (feedforward and deep) neural network, or DNN, is a tuple $\mathcal{N}=(L,T,\Phi)$ such that $L=\{L_{k}|k\in\{1,\dots,K\}\}$ is a set of layers, $T\subseteq L\times L$ is a set of connections between layers, and $\Phi=\{\phi_{k}|k\in\{2,\dots,K\}\}$ is a set of activation functions. Each layer $L_{k}$ consists of $s_{k}$ neurons, and the $l$-th neuron of layer $k$ is denoted by $n_{k,l}$. We use $v_{k,l}$ to denote the value of $n_{k,l}$. Values of neurons in hidden layers (with $1<k<K$) need to pass through a Rectified Linear Unit (ReLU) . For convenience, we explicitly denote the activation value before the ReLU as $u_{k,l}$ such that

ReLU is the most popular activation function for neural networks.

Except for inputs, every neuron is connected to neurons in the preceding layer by pre-defined weights such that $\forall 1<k\leq K,\forall 1\leq l\leq s_{k}$,

where $w_{k-1,h,l}$ is the pre-trained weight for the connection between $n_{k-1,h}$ (i.e., the $h$-th neuron of layer $k-1$) and $n_{k,l}$ (i.e., the $l$-th neuron of layer $k$), and $b_{k,l}$ is the bias.

Due to the existence of ReLU, the neural network is a highly non-linear function. In this paper, we use variable $x$ to range over all possible inputs in the input domain $D_{L_{1}}$ and use $t,t_{1},t_{2},...$ to denote concrete inputs. Given a particular input $t$, we say that the DNN $\mathcal{N}$ is instantiated and we use $\mathcal{N}[t]$ to denote this instance of the network.

Given a network instance $\mathcal{N}[t]$, the activation values of each neuron $n_{k,l}$ of the network before and after ReLU are denoted as $u[t]_{k,l}$ and $v[t]_{k,l}$, respectively, and the final classification label is $label[t]$. We write $u[t]_{k}$ and $v[t]_{k}$ for $1\leq k\leq s_{k}$ to denote the vectors of activations for neurons in layer $k$.

When the input is given, the activation or deactivation of each ReLU operator in the DNN is determined.

We remark that, while for simplicity the definition focuses on DNNs with fully connected and convolutional layers, as shown in the experiments (Section 10) our method also applies to other popular layers, e.g., maxpooling, used in state-of-the-art DNNs.

Test Coverage for DNNs

A software program has a set of concrete execution paths. Similarly, a DNN has a set of linear behaviours called activation patterns .

Given a network $\mathcal{N}$ and an input $t$, the activation pattern of $\mathcal{N}[t]$ is a function $ap[\mathcal{N},t]$ that maps the set of hidden neurons to $\{\textsf{true},\textsf{false}\}$. We write $ap[t]$ for $ap[\mathcal{N},t]$ if $\mathcal{N}$ is clear from the context. For an activation pattern $ap[t]$, we use $ap[t]_{k,i}$ to denote whether the ReLU operator of the neuron $n_{k,i}$ is activated or not. Formally,

Intuitively, $ap[t]_{k,l}=\textsf{true}$ if the ReLU of the neuron $n_{k,l}$ is activated, and $ap[t]_{k,l}=\textsf{false}$ otherwise.

Given a DNN instance $\mathcal{N}[t]$, each ReLU operator’s behaviour (i.e., each $ap[t]_{k,l}$) is fixed and this results in the particular activation pattern $ap[t]$, which can be encoded by using a Linear Programming (LP) model .

Computing a test suite that covers all activation patterns of a DNN is intractable owing to the large number of neurons in pratically-relevant DNNs. Therefore, we identify a subset of the activation patterns according to certain coverage criteria, and then generate test inputs that cover these activation patterns.

2 Formalizing Test Coverage Criteria

We use a specific fragment of Quantified Linear Arithmetic over Rationals (QLAR) to express the coverage requirements on the test suite for a given DNN. This enables us to give a single test input generation algorithm (Section 8) for a variety of coverage criteria. We denote the set of formulas in our fragment by DR.

Given a network $\mathcal{N}$, we write $IV=\{x,x_{1},x_{2},...\}$ for a set of variables that range over the all inputs $D_{L_{1}}$ of the network. We define $V=\{u[x]_{k,l},v[x]_{k,l}~{}|~{}1\leq k\leq K,1\leq l\leq s_{k},x\in IV\}$ to be a set of variables that range over the rationals. We fix the following syntax for DR formulas:

where $Q\in\{\exists,\forall\}$, $w\in V$, $c,p\in$, $q\in\mathds{N}$, $\bowtie\in\{\leq,<,=,>,\geq\}$, and $x,x_{1},x_{2}\in IV$. We call $r$ a coverage requirement, $e$ a Boolean formula, and $a$ an arithmetic formula. We call the logic DR+ if the negation operator $\neg$ is not allowed. We use $\mathfrak{R}$ to denote a set of coverage requirement formulas.

The formula $\exists x.e$ expresses that there exists an input $x$ such that $e$ is true, while $\forall x.e$ expresses that $e$ is true for all inputs $x$. The formulas $\exists x_{1},x_{2}.e$ and $\forall x_{1},x_{2}.e$ have similar meaning, except that they quantify over two inputs $x_{1}$ and $x_{2}$. The Boolean expression $|\{e_{1},...,e_{m}\}|\bowtie q$ is true if the number of true Boolean expressions in the set $\{e_{1},...,e_{m}\}$ is in relation $\bowtie$ with $q$. The other operators in Boolean and arithmetic formulas have their standard meaning.

Although $V$ does not include variables to specify an activation pattern $ap[x]$, we may write

to require that $x_{1}$ and $x_{2}$ have, respectively, the same and different activation behaviours on neuron $n_{k,l}$. These conditions can be expressed in the syntax above using the expressions in Equation (3). Moreover, some norm-based distances between two inputs can be expressed using our syntax. For example, we can use the set of constraints

to express $||x_{1}-x_{2}||_{\infty}\leq q$, i.e., we can constrain the Chebyshev distance $L_{\infty}$ between two inputs $x_{1}$ and $x_{2}$, where $x(i)$ is the $i$-th dimension of the input vector $x$.

We define the satisfiability of a coverage requirement $r$ by a test suite $\mathcal{T}$.

Given a set $\mathcal{T}$ of test inputs and a coverage requirement $r$, the satisfiability relation $\mathcal{T}\models r$ is defined as follows.

$\mathcal{T}\models\exists x.e$ if there exists some test $t\in\mathcal{T}$ such that $\mathcal{T}\models e[x\mapsto t]$, where $e[x\mapsto t]$ denotes the expression $e$ in which the occurrences of $x$ are replaced by $t$.

$\mathcal{T}\models\exists x_{1},x_{2}.e$ if there exist two tests $t_{1},t_{2}\in\mathcal{T}$ such that $\mathcal{T}\models e[x_{1}\mapsto t_{1}][x_{2}\mapsto t_{2}]$

The cases for $\forall$ formulas are similar. For the evaluation of Boolean expression $e$ over an input $t$, we have

$\mathcal{T}\models a\bowtie 0$ if $a\bowtie 0$

$\mathcal{T}\models e_{1}\land e_{2}$ if $\mathcal{T}\models e_{1}$ and $\mathcal{T}\models e_{2}$

$\mathcal{T}\models\neg e$ if not $\mathcal{T}\models e$

$\mathcal{T}\models|\{e_{1},...,e_{m}\}|\bowtie q$ if $|\{e_{i}~{}|~{}\mathcal{T}\models e_{i},i\in\{1,...,m\}\}|\bowtie q$

For the evaluation of arithmetic expression $a$ over an input $t$,

$u[t]_{k,l}$ and $v[t]_{k,l}$ derive their values from the activation patters of the DNN for test $t$, and $c\cdot u[t]_{k,l}$ and $c\cdot v[t]_{k,l}$ have the standard meaning where $c$ is a coefficient,

$p$, $a_{1}+a_{2}$, and $a_{1}-a_{2}$ have the standard semantics.

Note that $\mathcal{T}$ is finite. It is trivial to extend the definition of the satisfaction relation to an infinite subspace of inputs.

Complexity

Given a network $\mathcal{N}$, a DR requirement formula $r$, and a test suite $\mathcal{T}$, checking $\mathcal{T}\models r$ can be done in time that is polynomial in the size of $\mathcal{T}$. Determining whether there exists a test suite $\mathcal{T}$ with $\mathcal{T}\models r$ is NP-complete.

3 Test Coverage Metrics

Now we can define test coverage criteria by providing a set of requirements on the test suite. The coverage metric is defined in the standard way as the percentage of the test requirements that are satisfied by the test cases in the test suite $\mathcal{T}$.

Given a network $\mathcal{N}$, a set $\mathfrak{R}$ of test coverage requirements expressed as DR formulas, and a test suite $\mathcal{T}$, the test coverage metric $M(\mathfrak{R},\mathcal{T})$ is as follows:

The coverage is used as a proxy metric for the confidence in the safety of the DNN under test.

Specific Coverage Requirements

In this section, we give DR+ formulas for several important coverage criteria for DNNs, including Lipschitz continuity and test coverage criteria from the literature . The criteria we consider have syntactical similarity with structural test coverage criteria in conventional software testing. Lipschitz continuity is semantic, specific to DNNs, and has been shown to be closely related to the theoretical understanding of convolutional DNNs and the robustness of both DNNs and Generative Adversarial Networks . These criteria have been studied in the literature using a variety of formalisms and approaches.

Each test coverage criterion gives rise to a set of test coverage requirements. In the following, we discuss the three coverage criteria from , respectively. We use $||t_{1}-t_{2}||_{q}$ to denote the distance between two inputs $t_{1}$ and $t_{2}$ with respect to a given distance metric $||\cdot||_{q}$. The metric $||\cdot||_{q}$ can be, e.g., a norm-based metric such as the $L_{0}$-norm (the Hamming distance), the $L_{2}$-norm (the Euclidean distance), or the $L_{\infty}$-norm (the Chebyshev distance), or a structural similarity distance, such as SSIM . In the following, we fix a distance metric and simply write $||t_{1}-t_{2}||$. Section 10 elaborates on the particular metrics we use for our experiments.

We may consider requirements for a set of input subspaces. Given a real number $b$, we can generate a finite set $\mathcal{S}(D_{L_{1}},b)$ of subspaces of $D_{L_{1}}$ such that for all inputs $x_{1},x_{2}\in D_{L_{1}}$, if $||x_{1}-x_{2}||\leq b$, then there exists a subspace $X\in\mathcal{S}(D_{L_{1}},b)$ such that $x_{1},x_{2}\in X$. The subspaces can be overlapping. Usually, every subspace $X\in\mathcal{S}(D_{L_{1}},b)$ can be represented with a box constraint, e.g., $X=[l,u]^{s_{1}}$, and therefore $t\in X$ can be expressed with a Boolean expression as follows.

In , Lipschitz continuity has been shown to hold for a large class of DNNs, including DNNs for image classification.

A network $\mathcal{N}$ is said to be Lipschitz continuous if there exists a real constant $c\geq 0$ such that, for all $x_{1},x_{2}\in D_{L_{1}}$:

Recall that $v[x]_{1}$ denotes the vector of activation values of the neurons in the input layer. The value $c$ is called the Lipschitz constant, and the smallest such $c$ is called the best Lipschitz constant, denoted as $c_{\mathit{best}}$.

Since the computation of $c_{\mathit{best}}$ is an NP-hard problem and a smaller $c$ can significantly improve the performance of verification algorithms , it is interesting to determine whether a given $c$ is a Lipschitz constant, either for the entire input space $D_{L_{1}}$ or for some subspace. Testing for Lipschitz continuity can be guided using the following requirements.

Given a real $c>0$ and an integer $b>0$, the set $\mathfrak{R}_{Lip}(b,c)$ of requirements for Lipschitz coverage is

where the $\mathcal{S}(D_{L_{1}},b)$ are given input subspaces.

Intuitively, for each $X\in\mathcal{S}(D_{L_{1}},b)$, this requirement expresses the existence of two inputs $x_{1}$ and $x_{2}$ that refute that $c$ is a Lipschitz constant for $\mathcal{N}$. It is typically impossible to obtain full Lipschitz coverage, because there may exist inconsistent $r\in\mathfrak{R}_{Lip}(b,c)$. Thus, the goal for a test case generation algorithm is to produce a test suite $\mathcal{T}$ that satisfies the criterion as much as possible.

2 Neuron Coverage

Neuron Coverage (NC) is an adaptation of statement coverage in conventional software testing to DNNs. It is defined as follows.

Neuron coverage for a DNN $\mathcal{N}$ requires a test suite $\mathcal{T}$ such that, for any hidden neuron $n_{k,i}$, there exists test case $t\in\mathcal{T}$ such that $ap[t]_{k,i}=\textsf{true}$.

This is formalised with the following requirements $\mathfrak{R}_{NC}$, each of which expresses that there is a test with an input $x$ that activates the neuron $n_{k,i}$, i.e., $ap[x]_{k,i}=\textsf{true}$.

The set $\mathfrak{R}_{NC}$ of coverage requirements for Neuron Coverage is

3 Modified Condition/Decision (MC/DC) Coverage

In , a family of four test criteria is proposed, inspired by MC/DC coverage in conventional software testing. We will restrict the discussion here to Sign-Sign Coverage (SSC). According to , each neuron $n_{k+1,j}$ can be seen as a decision where the neurons in the previous layer (i.e., the $k$-th layer) are conditions that define its activation value, as in Equation (2). Adapting MC/DC to DNNs, we must show that all condition neurons can determine the outcome of the decision neuron independently. In the case of SSC coverage we say that the value of a decision or condition neuron changes if the sign of its activation function changes. Consequently, the requirements for SSC coverage are defined as follows.

For SCC coverage, we first define a requirement $\mathfrak{R}_{SSC}(\alpha)$ for a pair of neurons $\alpha=(n_{k,i},n_{k+1,j})$:

That is, for each pair $(n_{k,i},n_{k+1,j})$ of neurons in two adjacent layers $k$ and $k+1$, we need two inputs $x_{1}$ and $x_{2}$ such that the sign change of $n_{k,i}$ independently affects the sign change of $n_{k+1,j}$. Other neurons at layer $k$ are required to maintain their signs between $x_{1}$ and $x_{2}$ to ensure that the change is independent. The idea of SS Coverage (and all other criteria in ) is to ensure that not only the existence of a feature needs to be tested but also the effects of less complex features on a more complex feature must be tested.

4 Neuron Boundary Coverage

Neuron Boundary Coverage (NBC) aims at covering neuron activation values that exceed a given bound. It can be formulated as follows.

Given two sets of bounds $h=\{h_{k,i}|2\leq k\leq K-1,1\leq i\leq s_{k}\}$ and $l=\{l_{k,i}|{2\leq k\leq K-1,1\leq i\leq s_{k}}\}$, the requirements $\mathfrak{R}_{\mathit{NBC}}(h,l)$ are

where $h_{k,i}$ and $l_{k,i}$ are the upper and lower bounds on the activation value of a neuron $n_{k,i}$.

Overview of our Approach

This section gives an overview of our method for generating a test suite for a given DNN. Our method alternates between concrete evaluation of the activation patterns of the DNN and symbolic generation of new inputs. The pseudocode for our method is given as Algorithm 1. It is visualised in Figure 1.

Algorithm 1 takes as inputs a DNN $\mathcal{N}$, an input $t_{0}$ for the DNN, a heuristic $\delta$, and a set $\mathfrak{R}$ of coverage requirements, and produces a test suite $\mathcal{T}$ as output. The test suite $\mathcal{T}$ initially only contains the given test input $t_{0}$. The algorithm removes a requirement $r\in\mathfrak{R}$ from $\mathfrak{R}$ once it is satisfied by $\mathcal{T}$, i.e., $\mathcal{T}\models r$.

The function $requirement\_evaluation$ (Line 7), whose details are given in Section 7, looks for a pair $(t,r)$ For some requirements, we might return two inputs $t_{1}$ and $t_{2}$. Here, for simplicity, we describe the case for a single input. The generalisation to two inputs is straightforward. of input and requirement that, according to our concrete evaluation, is the most promising candidate for a new test case $t^{\prime}$ that satisfies the requirement $r$. The heuristic $\delta$ is a transformation function that maps a formula $r$ with operator $\exists$ to an optimisation problem. This step relies on concrete execution.

After obtaining $(t,r)$, $\mathit{symbolic\_analysis}$ (Line 8), whose details are in Section 8, is applied to obtain a new concrete input $t^{\prime}$. Then a function $\mathit{validity\_chec}k$ (Line 9), whose details are given in Section 9, is applied to check whether the new input is valid or not. If so, the test is added to the test suite. Otherwise, ranking and symbolic input generation are repeated until a given computational cost is exceeded, after which test generation for the requirement is deemed to have failed. This is recorded in the set $F$.

The algorithm terminates when either all test requirements have been satisfied, i.e., $\mathfrak{R}=\emptyset$, or no further requirement in $\mathfrak{R}$ can be satisfied, i.e., $F=\mathfrak{R}$. It then returns the current test suite $\mathcal{T}$.

Finally, as illustrated in Figure 1, the test suite $\mathcal{T}$ generated by Algorithm 1, is passed to an oracle in order to evaluate the robustness of the DNN. The details of the oracle are in Section 9.

Ranking Coverage Requirements

This section presents our approach for Line 7 of Algorithm 1. Given a set of requirements $\mathfrak{R}$ that have not yet been satisfied, a heuristic $\delta$, and the current set $\mathcal{T}$ of test inputs, the goal is to select a concrete input $t\in\mathcal{T}$ together with a requirement $r\in\mathfrak{R}$, both of which will be used later in a symbolic approach to compute the next concrete input $t^{\prime}$ (to be given in Section 8). The selection of $t$ and $r$ is done by means of a series of concrete executions.

The general idea is as follows. For all requirements $r\in\mathfrak{R}$, we transform $r$ into $\delta(r)$ by utilising operators $\arg opt$ for $opt\in\{\max,\min\}$ that will be evaluated by concretely executing tests in $\mathcal{T}$. As $\mathfrak{R}$ may contain more than one requirement, we return the pair $(t,r)$ such that

Note that, when evaluating $\arg opt$ formulas (e.g., $\arg\min_{x}a:e$), if an input $t\in\mathcal{T}$ is returned, we may need the value ($\min_{x}a:e$) as well. We use $val(t,\delta(r))$ to denote such a value for the returned input $t$ and the requirement formula $r$.

The formula $\delta(r)$ is an optimisation objective together with a set of constraints. We will give several examples later in Section 7.1. In the following, we extend the semantics in Definition 3 to work with formulas with $\arg opt$ operators for $opt\in\{\max,\min\}$, including $\arg opt_{x}a:e$ and $\arg opt_{x_{1},x_{2}}a:e$. Intuitively, $\arg\max_{x}a:e$ ($\arg\min_{x}a:e$, resp.) determines the input $x$ among those satisfying the Boolean formula $e$ that maximises (minimises) the value of the arithmetic formula $a$. Formally,

the evaluation of $\arg\min_{x}a:e$ on $\mathcal{T}$ returns an input $t\in\mathcal{T}$ such that, $\mathcal{T}\models e[x\mapsto t]$ and for all $t^{\prime}\in\mathcal{T}$ such that $\mathcal{T}\models e[x\mapsto t^{\prime}]$ we have $a[x\mapsto t]\leq a[x\mapsto t^{\prime}]$.

the evaluation of $\mathcal{T}\models\arg\min_{x_{1},x_{2}}a:e$ on $\mathcal{T}$ returns two inputs $t_{1},t_{1}\in\mathcal{T}$ such that, $\mathcal{T}\models e[x_{1}\mapsto t_{1}][x_{2}\mapsto t_{2}]$ and for all $t_{1}^{\prime},t_{2}^{\prime}\in\mathcal{T}$ such that $\mathcal{T}\models e[x_{1}\mapsto t_{1}^{\prime}][x_{2}\mapsto t_{2}^{\prime}]$ we have $a[x_{1}\mapsto t_{1}][x_{2}\mapsto t_{2}]\leq a[x_{1}\mapsto t_{1}^{\prime}][x_{2}\mapsto t_{2}^{\prime}]$.

The cases for $\arg\max$ formulas are similar to those for $\arg\min$, by replacing $\leq$ with $\geq$. Similarly to Definition 3, the semantics is for a set $\mathcal{T}$ of test cases and we can adapt it to a continuous input subspace $X\subseteq D_{L_{1}}$.

We present the heuristics $\delta$ we use the coverage requirements discussed in Section 5. We remark that, since $\delta$ is a heuristic, there exist alternatives. The following definitions work well in our experiments.

When a Lipschitz requirement $r$ as in Equation (10) is not satisfied by $\mathcal{T}$, we transform it into $\delta(r)$ as follows:

I.e., the aim is to find the best $t_{1}$ and $t_{2}$ in $\mathcal{T}$ to make $||v[t_{1}]_{1}-v[t_{2}]_{1}||-c\cdot||t_{1}-t_{2}||$ as large as possible. As described, we also need to compute $val(t_{1},t_{2},r)=||v[t_{1}]_{1}-v[t_{2}]_{1}||-c\cdot||t_{1}-t_{2}||$.

1.2 Neuron Cover

When a requirement $r$ as in Equation (11) is not satisfied by $\mathcal{T}$, we transform it into the following requirement $\delta(r)$:

We obtain the input $t\in\mathcal{T}$ that has the maximal value for $c_{k}\cdot u_{k,i}[x]$.

The coefficient $c_{k}$ is a per-layer constant. It motivated by the following observation. With the propagation of signals in the DNN, activation values at each layer can be of different magnitudes. For example, if the minimum activation value of neurons at layer $k$ and $k+1$ are $-10$ and $-100$, respectively, then even when a neuron $u[x]_{k,i}=-1>-2=u[x]_{k+1,j}$, we may still regard $n_{k+1,j}$ as being closer to be activated than $u_{k,i}$ is. Consequently, we define a layer factor $c_{k}$ for each layer that normalises the average activation valuations of neurons at different layers into the same magnitude level. It is estimated by sampling a sufficiently large input dataset.

1.3 SS Coverage

In SS Coverage, given a decision neuron $n_{k+1,j}$, the concrete evaluation aims to select one of its condition neurons $n_{k,i}$ at layer $k$ such that the test input that is generated negates the signs of $n_{k,i}$ and $n_{k+1,j}$ while the remainder of $n_{k+1,j}$’s condition neurons preserve their respective signs. This is achieved by the following $\delta(r)$:

Intuitively, given the decision neuron $n_{k+1,j}$, Equation (18) selects the condition that is closest to the change of activation sign (i.e., yields the smallest $|u[x]_{k,i}|$).

1.4 Neuron Boundary Coverage

We transform the requirement $r$ in Equation (19) into the following $\delta(r)$ when it is not satisfied by $\mathcal{T}$; it selects the neuron that is closest to either the higher or lower boundary.

Symbolic Generation of New Concrete Inputs

This section presents our approach for Line 8 of Algorithm 1. That is, given a concrete input $t$ and a requirement $r$, we need to find the next concrete input $t^{\prime}$ by symbolic analysis. This new $t^{\prime}$ will be added into the test suite (Line 10 of Algorithm 1). The symbolic analysis techniques to be considered include the linear programming in , global optimisation for the $L_{0}$ norm in , and a new optimisation algorithm that will be introduced below. We regard optimisation algorithms as symbolic analysis methods because, similarly to constraint solving methods, they work with a set of test cases in a single run.

To simplify the presentation, the following description may, for each algorithm, focus on some specific coverage requirements, but we remark that all algorithms can work with all the requirements given in Section 5.

As explained in Section 4, given an input $x$, the DNN instance $\mathcal{N}[x]$ maps to an activation pattern $ap[x]$ that can be modeled using Linear Programming (LP). In particular, the following linear constraints yield a set of inputs that exhibit the same ReLU behaviour as $x$:

Continuous variables in the LP model are emphasized in bold.

The activation value of each neuron is encoded by the linear constraint in (20), which is a symbolic version of Equation (2) that calculates a neuron’s activation value.

Given a particular input $x$, the activation pattern (Definition 1) $ap[x]$ is known: $ap[x]_{k,i}$ is either true or false, which indicates whether the ReLU is activated or not for the neuron $n_{k,i}$. Following (3) and the definition of ReLU in (1), for every neuron $n_{k,i}$, the linear constraints in (21) encode ReLU activation (when $ap[x]_{k,i}=\textsf{true}$) or deactivation (when $ap[x]_{k,i}=\textsf{false}$).

The linear model (denoted as $\mathcal{C}$) given by (20) and (21) represents an input set that results in the same activation pattern as encoded. Consequently, the symbolic analysis for finding a new input $t^{\prime}$ from a pair $(t,r)$ of input and requirement is equivalent to finding a new activation pattern. Note that, to make sure that the obtained test case is meaningful, an objective is added to the LP model that minimizes the distance between $t$ and $t^{\prime}$. Thus, the use of LP requires that the distance metric is linear. For instance, this applies to the $L_{\infty}$-norm in (6), but not to the $L_{2}$-norm.

The symbolic analysis of neuron coverage takes the input test case $t$ and requirement $r$ on the activation of neuron $n_{k,i}$, and returns a new test $t^{\prime}$ such that the test requirement is satisfied by the network instance $\mathcal{N}[t^{\prime}]$. We have the activation pattern $ap[t]$ of the given $\mathcal{N}[t]$, and can build up a new activation pattern $ap^{\prime}$ such that

This activation pattern specifies the following conditions.

$n_{k,i}$’s activation sign is negated: this encodes the goal to activate $n_{k,i}$.

In the new activation pattern $ap^{\prime}$, the neurons before layer $k$ preserve their activation signs as in $ap[t]$. Though there may exist multiple activation patterns that make $n_{k,i}$ activated, for the use of LP modeling one particular combination of activation signs must be pre-determined.

Other neurons are irrelevant, as the sign of $n_{k,i}$ is only affected by the activation values of those neurons in previous layers.

Finally, the new activation pattern $ap^{\prime}$ defined in (22) is encoded by the LP model $\mathcal{C}$ using (20) and (21), and if there exists a feasible solution, then the new test input $t^{\prime}$, which satisfies the requirement $r$, can be extracted from that solution.

1.2 SS Coverage

To satisfy an SS Coverage requirement $r$, we need to find a new test case such that, with respect to the input $t$, the activation signs of $n_{k+1,j}$ and $n_{k,i}$ are negated, while other signs of other neurons at layer $k$ are equal to those for input $t$.

To achieve this, the following activation pattern $ap^{\prime}$ is constructed.

1.3 Neuron Boundary Coverage

In case of the neuron boundary coverage, the symbolic analysis aims to find an input $t^{\prime}$ such that the activation value of neuron $n_{k,i}$ exceeds either its higher bound $h_{k,i}$ or its lower bound $l_{k,i}$.

To achieve this, while preserving the DNN activation pattern $ap[t]$, we add one of the following constraints to the LP program.

If $u[x]_{k,i}-h_{k,i}>l_{k,i}-u[x]_{k,i}$: ${u_{k,i}}>h_{k,i}$;

2 Symbolic Analysis using Global Optimisation

The symbolic analysis for finding a new input can also be implemented by solving the global optimisation problem in . That is, by specifying the test requirement as an optimisation objective, we apply global optimisation to compute a test case that satisfies the test coverage requirement.

For Neuron Coverage, the objective is to find a $t^{\prime}$ such that the specified neuron $n_{k,i}$ has ${ap[t^{\prime}]_{k,i}}=$true.

In case of SS Coverage, given the neuron pair $(n_{k,i},n_{k+1,j})$ and the original input $t$, the optimisation objective becomes

Regarding the Neuron Boundary Coverage, depending on whether the higher bound or lower bound for the activation of $n_{k,i}$ is considered, the objective of finding a new input $t^{\prime}$ is either $u[t^{\prime}]_{k,i}>h_{k,i}$ or $u[t^{\prime}]_{k,i}<l_{k,i}$.

Readers are referred to for the details of the algorithm.

3 Lipschitz Test Case Generation

where $||*||_{D_{1}}$ and $||*||_{D_{2}}$ denote norm metrics such as the $L_{0}$-norm, $L_{2}$-norm or $L_{\infty}$-norm, and $\Delta$ is the radius of a norm ball (for the $L_{1}$ and $L_{2}$-norm) or the size of a hypercube (for the $L_{\infty}$-norm) centered on $t_{0}$. The constant $\Delta$ is a hyper-parameter of the algorithm.

The above problem can be efficiently solved by a novel alternating compass search scheme. Specifically, we alternate between solving the following two optimisation problems through relaxation , i.e., maximizing the lower bound of the original Lipschitz constant instead of directly maximizing the Lipschitz constant itself. To do so, we reformulate the original non-linear proportional optimisation as a linear problem when both norm metrics $||*||_{D_{1}}$ and $||*||_{D_{2}}$ are the $L_{\infty}$-norm.

The objective above enables the algorithm to search for an optimal $t_{1}$ in the space of a norm ball or hypercube centered on $t_{0}$ with radius $\Delta$, maximising the norm distance of $v[t_{1}]_{1}$ and $v[t_{0}]_{1}$. The constraint implies that $\sup_{||t_{1}-t_{0}||_{D_{2}}\leq\Delta}||t_{1}-t_{0}||_{D_{2}}=\Delta$. Thus, a smaller $F(t_{1},t_{0})$ yields a larger Lipschitz constant, considering that $\mathbf{Lip}(t_{1},t_{0})=-F(t_{1},t_{0})/||t_{1}-t_{0}||_{D_{2}}\geq-F(t_{1},t_{0})/\Delta$, i.e., $-F(t_{1},t_{0})/\Delta$ is the lower bound of $\mathbf{Lip}(t_{1},t_{0})$. Therefore, the search for a trace that minimises $F(t_{1},t_{0})$ increases the Lipschitz constant.

To solve the problem above we use the compass search method , which is efficient, derivative-free, and guaranteed to provide first-order global convergence. Because we aim to find an input pair that refutes the given Lipschitz constant $c$ instead of finding the largest possible Lipschitz constant, along each iteration, when we get $\bar{t}_{1}$, we check whether $\mathbf{Lip}(\bar{t}_{1},t_{0})>c$. If it holds, we find an input pair $\bar{t}_{1}$ and $t_{0}$ that satisfies the test requirement; otherwise, we continue the compass search until convergence or a satisfiable input pair is generated. If Equation (24) is convergent and we can find an optimal $t_{1}$ as

but we still cannot find a satisfiable input pair, we perform the Stage Two optimisation.

3.2 Stage Two

Similarly, we use derivative-free compass search to solve the above problem and check whether $\mathbf{Lip}(t_{1}^{*},t_{2})>c$ holds at each iterative optimisation trace $\bar{t}_{2}$. If it holds, we return the image pair $t_{1}^{*}$ and $\bar{t}_{2}$ that satisfies the test requirement; otherwise, we continue the optimisation until convergence or a satisfiable input pair is generated. If Equation (25) is convergent at $t_{2}^{*}$, and we still cannot find such a input pair, we modify the objective function again by letting $t_{1}^{*}=t_{2}^{*}$ in Equation (25) and continue the search and satisfiability checking procedure.

3.3 Stage Three

If the function $\mathbf{Lip}(t_{1}^{*},t_{2}^{*})$ fails to make progress in Stage Two, we treat the whole search procedure as convergent and have failed to find an input pair that can refute the given Lipschitz constant $c$. In this case, we return the best input pair we found so far, i.e., $t_{1}^{*}$ and $t_{2}^{*}$, and the largest Lipschitz constant $\mathbf{Lip}(t_{1}^{*},t_{2})$ observed. Note that the returned constant is smaller than $c$.

In summary, the proposed method is an alternating optimisation scheme based on compass search. Basically, we start from the given $t_{0}$ to search for an image $t_{1}$ in a norm ball or hypercube, where the optimisation trajectory on the norm ball space is denoted as $S(t_{0},\Delta(t_{0}))$) such that $Lip(t_{0},t_{1})>c$ (this step is symbolic execution); if we cannot find it, we modify the optimisation objective function by replacing $t_{0}$ with $t_{1}^{*}$ (the best concrete input found in this optimisation run) to initiate another optimisation trajectory on the space, i.e., $S(t_{1}^{*},\Delta(t_{0}))$. This process is repeated until we have gradually covered the entire space $S(\Delta(t_{0}))$ of the norm ball.

Test Oracle

We provide details about the validity checking performed for the generated test inputs (Line 9 of Algorithm 1) and how the test suite is finally used to quantify the safety of the DNN.

We are given a set $O$ of inputs for which we assume to have a correct classification (e.g., the training dataset). Given a real number $b$, a test input $t^{\prime}\in\mathcal{T}$ is said to be valid if

Intuitively, a test case $t$ is valid if it is close to some of the inputs for which we have a classification. Given a test input $t^{\prime}\in\mathcal{T}$, we write $O(t^{\prime})$ for the input $t\in O$ that has the smallest distance to $t^{\prime}$ among all inputs in $O$.

To quantify the quality of the DNN using a test suite $\mathcal{T}$, we use the following robustness criterion.

Given a set $O$ of classified inputs, a test case $t^{\prime}$ passes the robustness oracle if

Whenever we identify a test input $t^{\prime}$ that fails to pass this oracle, then it serves as evidence that the DNN lacks robustness.

Experimental Results

We have implemented the concolic testing approach presented in this paper in a tool we have named DeepConcolicThe implementation and all data in this section are available online at https://github.com/TrustAI/DeepConcolic. We compare it with other tools for testing DNNs. The experiments are run on a machine with 24 core Intel(R) Xeon(R) CPU E5-2620 v3 and 2.4 GHz and 125 GB memory. We use a timeout of 12 h. All coverage results are averaged over 10 runs or more.

We now compare DeepConcolic and DeepXplore on DNNs obtained from the MNIST and CIFAR-10 datasets. We remark that DeepXplore has been applied to further datasets.

For each tool, we start neuron cover testing from a randomly sampled image input. Note that, since DeepXplore requires more than one DNN, we designate our trained DNN as the target model and utilise the other two default models provided by DeepXplore. Table 2 gives the neuron coverage obtained by the two tools. We observe that DeepConcolic yields much higher neuron coverage than DeepXplore in any of its three modes of operation (‘light’, ‘occlusion’, and ‘blackout’). On the other hand, DeepXplore is much faster and terminates in seconds.

Figure 2 presents several adversarial examples found by DeepConcolic (with $L_{\infty}$-norm and $L_{0}$-norm) and DeepXplore. Although DeepConcolic does not impose particular domain-specific constraints on the original image as DeepXplore does, concolic testing generates images that resemble “human perception”. For example, based on the $L_{\infty}$-norm, it produces adversarial examples (Figure 2, top row) that gradually reverse the black and white colours. For the $L_{0}$-norm, DeepConcolic generates adversarial examples similar to those of DeepXplore under the ‘blackout’ constraint, which is essentially pixel manipulation.

2 Results for NC, SCC, and NBC

We give the results obtained with DeepConcolic using the coverage criteria NC, SSC, and NBC. DeepConcolic starts NC testing with one single seed input. For SSC and NBC, to improve the performance, an initial set of 1000 images are sampled. Furthermore, we only test a subset of the neurons for SSC and NBC. A distance upper bound of 0.3 ($L_{\infty}$-norm) and 100 pixels ($L_{0}$-norm) is set up for collecting adversarial examples.

The full coverage report, including the average coverage and standard derivation, is given in Figure 3. Table 3 contains the adversarial example results. We have observed that the overhead for the symbolic analysis with global optimisation (Section 8.2) is too high. Thus, the SSC result with $L_{0}$-norm is excluded.

Overall, DeepConcolic achieves high coverage and, using the robustness check (Definition 12), detects a significant number of adversarial examples. However, coverage of corner-case activation values (i.e., NBC) is limited.

Concolic testing is able to find adversarial examples with the minimum possible distance: that is, $\frac{1}{255}\approx 0.0039$ for the $L_{\infty}$ norm and $1$ pixel for the $L_{0}$ norm. Figure 4 gives the average distance of adversarial examples (from one DeepConcolic run). Remarkably, for the same network, the number of adversarial examples found with NC can vary substantially when the distance metric is changed. This observation suggests that, when designing coverage criteria for DNNs, they need to be examined using a variety of distance metrics.

3 Results for Lipschitz Constant Testing

This section reports experimental results for the Lipschitz constant testing on DNNs. We test Lipschitz constants ranging over $\{0.01:0.01:20\}$ on 50 MNIST images and 50 CIFAR-10 images respectively. Every image represents a subspace in $D_{L_{1}}$ and thus a requirement in Equation (10).

Since this paper is the first to test Lipschitz constants of DNNs, we compare our method with random test case generation. For this specific test requirement, given a predefined Lipschitz constant $c$, an input $t_{0}$ and the radius of norm ball (e.g., for $L_{1}$ and $L_{2}$ norms) or hypercube space (for $L_{\infty}$-norm) $\Delta$, we randomly generate two test pairs $t_{1}$ and $t_{2}$ that satisfy the space constraint (i.e., $||t_{1}-t_{0}||_{D_{2}}\leq\Delta$ and $||t_{2}-t_{0}||_{D_{2}}\leq\Delta$), and then check whether $\mathbf{Lip}(t_{1},t_{2})>c$ holds. We repeat the random generation until we find a satisfying test pair or the number of repetitions is larger than a predefined threshold. We set such threshold as $N_{rd}=1,000,000$. Namely, if we randomly generate 1,000,000 test pairs and none of them can satisfy the Lipschitz constant requirement $>c$, we treat this test as a failure and return the largest Lipschitz constant found and the corresponding test pair; otherwise, we treat it as successful and return the satisfying test pair.

3.2 Experimental Results

Figure 5 (a) depicts the Lipschitz Constant Coverage generated by 1,000,000 random test pairs and our concolic test generation method for image-1 on MNIST DNNs. As we can see, even though we produce 1,000,000 test pairs by random test generation, the maximum Lipschitz converage reaches only 3.23 and most of the test pairs are in the range $[0.01,2]$. Our concolic method, on the other hand, can cover a Lipschitz range of $[0.01,10.38]$, where most cases lie in $[3.5,10]$, which is poorly covered by random test generation.

Figure 5 (b) and (c) compare the Lipschitz constant coverage of test pairs from the random method and the concolic method on both MNIST and CIFAR-10 models. Our method significantly outperforms random test case generation. We note that covering a large Lipschitz constant range for DNNs is a challenging problem since most image pairs (within a certain high-dimensional space) can produce small Lipschitz constants (such as 1 to 2). This explains the reason why randomly generated test pairs concentrate in a range of less than 3. However, for safety-critical applications such as self-driving cars, a DNN with a large Lipschitz constant essentially indicates it is more vulnerable to adversarial perturbations . As a result, a test method that can cover larger Lipschitz constants provides a useful robustness indicator for a trained DNN. We argue that, for safety testing of DNNs, the concolic test method for Lipschitz constant coverage can complement existing methods to achieve significantly better coverage.

Conclusions

In this paper, we propose the first concolic testing method for DNNs. We implement it in a software tool and apply the tool to evaluate the robustness of well-known DNNs. The generation of the test inputs can be guided by a variety of coverage metrics, including Lipschitz continuity. Our experimental results confirm that the combination of concrete execution and symbolic analysis delivers both coverage and automates the discovery of adversarial examples.

This document is an overview of UK MOD (part) sponsored research and is released for informational purposes only. The contents of this document should not be interpreted as representing the views of the UK MOD, nor should it be assumed that they reflect any current or future UK MOD policy. The information contained in this document cannot supersede any statutory or contractual requirements or liabilities and is offered without prejudice or commitment.

References