基于AADL 模型的軟件安全性評估

劉璐璐 惠曾強

AADL 建模語言可以支持架構層面的軟件安全性分析，引入AADL 錯誤附件，將其進行擴展，構建了基于AADL 的安全模型，根據轉換規則將安全模型轉換為Markov 鏈模型，并對其轉換后的Markov 鏈模型進行安全性分析。以飛機機翼系統為應用場景進行實驗，通過計算系統的MTBUF（Mean Time Between Unfailures，非安全失效平均間隔時間）和系統失效率，并將結果與經驗數據進行對比，實現對軟件系統的安全性評估。

軟件安全性問題在航空、航天、武器裝備等各個領域日益突出和嚴峻，根據軟件結構的特點以及其安全性影響因素的不同，有必要研究新的軟件安全性分析技術。本文引入了AADL（The Architecture Analysis &Design Language）錯誤附件，提出基于AADL 錯誤附件及其擴展的軟件安全模型，為軟件安全性的進一步研究與分析奠定基礎。

AADL 錯誤模型

AADL 錯誤附件作為AADL 模型的一種標準擴展，它為AADL 組件添加了描述可靠性和安全性等相關信息的能力。錯誤模型有兩個層次的描述：錯誤類型層和錯誤實現層。錯誤模型的類型定義了一組錯誤狀態，同時也能描述無錯狀態；錯誤模型類型定義了一組錯誤事件和事件的發生概率（如果概率是已知的）。一個錯誤事件的發生概率可以是固定的（語法使用關鍵字fixed 定義），指數分布的（語法使用關鍵字poisson 定義），或者是用戶自定義的非標準分布。一個錯誤模型的實現聲明了錯誤狀態之間的轉換關系，這些轉換可以由內部錯誤事件或者外部構件的錯誤傳播來觸發。

基于AADL 良好的可擴展性與對系統故障概率和傳播的可描述特性，使其在系統軟件安全性研究方面有一定的應用前景。

基于AADL 錯誤附件的安全性模型

AADL 錯誤模型是AADL 的標準附件，可以對組件的故障狀態，故障傳播等信息進行描述。為了能更好的對系統安全性進行分析，在AADL 錯誤模型的基礎上，將安全性信息與AADL 錯誤模型相結合，形成AADL 安全附件。AADL 安全性模型結構如圖1 所示。

AADL 安全附件能更好的描述系統在運行時的安全狀態，從而更好的分析系統安全性。AADL 安全附件是根據SAE5506-1 標準，在AADL 錯誤模型基礎上擴充，將上述安全性狀態等級等安全性信息和AADL 錯誤模型結合后擴展而成。AADL 安全附件描述了在發生不同安全事件時，系統處于不同安全狀態等級等安全性信息。

基于AADL 模型的軟件安全性評估

影響系統安全性的主要因素為MTBUF 和系統失效率。以AADL 錯誤附件以及擴展建立安全模型，根據AADL 到Markov 鏈的轉換規則，將安全模型中的元素與Markov 鏈模型中的元素一一對應，不會造成模型轉換后的信息丟失。然后通過對Markov 鏈模型的分析，計算影響系統軟件安全性因素MTBUF 和系統失效率，從而實現對軟件安全性評估。

由安全性模型向Markov 鏈模型的轉換

由基于AADL 安全模型同樣描述了系統從一個狀態轉換到另一個狀態和這個狀態遷移事件的轉換概率。因此，安全性模型與Markov 鏈模型之間的轉換規則為安全性模型的狀態對應Markov 鏈模型的狀態，安全性模型的狀態遷移對應Markov 鏈模型的遷移，安全性模型的狀態遷移發生概率對應Markov 鏈模型的概率。為了實現安全性模型所有信息和Markov 鏈模型信息的一一對應，本文提出了一個擴展的Markov 鏈模型。

圖1 AADL 安全性模型結構圖

定義1 一個MK=（S，S0，∑，P，Q），其中

1）S 表示系統所有狀態集合，該集合必須是一個隨機且有限的狀態集合。Si 表示S 有限集合中的第i 個元素（1 ≤i ≤n）。Si 是二元組，一個Si={State，Level}。State 是狀態名，Level 是該狀態對應的安全性狀態等級，Level 包括五個等級：Normal，Light，Heavy，Serious，Crash。

2）S0 表示系統的初始狀態，且S0 ∈S。

3）∑表示系統所有安全事件或狀態傳播集合，該集合必須是一個有限的集合。∑i 表示∑有限集合中的第i 個元素（1 ≤i ≤n）。∑i 是二元組，一個∑i={TriggerName，TriggerType}，TriggerType 是引起狀態傳播的事件類型，TriggerType 包含兩個類型：安全事件和狀態傳播。TriggerName 是事件名稱。

4）P 是狀態之間傳播的概率集合，該集合為一個有限的集合。Pi 表示P 集合中的第i 個元素（1 ≤i ≤n）。Pi 是三元組，一個Pi={Probability，ProbabilityType，ProbabilityDefinition}，Probability 是錯誤傳播的概率，ProbabilityType 用于區分該概率為失效概率還是維修概率，ProbabilityDefinition 表明概率的范圍，其范圍可以是[0，1]的自然數，也可以是指數級別的泊松分布。

5）Q 表示狀態之間的遷移關系：S×∑→S。

根據定義，可以得到AADL 安全模型與Markov 鏈模型中元素的對應關系，如下表1 所示。

表1 AADL 安全模型與Markov 鏈模型中元素對應表

系統失效率與MTBUF 計算

在一個系統中，當一個組件和其它組件之間的交互十分緊密時，它表明其它組件對這個組件依賴較大，則說明該組件對于系統是重要的。C 表示組件與組件之間交互的數目，第i 個組件的交互數表示為Ci（0 ≤ i ≤n），初始化為0。當一個組件與其它組件進行交互時，此組件的交互數增加1。計算出各組件的交互數為C1，C2，...，Cn。第i 個組件的重要性指數為ImpAi（1 ≤ i ≤n）

從組件狀態的角度對系統中各個組件的重要性予以計算。S 表示組件中最高狀態等級，根據組件的安全性狀態等級，可以得出與之對應的安全狀態等級數。如表2 所示。

表2 安全狀態等級數

第i 個組件的安全狀態等級數表示為Si（1 ≤ i ≤n），初始化為1。根據上表，可以得出各個組件的最高狀態數，計算出各組件的安全狀態等級數為S1，S2，...，Sn。第i個組件的重要性指數為ImpBi（1 ≤ i ≤n）：

組件最終重要性為：

系統中的各個組件的失效率λi 和組件維修率μ 可以通過組件分析得出，各組件的MTBUF 為：

系統整體失效率為：

其中λi 是第i 個組件的失效率。系統整體的MTBUF 為，

MTBUFi 是第i 個元素的穩定狀態下的MTBUF。

對Markov 鏈模型的軟件安全性評估的實現

本節將對飛機機翼控制系統進行安全性建模，并將安全性模型轉換至機翼控制系統的Markov 鏈模型，最后進行安全性進行分析與評估。

飛機機翼控制系統為航天器飛行控制系統中的機翼控制和計算部分，本系統主要關注其機翼收放控制，將飛行速度、飛行高度以及氣壓信息計算結果發送到系統，從而控制機翼收放。飛機機翼控制系統的AADL 體系架構模型如圖2 所示，主要包括兩 Aerofoil_System 子系統和FCI_System 子系統，這兩子系統通過 LAN 總線進行交互，互相傳遞信息。

根據機翼控制系統的 AADL 體系架構模型以及每個組件實際的動態運行情況，給每個組件增加相應的安全附件。安全附件類型中定義了安全性狀態、安全事件和狀態傳播。安全附件實現中定義了安全性狀態之間因安全事件、向外狀態傳播和向內接受狀態而發生遷移。

圖2 機翼控制系統AADL 體系架構圖

圖3 機翼控制系統的Markov 鏈模型

圖4 AAXL 文件解析

圖5 系統需求參數輸入

圖6 系統安全性分析結果

將該安全性附件與圖2 中的機翼控制系統的AADL 體系架構模型相結合組成機翼控制系統的AADL安全性模型，然后利用軟件安全性分析工具實現機翼控制系統的AADL安全性模型向Markov 鏈模型的轉換，然后對Markov 鏈模型進行安全性分析與評估。機翼控制系統 AADL 安全性模型轉換到Markov 鏈模型的結果如圖3 所示。

經過 AADL 安全性模型向Markov 鏈模型轉換后，利用軟件安全性分析工具對Markov 鏈模型進行安全性分析，得到模型的安全性評估結果。（計算結果的由來：基于Markov 鏈模型上進行系統失效率及MTBUF 安全性關鍵因素計算）其具體操作過程如圖4 所示。

選擇需要解析的AAXL 文件，完成AADL 安全性模型至Markov鏈模型轉換。系統解析完成后，將系統需求失效率以及系統需求MTBUF參數輸入軟件中以供評估。圖5 所示。

本次系統安全性分析中共有8 個組件，各個組件以及系統總體的安全性分析如圖6 所示。

根據軟件安全性分析工具生成的分析報告，可以看出：

1）系統失效率并不能滿足系統安全性需求。由組件安全性結果可以看出，T_AF_Computer 和T_AF_Params 的失效率過大，可以降低這兩個組件的效率以降低系統的失效率；

2）由組件安全性結果可以得出，對系統影響性最大的是T_FCI_CH_Input，若該組件發生了災難性的狀態，對系統影響很大。

通過對數據進行分析可以看出，在系統架構設計過程中，可以根據系統對各個組件的安全性需求來調整關鍵組件的安全事件的發生概率，直到滿足組件的安全性需求為止。如果通過調整安全事件的發生概率不能滿足需求時，那么就需要在組件這一級別對系統進行重新設計。

結語

本文在AADL 錯誤模型基礎上，將其理論進行應用，提出AADL 安全性模型，并在AADL 安全性模型的基礎上將其轉化為Markov 鏈模型對軟件安全性分析計算，為進一步分析系統的安全性及系統安全性優化提供了理論依據。