[發明專利]基于需求的IMA安全驗證分析方法

有效

• 申請號: 201710252450.3
• 申請日: 2017-04-18
• 公開（公告）號: CN107220539B
• 公開（公告）日: 2020-07-24
• 發明（設計）人: 王立松;汪圓圓;胡軍;周穎
• 申請（專利權）人: 南京航空航天大學
• 主分類號: G06F21/53
• 分類號: G06F21/53;G06F21/57
• 代理公司: 南京鐘山專利代理有限公司 32252
• 代理人: 戴朝榮

1.一種基于需求的IMA安全驗證分析方法，其特征在于包含以下步驟：

步驟一：確定系統級危害和安全約束；

步驟二：構建出系統的控制結構圖，通過控制結構圖找出不安全的控制行為，進而得到系統的安全需求；

步驟三：用SCR模型對安全需求進行建模，對描述不準確的需求進行修改，并用形式化的方法驗證需求的可靠性和準確性；

所述步驟一具體為，從IMA系統提供的服務出發，找到IMA提供的與分區通信相關的服務，然后找到會導致相關服務失效的危險，確定分區通信的系統級危險，若IMA的分區間通信服務失效，則會導致分區通信系統的系統級危險；

所述分區通信的系統級危險包含，

H1 通道沒有正確獲取發送進程發送的消息；

H2 通道接收進程沒有正確接收通道的消息；

H3 通道分區通信初始化過程出現錯誤；

進而產生系統級的安全約束：

SC1通道必須要正確獲取發送進程發送的消息；

SC2通道接收進程必須正確接收通道的消息；

SC3通道分區通信初始化過程不能出錯。

2.按照權利要求1所述的基于需求的IMA安全驗證分析方法，其特征在于：所述步驟二包含，

2.1基于整個系統的工作方式和系統結構，找出系統的所有獨立的組件，分析每個組件在系統中的作用，提取控制動作和反饋動作，構建出控制結構圖；

2.2從控制結構圖中提取控制動作，從“沒有提供所需的安全控制行為”，“提供了不正確的控制行為”，“不正確的時間/順序”，“停止過快/過慢”四類控制不力的情況出發，分析每個控制動作可能會導致的系統危險，得到不安全的控制行為，并根據不安全的控制動作得出安全約束；

2.3分析不安全控制行為產生原因，原因包含系統缺陷、組件失效、算法缺陷和外界環境干擾；

2.4把提取出的安全約束作為系統的安全需求，提取需求中的變量。

3.按照權利要求2所述的基于需求的IMA安全驗證分析方法，其特征在于：所述2.1具體為，IMA分區通信分為兩個階段：初始化階段和通信階段，針對兩個不同階段分別構建控制結構圖，以提取不同階段的安全需求；在構建通信階段的控制結構圖時，先構建通信階段的流程圖，然后在流程圖中提取控制動作和反饋動作，找出控制方和被控制方，構建出通信階段的控制結構圖。

4.按照權利要求2所述的基于需求的IMA安全驗證分析方法，其特征在于：所述2.2具體為，從控制結構圖中提取控制動作得到分區通信模塊14個控制動作，其中初始化階段4個控制動作，通信階段10個控制動作，按照STPA方法從“沒有提供所需的安全控制行為”、“提供了不正確的控制行為”、“不正確的時間/順序”、“停止過快/過慢”四類控制不力的情況出發，分析每個控制動作會導致的系統危險，得到不安全的控制行為，通過對14個控制動作的分析，得到70個UCA，其中初始化階段有16個UCA，通信階段有54個UCA，識別出不安全控制行為可以轉換為有關系統組件行為的安全約束，即得到系統的安全需求，通過對得到的70個UCA的分析，得到分區通信的安全約束。

5.按照權利要求1所述的基于需求的IMA安全驗證分析方法，其特征在于：所述步驟三包含，

3.1根據安全需求，構建變量之間的關系，建立SCR模型，驗證安全需求的描述準確性，對描述不準確的需求進行修改；

3.2把建立好的SCR模型在T-VEC工具上進行模擬，進行形式化驗證。

6.按照權利要求5所述的基于需求的IMA安全驗證分析方法，其特征在于：所述3.1具體為，提取完安全需求的變量之后，找到變量之間的關系，把安全需求用形式化的語言描述，對不明確的安全需求進行相應的修改完善，對形式化表述之后的安全需求構建SCR關系表。

7.按照權利要求5所述的基于需求的IMA安全驗證分析方法，其特征在于：所述3.2具體為，把構建好的SCR模型在T-VEC工具上進行模擬，進行形式化驗證，確保系統需求各變量和需求間的依賴關系符合系統要求，且需求所描述的系統行為滿足安全性，通過T-VEC工具可以自動生成測試向量。