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

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

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

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

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