# 神经网络中重要性分析和对抗生成的符号执行
Symbolic Execution for Importance Analysis and Adversarial Generation in Neural Networks
# 摘要
深度神经网络(DNN)越来越多地应用于各种应用中，其中许多应用具有严重的安全性和安全性问题。本文描述了DeepCheck，这是一种基于程序分析(特别是符号执行)的核心思想来验证dnn的新方法。DeepCheck实现了DNN轻量级符号分析的新技术，并将其应用于解决DNN分析中的两个具有挑战性的问题:1)识别重要的输入特征，2)利用这些特征创建对抗性输入。使用MNIST图像分类网络和文本数据情感网络进行的实验结果表明，DeepCheck有望成为深度神经网络分析的一个有价值的工具。
# 介绍
深度神经网络(Deep Neural Networks, DNN)越来越多地应用于各种应用中，其中许多应用都存在重大的安全和安保问题[20]。我们在本文中的重点是分类器:dnn接受复杂的高维输入，将其通过多层转换，最后为其分配特定的输出标签。如今，特斯拉(Tesla)、宝马(BMW)、福特(Ford)等大型汽车公司正将这种网络集成到自动或半自动汽车的感知模块中。预计这一趋势将继续并加剧。
由于在需要高保证保证的安全关键应用中使用神经网络的趋势日益增加，传统上强调dnn获得高准确性的目标正在被安全和安保目标所增强[16]。然而，由于创建这些模型的学习技术的性质，验证dnn是复杂和具有挑战性的。例如，为什么DNN，比如图像分类器，会给出一个特定的输出，我们还没有很好地理解。
无法解释深度神经网络的决定阻碍了它们在安全关键领域的应用，比如自动驾驶。
此外，由于此类网络的巨大输入空间，评估网络对概念上简单但有效的攻击的鲁棒性是一个困难的技术问题。
本文提出了一种基于符号执行的深度神经网络分析方法[7]，[19]。符号执行是一种众所周知的程序分析技术，近年来取得了许多进展[3]，[4]，[12]，[18]，[27]，并在各个领域得到了应用，如安全[6]，[8]，智能手机应用[1]，操作系统[36]和数据库[10]。该技术在符号输入上执行程序，并根据代码中的分支条件系统地收集符号数学约束。这些约束用现成的求解器求解，以获得执行可行程序路径的新输入。
我们注意到，采用分段线性激活函数的神经网络可以被视为命令式程序，这使得它们适用于程序分析技术。一类流行的神经网络使用整流线性单元(ReLUs)激活函数和最大池化操作(卷积神经网络)。这样的网络可以自然地翻译成分支结构，因此通过神经网络的路径可以在概念上被视为通过翻译程序的路径。这使得符号执行的应用程序能够为通过网络的路径构建路径条件。我们应用符号执行来选择感兴趣的程序路径，例如，来自网络训练数据集的特定输入所采取的路径。
然而，仅仅为一条路径构建路径条件，使用直接的concolic(或动态符号)执行[3]，[4]，[12]，[27]，可能会花费相当多的时间，并且仅使用一个符号变量来解决路径条件会给现代约束求解器带来压力。我们执行轻量级分析(没有任何约束求解)来确定对分类决策影响最大的输入，并执行定向符号执行方法，以生成对抗性输入，以最小的约束求解来评估网络鲁棒性。
本文的贡献如下:
•**想法。**我们提出了一个用于神经网络的符号执行分析框架，该框架侧重于识别重要的输入特征并使用它们来指导对抗性攻击生成的符号执行。
•方法。我们描述了DeepCheck方法，它由两种技术体现:DeepCheckImp，它应用符号执行来识别重要的输入特征，直观地提供解释网络的决定;以及DeepCheckattack，它应用符号执行来创建对抗性攻击。
•评估。我们对使用广泛研究的MNIST数据集的图像分类网络和对文本数据操作的情感网络进行了实验评估。结果强调了使用符号执行来识别重要输入特征和创建攻击的可行性，并且还表明识别的重要特征使生成对抗性示例的方法更具可扩展性。据我们所知，这是以有效的方式为文本分析应用程序生成有意义的对手的第一种方法之一。
•健壮性保证。尽管图像分类网络产生的对抗性攻击很简单，并且在之前已经被研究过[30]，但我们惊人地发现，即使沿着与有效分类输入遵循相同激活模式的路径，神经网络也容易受到这种攻击。以前的测试技术[26]，[31]，[34]没有注意到这种攻击，这些测试技术侧重于生成增加激活神经元覆盖率的测试，因此没有检查沿着同一路径的攻击。此外，如果没有发现这样的攻击，我们的工具就能够提供正式的保证，保证网络的行为符合预期。
# 背景
# A.神经网络
一个神经网络定义了一个函数F: IRn !将实数的输入向量x2irn映射到输出向量y2irm。对于分类网络，输出通常定义m个类的得分(或概率)，得分最高的类通常是预测的类。前馈网络被组织为从输入层开始的一系列层。每个中间层由称为神经元的计算单元组成。每个神经元消耗前一层神经元输出的线性组合，对其应用非线性激活函数，并将输出传播到下一层。输出向量Y是最后一层神经元输出的线性组合。例如，在整流线性单元(ReLU)网络中，每个神经元应用激活函数ReLU(x) = max(0;因此，每个神经元的输出形式为ReLU(w1·v1 +:::+wp·vp +b)，其中v1;::: vp是前一层w1神经元的输出;:::;Wp为权重参数，b为神经元的偏置参数。
大多数基于relu的分类网络通常在输出层应用softmax函数将输出转换为概率分布。
我们将这样的网络表示为F:= softmax (G)，其中G为纯ReLU网络，然后重点分析网络G
图1:(a)带有预测标签3的样例图像。(b) DeepCheckImp识别的前5%重要像素(绿色突出显示)。
(c) DeepCheckImp识别的前10%重要像素(绿色)。
(d) DeepCheckattack识别的1像素攻击(红色突出显示);将红色像素更改为黑色将预测标签更改为8。(e) 2像素攻击(红色)，其中包含可用于1像素攻击的可攻击像素
# B.符号执行
传统的符号执行是在符号上执行程序，而不是在具体的输入上进行系统的探索程序路径(在给定深度范围内)。对于探索的每条路径，它构建路径条件，即基于代码中的条件分支执行该路径的程序输入的约束。为了说明，当一个条件语句，比如“if(c):::”被执行时，两个条件分支中的每一个都被单独探索，并且路径条件cp被更新为cp ^c (then分支)和cp ^:c (else分支)。
路径条件的可行性使用现成的约束解算器进行检查，例如可满足模理论(SMT)解算器[2]，[9]，因为在符号执行过程中会遇到分支条件，以检测和避免不可行的路径(如果可能的话)，并生成执行可行路径的测试输入(如所需)。总的来说，程序效果是作为符号输入的函数来计算的。
# 深度检查方法
本节给出了我们在MNIST数据集上训练的图像分类网络方法的说明性概述，这是我们的案例研究主题之一。图1(a)显示了来自标准MNIST训练数据的示例图像，其预测标签为3(与真实标签相同)。我们的技术执行以下三个步骤:
节点i (S h−1)是一个命令式函数，表示神经元i在h层的分支变换
# A.转译(DeepCheck)
我们把训练好的模型转换成一个命令式程序。典型的神经网络结构没有分支。
然而，观察到在整流线性单元(ReLU)的情况下，激活函数f(x) = max(0;X)可以自然地转换成分支指令，如果(X > 0)则返回X;否则返回0;因此，一条通过神经的路径网络可以看作是经过翻译程序的路径，其中每个执行的分支对应于激活或不激活的各自的ReLU节点。为简单起见，我们在这里只讨论ReLU网络，但我们的方法适用于其他分段线性网络。
考虑一个输入向量X = hx0的网络N;:::;xn−1i，输出向量Y = hy0;:::;Ym−1i和l层。
任何层h有n h个ReLU节点，并产生一个输出向量，V h = hv h 0;:::;Vh nh−1 i，作为下一层的输入。每个神经元消耗前一层神经元输出的线性组合，对其应用非线性激活函数(在我们的例子中是max)，并将输出传播到下一层。DeepCheckτ的目标是将该模型转换为语义等效的程序P, s.t.，对于任何输入x, N (x)≡P(x)。
设P的输入状态为S inp，即$ X，输出状态为S op，隐层节点的输出表示为中间状态S h = hs h 0;:::;h层的任意ReLU节点i应用函数hW;b(V h−1)产生输出V h i。W为权矩阵，b为偏置项(W h−1 j);i为h−1层节点j与h层节点i连接的边的权值，b h−1 i为h层节点i添加的偏置项)。h层ReLU节点i对应的命令编码函数(Nodeh i (S h−1))如图2所示。调用这个函数n h次，产生状态列表，S h = hs h 0;:::;sh nh−1 i，相当于神经网络中间层h的输出，V h = hv h 0;:::;i.对每一层应用相同的过程，直到softmax，得到输出状态集S op，它是网络的输出≡Y。
# B.重要输入标识(DeepCheck[imp])
这一步旨在识别对网络决策影响最大的输入变量。我们在输入I上执行程序P，并根据输入变量(MNIST的情况下为784像素)获得每个输出变量的数学特征。
任何隐藏神经元的输出都可以用输入变量来表示。让我们考虑一个全连接网络的第二层隐藏层的神经元i。应用ReLU函数前神经元的输出可以表示为:w0;i·(w0 0;0·x0+ w0 1;0·x1 +:::+ w0 n - 1;0·xn - 1+ b0 0)+ w1 1;i·(w0 0;1·x0+ w0 n - 1;1·x1 +:::+ w1 n1 - 1;i·(w0 0;n1 - 1·x0+:: + w0 n - 1;n1 - 1·xn - 1+ b0 n1 - 1)+ b1 i。因此，通过归纳，每个输出元素yi可以表示为yi = Ci;0·x0 + Ci;1·x1 +::: + Ci;n−1·xn−1 + Bi，其中Bi是常数项，Ci;j是线性多项式的系数(带符号)，可以用xj到yi的非零边的权值计算，如下图所示;
式中P paths (i;j)表示输入节点xj到输出节点yi的路径集，Edgesp表示路径P上的边集，w(e)表示边e的权值。
注意系数项Ci;j精确地对应于输出变量yi w.r.t对输入变量xj的偏导数(dyi=dxj)。因此，我们使用输入变量的系数值来确定其对输出变量的影响，类似于基于梯度的方法，使用偏导数来确定每个输入变量的影响。请注意，我们可以使用任何现有的基于梯度的方法来识别重要的输入变量。
DeepCheck技术是建立在一个用于攻击生成的符号执行框架上的，而系数是符号执行应用的副产品。因此，我们使用它们进行重要性分析。
我们使用与预测标签对应的表达式中输入变量的系数(在示例中为3)，为每个输入变量分配重要性分数。如果分类决策受x1的影响大于x2，则认为输入变量x1比另一个x2更重要。DeepCheckImp使用了三个重要性指标:abs(coeff的绝对值)，co(coeff的实际带符号值)，coi(coeff的实际值×输入值)。然后将输入变量(像素)按其分数降序进行排序，并且那些位于该有序列表的最高阈值%的变量被认为是重要的。其基本原理是，对于重要像素而言，对图像进行微小的更改，例如仅更改一个重要像素的值，可能会对分类决策产生很大影响，并可能导致发现对抗性示例——新图像与原始图像仅相差一个像素的值，但这会使网络错误地为该图像分配不同的标签。
图1(b)显示了前5%，即39个，用绿色突出显示的重要像素。请注意，重要的像素如何跟踪数字3的形状，而不指向图像中与被标识为3的数字无关的区域，例如背景或边缘。图1(c)显示了前10%，即78个重要像素，用绿色突出显示。这些重要的像素形成了一个更密集的模式，可以追踪数字3的形状。这突出了基于其基于重要性分数的系数的短列表像素可以帮助解释分类决策。
# C.对抗性攻击生成(DeepCheck[attack])
我们的对抗性攻击生成算法DeepCheckattack旨在创建一个在t个输入变量上与原始输入不同的新输入，并且具有(1)与原始输入相同的激活模式，但(2)不同的标签。对于给定的输入图像I，具有t个符号输入变量，从程序P到输出层Y的路径条件是P C形式不等式(由ReLU函数引入)的结合。Bj是第j个隐藏神经元输出值的偏置项;
γ 2f >;≤g，由第j个隐藏神经元的活跃度决定。实际上，连接子句的数量小于A，因为有时符号值(Cj;i)的所有系数都为0，在这种情况下，整个连接子句的计算结果为真。
假设网络对输入I预测标签l(0到n-1)，则DeepCheckattack增加约束AC = nV j=1;j6= l0 fj (X) < fl 0 (X)，要求网络预测标签l0，其中l6 = l0。如果找到解决方案，DeepCheckattack通过将求解器返回的具体值设置为X，并且网络预测的标签l0与具有相同神经元激活模式的原始预测标签l不同，从而在对抗性攻击中成功。如果没有找到解决方案，这证明了网络对涉及t个输入特征或变量的对抗性扰动的鲁棒性。
图1(d)显示了通过我们的方法对图像I识别的1像素攻击;将红色像素更改为黑色将图像的预测标签更改为8。这个可攻击的像素实际上位于DeepCheckImp识别的前5%(前39)重要像素中。该可攻击像素的重要度降序为21。因此，将1个像素的攻击集中在重要的像素上，可以比检查每个像素的可攻击性更快地找到攻击。
事实上，这个图像只有一个1像素的攻击。从第一个图像像素(左上角)开始，从左到右扫描的线性搜索需要346次尝试才能找到这个攻击像素，这超过了可攻击像素的16倍秩序(21)。我们相信重要的像素可以为更可扩展的方法提供实用的启发来创建攻击。
为了创建2像素攻击，我们将deepcheck攻击集中在DeepCheckImp识别的重要像素上，特别是前5%的重要像素。我们用39 2 = 741对所选的重要像素进行无序配对，对于每对，我们将两个对应的变量设置为符号，因此符号执行创建的每个路径条件都恰好包含两个符号变量。对741对应用DeepCheckattack会导致93种独特的潜在2像素攻击。所述2像素攻击对中有38个包含作为元素的像素，该像素先前被识别为所述1像素攻击，而所述55个对仅包含不可攻击的像素;图1(e)用红色显示了这样一对。DeepCheckImp识别的重要像素在聚焦DeepCheckattack以发现2像素攻击中起着关键作用。在这个例子中，DeepCheckattack发现的第一个攻击包括3个最重要的像素中的2个。因此，在本例中搜索2像素攻击只需要检查不超过32 2 = 3对。这些结果说明了使用符号执行识别重要像素和创建1像素和2像素攻击的潜力，以及重要像素在查找可攻击像素和像素对方面的价值。
# 评价
在本节中，我们将介绍在两个网络上应用DeepCheck的两个案例研究;一个用于MNIST数据集的图像分类网络和一个用于文本数据的情感网络。DeepCheck已经在Java中实现(使用Z3求解器)，也有一个Python版本(使用pulp)，以方便与TensorFlow的简单接口。
镜像网络是一个完全连接的网络，具有以下配置784×10×10×10×10。它在MNIST数据集的60,000张图像上进行了训练[22]，准确率为92%。文本网络由一个卷积层(3×30, 64个过滤器)和一个密集层(1792×1)组成，其中第一层使用ReLU激活，最后一层使用sigmoid激活。该网络在大小为50000的IMDB电影评论数据集上进行训练。数据集的一半用于训练，另一半用于测试。对于训练，只保留前10000个单词，并且每个文本被填充或修剪为30个单词长(对于任何超过30个单词的输入，我们使用最后30个单词)。我们使用word2vec算法训练的大小为30的嵌入，其准确率为76%。虽然网络的准确性低于最先进的水平，但网络的简单性使它们可以用我们的实现进行分析。
我们试图解决以下研究问题作为我们评估的一部分。
RQ1: DeepCheckImp识别的输入特征对解释分类决策有用吗?
RQ2:攻击生成技术DeepCheckattack在生成对抗性输入方面有多有效?
RQ3: DeepCheckImp识别的重要输入特征对对抗性扰动敏感吗?它们是否有助于更快地生成攻击?
RQ4:在准确识别影响网络决策的输入特征方面，重要性指标(abs, co, coi)是如何比较的?
RQ5: DeepCheck与另一种对抗性攻击生成方法相比如何?
# A.图像分类网络
我们首先展示了我们的技术在MNIST网络上的应用结果，用于重要的像素识别和对抗性攻击生成。
1)重要的像素识别:我们从数据集中使用了10张图像(覆盖了所有10个标签)。对于每张图像，我们应用DeepCheckImp根据三个指标(abs, co, coi)的相对重要性计算像素的排名列表。表1显示了DeepCheckImp对重要像素的top-5%、top-10%和top-30%这三个指标产生的结果。对于每个图像(数字)，原始图像中的像素值以白色和黑色显示，而绿色突出显示被识别为重要的像素。
对于前5%和前10%的图像，可以观察到，每个度量都将图像中心部分的像素标记为最重要的，而前30%的图像似乎向边缘扩散。MNIST图像的中心部分存放数字。这突出表明，重要性度量确实正确地指向了图像中帮助网络做出分类决策的部分，随着阈值%的增加，精度降低。
abs和Co指标在中心区域显示类似的模式，而coi指标最接近数字的形状。具体来说，前10%像素的coi度量形成一个密集的模式，跟踪数字的形状。
2)对抗生成:我们评估了以下版本的DeepCheckattack。
•Baseline:执行图像的穷举搜索，一次一个像素，从左上角(0)到右下角(783)。我们使用DeepCheckattack来检查每个像素的可攻击性。可以给可攻击像素(ap)一个不同的值来改变图像的预测标签，同时保留路径中所有神经元的激活模式。对每个图像识别所有可能的可攻击像素(1像素对抗性攻击)。
•**Ordered:**像素是根据DeepCheckImp分配的重要性分数排序的。我们在这个有序列表上每次应用一个像素的DeepCheckattack，并识别所有可攻击的像素(1像素对抗)
•Short-list-threshold%:我们对较短版本的有序列表应用DeepCheckattack:例如，shortlist-5%根据DeepCheckImp分配的重要性分数对排序的前5%像素应用DeepCheckattack。我们使用这种技术在短列表中找到所有1像素攻击和2像素攻击。
a) 1-pixel攻击:我们应用基线、有序和短列表阈值%(阈值5,10,30)版本的DeepCheckattack来识别10张图像中的1像素攻击。
图3(a)对每个数字突出显示了1像素攻击的每个可攻击像素(红色)。可攻击像素位于或非常接近相应数字的形状。一些图像，例如，数字2，包含784个像素中的一个可攻击像素，而其他一些图像包含多个，例如，数字7的47。除数字6外的所有图像在受到攻击时都会得到一个唯一的错误标签。数字6有两次攻击，分别导致错误的标签5和8，都使用相同的像素
表2显示了所有技术发现的可攻击像素的数量。DeepCheckattack的基线和有序版本检测所有可能的1像素攻击的可攻击像素(# ap)。然而，使用有序列表有助于更快地发现攻击。表III显示了在发现第一次攻击之前需要尝试的像素数。对于所有指标和所有图像，不超过重要像素的前三分之一需要由有序版本检查，以找到可攻击的像素。此外，对于所有指标，需要检查少于10个像素才能发现至少一半图像的可攻击像素。coi度量要求最少的尝试次数(在所有图像中最多检查21个像素)，对于4个图像，coi识别的最重要的顶部像素是可攻击的像素。这突出了基于重要性分数对像素排序绝对有助于减少查找攻击的时间。
在DeepCheckattack的短列表阈值%版本中，我们分别只考虑前39个(5%)、78个(10%)和235个(30%)像素来产生攻击。表II显示，对于一半的图像，使用前10%的像素足以覆盖所有可能的1像素攻击。即使对于剩下的图像，短列表-10%发现了总攻击次数的一半。数字7和5最容易受到1像素的攻击。我们发现DeepCheckImp有助于捕捉微妙的对抗性攻击:即，对于网络对攻击者最强大的图像(例如只有1个可攻击像素的数字3和6)，重要性评分有助于识别对对抗性扰动敏感的像素。
b) 2-pixel攻击:应用基线或有序版本的DeepCheckattack来检查所有可能的2像素攻击是不可扩展的。因此，我们使用按coi指标排序的列表应用short-list-5%。对于每个图像，我们选择了所有39 2 = 741个无序对，这些对可以使用候选像素形成。然后我们对每一对进行评估，以确定它们是否产生了攻击。对于每个数字，图3(b)显示了任何2像素攻击中所有像素的并集，并显示了它们的位置。这些像素位于或非常接近相应数字的形状。表II显示了由DeepCheckattack识别的包含2像素攻击的可攻击像素(# ap)的数量，以及这些攻击中不包含任何可攻击像素的1像素攻击(# ap-new)的数量。
正如预期的那样，许多2像素的攻击由一个可攻击1像素的像素组成。然而，发现了一些新的攻击对，这些攻击对不包含任何可被1像素攻击的像素。10个数字中有4个可以被攻击，产生多个错误的标签，例如，数字8可以被攻击，使用3个不同的2像素攻击，使网络错误地将其分类为1、2或3。
表III给出了寻找每个图像(数字)的第一个2像素攻击的重要像素的数量。最糟糕的情况是数字2，其中必须考虑前19个重要像素才能找到2像素攻击。最好的情况发生在10个数字中的7个，其中前2个重要像素允许deepcheckattack创建2个像素的攻击。
# B.情感分析网络
情感分析网络的输入是单词序列，而不是图像。每个词都用一个叫做词嵌入的向量来表示，这个向量试图捕捉词之间的语义关系。在这个向量空间中，在相似上下文中使用的单词具有相似的嵌入，这可以帮助学习自然语言处理(NLP)任务[21]。这带来了一个挑战，即识别重要性或对单个值进行攻击并不意味着什么，因为单词被表示为向量，因此我们需要识别重要向量并对向量进行攻击。
为了克服这个挑战，我们必须修改重要性计算。我们计算了向量上每个元素的重要性分数，类似于像素的重要性分数计算(第III节)。然而，我们然后将这些分数加在词嵌入向量上，以获得一个词的重要性分数。然后，我们根据单词的重要性分数对它们进行排名，使前k个单词的嵌入向量的所有元素具有符号性，并应用DeepCheckattack算法来找到可行的攻击。
我们使用Python版本的DeepCheckattack，使用名为puLP的Python LP求解器库实现，以实现可扩展性。求解器返回的解是赋给每个符号元素的一组值。但是，这些值可能不代表单词的有效嵌入。
因此，我们为我们的解决方案中的每个向量(使用L2距离度量)找到最近的有效词嵌入(从词嵌入的词汇表中)。然后，我们将原始句子中与这些向量对应的单词替换为与之最接近的单词，并通过改变情感来测试这个新句子确实代表了对网络的有效攻击。
我们将基于重要性选择的攻击生成与基于随机选择的攻击生成进行比较，看看基于重要性选择单词是否有助于我们生成更短的攻击。较短的攻击是可取的，因为它们涉及替换原始句子中较少的单词，以保留原始句子的一些含义。因此，用于攻击的句子与原始句子具有语义相似性，因此理想情况下应该由网络赋予相同的情感。让我们考虑第7句(表四)，以消极情绪为例。重要性分析确定“恼人的”和“这个”是前两个最重要的词。
我们对这两个词的嵌入向量进行符号化处理，得到了一个网络标记为积极情绪的解。与这个解决方案最接近的有效嵌入词是“愚蠢”和“模式”，分别表示“烦人”和“这个”。我们生成了一个新的句子来取代这两个词，它仍然代表一种消极的情绪，但被网络分类为一种积极的情绪。如果我们随机选择要替换的单词，我们可以通过平均替换5个单词来找到攻击。
让我们考虑另一个例子，对于第9句(表四)，我们可以通过将三个最重要的单词“good”替换为“breakdown”，“film”替换为“facing”，“highly”替换为“terrific”来获得攻击。攻击使得句子的第一部分“崩溃对抗”有点荒谬，但积极的情绪仍然在文本中，但网络将这句话分类为消极的。相比之下，在没有重要性选择的情况下，我们可以通过改变14个单词来获得攻击，几乎是整个输入文本的一半。
这个实验强调了一个事实，即重要性分析可以帮助我们产生更集中的攻击，与随机选择相比，变化更少
请注意，在用最接近各自解决方案的有效单词替换句子后，我们只使用了导致网络攻击的解决方案。对于这两种方法，在某些情况下，当用最接近的有效词替换解决方案时，并没有改变情绪。我们将这种行为归因于向量空间中单词的稀疏性，这可能会影响最近单词的距离，以及当解被这些单词取代时激活模式的变化。我们的实验结果见表4。
# C.讨论
在本节中，我们将根据实验结果解决研究问题。
RQ1:对于图像分类网络，根据我们的观察(表1)，我们可以推断，DeepCheckImp能够识别定义输入数字形状的输入像素。因此，可以认为识别的像素负责分类决策。基于文本模型的结果，我们观察到DeepCheckImp有助于识别重要的输入特征，例如对网络决策影响最大的单词。
RQ2:表2的结果显示，我们能够生成126个1像素的攻击，并为图像分类网络发现819个2像素的可攻击像素。我们还能够成功地生成对文本模型的攻击(表4)，这比仅仅修改图像中的像素要复杂得多。因此，我们能够使用DeepCheckattack在规模较大的网络和真实数据集上生成攻击。
RQ3:由DeepCheckImp识别的重要像素确实对应于那些对对抗性扰动敏感的像素，如表2所示。只探索前10%的重要像素有助于生成所有可能的1像素攻击。使用DeepCheckImp可以生成2像素攻击，否则需要考虑784 2 = 306946潜在的可攻击对。在文本模型上的实验表明，选择由DeepCheckImp识别的重要单词比随机选择单词更有效地增加了发现语义上有意义攻击的机会。总的来说，可以推断使用DeepCheckImp使攻击生成过程可扩展，并有助于识别微妙的对手。
RQ4:重要性度量指标coi似乎在识别影响分类决策且容易受到攻击的像素方面表现最好。对于MNIST图像，这似乎有点明显，因为背景总是黑色的(像素值为零)。
然而，即使在文本模型上，我们也观察到coi度量标准始终比co和abs更好地识别可攻击词。
RQ5:快速梯度符号方法(Fast Gradient Sign Method, FGSM)[13]是一种针对MNIST图像生成对手的现有流行方法。在这种技术中，通过同时修改多个像素的强度来生成潜在的对手，从而使模型的损失函数减少了。我们使用这种方法为图1(a)中数字3的图像生成一个对手(图4)。我们观察到，为了使用FGSM生成这个对手，数字3形状上的几乎每个像素的值都必须被扰动。另一方面，我们能够在使用DeepCheck修改1个像素的同一图像上生成攻击(图1(d))。此外，我们还观察到，使用FGSM生成的攻击者追踪的激活模式或路径与原始有效标记的输入有很大不同。然而，通过构造，由DeepCheck生成的攻击保留了激活模式。使用来自模型的语义信息的好处是有助于生成网络与原始图像相似但给出不同分类的对手。这样的对手在调试网络和修复网络时可能很有用。例如，防御这种攻击的一种可能方法是进行更集中的对抗性训练;用更多的输入来重新训练网络，这些输入沿着相同的路径通过网络
# 相关工作
最近与我们同时进行的独立工作提出了深度神经网络的共结测试[31]。
然而，他们的焦点是定义和实现测试覆盖需求，尽管他们的方法也会产生对抗的图像。相反，我们使用符号执行来识别重要像素和特定的1像素和2像素攻击，其目标是与原始图像相同的激活模式;此外，我们使用重要的像素来集中搜索可攻击的像素。
其他相关的近期技术包括深度神经网络的形式化方法[16]，[17]和测试[26]，[34]。
然而，之前的工作都没有使用正式的方法来识别重要的像素，或者更一般地说，用于神经网络的可解释性。此外，它们不会检查相同激活模式下的攻击。
在我们的工作中，我们使用Z3作为现成的约束求解器，我们从软件分析工具[25]继承了它。
我们注意到，在我们的分析中可以插入其他约束求解器。例如，一个很好的选择是Reluplex[16]，[17]，它专门针对ReLU激活的神经网络分析进行了优化。然而，我们的方法是通用的，原则上可以应用于其他具有线性单元的网络，如卷积神经网络，这不能由Reluplex处理。另一种选择是使用线性规划，如[31]，因为对于固定的激活模式，要解决的问题是线性的。然而，当不存在解时，线性求解器可能会表现出意想不到的行为，并且由于溢出可能会给出不可靠的结果[35]。
据我们所知，现有的测试、正式验证和归因方法尚未应用于文本模型。本节的其余部分描述了神经网络中与归因或可解释性相关的现有技术，以及对抗示例生成的现有技术。
# A.归因技巧
尽管神经网络被广泛采用，但大多数深度神经网络分类器都是黑盒子。为了在模型中建立信任，理解这些分类器预测背后的原因是至关重要的。因此，在为预测生成解释的领域已经探索了许多技术。归因是一类特定的方法，主要适用于图像分类应用，其中该技术试图为每个输入特征或像素分配“相关性”，“贡献”，以进行分类决策。我们在下面描述归因方法的大类。
基于扰动的方法将每个输入特征的值单独改变一定数量[37]，在输入上重新运行网络，然后测量输出值的差异。然而，这些技术往往很慢，计算时间随着特征数量的增加而增加。
基于梯度的方法[28])在给定的输入上计算网络的单个向前和向后传递中每个特征的属性。他们计算每个输入变量的输出的有符号偏导数，并将其乘以输入值，以确定该变量对输出的影响。Integrated-gradients[32]提出了一种方法，从基线(用户自定义)到给定输入，沿线性路径计算属性的平均值。
显著性图[29]考虑每个输入变量的输出偏导数w.r.t的绝对值，以便识别受干扰最小的像素，以观察输出值的可观变化。
# B.对抗性攻击生成技术
据观察，最先进的网络极易受到对抗性扰动的影响:给定一个正确分类的输入x，有可能找到一个与x非常相似的新输入x 0，但被分配了不同的标签[33]。Goodfellow等人[14]引入了快速梯度符号法(Fast Gradient Sign Method)，利用模型损失函数相对于输入特征向量的导数来制作对抗性扰动。
他们表明，为MNIST和CIFAR-10分类任务训练的神经网络可以以很高的成功率被愚弄。
该方法的扩展以迭代的方式应用该技术[11]。基于jacobian的Saliency Map Attack (JSMA)[24]提出了一种针对目标错误分类的方法，该方法利用神经网络的正导数来寻找一个对抗的扰动，该扰动将迫使模型错误分类到特定的目标类别。Carlini等人[5]最近提出了一种无法被最先进的网络(如使用防御性蒸馏的网络)所抵制的方法。
他们的优化算法使用更好的损失函数和参数(经验确定)，并使用三种不同的距离度量。
DeepFool[23]技术通过考虑网络是完全线性的来简化域。它们计算分类器函数上一个点的切平面(正交投影)上的对抗性输入。然后，他们将非线性引入模型，并重复此过程，直到找到了一个真正的对抗性例子。深度学习验证(Deep Learning Verification, DLV)[16]是一种围绕已知输入定义安全区域并应用SMT求解来检查鲁棒性的方法。他们认为输入空间是离散的，并使用操作来改变输入，直到它与原始输入的距离最小，以产生可能的对抗性输入。DeepSafe[15]是一种首先在已知标签的输入上应用标签引导聚类算法来识别可以被一致标记的输入区域的方法。然后使用Reluplex求解器[17]来验证给定区域内所有可能的输入是否被网络分配了相同的标签。DeepRoad[38]介绍了一种基于dnn本身的无监督学习技术，用于验证基于dnn的自动驾驶驾驶员。
# 总结
我们描述了一种用于分析神经网络的符号执行方法。提出了两个分析:1)识别可以解释神经网络分类决策的重要输入;2)在重要输入的指导下，通过约束求解来创建攻击。这两种分析协同应用，并提供了一种更可扩展的方法来查找攻击。使用MNIST模型和文本模型的实验评估表明了该方法的有效性。对于未来，我们计划在具有更高准确性的更大网络上评估我们的技术;我们正在努力优化我们的工具来实现这一目标。