反馈控制器中的传感器欺骗攻击的相变及安全性保护

可在www.sciencedirect.com在线获取理论计算机科学电子笔记317（2015）141-153www.elsevier.com/locate/entcs攻击反馈控制器Ashish Tiwari Ashish Tiwari1，2计算机科学实验室美国门洛帕克摘要我们考虑在反馈控制器上生成传感器欺骗攻击的问题。 攻击者具有选择保持在隐形模式-其中它欺骗一些传感器，但只有一个量，与噪音无法区分。之后，攻击者可以发起全面攻击，试图迫使系统进入一个不安全的区域。使用有界模型检查的一个例子自适应巡航控制器，我们表明，（1）保持在一个隐形模式是不是很有利的攻击，（2）有两类攻击之间的相变：攻击是小，难以区分，但不能使系统本身不安全，以及大规模的攻击，并且可能容易被检测到，但是容易使系统处于不安全状态。初步实验表明，控制系统是最脆弱的时候，它只是从事（在离散开关）。此外，如果使用基于安全包络的监视器进行保护，并且可以忽略安全包络之外的传感器数据，则仅通过传感器欺骗来损害这种控制系统的安全性保留字：有界模型检验，反馈控制，传感器欺骗，安全性1介绍控制系统由传感器、控制器和执行器组成。传感器收集有关系统状态的数据。控制器使用传感器数据来计算适当的控制措施。然后，致动器执行控制动作，从而检测系统状态的变化，然后在下一个循环中再次由传感器感测到。在这样的反馈系统中，控制器依赖于传感器来提供高质量的数据，以确保系统即使在不确定的环境中也能正确和安全地运行。我们不断地将这种控制系统嵌入到更大的网络物理系统中，这些系统与外部世界的联系越来越因此，在本发明中，1这项工作由国防高级研究计划局（DARPA）和空军研究实验室（AFRL）根据合同FA 8750 -12-C-0284和国家科学基金会赞助。在CNS-1423298号资助下进行。 本报告所载的观点、意见及╱或发现乃以下人士的观点、意见及╱或发现：作者不应被解释为代表资助机构的官方观点或政策，无论是明示的还是暗示的。2电子邮件：tiwari@csl.sri.comhttp://dx.doi.org/10.1016/j.entcs.2015.10.0141571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。142A. Tiwari/理论计算机科学电子笔记317（2015）141攻击面正在迅速增长，欺骗传感器并将错误数据注入系统并不困难有已知的GPS欺骗攻击无人机的实例[1]。现代汽车也被证明有几个攻击面，攻击者可以利用这些攻击面来破坏汽车内的计算机/网络，并注入传感器欺骗攻击[5，2]。提高任何系统安全性的一种方法是消除攻击媒介。这是一场艰苦的战斗，因为系统越来越多地与其他设备连接并广泛通信在这里，我们认为完全消除所有攻击面将是困难的，并且不可避免地，总会有一些渠道可供攻击者利用。我们还假设可以执行异常检测并构建一种可以用来检测攻击的安全监视器。具体来说，可以计算系统标称运行的安全包络，然后在运行时监控系统是否保持在安全包络内[13]。在这样的设置中，向控制器发送“野生”传感器读数的传感器欺骗攻击攻击者只需稍微改变传感器的值就可以了。这样，攻击者就可以保持不被察觉，并使系统在发动全面攻击之前达到某种中间状态。这样的策略对攻击者有帮助吗？是否有好的偏差值供攻击者使用这些问题构成了本文研究的出发点我们的目标是在存在运行时监视器的情况下分析传感器欺骗攻击策略。我们的方法是基于使用正式的验证工具的控制器模型的自适应巡航控制。具体地说，我们建立了一个模型，两辆车在一维道路上移动，后方车辆控制器的目标是确保后车永远不会撞上前车。 我们假设攻击者可以欺骗后车的速度传感器我们创建系统模型的时间关系抽象，然后使用有限有界模型检查来回答上面提出的一些问题。我们在第2节中形式化了感兴趣的问题，我们在第3节中给出了我们的实验结果，此后，在第4节中，我们给出了我们的实验设置的细节。1.1相关工作近年来，人们对对抗性攻击下的控制系统和网络物理系统的在攻击恢复状态估计方面有相当多的工作，因为如果我们可以确定正确的状态（即使在存在攻击的情况下），那么系统的其余部分可以不变地使用，因为它只依赖于估计的状态[4，9，7，8]。对于线性系统，存在攻击的状态估计问题可以转换为优化问题[4，9]。Fawzi等人[4]假设存在冗余传感器，并提供理论上的保证，可以处理的攻击的最大数量。推广[4]中的工作，A. Tiwari/理论计算机科学电子笔记317（2015）141143在[7]中提出了攻击恢复状态估计过程，该过程也处理噪声和建模误差的存在。它表明，攻击者不能利用用于状态估计的模型和真实的物理系统之间的差异，使系统不在[6]中提出了一种用于对传感器输出进行编码以使得能够检测错误数据注入攻击假设传感器本身没有受到损害，[6]中的结果是传感器数据加密的低成本替代方案。这两种解决方案然而，仍然值得研究隐形攻击的后果。首先，弹性状态估计可能不可用，因为例如在系统中具有冗余传感器其次，用于编码传感器输出的算法在这种情况下，本文提出并部分回答的问题就变得相关了。2问题描述我们假设我们有一个被控制器控制的工厂。植物动力学由下式给出：d→x（一）=P（→x，→u）DT其中→x是平面的状态空间，→u是控制输入。 （执行器动力学包括在植物动力学中）。反馈控制器用于如下从传感器读数^y产生v a lues ^u。（2）→u=C（→y）C是一个函数。传感器值→y是当前状态的函数S当对传感器a_tta_k进行建模时，函数S可以包括a_tta_k模型。（3）→y=S（→x）通过将上述三个方程组合在一起，我们得到了一个受攻击的反馈控制系统的模型。让Sys表示该模型。当满足状态空间上的某些条件时，所研究的控制器被激活（或接合）。让Init表示这些条件。（4）初始化|→x|系统在集合Init中的某个初始状态下启动，然后生成一个根据等式1、等式2和等式3来执行跟踪。 通过稍微滥用符号，让Sys也表示将由传感器模型S、初始状态x→0和时间实例t组成的元组映射到在时间t处达到的状态的函数。（5）Sys（S，x→0，t）∈R|→x|函数Sys是系统的语义。系统被期望保持在某个安全的状态集内。设Safe表示安全集。144A. Tiwari/理论计算机科学电子笔记317（2015）141⎨⎨因此，等式7将采用以下形式：⎩（6）安全防护|→x|理想情况下，对于所有的初始状态x→0∈，对于所有的时间t≥0，我们设Sys（S，x→0，t）∈Init，并且对于所有合理的传感器攻击S。2.1传感器攻击让我们更具体地假设所有的工厂状态变量-X可以被感测（通过不同的传感器）。因此，当没有atta ck时，上面的函数S将只是恒等函数。为了简单起见，我们还假设攻击者只是通过从一个范围中选择的某个常数来设置传感器的值。因此，在这两个假设下，等式3采用以下形式：（7）→y=→x+→c→c∈D其中DRn是攻击域。 如果攻击者有能力欺骗单个传感器，那么D将包含只有一个非零条目的向量我们假设攻击以两种模式进行：隐形模式和明显模式。在隐身模式下，由攻击者引入的传感器值中的o值集在明显的模式下，这个o的集合要大得多。直觉上，攻击者试图在隐身模式下保持不被检测到，因此攻击者不会大量偏离正确的传感器值。现在，等式3采用以下形式：（八）→y=Sstealth（→x）ifit ea lthmod e证明t（→x）if in ev id ent模型（九）→y=n→x+→c→c∈D隐身，如果在隐身模式下→x+→c→c∈Devidentifineviddentmode假设恰好有一个传感器，比如对应于索引1的传感器，受到攻击 让我们确定攻击的领域。(10) D隐形={→c||C1| ≤stbound，ci=0或i=1}D明显={→c||C1| ≤evbound，ci=0或fi=1}这里，stbound和evbound是两个参数，使得stboundevbound。<我们还假设攻击者在隐身模式下停留t隐身时间，然后切换到明显模式。让ttoAttack表示攻击者在明显模式下将系统推入不安全状态所花费的时间(11) ttoAttack=i nf{t|Sys（Seviden t，x→1，t）/∈安全，x→1=Sys（Sstealth，x→0，tstealth），x→0∈Init}目的：研究stbound、evbound、t隐身等参数对攻击值t的影响。注2.1考虑攻击的一般性虽然我们说攻击者只是通过某个常数c来设置某个传感器的值，但是这个常数可以改变。A. Tiwari/理论计算机科学电子笔记317（2015）141145随着时间的推移 唯一的限制是c保持在攻击域D内。 因此，我们确实考虑了相当普遍的攻击形式注2.2安全监视器：安全监视器以隐形攻击定义的形式隐含在上述公式更准确地说，我们假设安全监视器在运行时检查传感器输出与预期传感器值之间的差异是否最大为stbound。因此，在隐身模式下，攻击者最多可以将传感器值更改（受损）stbound：如果攻击者更改的值超过该范围，则安全监视器将检测到攻击并采取纠正措施。备注2.3噪声：stbound值反映了传感器输出中存在噪声的事实我们将选择值stbound来保证，如果传感器输出中的误差由stbound限制，则系统保持安全。因此，先验地保证了攻击者不能通过总是处于隐身模式而3主要结果我们推迟到以后详细描述工厂和控制器。我们首先介绍了实验和实验结果。3.1无隐身模式我们首先考虑攻击者在隐身模式下花费的时间为零的情况，即tstealth=0。在图1中，我们绘制了到达不安全状态ttoAttack所需的时间（在y轴上）与明显攻击evbound的强度（在x轴上）。正如预期的那样，图1显示了达到不安全状态所需的时间随着我们增加可用于对受损传感器的值进行强制设置的值范围而减少请注意，在急剧下跌的情节后面是逐渐下降.在evbound = 2。1，攻击未能将系统带入不安全状态，并且evbound = 2。2，系统在短短6秒内被攻破 随着evbound从2增加，t toAttack值的下降更加平缓。2比6 5.如果针对该控制系统实施基于安全包线的监控方法，则值为2。1将是定义安全信封的好选择控制器能够确保传感器值偏差小于2的安全性。1;安全监视器可以“丢弃”超过2的传感器值。1.这样的安全监视器几乎可以保证系统的安全操作。 实际上，根据备注2.2和备注2.3，我们将选择stbound小于或等于2。我们做两个评论，适用于本文的所有情节。首先，ttoAttack的值不是连续变化的第二，数值24被用来代替任何大于24的数字，包括∞。146A. Tiwari/理论计算机科学电子笔记317（2015）1412520151050电话：+86-21 - 6555555传真：+86-21 - 6555555攻击强度，evbound图1.一、达到不安全状态t to Attack所 用 的 时 间 （在y轴上）与明显攻击的强度相比较evbound（在x轴上）。没有隐形模式。 当我们增加evbound时，ttoAttack的值减小。25201510500 5 10 15 20隐身时间，t隐身（秒）图二. 在明显模式下达到不安全状态所花费的时间（y轴，以秒为单位）与在隐身模式下所花费的时间（x轴，以秒为单位）绘制。当我们增加隐身时间时，将系统带入不安全区域将变得越来越困难。在这里，攻击者在隐身模式下不活动3.2攻击者隐形模式对于第二组结果，我们考虑了攻击者花费在隐身模式下的非零时间量（tstealth0），但攻击者不在隐身模式下更改传感器值（stbound=0）。对于这种情况，在图2中，我们绘制了到达不安全状态所需的时间ttoAttack（在y轴上）与隐身模式所需evbound=2.8evbound=2.7evbound=2.6evbound=2.55evbound= 2.54，2.53到达不安全状态的时间，t到攻击（秒）到达不安全状态的额外时间，tto Attack（秒）A. Tiwari/理论计算机科学电子笔记317（2015）141147的时间tstealth（在x轴上）。 我们在图中有一条线，146A. Tiwari/理论计算机科学电子笔记317（2015）1412525201510500 5 10 15 20隐身时间，t隐身（秒）图三. 在明显模式下达到不安全状态所花费的时间（y轴，以秒为单位）与在隐身模式下所花费的时间（x轴，以秒为单位）绘制。随着隐形时间的增加使系统进入不安全区域的困难。在这里，攻击者在隐身模式下是活跃的，但在传感器输出中仅明显攻击的强度估计值随着我们在隐身模式下花费的时间增加，在明显模式下达到不安全状态所需的时间也会增加。这与人们所期望的相匹配，因为在这里，在隐形模式下，我们有stbound= 0，因此系统不是直到隐形时间。因此，在t隐身单位的时间后，当控制器被占用时，控制器能够将系统带入值得将图2中的结果与图1中的结果进行比较。 当攻击者可以在控制器被占用时立即开始攻击时，值为2。2或更高的evbound值足以让攻击者在6秒内使系统进入不安全状态（图1）。但是，如果攻击者在开始攻击时晚了2秒（并且控制器只有2秒的“未被攻击”时间），则需要evbound的值大于2。6，使系统在6秒内进入不安全反馈控制器对攻击的容忍度随时间而增加。3.3隐身模式下的攻击者保守对于第三组结果，我们考虑了攻击者花费在隐身模式中的非零时间量（tstealth0），并且攻击者启动一个对于这种情况，在图3中，我们绘制了到达不安全状态所花费的时间ttoAttack（在y轴上）与隐身模式所花费的时间tstealth（在x轴上）。我们在图中为明显攻击的强度evboundevbound=2.8evbound=2.7evbound=2.6evbound=2.55evbound= 2.54，2.53到达不安全状态的额外时间，tto Attack（秒）A. Tiwari/理论计算机科学电子笔记317（2015）141149201510500 5 10 15 20隐身时间，t隐身（秒）见图4。 在明显模式下达到不安全状态所花费的时间（y轴，以秒为单位）与在隐身模式下所花费的时间（x轴，以秒为单位）绘制。随着隐形时间的增加使系统进入不安全区域的困难。这里，攻击者在隐身模式下是活跃的，并且在传感器输出中引入人们会期望攻击者可以利用在隐形模式中花费的时间将系统驱动到一种状态，在该状态下，它可以快速地迫使系统进入明显模式中的不安全状态。也就是说，我们期望ttoAttack随着tstealth的增加而减少，假设其他两个参数stbound和evbound保持不变。然而，图3中的曲线图显示了相反的情况。这表明攻击者无法通过增加t隐身来减少t toAttack。相反，ttoAttack随着tstealth的增加而增加，与攻击者在stealth模式下保持沉默时的情况大致相同（图2）。在某种意义上，反馈控制器能够保持参数evbound和tstealth固定不变，我们现在比较ttoAttack的变化和stbound的变化。为此，我们需要比较图3（攻击者在隐身模式下做了一些事情，stbound= 1）和图2（攻击者在隐身模式下什么也没做，stbound=0）。我们注意到，当stbound= 1时，ttoAttack的值不大于当stbound= 0时ttoAttack的值;在许多情况下，它略小。3.4潜行模式下攻击者不小心对于最终的结果集，我们考虑了攻击者花费在隐身模式中的非零时间量（tstealth0），并且攻击者启动一个对于这种情况，在图4中，我们绘制了到达不安全状态所花费的时间ttoAttack（在y轴上）与隐身模式所花费的时间tstealth（在x轴上）。我们在图中为明显攻击的强度evboundevbound=2.8evbound=2.7evbound=2.6evbound=2.55evbound= 2.54，2.53到达不安全状态的额外时间，tto Attack（秒）148A. Tiwari/理论计算机科学电子笔记317（2015）14125FL在这种情况下，我们确实得到了有趣的行为，其中ttoAttack减少为t隐身增加。 具体地说，当stbound= 2且evbound是{2。53，2。54，2。六二七二8}，我们观察到tto Attack随着tstealth的增加而减少从2到4。在这种情况下，攻击者确实可以通过保持隐身模式而受益。然而，对于所有小于4的tstealth值，ttoAttack随着tstealth的增加而增加，因此只有一个很小的窗口，攻击者可以从隐身模式中受益。我们再次注意到，比较图3和图4，增加stbound会导致ttoAttack减少，从stbound= 1到stbound= 2，ttoAttack请注意，值stbound = 2，我们开始从隐形模式中获益，接近安全包络的“边缘”，由值2定义。1从图1中的图。4巡航控制器我们现在简要介绍我们用于执行上述实验的模型如前所述，我们使用[10]中的自适应巡航控制器模型状态变量是gap，vf，vl，af，al，其中gap表示领导者（下标l）和跟随者（下标f）之间的间隙，vf，af是跟随者的速度和加速度，vl，al是领导者的速度和加速度。工厂模型很简单：三维间隙(12)(13)dt=vl−vfdvl=a(14)DTLdvf=adtf(15)daf=udt变量al是一个输入（扰动），但假设al被限制在−5m/s2和2m/s2之间。速度vl，vf总是非负的。变量u是控制器的输出。控制器设置变量u如下[10]：u=−3af− 3（vf−vl）+gap−（vf+10）当以下条件成立时，控制器被占用;换句话说，以下是初始状态的设置Init[10]。gap ≥5，0 ≤ v l，v f≤ 30，gap − 0。1（v2−v2）−10−（vf−vi）≥0由于在上面的第三个表达式中存在非线性项，在我们的分析中，我们在约束0≤vl，vf≤ 30下使用了它的线性欠近似（vf≥vl）gap− 10 −（vf−vl）− 0。1<$（vf−vl）< $60≥0）<$（vf≤vl<$gap− 10−（vf−vl）≥0）150A. Tiwari/理论计算机科学电子笔记317（2015）141安全状态集由约束间隙≥0定义4.1传感器攻击我们假设跟车的速度传感器可以被欺骗。因此，控制器不是看到速度vf，而是从传感器获得值vf+attack。结果，控制器实际上计算以下控制输出：u=−3ai−3（vf−vl）+gap−（vf+10）−4攻击在隐形模式下，变量攻击的值被约束为介于- stbound和stbound。在明显模式下，变量attack的值被限制在−evbound和evbound之间。我们在HybridSal中对完整系统进行建模[12]。该模型有两种模式。在模型中，我们还有一个参数tstealth，模型在时间tstealth内保持在stealth模式。完整的HybridSal模型见附录。4.2抽象和有界模型检验我们使用HybridSal支持的两步验证过程生成了第3节所示图的数据第一步，将模型抽象为一个无限状态的离散状态转移系统。第二步，对抽象模型进行模型检查。由于我们感兴趣的是发现攻击和将系统带到不安全状态所需的时间，因此我们使用HybridSal来创建系统的时间关系抽象[14给定一个持续时间Δ，一个时间关系抽象由一个转换关系组成，如果第二个状态可以在Δ时间单位内从第一个状态到达，则该转换关系将两个状态联系起来。使用它们的好处是它们是精确的：相对精确的时间关系抽象由HybridSal计算。另一方面，缺点是，如果每条路径的持续时间不是Δ的整数倍，则我们可能会错过检测到不安全状态的路径。对于我们在第3节中报告的结果，我们使用Δ = 2，这就是为什么tstealth和tto attack都是2的倍数抽象系统使用SAL无限有界模型检查器进行模型检查[3]。有界模型检查器使用Yices作为其约束求解器[11]。在我们的实验中，我们使用Δ =2，并且tstealth+ttoAttack大多数最多为40，因此大多数有界检查运行使用的深度小于或等于20。这些运行中只有少数几次花费了超过几分钟的实时时间。备注4.1受攻击传感器的选择：受攻击传感器的选择对我们的结果无关紧要。例如，如果gap的传感器受损（而不是vf的传感器），那么我们将获得相同的结果，但stbound和evbound的值中有一个常数因子。注4.2推广：我们的观察是基于对特殊反馈控制器的分析当然，我们可以使用相同的工具来执行类似的操作，A. Tiwari/理论计算机科学电子笔记317（2015）141151对其他系统的研究：事实上，HybridSal可以对更一般的混合动力系统建模，从而对模式切换和具有有限存储器的控制器建模。此外，在理论上（更一般地）进行类似的探索应该是可能的。直觉上，我们希望我们会得到类似的结果。5结论我们研究了反馈控制系统中的传感器欺骗问题我们假设一个场景，其中控制系统由运行时监视器主动保护，该监视器拒绝表面上虚假的传感器值。在我们的模型中，攻击者可以选择保持隐身模式，并在发动全面攻击之前对传感器值发动轻微攻击。我们使用巡航控制器的形式化模型、抽象和有界模型检查来发现不同参数与攻击存在之间的关系。主要结论是，反馈控制器是最敏感的，在一个短的时间窗口后不久，它被占用-即在监督控制器的离散开关处。此外，隐身模式下的弱攻击对攻击者没有太大帮助，因为反馈控制器能够处理它们（因为它处理噪声）。隐身模式下的强大攻击可以通过减少明显模式下达到不安全状态所需的时间来帮助攻击者，但即使在隐身模式下，它们也使攻击者更容易被检测到。引用[1] 维基百科，自由的百科全书。en.wikipedia.org/wiki/Iran-U.S._ RQ-170事件[2] S. Checkoway，D.麦考伊湾Kantor，D.Anderson，H.Shacham，S.萨维奇，K。Koscher，A.C. 安，F. Roesner和T. 科诺汽车攻击面的综合实验分析。在USENIX Security，2011年。[3] L. de Escherichia，S.奥雷Ruewald，J.Rushby，N.尚卡尔，M。Sorea和A.蒂瓦里Sal 2.In R.和D. Peled，编辑，计算机辅助验证，CAV，LNCS第3114卷，第496-500页。Springer，2004年7月。[4] H. Fawzi，P. Tabuada，and S. N.迪格维信息物理系统的安全评估与控制 在敌对的攻击下。IEEE自动变速器- 是的，59（6）：1454[5] K. Koscher，A.Czeskis，F.Roesner，S.Patel，T.Kohno，S.Checkoway，D.麦考伊湾坎特，D. Anderson，H. Shacham和S. 野人 现代汽车的安全性试验分析。在IEEE研讨会论文集和安全与隐私，奥克兰，CA，2010年。[6] F.苗湾，澳-地Zhu，M. Pajic和G. J·帕帕斯 编码传感器输出用于注入攻击检测。第53届IEEE决策与控制会议（CDC），2014年。[7] M. Pajic，J. Weimer，N. Bezzo，P. Tabuada，O.索科尔斯基岛Lee和G. J·帕帕斯抗攻击状态估计器的鲁棒性。2014年第五届ACM/IEEE网络物理系统国际会议（ICCPS）[8] 帕克河作者：J.帕吉克和我。李你瞬时故障情况下的传感器攻击检测。2015年第六届ACM/IEEE网络物理系统国际会议（ICCPS）[9] F. Pasqualetti，F. Dor Der和F.布洛 网络物理系统中的攻击检测和识别。IEEE自动控制学报，58（11）：2715[10] A. Puri和P. Varaiya。安全驾驶智能汽车1995年美国控制会议论文集，1995年。152A. Tiwari/理论计算机科学电子笔记317（2015）141[11] SRI International. Yices：SMT求解器。 http://yices.csl.sri.com/。[12] A. 蒂 瓦 里 混 合 关 系 抽 象 器 。 在 procCAV ， LNCS第 7358 卷 ， 2012 年 。 http ： //www.csl.sri.com/ ~ tiwari/relational-abstraction/.[13] A.蒂瓦里湾Dutertre，D.约万诺维奇，T。作者声明：John M. Rushby，D. Sadigh和S. A.塞希亚安全信封。在第三届高置信度网络系统国际会议（CPS周的一部分），HiCoNSACM，2014年。[14] A. Zutshi，S. Sankaranarayanan和A.蒂瓦里采样数据控制系统的时间关系抽象。 在proc CAV，LNCS的第7358卷，第343 - 361页，2012年。一种HybridSal模型为了完整性，我们在这里包括HybridSal模型PVAtt：上下文=开始tstealth：REAL=4;隐身模式下的时间stbound：REAL =2;隐身模式下的攻击范围%evbound：REAL =2.8; 明显模式下的攻击范围%DeltaT：REAL =2;观察的采样周期 %控制：MOST = BEGIN时间间隔，vf，vl，af，时间：真实输入al，攻击：真实初始化return 0;afIN {x：REAL|-5< = x AND x< =2};vf IN{x ： REAL|0< = x AND x< =30}; vlIN{x：REAL|0< = x AND x< =30};间隙IN{x：REAL |05- 05 - 05 - 05（（vf>=vlANDx-10-（vf-vl）-0.1*（vf-vl）* 60 >=0） OR（vf<=vl ANDx-10- （vf-vl）-0.1*（vf-vl）* 0 >=0））};过渡期[vl>=0 ANDal>=-5 ANDal =2 AND vltimetstealthAND timeafdotgapdot[]vl>=0 ANDal>=-5 ANDal =2 AND vlA. Tiwari/理论计算机科学电子笔记317（2015）141153攻击<= evboundAND攻击>=-evbound AND时间>=tstealth-->afdotgapdot]END;正确：定理控制|-G（间隙>= 0或vf <= vl）;端