于斌，張南，陸旭，段振華，田聰

（西安電子科技大學計算機科學與技術學院，陜西 西安 710071）

1 引言

邊緣計算系統(tǒng)利用終端設備及終端附近的邊緣服務器的計算和存儲資源，提前對數(shù)據(jù)進行部分處理，減少要發(fā)送到云數(shù)據(jù)中心的數(shù)據(jù)量，從而減少網(wǎng)絡帶寬使用量，并使系統(tǒng)能夠在較低數(shù)據(jù)時延的情況下立即響應數(shù)據(jù)[1]。邊緣計算系統(tǒng)總體框架如圖1 所示。在邊緣計算系統(tǒng)中，邊緣服務器處于整個系統(tǒng)的中間層，起到連接云服務器和終端設備的作用，并承擔云服務器的部分計算任務。隨著服務器性能的不斷提升，越來越多的數(shù)據(jù)處理任務依托邊緣服務器來完成。

圖1 邊緣計算系統(tǒng)總體框架

然而，邊緣服務器的特點使其面臨新的挑戰(zhàn)[2-5]。首先，邊緣服務器常位于網(wǎng)絡邊緣，面臨更復雜的網(wǎng)絡環(huán)境。此外，邊緣服務器往往是地理分布式的，難以做到集中的設備安全保護，且每個邊緣服務器是不同的，此差異性給攻擊者帶來了更多的可選擇性。更嚴重的是，由于計算能力和存儲空間的限制，大多數(shù)邊緣服務器只關注業(yè)務邏輯的實現(xiàn)，而對可能受到的攻擊缺少防范和檢測。由以上分析可知，雖然邊緣服務器在邊緣計算中發(fā)揮重要作用，但其易攻擊的特征使其面臨嚴峻的攻擊威脅。

由于邊緣服務器的計算和存儲資源受限，極易被耗盡，因此，在邊緣計算系統(tǒng)面臨的多種攻擊中，針對邊緣服務器的拒絕服務（DoS,denial of service）攻擊很廣泛[6-10]。在DoS 攻擊中，惡意節(jié)點通過無限制地訪問指定的被攻擊邊緣服務器，向其發(fā)送大量的無效數(shù)據(jù)包，耗盡正在運行的服務器資源，阻礙邊緣服務器的正常運行。由于在邊緣計算架構中，邊緣服務器用于實現(xiàn)數(shù)據(jù)的部分處理以及數(shù)據(jù)與云服務器的傳輸，一旦邊緣服務器的通信鏈路堵塞或資源被耗盡，將直接造成預期的正常業(yè)務無法完成。

作為保障網(wǎng)絡安全的一種重要手段，入侵檢測能夠?qū)崟r監(jiān)測網(wǎng)絡活動，判斷設備狀態(tài)，及時發(fā)現(xiàn)DoS 中的受攻擊設備，主要包括異常檢測和誤用檢測2 種方法。其中，異常檢測方法基于被監(jiān)控對象的正常行為，其假設入侵是與正常行為必然不同的異常，因此，任何明顯偏離正常的行為都被認為是侵入性的；誤用檢測對正在監(jiān)視的事件進行匹配，符合已知攻擊特征的操作均被視為入侵行為。在現(xiàn)有針對邊緣計算系統(tǒng)的入侵檢測方法中，大部分方法利用模式識別或機器學習手段[11-18]，雖然能夠取得較好的檢測結(jié)果，但需提前訓練模型，在基于訓練好的模型進行實時檢測時需占用較大內(nèi)存。與之對應，以模型檢測和運行時驗證為代表的形式化驗證方法利用時序邏輯性質(zhì)，對網(wǎng)絡入侵的行為特征進行識別，不需要提前訓練模型，但由于需要構造自動機等理論模型，檢測效率往往不高，雖然在云計算等傳統(tǒng)網(wǎng)絡中得到應用[19-24]，但在邊緣計算系統(tǒng)中的研究仍處于初步階段。

鑒于邊緣計算系統(tǒng)中邊緣服務器的重要性和易攻擊性，以及面向邊緣服務器DoS 攻擊的廣泛性和威脅的嚴重性，如何構建一個高效準確的入侵檢測方法，是一個亟待解決的重要問題。作為輕量級形式化驗證方法，運行時驗證能夠監(jiān)視和分析真實系統(tǒng)的執(zhí)行情況，以檢查系統(tǒng)的運行軌跡是否滿足形式化描述的屬性，已逐漸被用于網(wǎng)絡入侵檢測中[19-20]。在邊緣計算系統(tǒng)中，由于邊緣服務器需要保持運行狀態(tài)，不斷響應終端設備的服務請求并完成期望的邏輯功能，因此，對其進行運行時驗證是必要和可行的。

考慮到邊緣服務器具有較強的計算能力，本文采用運行時驗證方法對DoS 攻擊進行檢測。為了充分利用邊緣服務器計算資源以提高驗證效率，解決目前運行時驗證方法中線性時序邏輯[25]和計算樹邏輯[26]表達能力不足的問題，本文結(jié)合誤用檢測和異常檢測，提出基于命題投影時序邏輯（PPTL,propositional projection temporal logic）[27-29]的并行運行時驗證方法。首先，基于統(tǒng)一建模語言（UML,unified modeling language）順序圖，使用PPTL 公式描述系統(tǒng)正常狀態(tài)下的行為特征；然后，使用PPTL 公式描述DoS 攻擊中針對TCP/IP 協(xié)議族最常見的Smurf 攻擊、SYN Flood（synchronize flood）攻擊以及Land 攻擊的行為特征；進而，將上述兩類PPTL 公式作為待驗證性質(zhì)，在邊緣計算系統(tǒng)運行過程中，在邊緣服務器上部署PPTL 公式的運行時驗證方法，基于搜集到的信息，利用邊緣服務器的多個線程，共同完成DoS 攻擊的入侵檢測。在此過程中，若發(fā)現(xiàn)第一類性質(zhì)不滿足，則表明邊緣服務器無法完成正常的請求響應；若發(fā)現(xiàn)第二類性質(zhì)中某性質(zhì)滿足，則表明檢測到某一特定類別的DoS 攻擊。最后，為了檢驗上述方法的有效性，本文進行了性能對比實驗，并對一個實際的基于邊緣計算的點對點（P2P,peer-to-peer）網(wǎng)絡智能停車系統(tǒng)進行針對邊緣服務器的模擬DoS 攻擊和攻擊檢測，實驗結(jié)果表明，所提方法能夠有效檢測出邊緣服務器的異常行為和所受DoS 攻擊類型。

本文貢獻主要包括以下三方面。

1) 采用PPTL 公式描述基于UML 順序圖的邊緣服務器正常行為特征和不同DoS 攻擊下邊緣服務器的異常行為特征，其中，PPTL 具有完全正則的表達能力，可直接用于描述邊緣服務器上不同模塊調(diào)用的區(qū)間相關與周期重復的性質(zhì)。

2) 基于PPTL 性質(zhì)描述，采用運行時驗證方法對邊緣服務器進行實時監(jiān)控，實現(xiàn)異常檢測和誤用檢測，在此過程中，基于并行運行時驗證框架，充分利用邊緣服務器的空閑計算與存儲資源，提高驗證效率，及時發(fā)現(xiàn)攻擊。

3) 將所提運行時驗證方法部署在實際智能停車系統(tǒng)，對其進行邊緣服務器監(jiān)控，實驗結(jié)果表明，邊緣計算系統(tǒng)中的DoS 攻擊能夠被有效識別。

2 相關理論

2.1 命題投影時序邏輯

PPTL 公式P歸納定義為

其中，Prop 為一個可數(shù)的原子命題集合，p∈Prop表示原子命題，P1,…,Pm和P是PPTL 公式。PPTL的語義已在文獻[27-29]中明確給出。PPTL 派生的時態(tài)公式為

任何PPTL 公式都能夠轉(zhuǎn)換為對應的范式[29]，基于范式，能夠構造出其對應的帶標簽的范式圖（LNFG,labeled normal form graph）。LNFG 中的有窮路徑π=＜n0,p0,…,ε＞是從初始節(jié)點到ε節(jié)點的節(jié)點和邊的交替序列，其一定是可接收的。無窮路徑π=＜n0,p0,…,(ni,pi,…,nj,pj)ω＞是節(jié)點和邊的無窮交替序列，若路徑上無限出現(xiàn)的節(jié)點的集合（用Inf(π)表示）不存在被所有節(jié)點同時擁有的標簽，則該路徑是可接收的。

圖2 展示了PPTL 公式◇(p∧□(?q))對應的LNFG，圖中每個節(jié)點代表一個PPTL 公式；每條邊為一個狀態(tài)公式；額外引入的命題lk用于識別一條路徑是否為可接收的。例如，有窮路徑π1=＜1,p∧?q,3,?q,4＞為可接收路徑；對于無窮路徑π2=＜1,true,(2,true)ω＞，由于Inf(π2)={2}?L1={2}，意味著無窮循環(huán)的節(jié)點擁有相同的標記l1，因此這條路徑是不可接收的。

圖2 PPTL 公式◇(p∧□(?q))對應的LNFG

2.2 傳統(tǒng)運行時驗證方法

對于待驗證程序M，若采用傳統(tǒng)的運行時驗證方法驗證其是否滿足期望的PPTL 性質(zhì)P，需要首先對程序M進行插樁，并構建?P對應的LNFGG；然后，在插樁后的程序M執(zhí)行過程中，每個狀態(tài)上出現(xiàn)在P中的變量的值被記錄下來，基于這些變量的值，可以得到G中對應邊上的狀態(tài)公式的真值；進而，探索G中的可接收路徑，若能夠在G中發(fā)現(xiàn)一條可接收路徑，則表明程序的當前執(zhí)行路徑不滿足性質(zhì)P；若不存在可接收路徑，則表明程序的當前執(zhí)行路徑滿足性質(zhì)P。

圖3 中的例子展示了傳統(tǒng)運行時驗證方法面臨的挑戰(zhàn)。圖3(a)展示了一個程序執(zhí)行產(chǎn)生的狀態(tài)序列，共包含 4 個狀態(tài)。假設待驗證的性質(zhì)為□(p→◇q)，其中原子命題p和q分別代表x＜=3 和y＞5。性質(zhì)□(p→◇q)的非，即◇(p∧□(?q))的LNFGG如圖2 所示。當程序執(zhí)行時，G中的路徑探索結(jié)果如圖3(b)所示，圖3 中的節(jié)點編號與圖2 中的節(jié)點編號保持一致。由于在G中存在多條從節(jié)點1 和節(jié)點2 出發(fā)的邊，在圖3(b)的前3 步中，越來越多的路徑產(chǎn)生。由于性質(zhì)對應的LNFG 中路徑的探索過程相當于程序解釋執(zhí)行的過程，其速度原本就遠小于程序編譯后生成狀態(tài)的速度，再加上LNFG 中不斷產(chǎn)生分支，因此在傳統(tǒng)的運行時驗證方法中，串行的驗證方法限制了驗證效率的提高。

圖3 傳統(tǒng)運行時驗證方法面臨的挑戰(zhàn)

3 DoS 攻擊檢測方法

為了有效檢測針對邊緣服務器的DoS 攻擊，本文提出基于運行時驗證的入侵檢測方法，該方法可部署在需要監(jiān)控的邊緣服務器上，在邊緣服務器提供服務的同時，實現(xiàn)針對邊緣服務器的異常檢測和誤用檢測。在檢測過程中，為了充分利用邊緣服務器的計算和存儲資源，本文提出了基于多線程的并行運行時驗證框架，以提高入侵檢測效率，及時發(fā)現(xiàn)攻擊的存在。攻擊檢測示意如圖4 所示。

圖4 攻擊檢測示意

在性質(zhì)描述方面，本文采用與完全正則式表達能力相同的PPTL 公式，其能夠直接表達區(qū)間相關和周期重復的性質(zhì)。為了提供異常檢測所需性質(zhì)，針對UML 順序圖中表達的模塊之間函數(shù)調(diào)用關系，使用PPTL 公式描述正常情況下不同函數(shù)的執(zhí)行序列；為了提供誤用檢測所需性質(zhì)，針對不同DoS 攻擊的行為特征進行分析，并使用PPTL 公式形式化描述此行為特征。

在程序執(zhí)行和驗證方面，首先針對上述待驗證PPTL 性質(zhì)中涉及的程序變量與函數(shù)，利用底層虛擬機（LLVM,low level virtual machine）平臺完成對被監(jiān)控程序的插樁，進而編譯成LLVM 統(tǒng)一的中間代碼（IR,intermediate representation）。在邊緣服務器程序運行過程中，狀態(tài)序列被分為多個子片段，并交由邊緣服務器中創(chuàng)建的不同線程，以實現(xiàn)驗證的并行化。在此過程中，為了實現(xiàn)多個線程的高效合作，需建立驗證任務分配和驗證結(jié)果合并的調(diào)度機制。

本節(jié)將對性質(zhì)描述與程序執(zhí)行和驗證方法進行具體描述。

3.1 基于PPTL 公式的性質(zhì)描述

3.1.1 基于UML 順序圖的PPTL 性質(zhì)描述

作為詳細設計階段的一種重要描述方法，UML順序圖用于描述函數(shù)調(diào)用的時間順序和消息傳遞，能夠表達函數(shù)間的動態(tài)交互關系。本文在UML2.0中增加了包括選擇（alt）和循環(huán)（loop）在內(nèi)的交互片段。

針對邊緣服務器的DoS 攻擊通過耗盡正在運行的邊緣服務器的計算、網(wǎng)絡和存儲等關鍵資源，使其性能不斷下降，直到不能提供正常服務，乃至系統(tǒng)崩潰，此時，UML 順序圖表達的系統(tǒng)正常行為將不能符合預期地被執(zhí)行。為此，本文將重點關注邊緣計算系統(tǒng)中邊緣服務器上不同函數(shù)是否能夠符合預期地被調(diào)用，在此過程中，將忽略UML順序圖上有關變量的數(shù)據(jù)流傳遞，只考慮模塊間的函數(shù)調(diào)用以及模塊內(nèi)的函數(shù)調(diào)用。為了將系統(tǒng)預期滿足的性質(zhì)用時序邏輯語言形式化表達，本文利用PPTL公式描述UML順序圖中表達的函數(shù)間調(diào)用關系。

將UML 順序圖形式化的工作已經(jīng)廣泛開展，例如，文獻[30]使用確定事件有限自動機描述UML順序圖，文獻[31]使用線性時序邏輯（LTL,linear-time temporal logic）公式形式化表達順序圖。相較于LTL 公式，PPTL 公式能夠表達區(qū)間相關與周期重復性質(zhì)，因此，本節(jié)將重點介紹采用PPTL公式描述UML 順序圖中的循環(huán)片段。UML 順序圖如圖5 所示。

圖5 UML 順序圖

圖5 展示了2 個模塊中函數(shù)的調(diào)用關系。模塊A 調(diào)用SendMessage 函數(shù)將相關消息發(fā)送給模塊B，模塊B 通過ReturnMessage 函數(shù)返回消息后，模塊A 循環(huán)調(diào)用ProcessData 和DeleteData函數(shù)來處理和刪除冗余數(shù)據(jù)?；诖薝ML 順序圖，可用如下PPTL 公式形式化描述模塊A 中的函數(shù)調(diào)用序列。

其中，原子命題 SendMessage、ProcessData 和DeleteData 表示對應函數(shù)被調(diào)用，子公式(ProcessData;DeleteData)+表 示 ProcessData 和DeleteData 被循環(huán)調(diào)用。上述整體PPTL 公式的含義為存在某個狀態(tài)，從該狀態(tài)開始，SendMessage函數(shù)被調(diào)用，進而，ProcessData 和DeleteData 函數(shù)被循環(huán)調(diào)用。若模塊A 被攻擊而無法提供服務，將導致系統(tǒng)的執(zhí)行路徑違反上述公式。

3.1.2 基于DoS 攻擊特征的PPTL 性質(zhì)描述

由于每種DoS 攻擊均具備不同特征，因此可以對不同的DoS 攻擊進行原理分析，得出當攻擊發(fā)生時，被攻擊節(jié)點發(fā)生的動作序列，并在此基礎上建立不同攻擊對應的PPTL 時序邏輯公式。本節(jié)將對最典型的3 種針對TCP/IP 協(xié)議族攻擊的DoS 攻擊行為，即Smurf、SYN Flood 和Land 進行形式化描述。

1) Smurf 攻擊

網(wǎng)際控制報文協(xié)議（ICMP,Internet control message protocol）為了判斷線路能否正常通信，首先向目標主機發(fā)送請求，目標主機在接收到該請求后，自動回復應答給源主機。

入侵攻擊者可利用ICMP 的工作原理制造針對邊緣計算系統(tǒng)的Smurf 攻擊，其將控制的設備接入邊緣計算網(wǎng)絡中，并將被攻擊邊緣服務器的主機地址作為請求回應的源地址，進而利用偽造的源地址向邊緣計算網(wǎng)絡中連續(xù)發(fā)送請求命令。接收到請求回應數(shù)據(jù)包后，被廣播的網(wǎng)絡主機均會發(fā)送回復應答，造成被攻擊的邊緣服務器的網(wǎng)絡擁塞甚至系統(tǒng)崩潰。Smurf 攻擊示意如圖6 所示。

圖6 Smurf 攻擊示意

Smurf 攻擊的行為特征可總結(jié)如下。

邊緣服務器沒有向該子網(wǎng)的廣播地址發(fā)送數(shù)據(jù)，但收到的數(shù)據(jù)均來自子網(wǎng)主機，可用如下PPTL公式形式化描述以上行為特征。

其中，原子命題send 表示被攻擊的邊緣服務器發(fā)送數(shù)據(jù)，receive 表示被攻擊的邊緣服務器接收響應數(shù)據(jù)。子公式(◇receive)+表示receive 行為不斷發(fā)生，即不斷接收到其他節(jié)點返回的數(shù)據(jù)包。上述整體PPTL 公式的含義為存在某個狀態(tài)，從該狀態(tài)開始，該設備雖然沒有發(fā)送數(shù)據(jù)包，但不斷接收到數(shù)據(jù)包。

2) SYN Flood 攻擊

基于TCP/IP 互聯(lián)網(wǎng)服務中，TCP 協(xié)議采用三次握手方式建立可靠連接，連接過程如圖7(a)所示。入侵攻擊者利用上述三次握手工作原理，發(fā)起SYN Flood 攻擊。具體來說，攻擊者偽裝成邊緣計算系統(tǒng)中的多個終端或邊緣服務器，在經(jīng)過第一次握手和第二次握手后，故意不向邊緣服務器發(fā)送第三次握手中所需的ACK 信息，使邊緣服務器不得不多次重新發(fā)送SYN-ACK 應答數(shù)據(jù)包；同時，邊緣服務器需維護大量連接隊列，造成大量消耗資源的現(xiàn)象。邊緣服務器一旦資源耗盡，就會出現(xiàn)速度極慢、無法連接邊緣服務器等情況。除了在第三次握手中故意不向被攻擊設備返回ACK 信息，攻擊者還可以將SYN 數(shù)據(jù)包的源地址直接偽造成不存在的地址，向目標邊緣服務器發(fā)起攻擊，也可以達到同樣的攻擊效果。SYN Flood 攻擊示意如圖7(b)所示。

圖7 SYN Flood 攻擊示意

SYN Flood 攻擊的行為特征可總結(jié)如下。

邊緣服務器收到某個主機發(fā)來的SYN 數(shù)據(jù)包，并且向該主機返回一個SYN-ACK 數(shù)據(jù)包后，一直未接收到對方再次返回的ACK 數(shù)據(jù)包，可用如下PPTL 公式形式化描述以上行為特征。

其中，原子命題receive.SYN、send.SYNACK 和receive.ACK 分別表示被攻擊的邊緣服務器接收到SYN 數(shù)據(jù)包、發(fā)送SYN-ACK 回應數(shù)據(jù)包和接收到 ACK 數(shù)據(jù)包。公式使用(receive.SYN;send.SYNACK)表示接收 SYN 數(shù)據(jù)包和發(fā)送SYN-ACK 數(shù)據(jù)包的行為先后發(fā)生。上述整體PPTL 公式的含義為存在某個狀態(tài)，從該狀態(tài)開始，邊緣服務器接收 SYN 數(shù)據(jù)包并進而發(fā)送SYN-ACK 數(shù)據(jù)包，但是在之后的所有狀態(tài)，都沒有接收到ACK 數(shù)據(jù)包。

3) Land 攻擊

與SYN Flood 攻擊類似，Land 攻擊同樣利用TCP 的連接建立過程。與正常報文不同的是，在向被攻擊的邊緣服務器發(fā)送的SYN 報文中，源地址和目的地址均為被攻擊邊緣服務器的IP 地址。

此操作將導致被攻擊的邊緣服務器首先向本機發(fā)送SYN-ACK 數(shù)據(jù)包，然后返回ACK 消息并創(chuàng)建一個空連接。值得注意的是，這些空連接將一直保留至超時。大規(guī)模的Land 攻擊將導致邊緣服務器服務不可用。Land 攻擊示意如圖8所示。

圖8 Land 攻擊示意

Land 攻擊的行為特征可總結(jié)如下。

被攻擊邊緣服務器收到SYN 數(shù)據(jù)包后，不斷試圖與自己建立連接，即不斷發(fā)送SYN-ACK 數(shù)據(jù)包和ACK 數(shù)據(jù)包，可用如下PPTL 公式形式化描述以上行為特征。

其中，原子命題receive.SYN、send.SYNACK 和send.ACK 分別表示被攻擊的邊緣服務器接收到SYN 數(shù)據(jù)包、發(fā)送SYN-ACK 數(shù)據(jù)包和發(fā)送ACK數(shù)據(jù)包。子公式 (send.SYNACK;send.ACK)+表示發(fā)送SYN-ACK 數(shù)據(jù)包和發(fā)送ACK 的行為不斷發(fā)生。上述整體PPTL 公式的含義為存在某個狀態(tài)，從該狀態(tài)開始，邊緣服務器接收到SYN 數(shù)據(jù)包，之后，不斷發(fā)送SYN-ACK 數(shù)據(jù)包和ACK 數(shù)據(jù)包。

3.2 入侵檢測方法

針對邊緣計算系統(tǒng)中邊緣服務器DoS 攻擊入侵檢測的并行運行時驗證方法基本框架如圖9 所示，包括執(zhí)行模塊和驗證模塊2 個同時運行的模塊。

圖9 并行運行時驗證方法基本框架

執(zhí)行模塊首先基于PPTL 公式表達的時序邏輯性質(zhì)，對邊緣服務器上待驗證的程序進行插樁，并基于LLVM 平臺將其編譯為IR 程序；然后在程序運行時，不斷產(chǎn)生的狀態(tài)序列被分為多個子片段。驗證模塊中，調(diào)度線程將不同序列片段的驗證任務分發(fā)給同時運行的不同線程，并將不同片段被驗證后的結(jié)果進行合并，得出最終驗證結(jié)果。

3.2.1 基于PPTL 性質(zhì)的代碼插樁

邊緣計算系統(tǒng)通過用C、C++、Java 等多種語言實現(xiàn)，而這些語言均能通過LLVM 平臺轉(zhuǎn)成統(tǒng)一的IR，進而由LLVM 完成中間代碼的優(yōu)化以及面向不同平臺的最終可執(zhí)行代碼的生成。LLVM 框架如圖10 所示。

圖10 LLVM 框架

為了保證入侵檢測方法的通用性，本文將基于LLVM 平臺對程序語法樹進行插樁。從3.1 節(jié)可看出，形式化描述后PPTL 公式重點關注程序變量和函數(shù)的調(diào)用情況。針對程序變量，由于其取值只有在其作為賦值語句左值時發(fā)生改變，因此，只有當性質(zhì)P中出現(xiàn)的程序變量作為賦值語句的左值時，與該變量有關的原子命題作為條件的條件語句會被插入此狀態(tài)之后。針對函數(shù)調(diào)用，只有當相關函數(shù)被調(diào)用時，才會將相應原子命題賦值為1，并記錄此時的程序狀態(tài)下標。需要指出的是，此算法不會保存每個狀態(tài)上原子命題的真值，而是在原子命題的真值可能發(fā)生改變時，將該狀態(tài)的下標記錄下來。由于在大多數(shù)程序中，原子命題的真值在很多狀態(tài)下是保持不變的，故該算法能夠在很大程度上節(jié)省存儲空間。

3.2.2 并行運行時驗證方法

在被監(jiān)測的邊緣服務器中，假設有n+2 個線程可用，其中，線程e用于執(zhí)行程序，線程s用于調(diào)度驗證任務和合并驗證結(jié)果，線程vi（1≤i≤n）用于驗證不同的序列片段。在線程e運行程序過程中，狀態(tài)序列首先被線程s分為若干片段，進而線程s將這些片段的信息發(fā)送給線程vi（1≤i≤n）完成相應驗證任務；最后，不同片段的驗證結(jié)果被返回給線程s，由其完成驗證結(jié)果的匯總，并得到最終驗證結(jié)果。在此過程中，若待驗證的序列片段較多，而提供驗證功能的線程較少，線程s與線程vi（1≤i≤n）將發(fā)生多次信息交互。該并行運行時驗證方法的步驟可概括如下。

1) 使用PPTL 公式P表達需檢測的性質(zhì)，將性質(zhì)取非后，利用MSV 工具集[29]中的P2G 工具構造對應的LNFGG，該LNFG 的信息將被驗證線程vi（1≤i≤n）共享。

2) 線程e執(zhí)行編譯后程序M′.exe，在此過程中，調(diào)度線程s和驗證線程vi（1≤i≤n）并行運行。

3) 當新生成的m個狀態(tài)能夠組成一個新的待驗證序列片段sgk時，序偶(k;i)被調(diào)度線程s加入集合L中，其中i=min(I)，集合I存儲目前沒有執(zhí)行驗證任務的所有線程（初始值I={1,2,…,n}）；然后，調(diào)度線程s將片段sgk的信息發(fā)送給驗證線程vi；此時，從集合I中刪除i；k=k+1。

4) 與線程s同時工作的驗證線程vi（1≤i≤n）中，一旦其被調(diào)用來驗證序列片段sgk，將基于sgk中的狀態(tài)信息，在?P對應的LNFGG上探索可擴展路徑，并將可擴展路徑集合Ak={(in,en)|(in,en)表示為至少存在一條從節(jié)點in 到en 的可擴展路徑}；進而，線程vi將(i,Ak)返回給調(diào)度線程s。

5) 當線程vi將序列片段sgk的驗證結(jié)果(k,Ak)返回給調(diào)度線程s后，(k,Ak)被加入map 容器中；調(diào)度線程s通過L=L-{(k;i)}操作，解除sgk與vi的對應關系；由于此時線程vi再次空閑，調(diào)度線程將i加入集合I中；將map 容器中的多個片段驗證結(jié)果合并后，如果能找到一條對應LNFG 中有窮路徑，則一條反例路徑被發(fā)現(xiàn)，即程序的當前執(zhí)行路徑不滿足性質(zhì)；若基于已有結(jié)果，能夠斷定LNFG 中不存在從初始節(jié)點出發(fā)到達ε節(jié)點的路徑，則表明程序當前執(zhí)行路徑滿足性質(zhì)；否則，調(diào)度線程s將繼續(xù)等待更多序列片段的驗證結(jié)果。

與傳統(tǒng)驗證方法中順序?qū)ふ曳蠢窂讲煌?，在并行驗證方法中，不同的狀態(tài)序列片段是同時驗證的，對于大部分狀態(tài)序列的片段來說，當它們開始驗證時，尚未得到之前片段的驗證結(jié)果。上述步驟4)對這些片段開展驗證時，無法獲知應從哪些節(jié)點開始探索可擴展路徑。因此，第一個片段的初始節(jié)點的所有可達的非終止節(jié)點都應作為后續(xù)片段的初始節(jié)點。驗證完成一個狀態(tài)序列片段后，序偶(in,en)表示LNFG 中至少存在一條從節(jié)點in到en 的可擴展路徑。一個序列片段被驗證后，這些相鄰片段上的序偶就會被連接以得到LNFG 中更長的可擴展路徑。

圖11 展示了一個程序狀態(tài)序列滿足性質(zhì)的情況。假設在驗證過程中，程序狀態(tài)序列被分為3段，每段包含 2 個狀態(tài)。若待驗證的性質(zhì)為□(p→◇q)，其中原子命題p和q分別代表x＜=3 和y＞4。基于圖2 展示的LNFG，對應于每一個序列片段，LNFG 中的可擴展路徑如圖11 的中間列所示。在將每個片段的驗證結(jié)果利用合成運算°進行合并后，得到A0°A1°A2=?，表明LNFG 中不存在從初始節(jié)點到達ε節(jié)點的路徑，即此狀態(tài)序列滿足性質(zhì)□(p→◇q)。

圖11 程序狀態(tài)序列滿足性質(zhì)的情況

4 實驗評估

KDD CUP99 是目前網(wǎng)絡異常檢測方法和系統(tǒng)評價中應用最廣泛的數(shù)據(jù)集。為了評估本文所提的針對Smurf、SYN Flood 和Land 三類DoS 攻擊檢測方法的可行性和有效性，從KDD CUP99 數(shù)據(jù)集中獲取相關記錄，攻擊行為數(shù)量分布如表1 所示。

表1 攻擊行為數(shù)量分布

針對所獲取的攻擊數(shù)據(jù)，將本文方法與相關文獻中模型檢測和機器學習方法進行對比。文獻[22]提出了一種攻擊特征描述語言（ASDL,attack signature description language），該語言能夠同時描述被監(jiān)控程序與待驗證性質(zhì)，并在此基礎上，提出了一種ASDL 模型檢測算法。文獻[17]提出了面向邊緣計算系統(tǒng)入侵檢測的機器學習方法，并與其他機器學習方法進行了性能比較。本文實驗使用Windows 10 操作系統(tǒng)，CPU 型號為Core i7-8700 @3.2 GHz，內(nèi)存為8 GB。需要指出的是，在使用本文方法進行入侵檢測時，所創(chuàng)建的驗證線程為3 條。實驗結(jié)果對比如表2 所示。

表2 實驗結(jié)果對比

分析實驗結(jié)果，本文得出如下結(jié)論。

1) 與基于RASL 的模型檢測方法相比，由于本文使用的PPTL 公式具有更強的表達能力，因此準確率較高；在檢測時間和消耗內(nèi)存方面，本文采用的多線程并行方法使驗證效率更高，但同時會占用更多內(nèi)存。

2) 與機器學習方法相比，本文方法比傳統(tǒng)機器學習方法BP（back propagation）神經(jīng)網(wǎng)絡和支持向量機（SVM,support vector machine）具有更高或相近的準確率，但與優(yōu)化后的樣本選擇極限學習機（SS-ELM,sample selected extreme learning machine）相比尚有不足；在所需時間和消耗內(nèi)存方面，由于不需要提前訓練模型，并且在驗證過程中采用了多線程并行方法，因此，本文方法能夠節(jié)省模型訓練時間，并在內(nèi)存消耗方面有較大優(yōu)勢，同時需要更短的檢測時間。

5 實例應用——智能停車系統(tǒng)

作為應用實例，本節(jié)將所提入侵檢測方法應用于實際開發(fā)的基于邊緣計算網(wǎng)絡的智能停車系統(tǒng)中，以驗證其在真實系統(tǒng)中的有效性。

5.1 模型概述

目前，智能停車系統(tǒng)已在智慧城市和智能交通系統(tǒng)中得到廣泛應用。為了使其更加友好高效，文獻[32]提出了一種基于邊緣計算的P2P 網(wǎng)絡智能停車系統(tǒng)，其利用云計算、邊緣計算和P2P 網(wǎng)絡技術提供大量的服務，包括停車位查詢、導航、車牌識別、支付和事故查詢等。智能停車系統(tǒng)共包括5 個重要部分。1) 移動終端設備代表車輛，例如汽車或卡車，作為活動節(jié)點，其他節(jié)點都供該節(jié)點使用。終端設備不時地與其他節(jié)點通信并與之交互，例如云端服務器和邊緣服務器。2) 停車場的邊緣服務器用于本地邊緣計算，完成所有與停車場有關的計算任務，例如云端注冊、位置判斷、車輛管理以及視頻監(jiān)控等。3) 第三方導航用于引導和服務車輛找到目的地停車場。4) 第三方付款用于處理停車活動產(chǎn)生的費用。5) 云端服務器用于與邊緣服務器節(jié)點和終端設備進行交互，存儲和提供一些數(shù)據(jù)量大且時延要求不高的數(shù)據(jù)。

5.2 性質(zhì)表達

為了保證車輛在停車過程中邊緣服務器能夠正常提供所有服務，在邊緣服務器提供服務的過程中，本節(jié)在邊緣服務器部署并行運行時驗證系統(tǒng)，對其行為進行入侵檢測，包括異常檢測和誤用檢測。為了實現(xiàn)異常檢測，首先用UML 順序圖對車輛從進入停車場開始的停車過程中各模塊的行為進行建模，部分模型如圖12 所示。

圖12 智能停車系統(tǒng)部分UML 順序圖

由于本文只關注邊緣服務器行為，因此只需分析邊緣服務器生命線上的相關函數(shù)調(diào)用序列，可用如下PPTL 公式對其進行形式化描述。

其中，操作符+表示對于不同的車輛進入請求，邊緣服務器將不斷重復執(zhí)行各個函數(shù)?？傮w來看，此PPTL 公式表示從某一時刻起，邊緣服務器將循環(huán)執(zhí)行函數(shù)identifyEnter、vehicleReserved、sendSpace、sendStatus、returnStatus、identifyLeave、calculateFee和sendFee。

針對P1公式的運行時驗證能夠?qū)崿F(xiàn)邊緣服務器的異常檢測，實時監(jiān)控其各個函數(shù)是否被順利調(diào)用執(zhí)行，一旦發(fā)現(xiàn)P1公式不被滿足，可立即發(fā)出警告提示。在對邊緣服務器進行異常檢測的同時，可對Smurf、SYN Flood 和Land 攻擊進行誤用檢測，即對3.1.2 節(jié)中相對應的PPTL 公式實施運行時驗證，以判斷攻擊的類型，具體如下

當P2、P3和P4中某一個公式被滿足時，即表明檢測出相應類型的攻擊。

5.3 系統(tǒng)驗證

為了表明所提方法的有效性，針對智能停車系統(tǒng)，本節(jié)將運行時驗證模塊部署在邊緣服務器以實時監(jiān)控P1公式是否被違反（即邊緣服務器不能正常提供服務），以及P2～P4中某個公式是否成立（即檢測到某個DoS 攻擊行為）。在實驗中，使用安卓手機作為終端，5 臺PC 機作為邊緣服務器，騰訊云提供云端服務。

實驗共分為三組，分別使用邊緣服務器中的單個驗證線程來實現(xiàn)傳統(tǒng)的運行時驗證方法，以及3 個和5 個驗證線程實現(xiàn)并行運行時驗證方法，其中每次驗證的序列片段包含1 000 個程序狀態(tài)。在每組實驗中，將一個惡意節(jié)點加入邊緣計算網(wǎng)絡后，對邊緣服務器實施Smurf 攻擊，為了證明所提方法的有效性以及驗證效率的準確性，均重復攻擊10 次。針對Smurf 攻擊的檢測結(jié)果如表3 所示。

表3 中，第一列為待驗證的PPTL 公式，包括用于異常檢測的公式P1以及用于誤用檢測的公式P2～P4；第二列表示驗證工具給出的驗證結(jié)果，即程序是否滿足相應性質(zhì)，P1為×表明檢測出邊緣服務器沒有正常提供服務，P2為√表明檢測出攻擊類型為Smurf 攻擊；第三列至第五列給出了在邊緣服務器中，不同數(shù)量驗證線程提供驗證算力的情況下，每驗證1 000 個狀態(tài)所需要的時間。比較第三列至第五列給出的驗證時間可以發(fā)現(xiàn)，當3 個驗證線程提供驗證算力時，驗證效率最高，而當5 個驗證線程提供驗證算力時，驗證效率反而會降低。這是由于邊緣服務器雖然能夠支持一定數(shù)量的并行線程，但邊緣服務器的CPU 計算能力不強，5 個驗證線程導致CPU 的線程切換開銷過大，影響整體性能?？傮w來看，3 個驗證線程提供驗證算力的情況下，在Smurf 攻擊實施7 s 內(nèi)，本文所提的并行運行時驗證方法能夠檢測出入侵攻擊。針對SYN Flood 和Land 攻擊的檢測結(jié)果能得到相似結(jié)論。

表3 針對Smurf 攻擊的檢測結(jié)果

6 結(jié)束語

針對邊緣計算系統(tǒng)中邊緣服務器面臨的DoS攻擊，本文提出了一種并行運行時驗證方法，該方法結(jié)合誤用檢測和異常檢測，充分利用邊緣服務器的計算與存儲資源。首先使用PPTL 公式，分別描述系統(tǒng)正常狀態(tài)和3 種典型的DoS 攻擊的行為特征；然后將上述兩類PPTL 公式作為待驗證性質(zhì)，在邊緣服務器上部署并行運行時驗證方法，在邊緣服務器程序運行過程中，利用邊緣服務器中的多個驗證線程，完成DoS 攻擊的入侵檢測；最后通過對比實驗，驗證了所提方法的可行性和有效性，并對一個實際的基于邊緣計算的P2P 網(wǎng)絡智能停車系統(tǒng)進行模擬DoS 攻擊和攻擊檢測。實驗表明，所提方法能夠有效識別Smurf、SYN Flood 和Land 攻擊。在今后的研究工作中，將進一步提高基于運行時驗證的入侵檢測效率，且對更多類型的入侵攻擊進行形式化描述與檢測。