基于运行时验证的边缘服务器DoS 攻击检测方法

于斌，张南，陆旭，段振华，田聪

（西安电子科技大学计算机科学与技术学院，陕西 西安 710071）

1 引言

边缘计算系统利用终端设备及终端附近的边缘服务器的计算和存储资源，提前对数据进行部分处理，减少要发送到云数据中心的数据量，从而减少网络带宽使用量，并使系统能够在较低数据时延的情况下立即响应数据[1]。边缘计算系统总体框架如图1 所示。在边缘计算系统中，边缘服务器处于整个系统的中间层，起到连接云服务器和终端设备的作用，并承担云服务器的部分计算任务。随着服务器性能的不断提升，越来越多的数据处理任务依托边缘服务器来完成。

图1 边缘计算系统总体框架

然而，边缘服务器的特点使其面临新的挑战[2-5]。首先，边缘服务器常位于网络边缘，面临更复杂的网络环境。此外，边缘服务器往往是地理分布式的，难以做到集中的设备安全保护，且每个边缘服务器是不同的，此差异性给攻击者带来了更多的可选择性。更严重的是，由于计算能力和存储空间的限制，大多数边缘服务器只关注业务逻辑的实现，而对可能受到的攻击缺少防范和检测。由以上分析可知，虽然边缘服务器在边缘计算中发挥重要作用，但其易攻击的特征使其面临严峻的攻击威胁。

由于边缘服务器的计算和存储资源受限，极易被耗尽，因此，在边缘计算系统面临的多种攻击中，针对边缘服务器的拒绝服务（DoS,denial of service）攻击很广泛[6-10]。在DoS 攻击中，恶意节点通过无限制地访问指定的被攻击边缘服务器，向其发送大量的无效数据包，耗尽正在运行的服务器资源，阻碍边缘服务器的正常运行。由于在边缘计算架构中，边缘服务器用于实现数据的部分处理以及数据与云服务器的传输，一旦边缘服务器的通信链路堵塞或资源被耗尽，将直接造成预期的正常业务无法完成。

作为保障网络安全的一种重要手段，入侵检测能够实时监测网络活动，判断设备状态，及时发现DoS 中的受攻击设备，主要包括异常检测和误用检测2 种方法。其中，异常检测方法基于被监控对象的正常行为，其假设入侵是与正常行为必然不同的异常，因此，任何明显偏离正常的行为都被认为是侵入性的；误用检测对正在监视的事件进行匹配，符合已知攻击特征的操作均被视为入侵行为。在现有针对边缘计算系统的入侵检测方法中，大部分方法利用模式识别或机器学习手段[11-18]，虽然能够取得较好的检测结果，但需提前训练模型，在基于训练好的模型进行实时检测时需占用较大内存。与之对应，以模型检测和运行时验证为代表的形式化验证方法利用时序逻辑性质，对网络入侵的行为特征进行识别，不需要提前训练模型，但由于需要构造自动机等理论模型，检测效率往往不高，虽然在云计算等传统网络中得到应用[19-24]，但在边缘计算系统中的研究仍处于初步阶段。

鉴于边缘计算系统中边缘服务器的重要性和易攻击性，以及面向边缘服务器DoS 攻击的广泛性和威胁的严重性，如何构建一个高效准确的入侵检测方法，是一个亟待解决的重要问题。作为轻量级形式化验证方法，运行时验证能够监视和分析真实系统的执行情况，以检查系统的运行轨迹是否满足形式化描述的属性，已逐渐被用于网络入侵检测中[19-20]。在边缘计算系统中，由于边缘服务器需要保持运行状态，不断响应终端设备的服务请求并完成期望的逻辑功能，因此，对其进行运行时验证是必要和可行的。

考虑到边缘服务器具有较强的计算能力，本文采用运行时验证方法对DoS 攻击进行检测。为了充分利用边缘服务器计算资源以提高验证效率，解决目前运行时验证方法中线性时序逻辑[25]和计算树逻辑[26]表达能力不足的问题，本文结合误用检测和异常检测，提出基于命题投影时序逻辑（PPTL,propositional projection temporal logic）[27-29]的并行运行时验证方法。首先，基于统一建模语言（UML,unified modeling language）顺序图，使用PPTL 公式描述系统正常状态下的行为特征；然后，使用PPTL 公式描述DoS 攻击中针对TCP/IP 协议族最常见的Smurf 攻击、SYN Flood（synchronize flood）攻击以及Land 攻击的行为特征；进而，将上述两类PPTL 公式作为待验证性质，在边缘计算系统运行过程中，在边缘服务器上部署PPTL 公式的运行时验证方法，基于搜集到的信息，利用边缘服务器的多个线程，共同完成DoS 攻击的入侵检测。在此过程中，若发现第一类性质不满足，则表明边缘服务器无法完成正常的请求响应；若发现第二类性质中某性质满足，则表明检测到某一特定类别的DoS 攻击。最后，为了检验上述方法的有效性，本文进行了性能对比实验，并对一个实际的基于边缘计算的点对点（P2P,peer-to-peer）网络智能停车系统进行针对边缘服务器的模拟DoS 攻击和攻击检测，实验结果表明，所提方法能够有效检测出边缘服务器的异常行为和所受DoS 攻击类型。

本文贡献主要包括以下三方面。

1) 采用PPTL 公式描述基于UML 顺序图的边缘服务器正常行为特征和不同DoS 攻击下边缘服务器的异常行为特征，其中，PPTL 具有完全正则的表达能力，可直接用于描述边缘服务器上不同模块调用的区间相关与周期重复的性质。

2) 基于PPTL 性质描述，采用运行时验证方法对边缘服务器进行实时监控，实现异常检测和误用检测，在此过程中，基于并行运行时验证框架，充分利用边缘服务器的空闲计算与存储资源，提高验证效率，及时发现攻击。

3) 将所提运行时验证方法部署在实际智能停车系统，对其进行边缘服务器监控，实验结果表明，边缘计算系统中的DoS 攻击能够被有效识别。

2 相关理论

2.1 命题投影时序逻辑

PPTL 公式P归纳定义为

其中，Prop 为一个可数的原子命题集合，p∈Prop表示原子命题，P1,…,Pm和P是PPTL 公式。PPTL的语义已在文献[27-29]中明确给出。PPTL 派生的时态公式为

任何PPTL 公式都能够转换为对应的范式[29]，基于范式，能够构造出其对应的带标签的范式图（LNFG,labeled normal form graph）。LNFG 中的有穷路径π=＜n0,p0,…,ε＞是从初始节点到ε节点的节点和边的交替序列，其一定是可接收的。无穷路径π=＜n0,p0,…,(ni,pi,…,nj,pj)ω＞是节点和边的无穷交替序列，若路径上无限出现的节点的集合（用Inf(π)表示）不存在被所有节点同时拥有的标签，则该路径是可接收的。

图2 展示了PPTL 公式◇(p∧□(¬q))对应的LNFG，图中每个节点代表一个PPTL 公式；每条边为一个状态公式；额外引入的命题lk用于识别一条路径是否为可接收的。例如，有穷路径π1=＜1,p∧¬q,3,¬q,4＞为可接收路径；对于无穷路径π2=＜1,true,(2,true)ω＞，由于Inf(π2)={2}⊆L1={2}，意味着无穷循环的节点拥有相同的标记l1，因此这条路径是不可接收的。

图2 PPTL 公式◇(p∧□(¬q))对应的LNFG

2.2 传统运行时验证方法

对于待验证程序M，若采用传统的运行时验证方法验证其是否满足期望的PPTL 性质P，需要首先对程序M进行插桩，并构建¬P对应的LNFGG；然后，在插桩后的程序M执行过程中，每个状态上出现在P中的变量的值被记录下来，基于这些变量的值，可以得到G中对应边上的状态公式的真值；进而，探索G中的可接收路径，若能够在G中发现一条可接收路径，则表明程序的当前执行路径不满足性质P；若不存在可接收路径，则表明程序的当前执行路径满足性质P。

图3 中的例子展示了传统运行时验证方法面临的挑战。图3(a)展示了一个程序执行产生的状态序列，共包含 4 个状态。假设待验证的性质为□(p→◇q)，其中原子命题p和q分别代表x＜=3 和y＞5。性质□(p→◇q)的非，即◇(p∧□(¬q))的LNFGG如图2 所示。当程序执行时，G中的路径探索结果如图3(b)所示，图3 中的节点编号与图2 中的节点编号保持一致。由于在G中存在多条从节点1 和节点2 出发的边，在图3(b)的前3 步中，越来越多的路径产生。由于性质对应的LNFG 中路径的探索过程相当于程序解释执行的过程，其速度原本就远小于程序编译后生成状态的速度，再加上LNFG 中不断产生分支，因此在传统的运行时验证方法中，串行的验证方法限制了验证效率的提高。

图3 传统运行时验证方法面临的挑战

3 DoS 攻击检测方法

为了有效检测针对边缘服务器的DoS 攻击，本文提出基于运行时验证的入侵检测方法，该方法可部署在需要监控的边缘服务器上，在边缘服务器提供服务的同时，实现针对边缘服务器的异常检测和误用检测。在检测过程中，为了充分利用边缘服务器的计算和存储资源，本文提出了基于多线程的并行运行时验证框架，以提高入侵检测效率，及时发现攻击的存在。攻击检测示意如图4 所示。

图4 攻击检测示意

在性质描述方面，本文采用与完全正则式表达能力相同的PPTL 公式，其能够直接表达区间相关和周期重复的性质。为了提供异常检测所需性质，针对UML 顺序图中表达的模块之间函数调用关系，使用PPTL 公式描述正常情况下不同函数的执行序列；为了提供误用检测所需性质，针对不同DoS 攻击的行为特征进行分析，并使用PPTL 公式形式化描述此行为特征。

在程序执行和验证方面，首先针对上述待验证PPTL 性质中涉及的程序变量与函数，利用底层虚拟机（LLVM,low level virtual machine）平台完成对被监控程序的插桩，进而编译成LLVM 统一的中间代码（IR,intermediate representation）。在边缘服务器程序运行过程中，状态序列被分为多个子片段，并交由边缘服务器中创建的不同线程，以实现验证的并行化。在此过程中，为了实现多个线程的高效合作，需建立验证任务分配和验证结果合并的调度机制。

本节将对性质描述与程序执行和验证方法进行具体描述。

3.1 基于PPTL 公式的性质描述

3.1.1 基于UML 顺序图的PPTL 性质描述

作为详细设计阶段的一种重要描述方法，UML顺序图用于描述函数调用的时间顺序和消息传递，能够表达函数间的动态交互关系。本文在UML2.0中增加了包括选择（alt）和循环（loop）在内的交互片段。

针对边缘服务器的DoS 攻击通过耗尽正在运行的边缘服务器的计算、网络和存储等关键资源，使其性能不断下降，直到不能提供正常服务，乃至系统崩溃，此时，UML 顺序图表达的系统正常行为将不能符合预期地被执行。为此，本文将重点关注边缘计算系统中边缘服务器上不同函数是否能够符合预期地被调用，在此过程中，将忽略UML顺序图上有关变量的数据流传递，只考虑模块间的函数调用以及模块内的函数调用。为了将系统预期满足的性质用时序逻辑语言形式化表达，本文利用PPTL公式描述UML顺序图中表达的函数间调用关系。

将UML 顺序图形式化的工作已经广泛开展，例如，文献[30]使用确定事件有限自动机描述UML顺序图，文献[31]使用线性时序逻辑（LTL,linear-time temporal logic）公式形式化表达顺序图。相较于LTL 公式，PPTL 公式能够表达区间相关与周期重复性质，因此，本节将重点介绍采用PPTL公式描述UML 顺序图中的循环片段。UML 顺序图如图5 所示。

图5 UML 顺序图

图5 展示了2 个模块中函数的调用关系。模块A 调用SendMessage 函数将相关消息发送给模块B，模块B 通过ReturnMessage 函数返回消息后，模块A 循环调用ProcessData 和DeleteData函数来处理和删除冗余数据。基于此UML 顺序图，可用如下PPTL 公式形式化描述模块A 中的函数调用序列。

其中，原子命题 SendMessage、ProcessData 和DeleteData 表示对应函数被调用，子公式(ProcessData;DeleteData)+表 示 ProcessData 和DeleteData 被循环调用。上述整体PPTL 公式的含义为存在某个状态，从该状态开始，SendMessage函数被调用，进而，ProcessData 和DeleteData 函数被循环调用。若模块A 被攻击而无法提供服务，将导致系统的执行路径违反上述公式。

3.1.2 基于DoS 攻击特征的PPTL 性质描述

由于每种DoS 攻击均具备不同特征，因此可以对不同的DoS 攻击进行原理分析，得出当攻击发生时，被攻击节点发生的动作序列，并在此基础上建立不同攻击对应的PPTL 时序逻辑公式。本节将对最典型的3 种针对TCP/IP 协议族攻击的DoS 攻击行为，即Smurf、SYN Flood 和Land 进行形式化描述。

1) Smurf 攻击

网际控制报文协议（ICMP,Internet control message protocol）为了判断线路能否正常通信，首先向目标主机发送请求，目标主机在接收到该请求后，自动回复应答给源主机。

入侵攻击者可利用ICMP 的工作原理制造针对边缘计算系统的Smurf 攻击，其将控制的设备接入边缘计算网络中，并将被攻击边缘服务器的主机地址作为请求回应的源地址，进而利用伪造的源地址向边缘计算网络中连续发送请求命令。接收到请求回应数据包后，被广播的网络主机均会发送回复应答，造成被攻击的边缘服务器的网络拥塞甚至系统崩溃。Smurf 攻击示意如图6 所示。

图6 Smurf 攻击示意

Smurf 攻击的行为特征可总结如下。

边缘服务器没有向该子网的广播地址发送数据，但收到的数据均来自子网主机，可用如下PPTL公式形式化描述以上行为特征。

其中，原子命题send 表示被攻击的边缘服务器发送数据，receive 表示被攻击的边缘服务器接收响应数据。子公式(◇receive)+表示receive 行为不断发生，即不断接收到其他节点返回的数据包。上述整体PPTL 公式的含义为存在某个状态，从该状态开始，该设备虽然没有发送数据包，但不断接收到数据包。

2) SYN Flood 攻击

基于TCP/IP 互联网服务中，TCP 协议采用三次握手方式建立可靠连接，连接过程如图7(a)所示。入侵攻击者利用上述三次握手工作原理，发起SYN Flood 攻击。具体来说，攻击者伪装成边缘计算系统中的多个终端或边缘服务器，在经过第一次握手和第二次握手后，故意不向边缘服务器发送第三次握手中所需的ACK 信息，使边缘服务器不得不多次重新发送SYN-ACK 应答数据包；同时，边缘服务器需维护大量连接队列，造成大量消耗资源的现象。边缘服务器一旦资源耗尽，就会出现速度极慢、无法连接边缘服务器等情况。除了在第三次握手中故意不向被攻击设备返回ACK 信息，攻击者还可以将SYN 数据包的源地址直接伪造成不存在的地址，向目标边缘服务器发起攻击，也可以达到同样的攻击效果。SYN Flood 攻击示意如图7(b)所示。

图7 SYN Flood 攻击示意

SYN Flood 攻击的行为特征可总结如下。

边缘服务器收到某个主机发来的SYN 数据包，并且向该主机返回一个SYN-ACK 数据包后，一直未接收到对方再次返回的ACK 数据包，可用如下PPTL 公式形式化描述以上行为特征。

其中，原子命题receive.SYN、send.SYNACK 和receive.ACK 分别表示被攻击的边缘服务器接收到SYN 数据包、发送SYN-ACK 回应数据包和接收到 ACK 数据包。公式使用(receive.SYN;send.SYNACK)表示接收 SYN 数据包和发送SYN-ACK 数据包的行为先后发生。上述整体PPTL 公式的含义为存在某个状态，从该状态开始，边缘服务器接收 SYN 数据包并进而发送SYN-ACK 数据包，但是在之后的所有状态，都没有接收到ACK 数据包。

3) Land 攻击

与SYN Flood 攻击类似，Land 攻击同样利用TCP 的连接建立过程。与正常报文不同的是，在向被攻击的边缘服务器发送的SYN 报文中，源地址和目的地址均为被攻击边缘服务器的IP 地址。

此操作将导致被攻击的边缘服务器首先向本机发送SYN-ACK 数据包，然后返回ACK 消息并创建一个空连接。值得注意的是，这些空连接将一直保留至超时。大规模的Land 攻击将导致边缘服务器服务不可用。Land 攻击示意如图8所示。

图8 Land 攻击示意

Land 攻击的行为特征可总结如下。

被攻击边缘服务器收到SYN 数据包后，不断试图与自己建立连接，即不断发送SYN-ACK 数据包和ACK 数据包，可用如下PPTL 公式形式化描述以上行为特征。

其中，原子命题receive.SYN、send.SYNACK 和send.ACK 分别表示被攻击的边缘服务器接收到SYN 数据包、发送SYN-ACK 数据包和发送ACK数据包。子公式 (send.SYNACK;send.ACK)+表示发送SYN-ACK 数据包和发送ACK 的行为不断发生。上述整体PPTL 公式的含义为存在某个状态，从该状态开始，边缘服务器接收到SYN 数据包，之后，不断发送SYN-ACK 数据包和ACK 数据包。

3.2 入侵检测方法

针对边缘计算系统中边缘服务器DoS 攻击入侵检测的并行运行时验证方法基本框架如图9 所示，包括执行模块和验证模块2 个同时运行的模块。

图9 并行运行时验证方法基本框架

执行模块首先基于PPTL 公式表达的时序逻辑性质，对边缘服务器上待验证的程序进行插桩，并基于LLVM 平台将其编译为IR 程序；然后在程序运行时，不断产生的状态序列被分为多个子片段。验证模块中，调度线程将不同序列片段的验证任务分发给同时运行的不同线程，并将不同片段被验证后的结果进行合并，得出最终验证结果。

3.2.1 基于PPTL 性质的代码插桩

边缘计算系统通过用C、C++、Java 等多种语言实现，而这些语言均能通过LLVM 平台转成统一的IR，进而由LLVM 完成中间代码的优化以及面向不同平台的最终可执行代码的生成。LLVM 框架如图10 所示。

图10 LLVM 框架

为了保证入侵检测方法的通用性，本文将基于LLVM 平台对程序语法树进行插桩。从3.1 节可看出，形式化描述后PPTL 公式重点关注程序变量和函数的调用情况。针对程序变量，由于其取值只有在其作为赋值语句左值时发生改变，因此，只有当性质P中出现的程序变量作为赋值语句的左值时，与该变量有关的原子命题作为条件的条件语句会被插入此状态之后。针对函数调用，只有当相关函数被调用时，才会将相应原子命题赋值为1，并记录此时的程序状态下标。需要指出的是，此算法不会保存每个状态上原子命题的真值，而是在原子命题的真值可能发生改变时，将该状态的下标记录下来。由于在大多数程序中，原子命题的真值在很多状态下是保持不变的，故该算法能够在很大程度上节省存储空间。

3.2.2 并行运行时验证方法

在被监测的边缘服务器中，假设有n+2 个线程可用，其中，线程e用于执行程序，线程s用于调度验证任务和合并验证结果，线程vi（1≤i≤n）用于验证不同的序列片段。在线程e运行程序过程中，状态序列首先被线程s分为若干片段，进而线程s将这些片段的信息发送给线程vi（1≤i≤n）完成相应验证任务；最后，不同片段的验证结果被返回给线程s，由其完成验证结果的汇总，并得到最终验证结果。在此过程中，若待验证的序列片段较多，而提供验证功能的线程较少，线程s与线程vi（1≤i≤n）将发生多次信息交互。该并行运行时验证方法的步骤可概括如下。

1) 使用PPTL 公式P表达需检测的性质，将性质取非后，利用MSV 工具集[29]中的P2G 工具构造对应的LNFGG，该LNFG 的信息将被验证线程vi（1≤i≤n）共享。

2) 线程e执行编译后程序M′.exe，在此过程中，调度线程s和验证线程vi（1≤i≤n）并行运行。

3) 当新生成的m个状态能够组成一个新的待验证序列片段sgk时，序偶(k;i)被调度线程s加入集合L中，其中i=min(I)，集合I存储目前没有执行验证任务的所有线程（初始值I={1,2,…,n}）；然后，调度线程s将片段sgk的信息发送给验证线程vi；此时，从集合I中删除i；k=k+1。

4) 与线程s同时工作的验证线程vi（1≤i≤n）中，一旦其被调用来验证序列片段sgk，将基于sgk中的状态信息，在¬P对应的LNFGG上探索可扩展路径，并将可扩展路径集合Ak={(in,en)|(in,en)表示为至少存在一条从节点in 到en 的可扩展路径}；进而，线程vi将(i,Ak)返回给调度线程s。

5) 当线程vi将序列片段sgk的验证结果(k,Ak)返回给调度线程s后，(k,Ak)被加入map 容器中；调度线程s通过L=L-{(k;i)}操作，解除sgk与vi的对应关系；由于此时线程vi再次空闲，调度线程将i加入集合I中；将map 容器中的多个片段验证结果合并后，如果能找到一条对应LNFG 中有穷路径，则一条反例路径被发现，即程序的当前执行路径不满足性质；若基于已有结果，能够断定LNFG 中不存在从初始节点出发到达ε节点的路径，则表明程序当前执行路径满足性质；否则，调度线程s将继续等待更多序列片段的验证结果。

与传统验证方法中顺序寻找反例路径不同，在并行验证方法中，不同的状态序列片段是同时验证的，对于大部分状态序列的片段来说，当它们开始验证时，尚未得到之前片段的验证结果。上述步骤4)对这些片段开展验证时，无法获知应从哪些节点开始探索可扩展路径。因此，第一个片段的初始节点的所有可达的非终止节点都应作为后续片段的初始节点。验证完成一个状态序列片段后，序偶(in,en)表示LNFG 中至少存在一条从节点in到en 的可扩展路径。一个序列片段被验证后，这些相邻片段上的序偶就会被连接以得到LNFG 中更长的可扩展路径。

图11 展示了一个程序状态序列满足性质的情况。假设在验证过程中，程序状态序列被分为3段，每段包含 2 个状态。若待验证的性质为□(p→◇q)，其中原子命题p和q分别代表x＜=3 和y＞4。基于图2 展示的LNFG，对应于每一个序列片段，LNFG 中的可扩展路径如图11 的中间列所示。在将每个片段的验证结果利用合成运算∘进行合并后，得到A0∘A1∘A2=∅，表明LNFG 中不存在从初始节点到达ε节点的路径，即此状态序列满足性质□(p→◇q)。

图11 程序状态序列满足性质的情况

4 实验评估

KDD CUP99 是目前网络异常检测方法和系统评价中应用最广泛的数据集。为了评估本文所提的针对Smurf、SYN Flood 和Land 三类DoS 攻击检测方法的可行性和有效性，从KDD CUP99 数据集中获取相关记录，攻击行为数量分布如表1 所示。

表1 攻击行为数量分布

针对所获取的攻击数据，将本文方法与相关文献中模型检测和机器学习方法进行对比。文献[22]提出了一种攻击特征描述语言（ASDL,attack signature description language），该语言能够同时描述被监控程序与待验证性质，并在此基础上，提出了一种ASDL 模型检测算法。文献[17]提出了面向边缘计算系统入侵检测的机器学习方法，并与其他机器学习方法进行了性能比较。本文实验使用Windows 10 操作系统，CPU 型号为Core i7-8700 @3.2 GHz，内存为8 GB。需要指出的是，在使用本文方法进行入侵检测时，所创建的验证线程为3 条。实验结果对比如表2 所示。

表2 实验结果对比

分析实验结果，本文得出如下结论。

1) 与基于RASL 的模型检测方法相比，由于本文使用的PPTL 公式具有更强的表达能力，因此准确率较高；在检测时间和消耗内存方面，本文采用的多线程并行方法使验证效率更高，但同时会占用更多内存。

2) 与机器学习方法相比，本文方法比传统机器学习方法BP（back propagation）神经网络和支持向量机（SVM,support vector machine）具有更高或相近的准确率，但与优化后的样本选择极限学习机（SS-ELM,sample selected extreme learning machine）相比尚有不足；在所需时间和消耗内存方面，由于不需要提前训练模型，并且在验证过程中采用了多线程并行方法，因此，本文方法能够节省模型训练时间，并在内存消耗方面有较大优势，同时需要更短的检测时间。

5 实例应用——智能停车系统

作为应用实例，本节将所提入侵检测方法应用于实际开发的基于边缘计算网络的智能停车系统中，以验证其在真实系统中的有效性。

5.1 模型概述

目前，智能停车系统已在智慧城市和智能交通系统中得到广泛应用。为了使其更加友好高效，文献[32]提出了一种基于边缘计算的P2P 网络智能停车系统，其利用云计算、边缘计算和P2P 网络技术提供大量的服务，包括停车位查询、导航、车牌识别、支付和事故查询等。智能停车系统共包括5 个重要部分。1) 移动终端设备代表车辆，例如汽车或卡车，作为活动节点，其他节点都供该节点使用。终端设备不时地与其他节点通信并与之交互，例如云端服务器和边缘服务器。2) 停车场的边缘服务器用于本地边缘计算，完成所有与停车场有关的计算任务，例如云端注册、位置判断、车辆管理以及视频监控等。3) 第三方导航用于引导和服务车辆找到目的地停车场。4) 第三方付款用于处理停车活动产生的费用。5) 云端服务器用于与边缘服务器节点和终端设备进行交互，存储和提供一些数据量大且时延要求不高的数据。

5.2 性质表达

为了保证车辆在停车过程中边缘服务器能够正常提供所有服务，在边缘服务器提供服务的过程中，本节在边缘服务器部署并行运行时验证系统，对其行为进行入侵检测，包括异常检测和误用检测。为了实现异常检测，首先用UML 顺序图对车辆从进入停车场开始的停车过程中各模块的行为进行建模，部分模型如图12 所示。

图12 智能停车系统部分UML 顺序图

由于本文只关注边缘服务器行为，因此只需分析边缘服务器生命线上的相关函数调用序列，可用如下PPTL 公式对其进行形式化描述。

其中，操作符+表示对于不同的车辆进入请求，边缘服务器将不断重复执行各个函数。总体来看，此PPTL 公式表示从某一时刻起，边缘服务器将循环执行函数identifyEnter、vehicleReserved、sendSpace、sendStatus、returnStatus、identifyLeave、calculateFee和sendFee。

针对P1公式的运行时验证能够实现边缘服务器的异常检测，实时监控其各个函数是否被顺利调用执行，一旦发现P1公式不被满足，可立即发出警告提示。在对边缘服务器进行异常检测的同时，可对Smurf、SYN Flood 和Land 攻击进行误用检测，即对3.1.2 节中相对应的PPTL 公式实施运行时验证，以判断攻击的类型，具体如下

当P2、P3和P4中某一个公式被满足时，即表明检测出相应类型的攻击。

5.3 系统验证

为了表明所提方法的有效性，针对智能停车系统，本节将运行时验证模块部署在边缘服务器以实时监控P1公式是否被违反（即边缘服务器不能正常提供服务），以及P2～P4中某个公式是否成立（即检测到某个DoS 攻击行为）。在实验中，使用安卓手机作为终端，5 台PC 机作为边缘服务器，腾讯云提供云端服务。

实验共分为三组，分别使用边缘服务器中的单个验证线程来实现传统的运行时验证方法，以及3 个和5 个验证线程实现并行运行时验证方法，其中每次验证的序列片段包含1 000 个程序状态。在每组实验中，将一个恶意节点加入边缘计算网络后，对边缘服务器实施Smurf 攻击，为了证明所提方法的有效性以及验证效率的准确性，均重复攻击10 次。针对Smurf 攻击的检测结果如表3 所示。

表3 中，第一列为待验证的PPTL 公式，包括用于异常检测的公式P1以及用于误用检测的公式P2～P4；第二列表示验证工具给出的验证结果，即程序是否满足相应性质，P1为×表明检测出边缘服务器没有正常提供服务，P2为√表明检测出攻击类型为Smurf 攻击；第三列至第五列给出了在边缘服务器中，不同数量验证线程提供验证算力的情况下，每验证1 000 个状态所需要的时间。比较第三列至第五列给出的验证时间可以发现，当3 个验证线程提供验证算力时，验证效率最高，而当5 个验证线程提供验证算力时，验证效率反而会降低。这是由于边缘服务器虽然能够支持一定数量的并行线程，但边缘服务器的CPU 计算能力不强，5 个验证线程导致CPU 的线程切换开销过大，影响整体性能。总体来看，3 个验证线程提供验证算力的情况下，在Smurf 攻击实施7 s 内，本文所提的并行运行时验证方法能够检测出入侵攻击。针对SYN Flood 和Land 攻击的检测结果能得到相似结论。

表3 针对Smurf 攻击的检测结果

6 结束语

针对边缘计算系统中边缘服务器面临的DoS攻击，本文提出了一种并行运行时验证方法，该方法结合误用检测和异常检测，充分利用边缘服务器的计算与存储资源。首先使用PPTL 公式，分别描述系统正常状态和3 种典型的DoS 攻击的行为特征；然后将上述两类PPTL 公式作为待验证性质，在边缘服务器上部署并行运行时验证方法，在边缘服务器程序运行过程中，利用边缘服务器中的多个验证线程，完成DoS 攻击的入侵检测；最后通过对比实验，验证了所提方法的可行性和有效性，并对一个实际的基于边缘计算的P2P 网络智能停车系统进行模拟DoS 攻击和攻击检测。实验表明，所提方法能够有效识别Smurf、SYN Flood 和Land 攻击。在今后的研究工作中，将进一步提高基于运行时验证的入侵检测效率，且对更多类型的入侵攻击进行形式化描述与检测。