[發明專利]一種智能家居物聯網系統受攻擊安全驗證的方法和裝置

有效

• 申請號: 201910930600.0
• 申請日: 2019-09-29
• 公開（公告）號: CN110677413B
• 公開（公告）日: 2021-07-30
• 發明（設計）人: 卜磊;張秋萍;張時雨;王熙灶;沈思遠;王林章;李宣東
• 申請（專利權）人: 南京大學
• 主分類號: H04L29/06
• 分類號: H04L29/06;H04L29/08;G05B19/418;G05B15/02
• 代理公司: 江蘇銀創律師事務所 32242
• 代理人: 孫計良

1.一種智能家居物聯網系統受攻擊安全驗證的方法，其特征在于，包括以下步驟：

S1：獲取智能家居設備描述信息、設定的智能家居設備之間的IFTTT規則、設定的攻擊烈度設備禁止性行為參數；所述攻擊烈度設備禁止性行為參數包括攻擊烈度閾值、智能家居設備參數和禁止性狀態參數，用以表示在攻擊烈度不超過所述攻擊烈度閾值時所述智能家居設備參數所指向的智能家居設備不能出現所述禁止性狀態參數所表示的狀態；所述攻擊烈度是智能家居設備處于受攻擊狀態的設備數；

S2：根據所述的智能家居設備描述信息、所述的智能家居設備之間的IFTTT規則、智能家居設備是否受攻擊的狀態以及在受攻擊狀態下智能家居設備無法接受外部遷移指令和設備數據不真實的限制性假設條件，構建智能家居設備狀態變遷的有限狀態機模型；所述智能家居設備是否受攻擊的狀態采用布爾量attacked表示；所述在受攻擊狀態下智能家居設備無法接受外部遷移指令和設備數據不真實的限制性假設條件包括兩種限制性假設條件：在受攻擊狀態下智能家居設備無法接受外部遷移指令和在受攻擊狀態下設備數據不真實；所述在受攻擊狀態下智能家居設備無法接受外部遷移指令表示智能家居設備在變遷時所述布爾量attacked必須為假；所述在受攻擊狀態下設備數據不真實表示所述布爾量attacked為真時智能家居設備所顯示的數據不真實；

S3：根據預先設定的攻擊烈度規約模板和所述的攻擊烈度設備禁止性行為參數構建有關攻擊烈度的形式化規約；所述攻擊烈度規約模板是描述所述攻擊烈度設備禁止性行為參數內攻擊烈度閾值、智能家居設備參數和禁止性狀態參數之間表示攻擊烈度設備禁止性行為的規約模板；

S4：根據所述的有限狀態機模型和所述的有關攻擊烈度的形式化規約轉換成模型檢驗工具所對應輸入格式的模型描述文檔內容；

S5：采用所述模型檢驗工具對所述的模型描述文檔內容進行規約正確性驗證；若規約驗證正確，則表示系統安全，否則輸出反例路徑；

S6：根據所述模型檢驗工具所輸出的反例路徑，找出導致系統不安全的智能家居設備和相關的IFTTT規則。

2.如權利要求1所述的智能家居物聯網系統受攻擊安全驗證的方法，其特征在于，所述智能家居設備參數為設備類型。

3.一種智能家居物聯網系統受攻擊安全驗證的裝置，其特征在于，包括以下模塊：

M1，用于：獲取智能家居設備描述信息、設定的智能家居設備之間的IFTTT規則、設定的攻擊烈度設備禁止性行為參數；所述攻擊烈度設備禁止性行為參數包括攻擊烈度閾值、智能家居設備參數和禁止性狀態參數，用以表示在攻擊烈度不超過所述攻擊烈度閾值時所述智能家居設備參數所指向的智能家居設備不能出現所述禁止性狀態參數所表示的狀態；所述攻擊烈度是智能家居設備處于受攻擊狀態的設備數；

M2，用于：根據所述的智能家居設備描述信息、所述的智能家居設備之間的IFTTT規則、智能家居設備是否受攻擊的狀態以及在受攻擊狀態下智能家居設備無法接受外部遷移指令和設備數據不真實的限制性假設條件，構建智能家居設備狀態變遷的有限狀態機模型；所述智能家居設備是否受攻擊的狀態采用布爾量attacked表示；所述在受攻擊狀態下智能家居設備無法接受外部遷移指令和設備數據不真實的限制性假設條件包括兩種限制性假設條件：在受攻擊狀態下智能家居設備無法接受外部遷移指令和在受攻擊狀態下設備數據不真實；所述在受攻擊狀態下智能家居設備無法接受外部遷移指令表示智能家居設備在變遷時所述布爾量attacked必須為假；所述在受攻擊狀態下設備數據不真實表示所述布爾量attacked為真時智能家居設備所顯示的數據不真實；

M3，用于：根據預先設定的攻擊烈度規約模板和所述的攻擊烈度設備禁止性行為參數構建有關攻擊烈度的形式化規約；所述攻擊烈度規約模板是描述所述攻擊烈度設備禁止性行為參數內攻擊烈度閾值、智能家居設備參數和禁止性狀態參數之間表示攻擊烈度設備禁止性行為的規約模板；

M4，用于：根據所述的有限狀態機模型和所述的有關攻擊烈度的形式化規約轉換成模型檢驗工具所對應輸入格式的模型描述文檔內容；

M5，用于：采用所述模型檢驗工具對所述的模型描述文檔內容進行規約正確性驗證；若規約驗證正確，則表示系統安全，否則輸出反例路徑；

M6，用于：根據所述模型檢驗工具所輸出的反例路徑，找出導致系統不安全的智能家居設備和相關的IFTTT規則。

4.如權利要求3所述的智能家居物聯網系統受攻擊安全驗證的裝置，其特征在于，所述智能家居設備參數為設備類型。