The ability to deploy neural networks in real-world, safety-critical systems is severely limited by the presence of adversarial examples: slightly perturbed inputs that are misclassified by the network. In recent years, several techniques have been proposed for training networks that are robust to such examples; and each time stronger attacks have been devised, demonstrating the shortcomings of existing defenses. This highlights a key difficulty in designing an effective defense: the inability to assess a network's robustness against future attacks. We propose to address this difficulty through formal verification techniques. We construct ground truths: adversarial examples with a provably-minimal distance from a given input point. We demonstrate how ground truths can serve to assess the effectiveness of attack techniques, by comparing the adversarial examples produced by those attacks to the ground truths; and also of defense techniques, by computing the distance to the ground truths before and after the defense is applied, and measuring the improvement. We use this technique to assess recently suggested attack and defense techniques.
 While machine learning, and in particular neural networks, have seen significant success, recent work BID20 has shown that an adversary can cause unintended behavior by performing slight modifications to the input at test-time. In neural networks used as classifiers, these adversarial examples are produced by taking some normal instance that is classified correctly, and applying a slight perturbation to cause it to be misclassified (or even misclassified as a specific target label chosen by the adversary). This phenomenon, which has been shown to affect all state-of-the-art networks, poses a significant hindrance to deploying neural networks in safety-critical settings.Many effective techniques have been proposed for generating adversarial examples BID20 ; ; BID17 ; BID1 ; BID21 ; and, conversely, several techniques have been proposed for training networks that are more robust to these examples BID8 ; BID22 BID6 ; BID7 ; BID16 ; BID21 . Unfortunately, it has proven difficult to accurately assess the robustness of any given defense by evaluating it against existing techniques for generating adversarial examples. In several cases, a defensive technique that was at first thought to produce robust networks was later shown to be susceptible to new kinds of attacks BID2 . This ongoing cycle thus cast a doubt on any newly-proposed defensive technique.In recent years, new techniques have been proposed for the formal verification of neural networks BID18 BID19 ; BID12 ; BID9 ; BID3 . These techniques take a network and a desired property, and formally prove that the network satisfies the property -or provide an input for which the property is violated, if such an input exists. Specifically, for a given input point and some allowed amount of distortion under a given metric, verification can be used for finding an adversarial example or for soundly proving that no such examples exist within the allowed distortion. While verification tends to be significantly slower in finding adversarial examples than the aforementioned heuristic-based techniques BID19 ; BID11 BID0 , it can provide the much-needed rigor for assessing the adversarial robustness of neural networks.In this paper we propose a method for using formal verification to assess the effectiveness of techniques for producing adversarial examples or defending against them. The key idea is to examine networks and apply verification to identify ground-truth adversarial examples. Formally, given a neural network F , a distance metric d, and an input x, we say that another input x is a ground-truth adversarial example for x if it is the nearest point (with respect to the metric d) such that F assigns different labels to x and x . It follows that all points whose distance to x is smaller than the distance between x and x are assigned the same label as x. The distance to the ground truth is thus an indication of how robust the network is to adversarial attacks at point x. Ground truths can serve multiple purposes: (i) if ground-truth adversarial examples are known for a set of points drawn from some meaningful distribution thought to represent real-world inputs, they can serve to estimate the robustness of a network as a whole, against any possible attack; (ii) they can be used for assessing attack techniques, by measuring the proximity of the adversarial examples that these attacks produce to the ground truths; and (iii) they can be used for assessing the effectiveness of defense techniques, by computing new ground truths for the hardened network and comparing them to the ground truths of the original network.Our contributions can thus be summarized as follows:• We suggest to use ground-truth adversarial examples, the provably closest adversarial with respect to some distance metric, as a tool for studying attacks and defenses.• We find that first-order attack algorithms often produce near-optimal results, i.e. results that are close to a ground-truth adversarial example.• We study adversarial training and find that it does increase robustness and does not overfit to a specific attack, as long as the attack is iterative.The rest of this paper is organized as follows. In Section 2 we provide some necessary background. We then describe the experiments that we conducted in Section 3, and analyze their results in Section 4. Finally , we conclude with Section 5. Neural networks hold great potential as controllers in safety-critical systems, but their susceptibility to adversarial examples poses a significant hindrance. The development of defensive techniques is difficult when they are measured only against existing attacks. The burgeoning field of neural network verification can mitigate this problem, by allowing us to obtain an absolute measurement of the usefulness of a defense, regardless of the attack to be used against it.In this paper, we introduce ground-truth adversarial examples and show how to construct them with formal verification approaches. We evaluate one recent attack BID1 and find it often produces adversarial examples whose distance is within 5.9% to 12.9% of optimal, and one defense BID16 , and find that it increases distortion to the nearest adversarial example by an average of 427% on the MNIST dataset for our tested networks. To the best of our knowledge, this is the first proof of robustness increase for a defense.Currently available verification tools afford limited scalability, which means experiments can only be conducted on small networks. However, as better verification techniques are developed, this limitation is expected to be mitigated. Orthogonally, when preparing to use a neural network in a safetycritical setting, users may choose to design their networks as to make them particularly amenable to verification techniques -e.g., by using specific activation functions or network topologies -so that strong guarantees about their correctness and robustness may be obtained.
We use formal verification to assess the effectiveness of techniques for finding adversarial examples or for defending against adversarial examples. This paper proposes a method for computing adversarial examples with minimum distance to the original inputs. The authors propose to employ provably minimal-distance examples as a tool to evaluate the robustness of a trained network. The paper describes a method for generating adversarial examples that have minimal distance to the training example used to generate them