[發明專利]一種自動化協議形式化分析方法

在審

• 申請號: 202011081308.5
• 申請日: 2020-09-29
• 公開（公告）號: CN112202642A
• 公開（公告）日: 2021-01-08
• 發明（設計）人: 趙蕾;李楠芳;李宗容;馬先;鐘應壽;景延嶸;王旭;李勝春;尚西元;馬學智
• 申請（專利權）人: 國網青海省電力公司電力科學研究院;國網青海省電力公司;國家電網有限公司
• 主分類號: H04L12/26
• 分類號: H04L12/26
• 代理公司: 暫無信息
• 代理人: 暫無信息

本發明涉及一種自動化協議形式化分析方法，可以適用于多種協議的安全分析。協議作為安全分析的基本手段，可以利用形式化分析模型對某種協議進行數據建模，填充字段，設計工作流程，再用自動化腳本工具進行測試。形式化分析工具可以發現協議中存在的基礎性漏洞，這些漏洞往往會造成設備、系統的重大安全問題。

技術領域

本發明涉及一種自動化協議形式化分析方法，屬于協議測試技術領域。

背景技術

所謂形式化分析方法，是概念或者方法經過高度抽象后，使用一定的數學模型進行表示，通過程式化的推演計算來研究數學模型，進而揭示概念和方法內在規律的研究方法，安全協議的形式化分析則是采用一種正規標準的方法對安全協議進行分析，檢查協議是否滿足其預期的目標。

形式分析過程包括形式化描述協議運行的環境，準確的形式化描述安全協議的動作行為，準確的定義安全協議的安全屬性，驗證安全協議是否滿足預期的目標。

安全協議形式化分析的目標主要有：分析協議的可行性也就是分析協議的正確性，分析協議的目標性，即分析協議能否達到預期的目標(其中安全性是諸多目標中重要的一個目標)；分析協議的冗余性，即分析協議的步驟是否達到最優化，使用形式化分析工具的側重點在于分析協議是否能達到預計的安全目標。

形式化方法在信任算法的安全強度前提下，可以忽略算法的數學細節、來討論協議的安全性質，由符號以及使用這些符號的規則工作組成形式化分析系統，是信息安全領域中一個受到重視的安全研究方向。

發明內容

本發明所要解決的技術問題是提供一種自動化協議形式化分析方法，采用全新設計架構，能夠高效實現協議測試，提高工作效率。

本發明為了解決上述技術問題采用以下技術方案：本發明設計了一種自動化協議形式化分析方法，用于針對各目標協議實現安全測試，包括如下步驟：

步驟A.分別針對各目標協議，設計目標協議所對應的形式化分析工具，包括形式規約和形式驗證，然后進入步驟B；

步驟B.分別針對各目標協議，根據目標協議所對應的功能、以及預設測試分支，定義該目標協議所對應形式化分析工具中的各個測試套件，并進一步分別針對各個測試套件，根據預設各測試方法，定義測試套件所對應的各個測試腳本，待完成對應各目標協議的上述操作后，然后進入步驟C；

步驟C.分別針對各目標協議所對應形式化分析工具中、各測試套件所對應的各個測試腳本，生成各測試腳本分別所對應的測試策略和測試用例，然后進入步驟D；

步驟D.根據各測試腳本分別所對應的測試策略和測試用例，生成相對應的測試報文，即作為各目標協議分別所對應形式化分析工具中的各個測試報文，然后進入步驟E；

步驟E.分別針對各目標協議，應用目標協議所對應形式化分析工具中各個測試報文，結合該形式化分析工具中的形式化分析工具，針對該目標協議進行安全測試。

作為本發明的一種優選技術方案：所述形式化分析工具中的形式規約包括面向模型規約方法或面向性質規約方法。

作為本發明的一種優選技術方案：所述測試腳本支持用XML格式描述測試報文的序列，用于Fuzzer的測試。

作為本發明的一種優選技術方案：所述測試腳本包括收發包通道、采取的動作、以及收發動作中數據單元PDU的定義。

本發明所述一種自動化協議形式化分析方法，采用以上技術方案與現有技術相比，具有以下技術效果：

本發明所設計自動化協議形式化分析方法，可以適用于多種協議的安全分析。協議作為安全分析的基本手段，可以利用形式化分析模型對某種協議進行數據建模，填充字段，設計工作流程，再用自動化腳本工具進行測試。形式化分析工具可以發現協議中存在的基礎性漏洞，這些漏洞往往會造成設備、系統的重大安全問題。