基于狀態(tài)事件故障樹的軟件安全性分析方法研究.pdf

1、嵌入式軟件已廣泛應(yīng)用于航空航天、核工業(yè)、交通等領(lǐng)域，且嵌入式軟件已成為決定系統(tǒng)安全的主要因素。如何保障軟件安全性已成為學(xué)術(shù)界和工業(yè)界的重點(diǎn)問題。針對(duì)軟件安全需求進(jìn)行分析，以及針對(duì)軟件功能進(jìn)行設(shè)計(jì)，是軟件安全性分析的主要關(guān)注點(diǎn)，但二者在實(shí)際開發(fā)中通常是獨(dú)立進(jìn)行的，致使在軟件功能設(shè)計(jì)中，難以參照軟件安全需求分析結(jié)果進(jìn)行修改，軟件安全需求分析難以在軟件功能設(shè)計(jì)階段進(jìn)行，且基于軟件功能設(shè)計(jì)模型難以開展軟件安全性分析工作。已有基于故障樹的安全性分

2、析無法描述軟件的組件行為，且故障樹分析不能在軟件功能模型設(shè)計(jì)中確定是否存在故障之間的因果關(guān)系，而基于狀態(tài)圖的軟件設(shè)計(jì)模型能夠描述軟件的行為，但是難以發(fā)現(xiàn)其中隱藏的故障隱患。
　　針對(duì)以上問題，本文提出了一種基于狀態(tài)事件故障樹(State/Event Fault Tree, SEFT)的軟件安全性分析方法，使用SEFT(State/Event Fault Tree, SEFT)描述軟件發(fā)生的故障因果關(guān)系及導(dǎo)致故障的組件內(nèi)部行為，再提

3、取安全需求規(guī)約，并將其擴(kuò)展到狀態(tài)圖，最后通過模型檢測方法對(duì)擴(kuò)展模型進(jìn)行安全性驗(yàn)證與分析。論文主要研究內(nèi)容如下：
　?。?）使用SEFT描述軟件故障及導(dǎo)致軟件故障的組件內(nèi)部行為，并使用線性時(shí)序邏輯將其時(shí)序化，得到時(shí)序狀態(tài)事件故障樹(Liner Temporal SEFT, LTSEFT)，根據(jù)約簡規(guī)則將其約簡，最后根據(jù)其最小割集提取LTL（Linear Temporal Logic)規(guī)約。
　?。?）定義了SEFT邏輯門到狀態(tài)

4、圖元素的轉(zhuǎn)換規(guī)則，設(shè)計(jì)了安全需求到狀態(tài)圖元素的安全需求信息映射表，以及基于映射表和轉(zhuǎn)換規(guī)則自動(dòng)構(gòu)建系統(tǒng)安全需求擴(kuò)展?fàn)顟B(tài)圖的算法。
　?。?）通過模型轉(zhuǎn)換，將擴(kuò)展的狀態(tài)圖轉(zhuǎn)換到Promela，輸入到SPIN中，根據(jù)提取的安全屬性LTL規(guī)約進(jìn)行安全性驗(yàn)證和分析。
　　最后，運(yùn)用本文提出的方法對(duì)襟縫翼控制系統(tǒng)進(jìn)行案例分析。給出了構(gòu)建系統(tǒng)SEFT(State/Event Fault Tree, SEFT)及 LTSEFT(Liner