構(gòu)件化嵌入式軟件安全性分析方法研究.pdf

1、隨著嵌入式軟件系統(tǒng)在汽車、核工業(yè)、航空等安全關(guān)鍵領(lǐng)域的廣泛應(yīng)用，其失效將會導(dǎo)致財產(chǎn)的損失、環(huán)境的破壞甚至人員的傷亡，使得保障軟件安全性成為系統(tǒng)開發(fā)過程中的重要部分。此外，嵌入式軟件系統(tǒng)規(guī)模和復(fù)雜度的增加使其多采用構(gòu)件化分布式架構(gòu)。因此，針對構(gòu)件化嵌入式軟件系統(tǒng)進行安全性分析已成為現(xiàn)代嵌入式系統(tǒng)安全性保障的重要方法和研究熱點。而傳統(tǒng)的安全性分析方法主要應(yīng)用在軟件的需求分析階段，在軟件設(shè)計階段仍缺乏有效的安全性分析方法和工具。
　　形

2、式化方法是一種基于嚴格的數(shù)學(xué)理論為軟件和硬件系統(tǒng)提供精確規(guī)約、分析和驗證的方法。對于具有高安全性需求的嵌入式系統(tǒng)，建立有效的形式化分析驗證技術(shù)可以為安全性分析提供支持。因此，在嵌入式軟件設(shè)計階段的安全性建模中引入形式化方法對其進行分析，得到軟件安全性分析結(jié)果，可以有效提高嵌入式軟件安全性。
　　本文主要圍繞構(gòu)件化嵌入式軟件系統(tǒng)設(shè)計階段的安全性建模和分析問題展開研究。采用SysML和狀態(tài)事件故障樹建立安全性設(shè)計模型，對構(gòu)件化嵌入式軟

3、件系統(tǒng)設(shè)計階段模型的靜態(tài)結(jié)構(gòu)和動態(tài)失效行為兩方面的安全性分析工作進行研究。主要工作包含以下幾個方面：
　　(1)針對構(gòu)件化嵌入式軟件靜態(tài)結(jié)構(gòu)的構(gòu)件安全等級依賴問題，給出了分析構(gòu)件之間安全等級依賴與安全認證目標(biāo)之間一致性的方法。首先根據(jù)安全認證標(biāo)準(zhǔn)DO-178B分析軟件構(gòu)件安全等級依賴所必須達到的認證目標(biāo)，其次采用SysML塊定義圖建立帶有安全等級信息的軟件靜態(tài)結(jié)構(gòu)的安全性設(shè)計模型。由于SysML塊定義圖缺乏嚴格的形式語義，建立形式

4、化模型塊依賴圖對SysML塊定義圖進行形式化語義描述。在此基礎(chǔ)上給出算法用于分析構(gòu)件安全等級依賴與認證目標(biāo)之間的一致性。采用該方法對嵌入式軟件系統(tǒng)靜態(tài)結(jié)構(gòu)的安全等級依賴關(guān)系進行分析，能夠提高系統(tǒng)整體的安全性，并為安全認提供證據(jù)。
　　(2)針對構(gòu)件化嵌入式軟件動態(tài)失效行為因果鏈中的最小割序集分析問題，采用狀態(tài)事件故障樹建立系統(tǒng)的失效行為因果鏈。由于狀態(tài)事件故障樹缺乏嚴格的形式語義，提出形式化模型衛(wèi)式接口自動機對狀態(tài)事件故障樹行為方

5、面的形式化語義進行描述。在此基礎(chǔ)上，給出衛(wèi)式接口自動機的并行組合聚合框架用于生成狀態(tài)事件故障樹的形式化語義，并通過定義弱互模擬操作對組合過程中的狀態(tài)空間進行約簡。最后給出了基于該形式化語義的狀態(tài)事件故障樹最小割序集分析方法。分析結(jié)果可以為軟件的測試用例生成以及模型檢驗提供支持。
　　(3)針對構(gòu)件化嵌入式系統(tǒng)動態(tài)失效行為的安全性參數(shù)分析問題，提出了軟件失效行為的概率和時間特性分析方法。由于狀態(tài)事件故障樹能夠同時描述構(gòu)件化嵌入式系統(tǒng)

6、的動態(tài)失效行為和概率特性，在狀態(tài)事件故障樹最小割序集分析的基礎(chǔ)上，可進一步分析其概率時間參數(shù)。為了描述狀態(tài)事件故障樹帶概率信息的形式化語義，提出能夠同時描述功能行為和概率信息的形式化模型接口交互馬爾可夫鏈用于描述狀態(tài)事件故障樹的形式化語義。在此基礎(chǔ)上，給出接口交互馬爾可夫鏈的并行組合聚合框架用于獲得狀態(tài)事件故障樹的形式語義，并通過定義接口交互馬爾可夫鏈的弱互模擬操作對組合過程中的狀態(tài)空間進行約簡。最后，基于該形式語義分別采用已有的概率分

7、析工具MRMC和IMCA對狀態(tài)事件故障樹的概率和時間參數(shù)進行分析。分析結(jié)果可以為軟件安全性評估提供支持。
　　(4)基于上述方法，設(shè)計了一個構(gòu)件化嵌入式軟件安全性分析工具 T-CESSA(Tool for component-based embedded software safety analysis)，支持嵌入式軟件靜態(tài)結(jié)構(gòu)的安全等級依賴分析、動態(tài)失效行為的最小割序集以及安全性參數(shù)的分析，并且通過典型嵌入式軟件系統(tǒng)的實例分析說