王國(guó)卿，莊雷，王瑞民，宋玉，張坤麗

?

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

王國(guó)卿，莊雷，王瑞民，宋玉，張坤麗

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

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

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

1 引言

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3) 真實(shí)性：消息認(rèn)證能夠核實(shí)來(lái)源的真實(shí)。

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

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

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

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

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

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

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

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

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

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

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

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

3.1 預(yù)備知識(shí)

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

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

3.2 形式化表示

使用層次時(shí)間自動(dòng)機(jī)建模，整個(gè)系統(tǒng)表示為3個(gè)層次。

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

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

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

表4 模型中變量的含義

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

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

3.3 層次化建模

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

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

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

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

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

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

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

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

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

圖9 認(rèn)證中心模型（AC）

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

圖11 異常處理模型（Exception）

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

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

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

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

4.1 UPPAAL工具簡(jiǎn)介

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

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

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

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

1) 機(jī)密性驗(yàn)證

A[] AC.AlertToManager imply==0

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

2) 可用性驗(yàn)證

在頂層模型，檢測(cè)網(wǎng)關(guān)認(rèn)證狀態(tài)可達(dá)，可確保網(wǎng)關(guān)的合法身份和輪詢周期的不斷進(jìn)行；中間層及底層各模型入口狀態(tài)可達(dá)，可確保為用戶提供相應(yīng)服務(wù)。待驗(yàn)證性質(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) 真實(shí)性驗(yàn)證

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

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

4) 頑健性驗(yàn)證

A[] not deadlock

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

5) 完整性驗(yàn)證

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

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

6) 新鮮性驗(yàn)證

整個(gè)模型中設(shè)置了多處時(shí)間約束，目的就是保證消息的時(shí)效性。待驗(yàn)證性質(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驗(yàn)證器對(duì)上述6個(gè)性質(zhì)的全部語(yǔ)句逐條進(jìn)行驗(yàn)證，驗(yàn)證結(jié)果如表5所示。

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

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

5 結(jié)束語(yǔ)

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

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

下一步研究工作的重點(diǎn)有2個(gè)方面。

1) 進(jìn)一步研究其他安全協(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ù)，在實(shí)際環(huán)境中具體實(shí)現(xiàn)物聯(lián)網(wǎng)網(wǎng)關(guān)安全系統(tǒng)。

[1] 王良民, 熊書(shū)明. 物聯(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] 錢(qián)志鴻, 王義君. 物聯(lián)網(wǎng)技術(shù)與應(yīng)用研究[J]. 電子學(xué)報(bào), 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è)計(jì)與實(shí)現(xiàn)[J]. 計(jì)算機(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ì)[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ú)線傳感網(wǎng)絡(luò)中間件研究[J]. 通信學(xué)報(bào), 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é)報(bào)(自然科學(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

國(guó)家自然科學(xué)基金資助項(xiàng)目（No.61379079）；河南省科技攻關(guān)計(jì)劃基金資助項(xiàng)目（No.172102210478）；河南省國(guó)際科技合作計(jì)劃基金資助項(xiàng)目（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)

王國(guó)卿（1989-），男，山東臨沂人，鄭州大學(xué)博士生，主要研究方向?yàn)槟Ｐ蜋z測(cè)、形式化分析、物聯(lián)網(wǎng)安全等。

莊雷（1963-），女，山東日照人，博士，鄭州大學(xué)教授、博士生導(dǎo)師，主要研究方向?yàn)槟Ｐ蜋z測(cè)、未來(lái)網(wǎng)絡(luò)架構(gòu)、網(wǎng)絡(luò)虛擬化等。

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

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

張坤麗（1977-），女，河南鞏義人，鄭州大學(xué)講師，主要研究方向?yàn)槿斯ぶ悄?、自然語(yǔ)言處理等。