[發明專利]計及信息時效的嵌入式裝置安全通信協議驗證方法和系統

在審

• 申請號: 202010021115.4
• 申請日: 2020-01-09
• 公開（公告）號: CN111211945A
• 公開（公告）日: 2020-05-29
• 發明（設計）人: 梁云;黃莉;倪傳坤;汪強;陳獻慶;童和欽;張喬賓
• 申請（專利權）人: 全球能源互聯網研究院有限公司;許繼集團有限公司;國網遼寧省電力有限公司;國網遼寧省電力有限公司電力科學研究院;南瑞集團有限公司;國家電網有限公司
• 主分類號: H04L12/26
• 分類號: H04L12/26;H04L12/24
• 代理公司: 北京安博達知識產權代理有限公司 11271
• 代理人: 徐國文

本發明涉及計及信息時效的嵌入式裝置安全通信協議驗證方法和系統。包括:對預先建立的狀態與變遷模型中各層級進行狀態空間搜索，驗證安全通信過程的時效性是否正確；基于所述嵌入式裝置安全通信過程的時效性，對所述狀態與變遷模型中的通信時間消耗進行分析，驗證安全通信過程是否可以在預定的時間內完成；其中，所述狀態與變遷模型，是通過將嵌入式裝置安全通信協議的多個層級為基礎構建的。能夠基于模型檢驗方法，分析模型的有界性，緩解狀態空間爆炸問題，通過狀態空間搜索，驗證安全通信協議的可操作性。

技術領域

本發明涉及嵌入式裝置安全通信協議技術領域，具體涉及計及信息時效的嵌入式裝置安全通信協議驗證方法和系統。

背景技術

安全通信是嵌入式裝置穩定運行的前提。由于通信基礎設施的開放性，隨著電力物聯網高速發展，嵌入式裝置將廣泛采用無線通信技術，存在電磁干擾、黑客攻擊等風險。為了保證安全通信，可以在通信應用層增加安全通信協議，在開放的信道上實現安全可靠的通信。例如，中國電科院提出了一種融合協議過濾、雙向身份認證、訪問列表查詢和優先級控制等方法的智能電表雙向互動、多重防護安全通信協議BIMP(電力系統自動化，2016，Vol.40)，等等。

但是，嵌入式裝置安全通信協議的設計與測試是個復雜的技術問題，因為既涉及通信協議自身的功能，又涉及與通道有關的性能。嵌入式裝置除了用于電氣設備的狀態監測，更重要的功能是服務于電網的測量和控制，要保證功能的正確性，需要保證信息的時效性，在規定的時間內完成通信過程。

為了保證通信協議的高可靠性，需要進行測試和驗證。例如國電南自公司的發明專利201811522352.8(基于加密算法的通信協議雙向驗證自動化測試工具及方法)，能夠驗證廠站端電力系統網絡安全監測裝置與主站的正反向通信性能以及廠站端電力系統網絡安全監測裝置與主站通信規約的健壯性，等等。但是，此類方法基于典型的黑盒測試，存在測試用例不能完全覆蓋的問題。

目前，業界采用形式化驗證避免上述測試覆蓋率問題。模型檢驗(ModelChecking)是目前主要的形式化驗證方法，其基本思想是通過遍歷系統模型的狀態空間，來檢驗系統模型是否滿足給定的性質。例如南京郵電大學的授權發明專利201310140565.5(基于動態規劃的傳感器網絡軟件模型檢驗方法)，建立抽象的時間狀態自動機模型，采用基于動態規劃思想的記憶化搜索驗證方法，驗證相關網絡協議是否滿足要求。

上述方法可實現通信協議的功能驗證，為了保證信息的時效性，需要驗證在規定的時間內完成安全通信。例如南京大學的授權專利201310456973.1(一種基于模型檢驗的無線傳感器網絡安全協議驗證方法)，用時間自動機所組成的狀態遷移系統表示無線傳感器網絡安全協議，用模態/時序邏輯公式表示無線傳感器網絡中安全協議所需滿足的條件，并在模態/時序邏輯公式中加入時鐘約束條件。但是，該專利缺乏對通信協議棧中不同層次的分析，不能完全適用于嵌入式裝置中在開放的信道上實現安全通信的需求，特別在信道隨機干擾環境下的安全通信性能考慮不足。

發明內容

為克服上述現有技術的不足，本發明提出計及信息時效的嵌入式裝置安全通信協議驗證方法，包括：

對預先建立的狀態與變遷模型中各層級進行狀態空間搜索，驗證安全通信過程的時效性是否正確；

基于所述嵌入式裝置安全通信過程的時效性，對所述狀態與變遷模型中的通信時間消耗進行分析，驗證安全通信過程是否可以在預定的時間內完成；

其中，所述狀態與變遷模型，是通過將嵌入式裝置安全通信協議劃分后得到的多個層級構建的。

優選的，所述狀態與變遷模型的建立，包括：

將嵌入式裝置安全通信協議分為應用系統、傳輸層、信道，以及消息交互過程；

基于所述應用系統、傳輸層、信道，以及消息交互過程構建應用系統模型層級、傳輸層模型層級和信道模型層級；