Fooling a Complete Neural Network Verifier
Authors: Dániel Zombori
Balázs Bánhelyi
Tibor Csendes
István Megyeri
Márk Jelasity
Venue: ICLR 2021 Poster (2021)
Keywords: adversarial examples
complete verifiers
numerical errors

Abstract: The efficient and accurate characterization of the robustness of neural networks to input perturbation is an important open problem. Many approaches exist including heuristic and exact (or complete) methods. Complete methods are expensive but their mathematical formulation guarantees that they provide exact robustness metrics. However, this guarantee is valid only if we assume that the verified network applies arbitrary-precision arithmetic and the verifier is reliable. In practice, however, both the networks and the verifiers apply limited-precision floating point arithmetic. In this paper, we show that numerical roundoff errors can be exploited to craft adversarial networks, in which the actual robustness and the robustness computed by a state-of-the-art complete verifier radically differ. We also show that such adversarial networks can be used to insert a backdoor into any network in such a way that the backdoor is completely missed by the verifier. The attack is easy to detect in its naive form but, as we show, the adversarial network can be transformed to make its detection less trivial. We offer a simple defense against our particular attack based on adding a very small perturbation to the network weights. However, our conjecture is that other numerical attacks are possible, and exact verification has to take into account all the details of the computation executed by the verified networks, which makes the problem significantly harder.



Published as a conference paper at ICLR 2021
FOOLING A COMPLETE NEURAL NETWORK VERIFIER
Dániel Zombori, Balázs Ránhelyi, Tibor Csendes, István Megyeri, Márk Jelasity Institute of Informatics, University of Szeged, Hungary (zomborid, banhelyi, csendes, imegyeri, selaaity)einf.
ABSTRACT
The efficient and accurate characterization of the robustness of neural networks to imput perturbation is an important open problem. Many upproaches exist includ- ing heuristic and exact (or complete) methods. Complete methods are expensive but their mathematical formulation guarantees that they provide exact robustness metrics. However, this guarantee is valid only if we assume that the verified net- work applies rebitrary-precissee however, both the networks and the verifiers apply -niiedd-rrcciion floating point arithmetic. In this paper, we show that numerical roundoff errors can be exploited to craft adversarial networks, in which the actual robustness and the robustness computed by a Maateofftthe-rt complete verifier radically differ. We also show that such adversarial networks can be used to insert backdoor into any network in such a way that the backdoor is completely missed by the verifier. The attack is easy to detect in its naive form but, as we show, the adversarial network can be transformed to make its detection less trivial. We offer simple defense against our particular attack based on adding very small perturbation to the network weights. However, our conjecture is that other numerical attacks are possible, and exact verification has take into account all the details of the computation executed by the verified networks, which makes the problem significantly harder.
arithmetic and the verifier is reliable. In practice,
INTRODUCTION
In their seminal work, Szegedy al.) found that for given neural network and input example one can always find a very small adversarial input perturbation that results in an incorrect out- put (Szegedy et al., 2014). This striking discovery motivated a substantial amount of research. In this area, an important research direction is verification, that is, the characterization of the robustness of given network in a principled manner. A usual way of defining the verification problem involves the specification of an input domain and property that should hold over the entire domain. For ex- ample, we might require that all the points within a certain distance from an input example share the same output label as the example itself. The verification problem then to prove or disprove the property over the domain for a given network (Bunel et al. 2020).
There are a large number of verifiers offering different types of guarantees about their output. Com- plete verifiers offer the strongest guarantee: they are able to decide whether a given property holds in any given input domain. For example, the verifier of Tjeng et al.) is state-of-the-art complete verifier that we will focus on in this paper (Tjeng et al. 2019). However, it is currently standard practice to ignore the details of the computations that the network under investigation performs, such as the floating point representation or the order which input signals are summed.
In this paper, claim that such implicit assumptions make verifiers vulnerable to new kind of attack where the attacker designs a network that fools the verifier, exploiting the differences between how the verifier models the computation and how the computation is actually performed in the network. We will argue that such attacks can achieve an arbitrary divergence between the modeled and the actual behavior.
This new attack has practical implications well. Concerns about the safety of AI systems are expected to lead to the establishment of standard requirements certified by a designated author- ity (Salis-Madinier 2019). These certification procedures might involve verification methods as well. Fooling such methods makes it possible to get unsafe systems certified that might even contain backdoor allowing for triggering arbitrary behavior.

---

Published as a conference paper at ICLR 2021
Numerical precision has not been key practical concern in machine learning. Networks do some- times produce numerical errors (e.g., Inf or NaN values), most often due the non-linear operations within the loss function (Odena et al. 2019) or divergence during training. However, the network weights are normally robust to small perturbations due to stochastic learning algorithms (Bottou 2010), and due to regularizers such standard variants of weight decay and dropout (Srivastaval al. 2014). Due to this robustness, low precision arithmetic can be applied as well (Courbariaux et al. 2015 Gupta et al., 2015). Our results indicate that, when it comes to exact methods for ver- ification, numerical issues become a central problem that can cause arbitrary errors and enable backdoors.
Our contributions are the following, In Section 3 we introduce simple adversarial network that misleads the verifier Tjeng et al. (2019). In Section we show how to hide the large weights that present in the simple network. In Section 5 describe way to add backdoor to an existing network with the help of the adversarial networks we proposed. Finally, in Section 6 we offer a defense against the attack we presented.
2 BACKGROUND
Let us first formulate the verification problem, namely the problem of checking whether given property holds in a given domain. We adopt the notation used in (Tjeng et al. 2019). For a possible input æ, let (ax) denote the set of imputs that are considered similar to in the sense that expect all the points in (x) to get the same label as z. The set ((z) is normally defined as a ball around x in some metric space defined by suitable vector norm, The input domain we need to consider is given as (xx) (yaaid where Xpalid denotes the valid input points. For example, we have Xealid if the input is an image of m pixels with each pixel taking values from the interval [0, 1].
[0, 1]m²
We now have to formulate the property that we wish to have in this domain. Informally, we want all the points in the domain ((x) n Keatid to get the same classification label as x. Let X(x) denote the true label of and let (x;; 0) IR R" denote the neural network, parameterized by 0. This network has n outputs classifying each input & into n classes. The label of æ as predicted by the network is given by arg max; [a;; 0);- Using this notation, the property wish to have for an input x' E (g(x)
) n Xratid) is that ((x) = arg max; [a'; l);
Putting it all together, the verification problem can be expressed as deciding the feasibility of the constraint
x' E (g(x) n Xeatid) A (A(x) * arg max (x);
with x' as our variable. If this constraint is feasible then there is an x' that violates the property. If it is infeasible then (provided ((x) n Kealid is not empty) there is such x'.
2.1 APPROACHES TO VERIFICATION
There are many approaches to tackle this problem. We can, for example, search for a suitable x' in the given domain using some heuristic optimization methods (Goodfellow et al., 2013 Moosavi-
Deztooli et al. 2016; Kurakin el al., 2017 Carlini & Wagner 2017 Brendel et al. 2019). If the
search succeeds, can decide that equation L iis Teasible. Otherwise we cannot decide.
Other methods attempt to find a proof for the infeasibility of equation [ however, they do not
guarantee such proof. Examples include (Wong & Kolter 2018 WWngg et al.) 2018 Gehr al. 2018 Raghunathan et al.) 22018) (Snnh et al.) (2019). If proof is found, we can decide that equation infeasible. Otherwise cannot decide. Such methods sometimes called incomplete (Tjeng
ct al. 2019 Bunel et al. 2020).
The strongest guarantee is given by methods that are able to decide the feasibility of equation These methods are sometimes called complete (Tjeng al. 2019 Bunel et al.) (020)).
Examples for such methods include Reluplex (Katz et al. 2017), method based on an SMT solver.
A number of verifiers are based on MILP solvers, for example, (Cheng et al. 2017] Dutta et al. 2018). MIPVerify (Tjeng et al. 2019) also uses an MILP formulation along with several addi- tional techniques to improve efficiency (see Section 2.2 Symbolic interval propagation has also been proposed for ReLU networks by Wang et al. in Relu Val (Wang et al. 20188), and as part of Neurify (Wang et al. 2018a). In Neurify, interval propagation is used as technique tighten the
2

---

Published as a conference paper at ICLR 2021
bounds used for linear relaxation. Nnenum is another geometric method that is based on propagating linear star sets (Bak et al. 2020).
2.2 MIPVERIFY
Although the idea behind the attack is not specific to a particular verifier as we discuss in Sec- oi of the Appendix- we develop and evaluate the attack in detail for state-of-the the-the-art complete verifier: MIPVerify (Tjeng et al.) (211)). It is based on a mixed integer linear programming (MILP) formulation. As long the domain ((x) 7 T.. is the union of set of polyhedra, and the neural network fzz 0) is a piccewise linear function of x with parameters 6, the problem of checking the feasibility of the constraint in equation ! can be formulated as MILP instance.
(xx) is normally defined as a ball in suitable norm with x: as the center. loo or & norms (xx) is thus cube. Also, Realid is normally a box or set of boxes, so the domain is indeed the union of a set of polyhedra. The neural network is piecewise linear as long as the nonlinearities used are ReLUs (note that the last softmax normalization layer adds no extra information and can thus be ignored). For the details of the MILP formalization, please see (Tjeng al. 2019
Importantly, MIPVerify applies a presolve step that greatly increases its efficiency. In this step, the authors attempt tighten the bounds on the variables of the problem, including on the inputs each ReLU computation. in this step it turns out that the input of a ReLU gate is always non- -ossiiiiee,, the output can be fixed as a constant zero, and if the input is always non-negative then the ReLU gate can be removed from the model as it will have no effect.
The presolve step applies three approaches in progressive manner. First, fast but inaccurate interval arithmetic approach is used. The resulting bounds are further improved by solving relaxed LP problem on every variable. Finally, the full MILP problem is solved for the variables but with early stopping.
2.3 FLOATING POINT REPRESENTATION
Floating point real number representations are successful and efficient tools for most real life ap- plications (Muller et al. 2010). This arithmetic is available on most modern computers via sophis- ticated hardware implementations. A floating point number is represented as s b where 8 the signed significand, b is the base and e is the exponent. There are numerous standards to implement the exact details of this idea that differ mainly in the number of bits that the significand and the exponent use. The formula to compute the represented real number has several possible variations as well.
Here, we will use the double precision (binary64) arithmetic defined by the IEEE 754-1985 stan- dard (TEEE 1985). There, b and have sign bit, 11 bit exponent, and 53 bit significand (with 52 bits stored explicitly). The so called machine epsilon (the maximum relative rounding er- ror) is 2 53 1.11e-16. 16. This means that, for example, the computation -020 + 2020- 10 will result in zero in this representation, if executed in the specified order. In our attack, we will exploit roundoff errors of this type. Note, that in the order of 1020 1020 2020 obtain the correct result of 2020.
2.4
WHAT IS THE OBJECT OF VERIFICATION?
In related work, it is almost always implicitly assumed that the object of verification neural network computed using precise arithmetic. However, more appropriate and also more ambitious goal is to consider the network as is computed in practice, that is, using floating usongifoatting point arithmetic, with arbitrary ordering of the parallelizable or associative operations.
If we consider the less ambitious goal of the verification of the precise model, most complete meth- ods still fall short as they use floating point representation internally without any hard guarantees for precision. Those verifiers that are based on different linear programming formulations all belong to this category. Although Katz et al. explicitly consider this issue for Reluplex (Katz et al. 2017). they also propose floating point representation citing efficiency reasons.
However, striving for precision is wrong direction as actual networks use floating point representa- tion themselves. This fact means that actual networks include con-linearities that need to be modeled
3

---

Published as a conference paper at ICLR 2021
C
0.5
0
V1
-
-2
1
Y2
ADO
0
0
0
0.4
0.8
0.8
0.8
Figure 1: A naive adversarial network. The neurons (represented by circles) are ReLUs, the numbers the circles represent the additive bias, and the numbers over the connection represent the weight. The valid input range is assumed to be x E [0, 1]. Parameter a defines the steepness of the transition region in (x)) while the "large weight" parameter. The output of four different neurons is shown as a function of x, assuming = -3 and w 1027.
explicitly if our goal is verification with mathematical strength. For example, ReluVal (Wang et al., 2018b) a promising candidate to meet this challenge. is symbolic interval-based method that attempts to compute reliable lower and upper bounds for the network activations in a ReLU network. Unfortunately, when computing the parameters of the linear expressions for the symbolic intervals, it still uses floating point representation, which means the method is not completely reliable in its published form. Similarly, Nnenum is also deliberately implemented an unreliable manner due efficiency Bak et al. (2020).
Our main point here that any "sloppiness" in the definition of the object of verification cutting any corners for the sake efficiency are potential sources of security problems that compromise the reliability of verification. Here, we shall give example of successful attack MIPVerify. We will exploit the fact that-even if both the network and MIPVerify use the same floating point representation the order of exccution of the associative operations (like addition) is not necessarily the same.
A SIMPLE ADVERSARIAL NETWORK
Now we present our attack in its simplest possible form. We describe an adversarial network that results in incorrect output when given MIPVerify. The main idea is exploit the fact that the addition of numbers of different magnitude can become imprecise in floating point arithmetic due roundoff errors, as described previously in Section
Our attack crucially depends on the order in which the inputs and the bias are added within a unit. We assume that the bias is always the last to be added, when computing the forward pass. Note that the creator the network who submits for verification can control the execution of the network in actual applications, since the verification is only about the structure but not the minute details of execution such as the order of addition each unit. Nevertheless, we also conjecture that any fixed order of addition, or indeed any fixed algorithm for determining the order could similarly be exploited an attack.
In approaches such as MIPVerify, which rely on state-of-the-art commercial solvers like Gurobi (Gurobil [220),, the mapping of the actual computation such as the order of addition to computations performed by the solver is non-trivial and hard to control, as it is defined by the many (typically proprietary, hence black box) heuristics and techniques applied while solving the MILP problem.
The simplest form of adversarial network is shown in Figure 1 This network performs binary
4

---

Published as a conference paper at ICLR 2021
W11
11
win
wf w
1
X
-05
0
O
Y1
-2
W21
W22
W2n
w T
0
Y2
An adversarial network without extremely large weights. The network equivalent to that shown in Figure [] only parameter w is distributed over n layers, and the neuron with constant zero input is made less obvious with the help of an additional neuron with constant zero output over the valid input domain.
Figure 2:
classification over its input x: E [0, 1]. By construction, know that y1 E [0. 1]. Since MIPVerify expects multi-class models and thus two outputs, we add another technical output y2. such that the two classes are defined by y1 1/2 and y1 y2. respectively. Also, include neuron with constant input of zero.
The key element of the network is neuron C (Figure [}.
The idea is that the maximal value of C(xr) given by w - w + 1. The computation this value might lead to a roundoff error if w is too large and if 1 is not the last addend. For example, when using the 64 bit floating point representation, if > 253 (recall that
is the machine epsilon) then roundoff error is possible. In the case of a roundoff eгror w + 1 - w is computed to be zero, that is, C(x) 0, x E [o, 1j. This means that we get the incorrect output y1 (x) = x E [0, 1]. In other words. the entire input domain appears to belong to the y2 > Y1 class. The roundoff error thus masks the fact that there are input points that in reality belong to the other class. This property will be used later on add a backdoor an existing network.
The role of is more subtle. It defines the steepness of the transition region of B(x). We should set o so that the range of (xx) is the interval [o, 1]. This means that we need to have o < -2
It should be emphasized that the roundoff error drastically changes the behavior of the network. Our goal is not to generate a small perturbation to push the network over a decision boundary; instead, we create switch with two very distinct positions, which is turned on or off depending whether the roundoff error occurs or not.
Empirical evaluation shows that the attack is successful. We evaluated MIPVerify experimentally using two commercial solvers: Gurobi (Gurobi 2020), and CPLEX (CPLEX 2020), and the open source GLPK (GLPK) 2020). During these evaluations, we experimented with different values of and to see whether our adversarial networks could fool the MIPVerify approach. We randomly generated 500 values for a from the interval [-15, -2] and for all the sampled a values we tested values 204 255 ..... 27. For each parameter setting has an adversarial example within a radius of 1. Recall that the valid input range is x E [0, 1], so in fact evaluated the problem over the entire valid input range. Clearly, the correct answer is yes, that is, the constraint in equation [ is feasible. Yet, we found that all three solvers found the problem infeasible for all the parameter combinations we tried. That is, simple adversarial network reliably fools the MIPVerify model.
tested whether the input point æ 0.75
OBFUSCATING THE NETWORK
The naive network in Figure I works as an attack, but it is painfully obvious to spot it has very large weights (which is highly unusual) and it also has a neuron with constant zero input (which is also suspicious). Here, we argue that the network can be made to look more "normal" relatively easily. Obviously, this problem might also lead to an arms race between obfuscators and detectors, and it is not our goal to offer an undetectable obfuscation. We simply wish to argue that detection can be made harder if an attacker puts in some effort to hide the attack. Here, we focus on making the weight distribution more realistic.
Figure illustrates the construction. We wire the neuron that requires constant zero input neuron that has a constant zero output over the input domain, due to the application of the rectifier nonlinearity. We then add n extra layers and spread the weights and -w over these layers effec-
5

---

Published as a conference paper at ICLR 2021
Table I: Percentage of successful attacks when w = 261
0 E
[-15 15, -10]
|-10,-1 -6]
[-6, -4]
|-4, -3]
[-3, -2]
n
20
97.4
97.5
98.6
92.3
96.0
71 50
97.4 97.3 95.9
97.3
98.7
tively creating two large products II, wiy and II. w2/. The last weight on both the top and bottom paths is set such that the entire product is w and -w, respectively. Each weight wy is drawn from the normal distribution Wjs (N(w,, (w /4) independently, but negative values are redrawn until positive value is found.
The obfuscated attack is also successful. We evaluated these networks using Gurobi, GLPK and CPLEX. The values for parameter n (the number of layers) we tested were n 20 and n 50. In both cases, we experimented with the same values of a and w as in the case of the simple network, and followed the same evaluation methodology. We generated the network weights wiy based on the algorithm above, independently for all the pairs of a and w parameters. The algorithm was successful in generating a good network- where the product of the weights along the top and bottom paths is the same in absolute value-for the first try in at least 70% of the cases, so it is not that difficult generate a suitable network: we can simply try different random seed until the algorithm is successful.
We found that MIPVerify was fooled independently of what solver used, that is, the problem was found infeasible for all the parameter combinations we tried, when w > 2 For the value of 2 MIPVerify still found the problem infeasible for the vast majority of the networks with all three underlying solvers. In the remaining few cases, MIPVerify found an adversarial sample with at least one of the three solvers. Table I contains the percentage of the successful adversarial networks (that is, the networks that fooled MiPVerify with all three solvers) in different ranges of a.
Further ideas for obfuscation. The values of all the weights Wij are positive. One could also add negative weights if the desired mean weight is zero. Such links could point to "garbage" neurons that have no effect on the output by design. Besides, when using this network as a backdoor to some relatively larger legitimate network (see Section 5). one could imitate the weight distribution of the legitimate network and integrate the backdoor structurally as well into the legitimate network.
5 CREATING BACKDOORS
We shall now demonstrate that the adversarial network we described can be used to extend a non- trivial network with a backdoor, so that the extended network passes verification exactly as the original network, but in practice it will have backdoor that can be used to trigger arbitrary behavior. The idea that, when the backdoor pattern is present in the input, the integrated adversarial network will operate in the "interesting" domain in which the roundoff error is on, so the verified behavior will be different from the actual behavior. When the backdoor pattern is not present, the adversarial network will operate in the "boring" domain where its output is zero and the roundoff error does not have any effect.
We will work with the MNIST dataset and we fix the backdoor pattern to be the top left pixel being larger than 0.05 (assuming the pixels are in [0, 1)). Note that in the MNIST dataset the top left pixel is O in every example.
The legitimate network to insert the backdoor into. For evaluation, selected an MNIST classifier described in Wong & Kolter (2018) and used in (Tjeng et al., 2019) to evaluate Veriff.fy. We will refer to this network as WK17a. 7a. It has two convolutional layers (stride length: 2) with 16 and 32 filters (size: 4x4) respectively, followed by a fully-connen
layer with 100 units. All these layers use ReLU activations. (note that in (Tjeng et al. 2019)) it was referred to as CNN The network was trained be robust to attacks of radius 0.1 in the for norm by the method of Wong and Kolter.
Inserting the backdoor. The backdoor construction is shown in Figure 3 The basic idea is that we insert the adversarial network as a switch that is triggered by a pattern in the input. Here, the backdoor is activated (that is, the roundoff error becomes effective) whenever the top left pixel is

---

Published as a conference paper at ICLR 2021
WK17a (MNIST network)
convolttinal 2
July commacto
copy
tegits coggeehhifeed loglts
X
c1s +=1000
-2000
shifted copy:
-20
Adversary
1017
exteed
weight of top left pixel
-2000
-1017
Oriiinal
Figure 3: Diagram of the MNIST network extended with backdoor that is activated by the top left pixel of the input image z. If this pixel is larger than 0.05 then the backdoor is activated and shifts the predicted labels. The output y is the predicted distribution of the MNIST labels. The thick empty arrows signify multiple connections. Note that the backdoor is integrated into the convolutional architecture of WK17a (see text for further explanation).
larger than 0.05. To achieve this, the parameters of neuron A in the simple network in Figure I to be modified.
had
The backdoor is integrated into the convolutional architecture. FigureBii is a conceptual diagram. In reality, the adversarial network is fully integrated into the convolutional architecture WK17a. This requires the creation of an additional filter for each neuron in the corresponding layer. The output of every such neuron can then be recovered from the computed new feature map and can be used in the next layers. The neuron with the two large input weights is already in the fully connected layer, it can simply be added to that layer. This neuron wired just two pixels the two feature maps in the previous convolutional layer that correspond to the outputs of its two input neurons. The neurons in the last layer of the adversarial network are added to the logits layer of WK17a.
Implementing the backdoor behavior. When the backdoor is active, we will make the network shift its predictions by one position. This needs the addition of two extra layers after the logits layer of WK17a, as well as the modification of the WK17a logits layer. We empirically determined that the absolute value of the signal in each unit is always less than 1000 in the logits layer of WK17a, so we increase the bias of each unit by 1000. This constant is large enough to ensure that all the values are positive. This further means that the ReL.U activation (that we add because now this is no longer the last layer) will not alter these values.
The next layer is a new one, into which we copy the WK17a logits layer and we copy a shifted version of the same logits layer as well. Copying can be implemented by zero bias and input weights of I. Shifting can be implemented by wiring the units in a shifted pattern. The adversarial network is then used suppress either the original copy or the shifted copy. If the backdoor is activated then the original copy will be suppressed, otherwise the shifted one. Suppression is implemented by subtracting the value 2000 from all the inputs so that they become negative (the output signal of the corresponding switch neuron, adversarial or original, is 1). This way, the output will be zero due to the ReLU activation.
In the final layer, the original and shifted halves of the previous layer are added. Since exactly one of these halves has been suppressed, the last layer will be equal to either the original layer or the shifted layer. We then apply softmax normalization to obtain the predicted label distribution y. This distribution will be identical to the one predicted by the original MNIST network if the backdoor not active; otherwise it will be shifted, so that if the original prediction was then the shifted prediction is i+1 mod 10. Note that the backdoor could trigger an arbitrary behavior, shifting is used here as an ad hoc example.
Verification fails, as it misses the backdoor. We verified the backdoored network-thal is, WK 17a extended with the adversarial network that implements the backdoor mechanism-usinn MIPVerify
7

---

Published as a conference paper at ICLR 2021
with Gurobi solver over the test set of the MNIST dataset, using radius of 0.1 in the foo norm. The verification result was identical to that reported in (Teng et al. 2019), namely 4.38% adversarial error, as if no backdoor had been present. The correct verification result should have been 100% adversarial error because, by design, the backdoor mechanism is fully functional in the verified network, and the backdoor pattern is at a distance of at most 0.05, that is, well within the radius of 0.1 from any example. Also, when the backdoor pattern is active, the label is guaranteed to be different from the prediction of 1K17a. This means that if the original prediction was correct, the backdoor will certainly introduce an adversarial example.
A DEFENSE
A naive idea for a defense could be to use a precision that is higher than that of the network while solving the optimization problem. This might indeed work but it would open another similar attack, namely the network's 's design could deliberately activate a certain roundoff error that is missed by the verifier. Using combinations of different precisions also an option but here instead of attempting to predict the outcome of such an arms race-we assume that both the network and the optimizer use the same double precision internal representation.
Weight perturbation as a defense. We propose to add a very small perturbation to the parameters of the network. That is, we replace every parameter with v w + -Wee, [,)),, where e is the relative scale parameter of the uniform noise term. The key insight is that natural networks are very robust to small perturbations, so their normal behavior will not be affected. However, even small perturbation will change the numerical behavior of neuron C' in the simple adversarial network (Figure []. In particular, its positivity will no longer depend the roundoff error and so the verifier will correctly detect its behavior. Note that the roundoff error might still occur, only the positivity of C' will not depend on whether it occurs or not.
Accuracy is robust to small weight perturbation. We tested the sensitivity of the WK17a 7a network we studied in Section 5 We perturbed the parameters of both the original version and the backdoor version (see Figure 3. using various values of e and we measured the test accuracy of the networks. The results are shown in Table 2 (the results are averages of 10 independent perturbed networks). Although the network with a backdoor is somewhat less robust, for small noise such as 10-9 the prediction performance of both networks remains unaltered. Note that the test examples do not activate the backdoor.
Table 2: Test accuracy of the WK17a MNIST network with perturbed parameters (average of 10 independent perturbed networks).
10-1
10-2
10-3
10-4
10-5
10-6
10-9
original
0.9788
0
0.9810
0.9811 0.98105
0.9811 0.98105
0.9811
0.9811 0.9811
0.9811
with backdoor
0.1118
0.3744
0.9725
0.9811
0.9811
Adversarial error is robust to small weight perturbation. We also verified a perturbed WK17a network without the backdoor with MIPVerify, with 10-3, 10-6 and 10-9, and the results are identical to that of the unperturbed network for every single test example for e = 10-6 and 10-9, yielding 4.38% adversarial eиror. For 10-3 the adversarial error was 4.37%. Thus, in this network, even adversarial robustness is remarkably robust to small weight perturbation not only test accuracy.
The backdoor is revealed to verification with a 50% % probability. As mentioned above, the pos- itivity of neuron C' in the adversarial network will no longer depend on whether the roundoff error occurs or not. This because, due to the small noise, the two large incoming weights will no longer sum to zero but instead their sum will be positive or negative with an absolute value that is several orders of magnitude larger than the bias of neuron C, that is, These two cases both have a prob- ability of 50%. The same reasoning applies to the obfuscated network as well. A detailed analysis of this included in Section B in the Appendix. If the input weights of neuron C sum to a negative value then its output will be a constant zero If such a network is used as the switch for the backdoor then the backdoor will stay off permanently, independently of the input pattern. If the sum of the incoming weights is positive then C has a large positive output for the range x < 0.5 and so the behavior of the network remains intact, however, the verifier will now detect this behavior.
8

---

Published as a conference paper at ICLR 2021
Our empirical measurements support the theoretical predictions. We verified the simple as
well as the obfuscated networks (Figures 1 anddd 2), with 6 = 10 1016 and 10-9, using the same methodology as in the previous sections, with the same hyperparameters 0, and n, as before. We tested only those networks where the original behavior remained intact (which happens in approxi- mately 50% of the perturbed networks, as we argued above). With Gurobi, the verification revealed the true behavior in 100% of the cases for all our settings, so the defense indeed worked.
Finally, we verified a perturbed WK17a network with the backdoor added, perturbed with = 10 3,10- and 10-9, using Gurobi. In all three cases, we selected perturbation where the back- door switch remained functional. This time, the result of the verification successfully revealed the backdoor for 75.85%, 91.03% and 98.3% of the test examples, respectively. Since such a pertur- bation has a probability of only about 50%. it might be necessary to repeat the verification with independently sampled perturbations. This allows one to increase this probability to a desired level. Alternatively, the approval might be assigned to the perturbed network, as opposed to the original network. This way, if the perturbation turns the backdoor off permanently (and thus the verification does not find problems) the approval is still valid.
Selecting 6. Based on the observations above, we can summarize the requirements for selecting suitable value for c. First, we need the smallest possible c so that the behavior of the network is not changed. Second, we need a large enough so that ew > 1. Fortunately, these two requirements can easily be satisfied simultaneously since neural networks are in general very robust small weight perturbations, while w is very large. In our case, c = 10 was a suitable value.
7 CONCLUSIONS
We proposed attack against complete verifier, MIPVerifyy (Tjeng et al. 2019). The idea that we exploited a floating point roundoff error that was made by all the MILP solvers we tested to solve the MIPVerify model. The attack allowed us to modify any given network by adding backdoor that enables triggering arbitrary behavior using a specified pattern in the input. This backdoor was completely missed by the verification. Our preliminary results with other verifiers indicate that similar attack might be effective on number of other methods as well (see Appendix, Section [
Although we did offer a defense for the particular attack we presented, we believe that our work still implies that for a reliable verification, a verifier must take into account all the details of the imple- mentation of the network. This includes the details of the representation of the numeric parameters as well as the order of the operations. Otherwise, potentially exploitable differences in the actual computation and the model are guaranteed to exist. This way, though, the verification would be valid only for specific implementation. The implementation of a network can also be non-deterministic. For example, a parallel hierarchical implementation of addition can result in an exponential number of different actual executions of the same addition, depending network is running on. In this case, the verifier must make sure that its output is valid for every possible grouping and ordering of each operation performed during forward pass of the network.
the specifics of the hardware the
The attack we proposed is rather straightforward, just like the defense. However, without the de- fense, the attack can completely alter the behavior of any network undetected. This means that it is important to keep the numerical vulnerability of verification methods in mind, and further research is needed to find solutions that explicitly prevent numeric attacks in a scalable and efficient manner.
ACKNOWLEDGMENTS
This research was supported by the Ministry of Innovation and Technology NRDI Office within the framework of the Artificial Intelligence National Laboratory Program and the Artificial Intelligence National Excellence Program (grant 2018- 111.1.2.11-KKA N01.-----1-00000000 as well as grant NKFIH- 1279- 2/2020, project "Extending the activities of the HU-MATHS-IN IN Hungarian Industrial and Innova- tion Mathematical Service Network" (grant EFOP- Scholarship of the Hungarian Academy of Sciences, and the 1okp-19-4-Bolyyiee New National Ex- cellence Program of the Ministry of Human Capacities. We are also grateful to our reviewers and commenters for their very helpful feedback that helped us make the paper more complete and better organized.
the János Bolyai Research

---

Published as a conference paper at ICLR 2021
REFERENCES
Stanley Bak, Hoang-Dung Tran, Kerianne Hobbs, and Taylor T. Johnson. Improved geometric path enumeration for verifying relu neural networks. In Shuvendu K. Lahiri and Chao Wang (eds.), Computer Aided Verification, pp. 66-96, Cham, 2020. Springer International Publishing.
Léon Bottou. Large-scale machine learning with stochastic gradient descent. In Yves Lechevallier and Gilbert Saporta (eds.). Proceedings of COMPSTAT'010,, pp- 177-186, Heidelberg, 2010. Physica- Verlag HD. doi: 00000//978-37908-2200 3-7908-266----.166
Wieland Brendel, Jonas Rauber, Matthias Kümmerer, Ivan Ustyuzhaninov, and Matthias Bethge. Accurate, reliable and fast robustness evaluation. In H. Wallach, H. Larochelle, A. Beygelzimer, F. d' d'Alché-Buc, E. Fox, and R. Garnett (eds.), Advances Neu- ral Information Processing Systems, volume 32, pp. 12861-12871. Curran Associates, Inc., 2019. URL attpps://procesd/ www.innn...nnrureeeeeeeeeeeeneee nwwries....... httpppssccpppppppppeeeeeeeeeeeee cc/papper/219//11le 885fe656777008coo 35cc 72aaea456722be 5--pper pddf
Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Philip H.S. Torr, Pushmeet Kohli, and M. Pawan Kumar. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21 21(2)):1 1-39 2020. URL http: http:///mma...ooopppppps/s//////
html
Nicholas Carlini and David A. Wagner. Towards evaluating the robustness of neural networks In 2017 IEEE Symposium on Security and Privacy, 2017, San Jose, CA, USA, May 22-26, 2017, pp. 39-57, 2017. doi: 10. 1099...//... URL 04644
abs abs/g///bss//...../// 1608.
Chih- Baih-Hong Cheng, Georg Nührenberg, and Harald Ruess. Maximum resilience of artificial neu- ral networks. In Deepak D' S'Suzza and K. Narayan Kumar (eds.), Automated Technology for Verification and Analysis, pp. 251-268, Cham, 2017. Springer International Publishing. doi: 10. 000079778-3-319-6817--222-
URL /ttp://aaavvvvv/.v http://wwwwwwoopp///////////////
01040. pddf
Matthieu Courbariaux, Yoshua Bengio, and Jean-Pierre David, Training deep neural networks with low precision multiplications. In Yoshua Bengio and Yann LeCun (eds.), 3rd International Con- ference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Workshop Track Proceedings, 2015. URL http::/ttt//iiiiie .rg. abs/ /1//14122 7024
CPLEX. Cplex optimizer, 2020.
URL
https: www wtt.//...m.aaaaam htt.:///m/aaaiiss/////oo
splex-optimizer
Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. Output range analysis for deep feedforward neural networks. In Aaron Dutle, César A. Muñoz, and Anthony Narkawicz (eds.), NASA Formal Methods 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings, volume 10811 1 of Lecture Notes in Computer Science, pp. 121-138. Springer, 2018 doi: 10.1007/978-3-339-77955 pd199709.099 091.0.9100.20000 pdf
URL htttps:///aatttt http//axxvvvv.ga/a//..../..
Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen. Petar Tsankov, Swarat Chaudhuri, and Martin T. Vechev. A12: safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposiun on Security and Privacy, SP 2018, Proceedings, 21- 23 May 2018 San Francisco, California, USA, pp. 3-18. IEEE Computer Society, 2018. doi: 10.11099/P:2018.00000
GLPK. Gnu linear programming kit, 2020. URL. glpk/]
Ian Goodfellow. Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. In 3rd International Conference on Learning Representations (ICLR), 2015. URL
https::/ org/
abs//as//////oooo//////////aa /bs//11/1 6572
Suyog Gupta, Ankur Agrawal, Kailash Gopalakrishnan, and Pritish Narayanan. Deep learn ing with limited numerical precision. In Francis Bach and David Blei (eds.), Proceedings of the 32nd International Conference on Machine Learning, volume 37 of Proceedings of Ma- chine Learning Research, pp. 1737-1746, Lille, France, 07-09 Jul 2015. PMLR. URL http: 7/proceed ml www.m.r.....s....mmmmmmmmmmmmm.e v htpptaalpppll55pp html]
10

---

Published as a conference paper at ICLR 2021
Gurobi. Gurobi optimizer, 2020. URL
com/
IEEE. 154-1985-. IEEE standard for binary floating- arithmetic, 1985.
Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In Rupak Majumdar and Viktor Kunčak (eds.). Computer Aided Verification, pp. 97-117, Cham, 2017. Springer International Publishing. doi:
3-1-1-3--31----------8-38 URL https: waw.aaivvvv...../..aaaaaaaa..aaa oxq/ abs
Alexey Kurakin, Ian J. Goodfellow, and Samy Bengio. Adversarial machine learning scale. In 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24. 26, 2017, Conference Track Proceedings, 2017. URL wwwpoeeie...e..... net net/forumtt forum? id=BJm4T4kgx
Seyed-Mohsen Moosavi-Dezfooli, Alhussein Fawzi, and Pascal Frossard. Deepfool: A simple and accurate method to fool deep neural networks. In The IEEE Conf. on Computer Vision and Puttern Recognition (CVPR), pp. 2574-2582 2582, June 2016. URL
https://www wwwndctttoooooooooooomooom on. org/ oww.occese content. _ww___epr______ 2016/ Sew.roooll_eeeFFoooooo BaaFFFooo_________ d_Simple__cvp 2016_paperr.eeeepeppeppeppp pap.a..p..ff.............
Jean-Michel Muller, Nicolas Brisebarre, Florent de Dinechin, Claude-Pierre Jeannerod, Vincent Lefévre, Guillaume Melquiond, Nathalie Revol, Damien Stehlé, and Serge Torres Handbook of Floating-Poing Arithmetic. Birkhäuser Boston, 2010. doi: 10. 111007977--08117-477777
Augustus Odena, Catherine Olsson, David Andersen, and Ian Goodfellow. TensorFuzz: Dehugging neural networks with coverage-guidest fuzzing. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.), Proceedings of the 36th International Conference on Machine Learning. volume 97 of Proceedings of Machine Learning Research, pp. 49111, Long Beach, California, USA, 09- 15 Jun 2019. PMLR. URL/attpp://prceeee egg. mlr httpggg...........eeeeeree
19a html
Aditi Raghunathan, Jacob Steinhardt, and Percy Liang- Certified defenses against adversarial examples. In International Conference on Learning Representations, 2018. URL https:
//openzeview. wwwest//oommidddeeeeeeeeetee
Rb
Franca MaliseMadinier. Building trust in human-centric artificial intelligence. Communication INT/887-EESC-201 European Economic and Social Committee, Oct. 30. 2019. URL https:
7/ www. eesc.
887.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certify- ing neural networks. Proc. ACM Program. 3 January 2019. doi: 10.1145/3290354.
Nitish Srivastava, Geoffrey Hinton, Alex Krizhevsky, Ilya Sutskever, and Ruslan Salakhutdinov. Dropout: A simple way to prevent neural networks from overfitting. J. Mach. Learn. Res., 15(1): 1929-1958, January 2014.
Christian Szegedy, Wojeiech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfel- low, and Rob Fergus. Intriguing properties neural networks. In 2nd Internationaa Conference on Learning Representations (ICLR), 2014. URU.ttsp://cciivorrrr/// wwtp:/xwwwwi....x//x//oba//a///
6199
Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming, In International Conference on Learning Representations (ICLR), 2019.
URL
net. forum? Hd--niddiHyyydgRmm
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa- Bianchi, and R. Garnett (eds.), Advances in Neural Information Processing Systems, volume 31, pp. 6367-6377. Curran Associates, Inc., 2018a. URL BRLLhttps::2 https/////ooceeeeeeeeeeee newrips. neurii cc/ paper/2018/F5 http://2201//11//eeee//// occ.
74 920992d888 7228728868442555555
Shiqi Wang. Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Formal security analysis of neural networks using symbolic intervals. In Proceedings of the 27th USENIX Conference on Security Symposium, SEC' 18, pp. 1599-1614, USA, 201 8b. USENIX Association.
11

---

Published as a conference paper at ICLR 2021
Lily Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsich, Luca Daniel, Duane Bon- ing, and Inderjit Dhillon. Towards fast computation of certified robustness for ReLU net- works. In Jennifer Dy and Andreas Krause (eds.), Proceedings of the 35th International Con- ference on Machine Learning, volume of Proceedings of Machine Learning Research, pp- 5276-528 5285, Stockholmsmässan, Stockholm Sweden, 10-15 Jul 2018. PMLR. URL. http: iiproceedings www.s/mww...r.eeeeeemeeeeeeeeeee /tteess//v/vwee hatpa///vOOww/gglllge 8a html
Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In Jennifer Dy and Andreas Krause (eds.), Proceedings of the 35th Inter- national Conference on Machine Learning, volume 80 of Proceedings of Machine Learning Re- search, pp. 5286-5295, Stockholmsmässan Stockholm Sweden, 10-15 Jul 2018. PMLR. URL pwwss/v80/ woog//ogglloo Ba. ht.m
http::/pprocedd ngs htrp
A SPECIFICATION OF OUR EXPERIMENTAL ENVIRONMENT
Since our work depends on the internals commercial solvers, for reproducibility, we give the full specification of the environment that we used:
CPU: Intel(R) Xeon(R) CPU E5-2660 v4 @ 2.00GHz
Operating System: Ubuntu 18.04.4 LTS
GLIBC 2.27
Julia version 1.5.0
Gurobi: Gurobi Optimizer version 9.0.2 build v9.0.2rc0 (linux64)
Gurobi julia package: Gurobi v0.8.1
CPLEX: IBM(R) ILOG(R) CPLEX(R) Interactive Optimizer 12.10.0.0
CPLEX julia package: CPLEX v0.6.6
GLPK v4.64
GLPK julia package: GLPK v0.1 GLPKMaahProgInleffacc v0.5.0
MIPVerify julia package: MIPVerify v0.2.3
JuMP julia package: JuMP v0.18.6, ConditionalJuMP v0.1.0
MathProgBase julia package: MathProgBase v0.7.8
The code is shared wttttpss///tttn..cccoom///peeaaa
B ANALYSIS OF THE DEFENSE PERTURBATION
Let us consider the simple network in Figure The defense consists of adding small perturba- tion to the parameters of the network with uniform distribution. More precisely, we replace every parameter with v noise term.
2d(((1) w jwle), where is the relative scale parameter of the uniform
We will assume that 1, which means that adding noise weight will never change the sign of the weight. In practice, should be very small, for example, for double precision we used e = 10 From the construction, we also know that E [0, 1] and a -2. For simplification, here that w > 0 although that is not strictly necessary. Note that, in practice, we set w > 2 for attacking double precision floating point arithmetic, because smaller values do not guarantee adversariality.
will assume
For given input the output of every neuron is now a random variable depending on the random perturbation. From the definition of neuron A, however, we know that for every I < (1 c)/2 we have A(x) = 0. Formally, we have Pr(A(x) = Ojæ < (1- e)2) = 1. For this reason, the distribution of the output of every neuron independent of ær if < e)/2, because the output of each neuron depends on x only through neuron A. This means that it suffices to study x = 0 to describe the distribution of the output in this interval.
12

---

Published as a conference paper at ICLR 2021
From now on, any variable u, will denote a random variable with the distribution u; ((-, +c). We also assume that each variable u, is drawn independently. We have seen that A(0) = 0. From this, it follows that B(0) E - e. + e] because (0) = 1 + ug. Let us now examine the input
function of C, Sc. that we can derive from Figure [ We have (c) = w(1 +
wn w B(() - w(1 +
(2)(1 + u3) + (1 + u4) = =01 + (1)((1 + +uo) - ((++u2)) (1) + u3) + (1 + ua). From this, we can compute lower and upper bounds to get the range of fc()):
+
fc) E [--we + Awc c].
-
(2)
Within this interval, the distribution of (0) is symmetrical about the center of the interval, that is, 1. This further means that we have (0(fc(0) < 1 1/2. However, the probability mass of (o) very small in the interval [o, 1] for typical parameter settings, because we is several orders larger than I. For example, when = 10-8 and w = =24, we have we = 25 10-9 ~ 1.8e7. So, we have Pr(Sc(0) < 0) es 1/22.
If (c) < O then it is easy to see that fc(() < 0, x E J0, 1]. This is because (c(0) is an upper bound of fz)).. which follows from the fact that our only input has effect only through linear chain of neurons all of which will thus have a monotonous output. However, if fo(x) < 0 then
C(r) = 0 due to the ReLU activation, which means that yı (z) 0, thus y1 (2) (2(2) for all I E [0, l].
Now, let us consider the case where fc(0) > 0 and thus C(O) = f0). In this case, we have (0) < (0) if and only if C(0)(1 + us) < (1) + u6) + + u7. Here, we know that (1 < (1) + us) and -2C( + uz) +1+ u7 < 220 - +)+1+c From this, follows that if C(O) > 1 then we must have e > 1/2 to have (0) (2 with probability larger than zero. Since typical values of epsilon will be much smaller than 1/2, we conclude that if C(O) then y1 (0)= > (0). Previously, we showed that Pr(C(0) > 1) = 1/2. In the interval C(O) E [0, 1] the output depends on the value of epsilon as well as on the actual values of ut. "e and u7. However, mentioned earlier, the probability of perturbation that results in C(0) ending up in this interval is negligible.
Let us now consider the case where > (1- Looking at Figure I we notice that the transition interval where C(x) decreases from 1 to O is very short. We will show that, in fact, it is shorter than the machine epsilon, so C(0) is practically a step function. When adding noise, this transition interval becomes somewhat longer (that is, when C(O) > 0, because otherwise there would be no transition at all) and it will be in the order of é at most. To see this, we will need an upper bound on Sc and we need to derive the point where it reaches zero. We know that
fc(x) <
w(1 + Bc)(() w(1 - c)(1 - c) + (1+ $ a - ()x(x)) + (1+ and
(3)
B(x)
(4)
A(x) 2 x
2 (1 +c).
(5)
Note that we need a lower bound on A(x) because o < O. Now, we need to substitute the bounds on A(z) and B(x) into the bound on fc(x) and find x, for which this bound is zero. This gives
- 1 [1te
1 (1-
-1-c--1-- 1-c
1+
1
2e
1
w(1 S
(6)
1-2
2w(1-c) c)'
where we used the fact that a -2. This bound on xr is very close to 1/2. In fact, without perturbation (that is, with e = 0), the offset is just 1/2w which is less than the machine epsilon. for our settings of w. Since e² and 1/2w are negligibly small, we can approximate the bound as 1/2 + 2c. Since fa( is monotone decreasing, this means that fo(x) < 0 for E [1/2- + 2e, 1]. This further implies that C(x)= = for 2 E [1/2 + 2e, 1]. and thus y (z) < y2(z) over this interval.
To sum up, proved that if æ E 1/2 e then with at least 50% probability we have y1 (z) > y2(x)) and with almost 50% probability we have y1 (x) < y2(x)), and if x E [1/2 + 2e, 1] then we always have y1 (x) < (2))). When (x) 2 (2(2), the value of C(z) is large enough with overwhelming probability for reasonable parameter settings (e.g., c= 10 w 25 to prevent roundoff errors from occuring. The interval x E [1/2 c/2, 1/2 + 2c] was not discussed; here, the outcome depends on the actual noise values and the other parameters, however, this is an extremely short interval of length 2.5c.
As final note, the network in Figure can be treated in a very similar fashion, the only difference being that the noise that is effectively added to w and -w will follow a different distribution. Focus- ing on (-w is very similar), the noisy product has the form II, (w + u1:). The effective absolute
13

---

Published as a conference paper at ICLR 2021
noise added to w will be more similar to normal distribution it is mainly defined by the sum of the first order noise terms: Σi=1 Uji II Wik- Thus, the expectation is zero and the variance grows
with ew =_1 n Vn. The effective relative noise is thus increased by factor of vn, approximately. So, Pr(0 < C(x) < 1) is still very small, and the range of fc(x) is larger, so our arguments about the simple case transfer to the obfuscated case as well. The upper bound on the length of the transition interval will be somewhat larger due to the larger variance but it will still be very small.
C ATTACKING ADDITIONAL VERIFIERS
Although we focused on MIPVerify, the idea of the attack, and the attack itself is potentially viable for other state-of-the-art verifiers well. Here, briefly present number of preliminary mea- surements. We emphasize that these measurements are not intended to be thorough or systematic, but the result of simply making honest effort to run the public implementation of these ver- ifiers with no parameter tuning and only minimal modifications that were necessary to process our networks. Nevertheless, these preliminary results are still informative they support the conjecture that the type of attack we discussed is not specific to MIPVerify, and it could be viable for other verifiers as well. Further analysis of these verifiers is interesting direction for future work.
Table 3: Success of our attack various verifiers
simple adversarial network not fooled fooled
WK17a with backdoor
Relu Val
(Wang et al. 201 8b)
n.a. fooled
Neurify Wang al. 2018a
Nnenum Bak et al. 2020)
fooled (with small adjustment)
fooled
RefinePoly (Singh et al. 2019
n.a.
fooled
C.I RELUVAL
ReluVal (Wang et al. 2018b) is a complete method based on symbolic interval arithmetic. We used the implementation available on GitHut!] Since this implementation is not able process convolutional networks, we could test only our simple adversarial network. ReluVal was able to detect the adversarial example in any setting we tried. In other words, Relu Val was not fooled by our adversarial network.
We would like to add though that, inspecting the implementation. we found number of signs that suggest that the implementation itself is not completely reliable. For example, the outward rounding of intervals is done using a fixed constant, instead of an adaptive method. Also, the parameters of the linear expressions in the symbolic intervals are not treated reliably. This makes likely that one could design an attack specifically for this implementation.
C.2 NEURIFY
Neurify (Wang et al. 2018a) is a successor of ReluVal. It is much more efficient and it also uses linear relaxations that define an LP, which needs to be solved. This fact made likely that our attack might work. We used the GitHub implementationf? Neurify can process convolutional networks, so we could run the verification on both the simple adversarial network and the WK17a networks with or without the backdoor, although that required slight modification of the code: we had to fix trivial indexing bug that was unrelated to the verification itself.
For the simple adversarial network, Neurify was not able to correctly find adversarial examples, when the radius of the input ball was larger than about 0.85. Thus, this setup fools the method (or at least this implementation of it). With smaller radii, the adversarial examples were found.
We tested the original and backdoored variants of WK17a within the foo radii of 10% and 100% of the input space diameter. For the original WK17a network, the implementation was not able to process all the input examples, some of the examples caused error messages: "Not implemented: At
a/Reluva
w a/Neurify
14

---

Published as a conference paper at ICLR 2021
least node needs to be able to be split test the LP." Some other examples resulted in very long runs that never terminated. We were able to run the verification for a number of examples. For these examples, the verification was correct.
For the WK 17 network with the backdoor added, the verification terminated for all the 1000 exam- ples in the implementation, and in all the cases the answer was "safe", which is an incorrect answer. This means that this implementation Neurify is fooled by our backdoored network. This result might be due to an implementation issue, because for example, we saw Inf and NaN values among the bounds.
C.3 NNENUM
Nnenum Bak et al. 2020) is a geometric method that is based on propagating linear star sets. We used the GitHub implementation
We tested the simple adversarial network first, with an lo radius of 0.1. Nnenum is not fooled on this network. However, a small modification of the simple network allows us to fool the method. The original adversarial network in Figure I creates step function (C(x)) = 1, x I 0.5), while setting up roundoff error trap. We added new neuron, similar to neuron A, to the first layer with parameters so as to have neuron C' represent roughly rectangular function with C(x) 1, E (0.475, 0.5]. When testing this network with x = 0.55 and radius 0.1, Nnenum output "safe", which is incorrect.
On WK 1a with the backdoor, out of the 980 correctly classified examples we tested, 180 were incorrectly verified "safe" and the remaining 800 were "unknown". No example was verified as "unsafe" (using a timeout of minute).
C.4 ERAN REFINEPOLY
DeepPoly is verification method that is claimed to be sound to floating point operations (Singh ct al. 2019). We tested the GitHub implementation" ?
We were unable to process our simple adversarial network as it would have required substantial modifications of the code base. We verified WK17a and WK17a with the backdoor. We should add that we were not able to reproduce exactly the measurements in (Singh et al., 2019), although the results are close and we got no error messages or warnings. For this reason, our tests might not be entirely accurate.
We ran DeepPoly with the "complete" option, using the usual too radius of 0.1. This instance is referred to as RefinePoly, where DeepPoly is combined with MILP. RefinePoly was able to process WK17a and it correctly verified 928 safe examples out of the 980 correctly classified examples in the test set. For the rest of the examples it returned with a "failed" status, meaning it was not able decide about safety. However, for the backdoored version of WK17a, RefinePoly incorrectly output "safe" for 33 out of the 980 examples, all of which are in fact unsafe with respect to this network. For the remaining examples the output was "failed", which means that RefinePoly was unable to determine whether the input is safe or not. The 33 examples, over which RefinePoly fooled, represent small percentage, yet they are proof that RefinePoly is not immune our attack either.
D HEURISTIC ATTACKS
Our work focuses on complete verification, but it is still interesting ask how our backdoor con- struction performs against heuristic attacks such as PGD (Kurakin et al. 2017) or BrendelBethge (BB for short) (Brendel et al. 2019). We ran these attacks against the backdoored 1K17a network in the for norm. Both attacks successfully found adversarial examples created by the backdoor (PGD) (40 iterations) and BB have success rates of more than 30%, and 90%, respectively). The reason is that- although the backdoor switch network itself does not provide any useful gradient- needed because the PGD attack is led by the gradient of the original WK17a 7 network's loss function to the right direction (increasing the top left pixel value), while the BB attack starts from a random point that will be in the backdoor input space (top left pixel larger than 0.05) with high probability.
is not
https://github..com
15

---

Published as a conference paper at ICLR 2021
It interesting to note, though, that with small modification the backdoor can be hidden from these heuristic attacks as well. Namely, instead using just one pixel as a backdoor pattern, we can use more (say, a 3x3 area at the top left corner) requiring. for example, half of these pixels to be less than 0.05 and the other half to be larger than 0.05. The switch can easily modified be sensitive to this more complex pattern. When attacking this modified backdoor, both algorithms failed to find it, and instead their success rates became identical to that over the original unmodified WK17a network (less than 3% for both algorithms). This is because this more complex backdoor pattern represents subspace of relatively very small volume (hence BB will very rarely be initialized inside of it) and the natural gradient of W17a is very unlikely to point towards this specific pattern.
16


Reviews:
[{"review_id": "qpn5y0DAyhT", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper argues that, although existing complete neural network verifiers can provide some guarantees on the robustness, these verifiers have overlooked potential numerical roundoff errors in the verification, and in such cases the provided guarantees may be invalid. To show such a phenomenon, the authors propose to construct “adversarial neural networks” that can cause the complete verifier to produce imprecise results in floating point arithmetics and can thereby fool the verifier. They also showed it is possible to insert a backdoor to the network such that the backdoor is missed by the verifier while it can trigger some behavior desired by the attacker. Although this paper has also discussed a possible defense, I find the corresponding section not very clearly written.\n\nPros:\n* This paper raises an interesting problem in complete verifiers about potential numerical errors. This can be important to ensure the robustness of complete verifiers against some potential adversarial networks or backdoors.\n* The authors demonstrated the existence of the numerical error problem via constructing adversarial networks to fool complete verifiers.\n\nCons:\n* The structure of adversarial networks or inserted backdoors is not made to match some actual neural network architectures. E.g., in Figure 2, the network has a series of linear layers but has no activation between, and thus it does not look like an actual NN structure. Is it possible to construct adversarial networks on realistic architectures, e.g., MLP or CNN with ReLU activations? \n* Although defending against adversarial networks has been discussed in the paper, the writing appears inconsistent and unclear. (See additional comments below.)\n\nAdditional comments:\n* I find Sec. 6 is probably not very consistently and clearly written. In the beginning, it is said that adversarial networks are sensitive to weight perturbations (“The key insight is that some of the parameters of our adversarial network are rather sensitive to noise whereas non-adversarial networks are naturally robust to a very small perturbation of their parameters”), and later it is said that “the network with the backdoor appears to be robust to noise”. This looks confusing to me. Can you elaborate more whether you think the adversarial network is or is not robust to small noise? And the later paragraphs look difficult to understand. \n\n==========================================================================================\n\nUpdates after rebuttal:\n\nThanks to the authors for the reply. I have read the author response and understand that actually there are activations in the networks but just omitted from the figures. I am increasing my recommendation to 6.", "extra_scores": {}, "extra_text": {}}, {"review_id": "ggG7OG7-jB7", "reviewer": "AnonReviewer4", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The authors show that certain complete neural network verifiers can be mislead by carefully crafted neural networks that exploit round-off errors, which when large magnitude values overwhelm low magnitude values. Such a construction can be obfuscated by taking advantage of the compounding effect when there are many layers of the network. This can also be used to add backdoors to existing networks, albeit in a way that looks quite artificial.\n\nI definitely agree with the authors that is important to draw attention to edge cases where complete verifiers can fail given that \"completeness\" can lead to a false sense of security.  For that alone, I think this paper merits attention, even if 'numerical errors can mess up neural networks' is a well-known fact. \n\nThat being said, I think there are a few significant drawbacks to this work.\n\n(1) Presentation of the paper. The paper at times feels like more of a discussion than a detailed exploration of a certain attack type. As an example of why this is not optimal, it makes it difficult to figure out at a glance what each table is referring to. Also, it obfuscates the experimental results, of which there are quite a few in the paper. I believe the paper can benefit from a more formal style with paragraph headings and subsections breaking up the text, and the conclusions clearly highlighted as opposed to being spread throughout the text.\n\n(2) Flipping the answer from 'yes' to 'no' for a binary function requires a small perturbation near the decision boundaries, so the fact that numerical computations can lead to wrong answers in and of itself is not surprising. What would be much more interesting is the _degree_ to which such attacks can shift a continuous function. I believe that the method is this work leads to arbitrarily large differences, but I think this is something that should be explicitly explored.", "extra_scores": {}, "extra_text": {}}, {"review_id": "Hui2fA9RnNJ", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 7, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The paper shows that it is possible to fool exact verifiers using numerical instabilities. It proposes network architectures that can exploit numerical issues in order to get certificates from verifiers based on architecture such as MIPverifiy and that can at the same time accepts adversarial examples within the certificated epsilon-ball using a simple trigger. \nThis raises important security issues and as the author suggest, I do believe that such problem car arise in many situations. \n\nThe problem is first put into light on a very simple architecture and then on more complex ones and then with a added backdoor on existing network. Sereval optimizer for the verifiers are compared and behave similarly. A defence to this behavior is proposed, making all network parameters slightly noisy. \nWhile I'm convinced on the importance of the subject and I understand that it is probably mainly for illustration purposes, I have some questions mainly on the backdoor concept:\n* how can it be invisible to the verifier in section 5 (here I understand the only the original architecture and weights are provided to MIPVerify?) and detected in section 6 ? I miss a point there.\n* about the defence, I wish there were more experimental results with different epsilon values, to have a better intuition on the global behavior of the defence. I also think there could be more details on how the verifier detects the backdoor, as mentioned in previous point. ", "extra_scores": {}, "extra_text": {}}, {"review_id": "9OTZqSDDqdH", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The paper presents a method to create neural networks that, due to floating-point error, lead to wrong robustness certifications on most input images by a so-called \"complete verifier\" for neural network robustness. The authors show how to make their networks look a bit less suspicious and they discuss a way to detect neural networks that have been manipulated in the way they suggest.\n\nTo me, it was obvious a priori that any \"complete verifier\" for neural network robustness that treats floating-point arithmetic as a perfect representation of real arithmetic is unsound.\nHowever, I think works like the current one are important to publish such as to practically demonstrate the limitations of the \"guarantees\" given by certain robustness certification systems and to motivate further research. Therefore, I expect the target audience of the paper to be informed outsiders who have not so far questioned the validity of robustness certification research that did not explicitly address floating-point semantics. In light of this, the paper has several weaknesses related to presentation:\n- Terminology is often used in a confusing way. For example, the approach that is practically demonstrated to be unsound is called a \"complete verifier\" with the \"strongest guarantees\", wrongly implying that all other verifiers must be at least as unsound.\n- The related work is incomplete. For example, unsoundness due to floating-point-error has been previously practically observed in Reluplex: https://arxiv.org/pdf/1804.10829.pdf (in this case, it produced wrong adversarial examples, without any special measures having been taken to fool the verifier).\n- The related work is not properly discussed in relation to floating-point semantics. Some of the cited works are sound with respect to round-off, others are not. I would expect this to be the central theme of the related work section such as to properly inform the reader if and why certain approaches should be expected to be unsound with respect to round-off. The current wording that \"all the verifiers that work with a model of the network are potentially vulnerable\" is not fair to all authors of such systems; some have taken great care to ensure they properly capture round-off semantics.\n- I did not find obfuscation and defense particularly well-motivated. What is the practical scenario in which they would become necessary?\n- The paper sends a somewhat strange message: it (exclusively) suggests to combat floating-point unsoundness by employing heuristics to make it harder to find actual counterexamples. What about just employing verifiers with honest error bounds that explicitly take into account floating-point semantics? It may not be possible in the near-term to actually make correct \"complete verifiers\", but at least authors of incomplete verifiers will not have to succumb to pressure to make an unsound \"complete\" version in order to match precision, performance and/or \"guarantees\" of their competitors.\n\nThe technical sections are written well enough to be understandable, and the main technical contribution is a pattern of neurons we can insert into a neural network in order to make it behave in an arbitrary way that is invisible to the considered verifier. This is interesting and disproves any claim of \"completeness\", but scenarios where this would be a way to attack a system seem a bit contrived. Ideally, there would be an approach that can exploit round-off within a non-manipulated verified neural network to arbitrarily change the classification of a given input without changing the network. The paper might benefit from a discussion of this possibility and an explanation why it was not attempted.\n\n---\nThe new section 2.4 is appreciated, though it seems the paper still does not say that incomplete methods can deal with round-off error by sound overapproximation.", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: The authors demonstrate that complete neural network verification methods that use limited precision arithmetic can fail to detect the possibility of attacks that exploit numerical roundoff errors. They develop techniques to insert a backdoor into networks enabling such exploitation, that remains undetected by neural network verifiers and a simple defence against this particular backdoor insertion. 

The paper demonstrates an important and often ignored shortcoming of neural network verification methods, getting around which remains a significant challenge. Particularly in adversarial situations, this is a significant risk and needs to be studied carefully in further work.

All reviewers were in agreement on acceptance and concerns raised were adequately addressed in the rebuttal phase, hence I recommend acceptance. However, a few clarifications raised by the official reviewers and public comments should be addressed in the final revision:
1) Acknowledging that incomplete verification methods that rely on sound overapproximation do not suffer from this shortcoming.
2) Concerns around reproducibility of MIPVerify related experiments brought up in public comments.
Decision: Accept (Poster)