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

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

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

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

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

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

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

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