王國卿，莊雷，王瑞民，宋玉，張坤麗

?

基于時間自動機的物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)的建模及驗證

王國卿，莊雷，王瑞民，宋玉，張坤麗

（鄭州大學(xué)信息工程學(xué)院，河南 鄭州 450001）

物聯(lián)網(wǎng)是一個多網(wǎng)異構(gòu)融合網(wǎng)絡(luò)，其感知層常面臨各類安全威脅。物聯(lián)網(wǎng)網(wǎng)關(guān)作為感知層和網(wǎng)絡(luò)層的橋梁，應(yīng)當(dāng)具備安全管理功能，防止安全問題向上層擴散。針對物聯(lián)網(wǎng)網(wǎng)關(guān)目前安全方面的不足，以物聯(lián)網(wǎng)網(wǎng)關(guān)中間件技術(shù)為平臺，設(shè)計一個通用的物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)。該系統(tǒng)可以嵌入不同的安全協(xié)議或算法，然后進行建模與分析，能夠輔助安全網(wǎng)關(guān)的設(shè)計和具體實現(xiàn)。利用時間自動機對系統(tǒng)進行形式化建模與驗證，驗證結(jié)果表明物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)滿足機密性、可用性、真實性、頑健性、完整性和新鮮性6項安全需求。

物聯(lián)網(wǎng)網(wǎng)關(guān)；安全系統(tǒng)；中間件；時間自動機；模型檢測

1 引言

隨著第4次工業(yè)革命的到來，人類社會正逐步進入一個萬物互聯(lián)的時代，物聯(lián)網(wǎng)（IoT, Internet of things）應(yīng)運而生。物聯(lián)網(wǎng)是繼計算機、互聯(lián)網(wǎng)和移動通信之后的又一次革新發(fā)展，是信息化時代的重要發(fā)展階段[1]。物聯(lián)網(wǎng)是由具有自我標(biāo)識、感知和智能的物理實體基于通信技術(shù)相互連接而成的網(wǎng)絡(luò)，這些物理實體可以自發(fā)地進行協(xié)同和互動，以實現(xiàn)智能的識別、定位、監(jiān)控和管理，從而將人類社會、信息空間和物理系統(tǒng)進行有機的融合[2]。

物聯(lián)網(wǎng)的體系結(jié)構(gòu)如圖1所示，共分為3層。其中，感知層負責(zé)隨時獲取物理實體的信息，并將應(yīng)用層指令反饋給物理實體；網(wǎng)絡(luò)層負責(zé)實時傳輸各類信息、數(shù)據(jù)和指令；應(yīng)用層負責(zé)對海量數(shù)據(jù)和信息進行分析、處理及決策，接收用戶的服務(wù)定制。3個層次并不是相互獨立的，而是相互支撐、相互影響的，進而搭建起整個體系架構(gòu)。

網(wǎng)關(guān)技術(shù)在傳統(tǒng)互聯(lián)網(wǎng)中的運用比較成熟，應(yīng)用到物聯(lián)網(wǎng)體系中，將成為連接感知網(wǎng)絡(luò)與傳統(tǒng)通信網(wǎng)絡(luò)的紐帶。作為物聯(lián)網(wǎng)網(wǎng)關(guān)，可以實現(xiàn)感知網(wǎng)絡(luò)與通信網(wǎng)絡(luò)以及不同類型感知網(wǎng)絡(luò)之間的協(xié)議轉(zhuǎn)換[3]。物聯(lián)網(wǎng)網(wǎng)關(guān)還可以提供管理功能和安全策略[4]。通過物聯(lián)網(wǎng)網(wǎng)關(guān)設(shè)備可以管理底層的感知節(jié)點和運行設(shè)備，監(jiān)測各物理實體的運行狀態(tài)，實現(xiàn)遠程控制；帶有安全策略的物聯(lián)網(wǎng)網(wǎng)關(guān)可以屏蔽傳感器網(wǎng)絡(luò)和移動通信網(wǎng)的異構(gòu)性，實現(xiàn)從協(xié)議級到應(yīng)用級的保護。

在物聯(lián)網(wǎng)網(wǎng)關(guān)的體系結(jié)構(gòu)方面，許多學(xué)者設(shè)計并實現(xiàn)了網(wǎng)關(guān)的基本功能[5~8]，主要包括感知接入、協(xié)議適配、協(xié)議轉(zhuǎn)換、消息傳輸?shù)?，解決了物聯(lián)網(wǎng)網(wǎng)關(guān)的關(guān)鍵問題，即對異構(gòu)網(wǎng)絡(luò)的不同通信協(xié)議進行轉(zhuǎn)換和底層通信協(xié)議到上層通信協(xié)議的轉(zhuǎn)換，并在物聯(lián)網(wǎng)網(wǎng)關(guān)的管理與控制時，建立可統(tǒng)一識別指令及標(biāo)準(zhǔn)。但在網(wǎng)關(guān)安全方面沒有詳細設(shè)計，或默認安全策略已經(jīng)完備，或只是簡單說明而沒有具體實現(xiàn)。

圖1 物聯(lián)網(wǎng)體系結(jié)構(gòu)

關(guān)于物聯(lián)網(wǎng)網(wǎng)關(guān)安全方面的研究，文獻[9]針對IoT中機器對機器（M2M, machine to machine）通信，設(shè)計了一個安全網(wǎng)關(guān)應(yīng)用（SGA, security gateway application），其中，包括對稱密鑰加密協(xié)商功能、安全密鑰交換生成功能和信息安全傳遞功能，能夠滿足M2M服務(wù)層的基本安全需求；文獻[10]設(shè)計了一種基于動態(tài)優(yōu)先級調(diào)度算法的異構(gòu)物聯(lián)網(wǎng)網(wǎng)關(guān)，可支持RS485、藍牙、ZigBee等協(xié)議，通過實現(xiàn)高層協(xié)議保證了物聯(lián)網(wǎng)網(wǎng)關(guān)的數(shù)據(jù)安全性和可靠性；文獻[11]提出了一種結(jié)合物聯(lián)網(wǎng)智能設(shè)備與控制系統(tǒng)網(wǎng)關(guān)的實時響應(yīng)模型，通過加強身份驗證與授權(quán)的控制，以提高系統(tǒng)的安全性；文獻[12]討論了傳感器網(wǎng)絡(luò)、家庭網(wǎng)關(guān)和應(yīng)用終端的安全問題及相應(yīng)的解決方案，通過對這3個部分安全性進行有機整合，實現(xiàn)信息傳輸和用戶隱私的安全保護，最大限度地保護智能家居的安全；文獻[13]設(shè)計實現(xiàn)了基于Modbus協(xié)議的物聯(lián)網(wǎng)匯聚安全網(wǎng)關(guān)，通過在應(yīng)用層構(gòu)建網(wǎng)關(guān)覆蓋網(wǎng)，提供網(wǎng)關(guān)信任管理，有效解決了網(wǎng)關(guān)海量數(shù)據(jù)的擁塞控制問題，保證了網(wǎng)關(guān)虛擬網(wǎng)絡(luò)的安全性。上述研究成果大多針對某一特殊場景，例如，文獻[11,13]主要應(yīng)用于工業(yè)物聯(lián)網(wǎng)，文獻[12]主要應(yīng)用于智能家居。文獻[9,10]雖然應(yīng)用場景更寬泛一些，但在安全體系的設(shè)計上存在一些不足。文獻[9]集中考慮了密鑰管理體系，對其他安全技術(shù)沒有涉及；文獻[10]的安全網(wǎng)關(guān)在應(yīng)用層級，沒有考慮連接感知層和網(wǎng)絡(luò)層的網(wǎng)關(guān)安全性。

基于對當(dāng)前研究現(xiàn)狀的分析，針對物聯(lián)網(wǎng)網(wǎng)關(guān)安全方案存在的不足，利用物聯(lián)網(wǎng)安全常用的密鑰管理、身份認證、入侵檢測等技術(shù)，設(shè)計了一個通用的物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)。通過對系統(tǒng)的形式化分析與驗證，保證了系統(tǒng)的機密性、可用性、真實性、頑健性、完整性、新鮮性等相關(guān)安全特性，為網(wǎng)關(guān)中間件的設(shè)計和實現(xiàn)提供了理論框架。物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)可以嵌入各類安全協(xié)議或算法，然后進行建模與分析，驗證系統(tǒng)是否正確與可靠，對網(wǎng)關(guān)的具體設(shè)計和實現(xiàn)具有指導(dǎo)意義。

2 物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)的設(shè)計

物聯(lián)網(wǎng)是信息技術(shù)發(fā)展的趨勢，物聯(lián)網(wǎng)應(yīng)用在給人們生活帶來便利的同時，也帶來了很多安全隱患。尤其物聯(lián)網(wǎng)感知層作為物聯(lián)網(wǎng)體系結(jié)構(gòu)的底層，直接面向現(xiàn)實環(huán)境，承擔(dān)著信息感知和命令執(zhí)行的重任，其安全問題尤為重要。

物聯(lián)網(wǎng)網(wǎng)關(guān)作為感知層和網(wǎng)絡(luò)層的橋梁，由于硬件設(shè)備的迅猛發(fā)展，其功能不再局限于單一的協(xié)議轉(zhuǎn)換，可以向服務(wù)提供、設(shè)備管理、安全檢測等功能擴展[14]；中間件技術(shù)可屏蔽底層硬件細節(jié)，對外提供統(tǒng)一抽象接口，使用跨層設(shè)計的思想，在滿足應(yīng)用動態(tài)性的同時可滿足應(yīng)用異構(gòu)性，為安全系統(tǒng)的實現(xiàn)提供了平臺[15]。

2.1 物聯(lián)網(wǎng)網(wǎng)關(guān)安全需求

物聯(lián)網(wǎng)感知層的安全異常重要，作為底層感知和執(zhí)行設(shè)備，所有物聯(lián)網(wǎng)應(yīng)用能否正常運行全部依賴于感知層是否安全可靠。由于感知層自身有限的存儲空間和計算能力、有限的帶寬和通信能量以及網(wǎng)絡(luò)協(xié)議安全形式的多樣，感知層經(jīng)常面臨通信信道攻擊、拒絕服務(wù)攻擊、節(jié)點捕獲、假冒攻擊、路由協(xié)議攻擊等安全威脅[16]，如表1所示。

表1 物聯(lián)網(wǎng)感知層面臨的安全威脅

針對上述安全威脅，物聯(lián)網(wǎng)網(wǎng)關(guān)需要彌補感知層能力的不足，避免安全缺陷從感知層通過網(wǎng)關(guān)傳遞到網(wǎng)絡(luò)層，應(yīng)滿足以下6個方面的安全需求[17]。

1) 機密性：消息對非授權(quán)方是保密的。

2) 可用性：按約定向合法用戶提供服務(wù)。

3) 真實性：消息認證能夠核實來源的真實。

4) 頑健性：面對不確定因素具有強適應(yīng)性。

5) 完整性：收到的信息與源信息完全一致。

6) 新鮮性：保證消息的時效性。

網(wǎng)關(guān)技術(shù)具有有效的安全隔離、靈活的業(yè)務(wù)代理、成熟的技術(shù)積累等特點。為了應(yīng)對感知層安全威脅，避免感知層安全問題向上擴散，信息加密、認證與訪問控制、入侵檢測等信息安全技術(shù)可以綜合運用到物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)中，能夠和其他相關(guān)技術(shù)實現(xiàn)較好的銜接，從而滿足物聯(lián)網(wǎng)網(wǎng)關(guān)安全需求?；诰W(wǎng)關(guān)中間件及安全支撐平臺構(gòu)建的物聯(lián)網(wǎng)網(wǎng)關(guān)安全技術(shù)框架如圖2所示。

2.2 網(wǎng)關(guān)安全系統(tǒng)的邏輯流程

在傳感器網(wǎng)絡(luò)中，節(jié)點通過各種方式大量部署在被感知對象內(nèi)部或附近，這些節(jié)點通過自組織方式構(gòu)成無線網(wǎng)絡(luò)，以協(xié)作的方式感知、采集和處理網(wǎng)絡(luò)覆蓋區(qū)域中特定的信息，可以實現(xiàn)對任意地點信息在任意時間的采集、處理和分析。對于新加入或退出的節(jié)點，自組織網(wǎng)絡(luò)可設(shè)定生存時間檢測，通過多跳的方式連接至匯聚節(jié)點，節(jié)點收到數(shù)據(jù)連接安全網(wǎng)關(guān)，整個系統(tǒng)通過任務(wù)管理器來管理和控制。

圖2 物聯(lián)網(wǎng)網(wǎng)關(guān)安全技術(shù)框架

根據(jù)所設(shè)計的物聯(lián)網(wǎng)網(wǎng)關(guān)安全技術(shù)框架，物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)實現(xiàn)在物聯(lián)網(wǎng)網(wǎng)關(guān)中間件平臺上，其在完成物聯(lián)網(wǎng)網(wǎng)關(guān)基本功能的基礎(chǔ)上，添加了加密傳輸、輪詢檢測、身份校驗、異常處理等子模塊。物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)的邏輯流程如圖3所示。

為了便于建模與檢測，僅抽取主要流程分析并進行適當(dāng)假設(shè)。物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)的頂層主模塊在網(wǎng)關(guān)進行消息轉(zhuǎn)發(fā)等基本功能的基礎(chǔ)上實現(xiàn)了網(wǎng)關(guān)合法性認證及入侵檢測，以確保網(wǎng)關(guān)的安全啟動和運行，然后進入中間層輪詢模塊。終端在輪詢時一般處于工作狀態(tài)，需要安全系統(tǒng)發(fā)出控制指令檢測終端狀態(tài)。對于感知終端，由于感知節(jié)點的大規(guī)模和隨機性，安全系統(tǒng)主要連接匯聚節(jié)點進行監(jiān)測，匯聚節(jié)點的處理能力、存儲能力、通信能力相對較強，在實現(xiàn)通信協(xié)議棧轉(zhuǎn)換的同時，可發(fā)布網(wǎng)關(guān)的監(jiān)測任務(wù)。對于執(zhí)行終端，如果設(shè)備正在運行，則令設(shè)備在合法時間內(nèi)運行一段時間，如果在規(guī)定時間內(nèi)設(shè)備狀態(tài)能正確返回到安全系統(tǒng)，則認為輪詢成功，設(shè)備處于正常狀態(tài)，生成監(jiān)控信息。底層主要提供了密鑰算法、統(tǒng)一認證、入侵檢測、異常處理等安全服務(wù)，應(yīng)用于頂層和中間層的各個環(huán)節(jié)，以保證安全系統(tǒng)整體的安全可靠。

若暫不考慮底層安全服務(wù)模塊所選策略，設(shè)網(wǎng)關(guān)安全系統(tǒng)所需管理的終端數(shù)為，則頂層主模塊的時間復(fù)雜度為()，中間層輪詢模塊的時間復(fù)雜度為(2)，所以網(wǎng)關(guān)安全系統(tǒng)的時間復(fù)雜度為(2)。若進一步考慮底層安全服務(wù)模塊，則時間復(fù)雜度受到底層所選策略的影響可能會提高，但由于底層所選策略通常是成熟的算法，因此，應(yīng)用到網(wǎng)關(guān)安全系統(tǒng)中的總時間復(fù)雜度是可以接受的。

3 基于時間自動機的網(wǎng)關(guān)安全系統(tǒng)建模

由于物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)不僅需要滿足運行結(jié)果的邏輯正確性，部分功能還需要滿足時間的正確性，因此，選擇時間自動機進行形式化分析，可有效刻畫物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)的時間屬性，并可借助模型檢測工具UPPAAL進行驗證。

3.1 預(yù)備知識

圖3 物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)的邏輯流程

根據(jù)物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)流程的分層設(shè)計，可考慮引入層次時間自動機進行建模，它以層次方式對時間自動機進行了擴展，能有效解決建模時的復(fù)雜流程與蘊含邏輯。

3.2 形式化表示

使用層次時間自動機建模，整個系統(tǒng)表示為3個層次。

表2 模型中狀態(tài)位置的含義

其中，Top表示頂層主模塊，Middle表示中間層輪詢模塊，底層安全服務(wù)模塊包括KMS密鑰管理系統(tǒng)、AC認證中心、IDS入侵檢測系統(tǒng)及Exception異常處理。模型中狀態(tài)位置、同步通道、變量等符號的含義如表2~表4所示。

表3 模型中同步通道的含義

表4 模型中變量的含義

圖4 頂層主模塊模型（Top）

中間層及底層各模塊形式化模型依據(jù)頂層主模塊模型，結(jié)合圖例較容易得出，限于篇幅不再詳述。

3.3 層次化建模

根據(jù)層次時間自動機的定義，首先建立頂層主模塊模型，如圖4所示。

對于中間層輪詢模塊，通過通道StartMiddle開啟輪詢，并由通道FinishMiddle返回頂層主模塊。CheckCategory狀態(tài)控制輪詢邏輯的終端是感知終端還是執(zhí)行終端，兩者有不同的流程處理。所建立的中間層輪詢模塊模型如圖5所示。

圖5 中間層輪詢模塊模型（Middle）

當(dāng)=2時，對感知終端進行輪詢；當(dāng)=3時，對執(zhí)行終端進行輪詢。在2個輪詢流程中，根據(jù)不同的需求通過同步通道調(diào)用底層安全服務(wù)，具體過程可由狀態(tài)位置、同步通道、變量的含義解讀，在此不再贅述。特別地，在等待計時階段和設(shè)備保持運行狀態(tài)階段也添加了時間約束，例如，執(zhí)行終端需在5個時間單位內(nèi)返回運行狀態(tài)，持續(xù)運行需保持25個時間單位以上，以此來保證安全需求的新鮮性。

頂層主模塊模型和中間層輪詢模塊模型是物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)的通用框架，其安全性的實現(xiàn)最終依賴于底層的安全服務(wù)模塊，因此，需要完善底層安全服務(wù)模塊的模型構(gòu)建。圖3中給出了底層各個安全服務(wù)子模塊的常用算法或協(xié)議，用戶可根據(jù)實際場景和需要選擇適合的算法協(xié)議，然后在此框架下進行相應(yīng)的建模分析，從而指導(dǎo)網(wǎng)關(guān)安全系統(tǒng)在網(wǎng)關(guān)中間件平臺的設(shè)計與實現(xiàn)。

為了驗證所設(shè)計的物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)是否滿足安全需求，擬選取基于時間標(biāo)簽的AES密碼算法[20]為核心，建立密鑰管理、身份認證、入侵檢測及異常處理模型。需要說明的是，加、解密是密鑰管理系統(tǒng)常用的邏輯流程，為使結(jié)構(gòu)更加清晰，分別對加、解密進行了單獨建模。底層安全服務(wù)模塊建模如圖6~圖11所示。

圖6 密鑰管理系統(tǒng)模型（KMS）

圖7 AES算法加密模型（AESEncryption）

圖8 AES算法解密模型（AESDecryption）

圖9 認證中心模型（AC）

圖10 入侵檢測系統(tǒng)模型（IDS）

圖11 異常處理模型（Exception）

簡要對密鑰管理系統(tǒng)模型和基于時間標(biāo)簽的AES密碼算法進行介紹，其他安全服務(wù)模型限于篇幅不再贅述。密鑰管理系統(tǒng)首先檢測，如果=1，則更新密鑰，與終端通信獲取終端密鑰信息進行解密校驗，判斷是否需要更新，若需要更新則通過數(shù)據(jù)中心密鑰池分配新的密鑰，然后加密傳送回終端；如果=2，則驗證密鑰，將終端傳來的密文進行解密，然后提交數(shù)據(jù)中心比對處理，最后記錄數(shù)據(jù)中心反饋的驗證信息。

AES密碼算法包括加密過程、解密過程和密鑰擴展過程。其加密過程共10輪（或12輪、14輪），前9輪（或前11輪、前13輪）由字節(jié)代換、行移位、列混合和加輪密鑰等4種變換迭代完成，最后一輪沒有列混合變換；解密過程與加密過程的輪數(shù)一致，并且前若干輪變換是加密過程的逆變換，依次是逆字節(jié)代換、逆行移位、逆列混合和加輪密鑰變換，最后一輪沒有逆列混合變換。基于時間標(biāo)簽的AES密碼算法是在密鑰擴展階段引入時間標(biāo)簽，使輪密鑰可隨時間的變化進行動態(tài)更新，進而實現(xiàn)密文的變化，可以更有效地保證機密信息的安全性。因此，在建模過程中對加、解密模型的部分狀態(tài)位置和邊界添加了時間約束，以體現(xiàn)時間標(biāo)簽屬性。

4 網(wǎng)關(guān)安全系統(tǒng)的形式化驗證

可以對建立好的物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)的層次時間自動機模型使用模型檢測工具UPPAAL進行驗證，能夠有效發(fā)現(xiàn)模型的錯誤，并驗證模型的安全性質(zhì)是否滿足。

4.1 UPPAAL工具簡介

UPPAAL[21]是瑞典Uppsala大學(xué)和丹麥Aalborg大學(xué)于1995年聯(lián)合發(fā)布的基于時間自動機的自動化驗證工具，其名字的由來是2所學(xué)校名稱的前3個字母組合。UPPAAL的操作界面包含編輯器（editor）、模擬器（simulator）、驗證器（verifier）3個部分。編輯器用于對要分析的問題進行建模和編輯，是一個圖形化交互界面，可進行自定義及編程；模擬器用于模擬模型的執(zhí)行過程，可選擇步進執(zhí)行或隨機執(zhí)行，工具將生成時序圖和消息控制序列，以幫助設(shè)計者發(fā)現(xiàn)錯誤原因和路徑；驗證器用于驗證給定性質(zhì)是否滿足，在每個性質(zhì)驗證結(jié)束后給出驗證結(jié)果、驗證時間和內(nèi)存消耗，性質(zhì)的表示使用巴科斯范式（BNF, Backus-Naur form）描述。

4.2 安全需求性質(zhì)的驗證

本文通過編輯器建立物聯(lián)網(wǎng)安全系統(tǒng)模型，可以在模擬器模擬各層次的交互情況。時序圖詳細展示了各層次對象間的交互情況及各時間自動機模型的執(zhí)行情況，消息控制序列以圖文形式展示了各對象的運行流程和通信狀態(tài)，它們對于模型的分析和調(diào)試有極大幫助。

模擬器的模擬運行，其擇路條件隨機，不一定能夠完全遍歷模型狀態(tài)，因此，需要使用驗證器進行全面驗證。2.1節(jié)提到，物聯(lián)網(wǎng)網(wǎng)關(guān)的安全需求需要滿足機密性、可用性、真實性、頑健性、完整性、新鮮性6個性質(zhì)，使用BNF語法對上述性質(zhì)進行公式化表示，然后利用驗證器進行驗證。

1) 機密性驗證

A[] AC.AlertToManager imply==0

加密信息通過網(wǎng)關(guān)時，若密鑰驗證失敗，則安全監(jiān)控邏輯進行報警，拒絕消息繼續(xù)傳輸。

2) 可用性驗證

在頂層模型，檢測網(wǎng)關(guān)認證狀態(tài)可達，可確保網(wǎng)關(guān)的合法身份和輪詢周期的不斷進行；中間層及底層各模型入口狀態(tài)可達，可確保為用戶提供相應(yīng)服務(wù)。待驗證性質(zhì)表示如下。

E<> Top.CheckGS

E<> Top.EnterMiddle imply Middle.CheckCateg-ory

E<> Middle.UpdateKey imply KMS.CheckKT

E<> Top.Authentication imply AC.CheckCate-gory

E<> Middle.IntrusionDetection imply IDS.Init

E<> Top.Verify imply Exception.CheckEL

3) 真實性驗證

E<>==1 imply AC.==1

在消息認證時，需要同步驗證消息來源節(jié)點的私鑰以認證身份的合法性。如果認證中心的認證成功，則認為終端狀態(tài)正常，說明源節(jié)點是系統(tǒng)內(nèi)節(jié)點，而不是外部偽造的。

4) 頑健性驗證

A[] not deadlock

系統(tǒng)不存在死鎖，即面對任何情況都有處理路徑可執(zhí)行。

5) 完整性驗證

A[] AC.ObtainMessage imply AC.==1

消息認證碼（MAC, message authentication code）可同時提供基于校驗和的數(shù)據(jù)完整性和基于秘密密鑰的數(shù)據(jù)源完整性。如果接受的消息最終通過Hash運算處理后，2次計算的值相等，則認為數(shù)據(jù)未被篡改，解密并獲取發(fā)送方的信息。

6) 新鮮性驗證

整個模型中設(shè)置了多處時間約束，目的就是保證消息的時效性。待驗證性質(zhì)表示如下。

A[] Top.Restart imply≤300

A[] Top.Record imply≤600

A[] Middle.RetrieveData imply Middle.≥30

A[] Middle.WaitDevice imply Middle.≤5

A[] IDS.Analysis imply IDS.≤60

A[] AESEncryption.MUX imply AESEncryption.≤4

A[] AESDecryption.InShiftRows_ imply≥100

UPPAAL驗證器對上述6個性質(zhì)的全部語句逐條進行驗證，驗證結(jié)果如表5所示。

表5 模型檢測結(jié)果

驗證結(jié)果表明，所有性質(zhì)均通過驗證，所設(shè)計的物聯(lián)網(wǎng)安全系統(tǒng)滿足機密性、可用性、真實性、頑健性、完整性、新鮮性等安全需求。

5 結(jié)束語

物聯(lián)網(wǎng)作為新一代信息技術(shù)的重要組成部分，安全問題應(yīng)當(dāng)?shù)玫阶銐蛑匾?。物?lián)網(wǎng)感知層直面真實環(huán)境，其底層感知和執(zhí)行設(shè)備常常面臨各類安全威脅。物聯(lián)網(wǎng)網(wǎng)關(guān)負責(zé)連接感知層與網(wǎng)絡(luò)層，可彌補感知層能力的不足，避免安全問題的進一步擴散。目前，對物聯(lián)網(wǎng)網(wǎng)關(guān)體系結(jié)構(gòu)的研究主要解決了基本功能的實現(xiàn)，安全策略涉及不多；對物聯(lián)網(wǎng)網(wǎng)關(guān)安全措施的研究一般都有實際應(yīng)用背景，可借鑒性與通用性不強。

基于上述分析，結(jié)合現(xiàn)有的密鑰管理、身份認證、入侵檢測等安全技術(shù)，設(shè)計了一個通用的物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)，可在網(wǎng)關(guān)中間件平臺部署。利用時間自動機對系統(tǒng)3個層次進行形式化建模，并使用模型驗證工具UPPAAL進行性質(zhì)驗證，結(jié)果表明網(wǎng)關(guān)安全系統(tǒng)滿足機密性、可用性、真實性、頑健性、完整性、新鮮性等安全性質(zhì)。物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)還可以根據(jù)實際需要調(diào)整底層安全協(xié)議或算法，然后重新進行建模分析，有助于發(fā)現(xiàn)設(shè)計漏洞，輔助網(wǎng)關(guān)的設(shè)計和實現(xiàn)。

下一步研究工作的重點有2個方面。

1) 進一步研究其他安全協(xié)議或算法的建模方法，以便有效嵌入物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)，從而提升系統(tǒng)的普適性。

2) 結(jié)合物聯(lián)網(wǎng)網(wǎng)關(guān)的硬件設(shè)備及中間件技術(shù)，在實際環(huán)境中具體實現(xiàn)物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)。

[1] 王良民, 熊書明. 物聯(lián)網(wǎng)工程概論[M]. 北京: 清華大學(xué)出版社, 2011:45-52.

WANG L M, XIONG S M. The introduction of IoT engineering[M]. Beijing: Tsinghua University Press, 2011:45-52.

[2] 錢志鴻, 王義君. 物聯(lián)網(wǎng)技術(shù)與應(yīng)用研究[J]. 電子學(xué)報, 2012, 40(5):1023-1029.

QIAN Z H, WANG Y J. IoT technology and application[J]. Acta Electronica Sinica, 2012, 40(5):1023-1029.

[3] MORABITO R, BEIJAR N. A framework based on SDN and containers for dynamic service chains on IoT gateways[C]//The Workshop on Hot Topics in Container Networking and Networked Systems. 2017:42-47.

[4] SATHYADEVAN S, VEJESH V, DOSS R, et al. Portguard an authentication tool for securing ports in an IoT gateway[C]//IEEE International Conference on Pervasive Computing and Communications Workshops. 2017:624-629.

[5] SCHRICKTE L F, MONTEZ C B, OLIVEIRA R S D, et al. Design and implementation of a 6LoWPAN gateway for wireless sensor networks integration with the internet of things[J]. International Journal of Embedded Systems, 2016, 8(5/6):380-390.

[6] 陳琦, 韓冰, 秦偉俊, 等. 基于Zigbee/GPRS物聯(lián)網(wǎng)網(wǎng)關(guān)系統(tǒng)的設(shè)計與實現(xiàn)[J]. 計算機研究與發(fā)展, 2011, 48(s2):367-372.

CHEN Q, HAN B, QIN W J, et al. Design and implementation of the IoT gateway based on Zigbee/GPRS protocol[J]. Journal of Computer Research and Development, 2011, 48(s2):367-372.

[7] ZHANG L, ALHARBE N R, ATKINS A S. A self-adaptive distributed decision support model for Internet of things applications[J]. Transactions of the Institute of Measurement and Control, 2017, 39(4): 404-419.

[8] 羅俊海, 周應(yīng)賓, 鄧霄博. 物聯(lián)網(wǎng)網(wǎng)關(guān)系統(tǒng)設(shè)計[J]. 電信科學(xué), 2011, 27(2):105-110.

LUO J H, ZHOU Y B, DENG X B. Design for gateway system in Internet of things[J]. Telecommunications Science, 2011, 27(2): 105-110.

[9] CHEN H C, YOU I, WENG C E, et al. A security gateway application for end-to-end M2M communications[J]. Computer Standards & Interfaces, 2016, 44(C):85-93.

[10] MIN D, XIAO Z, SHENG B, et al. Design and implementation of heterogeneous IoT gateway based on dynamic priority scheduling algorithm[J]. Transactions of the Institute of Measurement and Control, 2014, 36(7):924-931.

[11] CONDRY M W, NELSON C B. Using smart edge IoT devices for safer, rapid response with industry IoT control operations[J]. Proceedings of the IEEE, 2016, 104(5):938-946.

[12] LI F, WAN Z, XIONG X, et al. Research on sensor-gateway-terminal security mechanism of smart home based on IoT[C]//IoT Workshop 2012, CCIS 312. 2012: 415-422.

[13] 石希, 陳震, 汪東升, 等. 物聯(lián)網(wǎng)匯聚安全網(wǎng)關(guān)關(guān)鍵技術(shù)研究[J]. 信息網(wǎng)絡(luò)安全, 2012(6):85-89.

SHI X, CHEN Z, WANG D S, et al. A research of the key technology of the aggregative security gateway of Internet of things[J]. Netinfo Security, 2012(6):85-89.

[14] SERDAROGLU K C, BAYDERE S. WiSEGATE: wireless sensor network gateway framework for Internet of things[J]. Wireless Networks, 2015, 22(5):1-17.

[15] 羅娟, 顧傳力, 李仁發(fā). 基于角色的無線傳感網(wǎng)絡(luò)中間件研究[J]. 通信學(xué)報, 2011, 32(1):79-86.

LUO J, GU C L, LI R F. Researches on role-based middleware in wireless sensor networks[J]. Journal on Communications, 2011, 32(1):79-86.

[16] 楊光, 耿貴寧, 都婧, 等. 物聯(lián)網(wǎng)安全威脅與措施[J]. 清華大學(xué)學(xué)報(自然科學(xué)版), 2011, 51(10):1335-1340.

YANG G, GENG G N, DU J, et al. Security threats and measures for the Internet of things[J]. Journal of Tsinghua University (Science and Technology), 2011, 51(10):1335-1340.

[17] 王浩, 鄭武, 謝昊飛, 等. 物聯(lián)網(wǎng)安全技術(shù)[M]. 北京: 人民郵電出版社, 2016:5-17.

WANG H, ZHENG W, XIE H F, et al. IoT security technology[M]. Beijing: Posts & Telecom Press, 2016:5-17.

[18] ALUR R, DILL D L. A theory of timed automata[J]. Theoretical Computer Science, 1994, 126(2):183-235.

[19] DAVID A, OLIVER M M. From HUPPAAL to UPPAAL: a translation from hierarchical timed automata to flat timed automata[R]. BRICS Report Series RS-01-11, Department of Computer Science, University of Aarhus, 2001.

[20] YIN A, WANG S. A novel encryption scheme based on timestamp in gigabit ethernet passive optical network using AES-128[J]. Optik, 2014, 125(3):1361-1365.

[21] BEHRMANN G, DAVID A, LARSEN K G. A tutorial on UPPAAL[M]//Formal Methods for the Design of Real-Time Systems. Springer Berlin Heidelberg, 2004:200-236.

Modeling and verifying based on timed automata of Internet of things gateway security system

WANG Guoqing, ZHUANG Lei, WANG Ruimin, SONG Yu, ZHANG Kunli

School of Information Engineering, Zhengzhou University, Zhengzhou 450001, China

The Internet of things (IoT) is a multiple heterogeneous network, and its perception layer is often faced with various security threats. As the bridge between the perception layer and the network layer, the IoT gateway should have the security management function to prevent the security issue from spreading to the upper layer. According to the current security deficiencies in IoT gateway, a universal IoT gateway security system was proposed based on the IoT gateway middleware technology. Various security protocols or algorithms can be embedded in IoT gateway security system, and the modeling and analysis can help the design and implementation of IoT gateway. The formal modeling and verification of the IoT gateway security system was performed by timed automata. The results show that the IoT gateway security system satisfies the security properties of confidentiality, availability, authenticity, robustness, integrity and freshness.

IoT gateway, security system, middleware, timed automata, model checking

TP393

A

10.11959/j.issn.1000-436x.2018042

2017-10-12；

2018-02-20

莊雷，ielzhuang@zzu.edn.cn

國家自然科學(xué)基金資助項目（No.61379079）；河南省科技攻關(guān)計劃基金資助項目（No.172102210478）；河南省國際科技合作計劃基金資助項目（No.152102410021）

The National Natural Science Foundation of China (No.61379079), The Science and Technology Key Project of Henan Province (No.172102210478), The International Cooperation Program of Henan Province (No.152102410021)

王國卿（1989-），男，山東臨沂人，鄭州大學(xué)博士生，主要研究方向為模型檢測、形式化分析、物聯(lián)網(wǎng)安全等。

莊雷（1963-），女，山東日照人，博士，鄭州大學(xué)教授、博士生導(dǎo)師，主要研究方向為模型檢測、未來網(wǎng)絡(luò)架構(gòu)、網(wǎng)絡(luò)虛擬化等。

王瑞民（1974-），男，河南安陽人，博士，鄭州大學(xué)副教授，主要研究方向為密碼學(xué)、信息安全、物聯(lián)網(wǎng)安全等。

宋玉（1969-），男，河南鄧州人，鄭州大學(xué)副教授，主要研究方向為數(shù)據(jù)挖掘、物聯(lián)網(wǎng)體系結(jié)構(gòu)、人工智能等。

張坤麗（1977-），女，河南鞏義人，鄭州大學(xué)講師，主要研究方向為人工智能、自然語言處理等。