一種基于STPA的軟件安全性分析與驗證方法

南京航空航天大學(xué) 讓 濤

?

一種基于STPA的軟件安全性分析與驗證方法

南京航空航天大學(xué) 讓 濤

【摘要】安全性苛求系統(tǒng)的安全性關(guān)系關(guān)系著人們生命財產(chǎn)安全，而軟件與系統(tǒng)的安全性緊密相關(guān)。形式化驗證方法可以證明軟件的正確性，但并不能保證軟件的安全性性。系統(tǒng)理論危害分析方法（System-Theoretic Process Analysis，STPA）是一種基于系統(tǒng)理論的危害分析方法，它可以識別系統(tǒng)中的危害并得到軟件相關(guān)的安全性需求。本文提出一個結(jié)合STPA與模型檢測的軟件安全性分析與驗證方法：使用STPA對系統(tǒng)進行危害分析得到軟件安全性需求，形式化描述軟件安全性性質(zhì)，最后使用模型檢測的方法驗證軟件安全性。

【關(guān)鍵詞】軟件安全性；安全性驗證；系統(tǒng)理論危害分析；模型檢測

1　引言

安全性苛求系統(tǒng)與人們生命財產(chǎn)安全息息相關(guān)，安全性苛求軟件是其中的一個要因素[1]。軟件不直接導(dǎo)致?lián)p失與損害，它控制一些設(shè)備可能會導(dǎo)致事故發(fā)生[2]。系統(tǒng)理論認為安全性是系統(tǒng)整體的屬性，且事故發(fā)生是由軟件設(shè)計錯誤、組件間不正常交互引起的[3]。STPA[4]是一種STAMP[6]的危險分析方法，在考慮組件失效的同時更注重于辨識交互帶來的危害。模型檢測[5]是目前流行的形式化驗證方法，它通過窮舉搜索軟件狀態(tài)空間的方式來驗證軟件是否滿足安全性需求。

圖1　軟件安全性分析與驗證方法過程

2　軟件安全性分析與驗證方法

本章將STPA危害分析方法與模型檢測結(jié)合，主要分為三個部分（如圖1所示）：（1）使用STPA方法對軟件控制的系統(tǒng)進行危害分析，提取相關(guān)的軟件安全性需求；（2）形式化描述安全性需求；（3）使用模型檢測工具驗證軟件安全性。

2.1系統(tǒng)危害分析與軟件安全性需求提取

提取安全性需求主要步驟：（1）構(gòu)建STPA分析基礎(chǔ)：系統(tǒng)危害與控制結(jié)構(gòu)圖；（2）識別控制器的控制行為和不安全控制行為；（3）明確過程模型進行危害場景分析；（4）生成軟件安全性需求。

分析軟件控制器產(chǎn)生的不安全控制行為產(chǎn)生的原因，安全性分析人員可以得到危害場景，得到軟件相關(guān)的安全性需求。過程變量模型的組合在某種上下文下會導(dǎo)致危害，意味著這種過程變量組合狀態(tài)下不能（或必須）提供控制行為。安全性需求SRi,j形式化定義為：

或

其中PWVi,j表示與控制行為CAi相關(guān)的過程模型變量值的組合，CAi表示第i個控制行為。

2.2軟件安全性驗證

安全性性質(zhì)：安全性需求SRi,j在軟件運行路徑上的所有狀態(tài)節(jié)點上都必須被滿足。用LTL描述性質(zhì)，得到如下時序邏輯公式：

表示運行路徑上的所有狀態(tài)。

安全性需求SRi,j表示為：

在建設(shè)少數(shù)民族幼兒音樂教育資源庫的過程中，一定要充分發(fā)掘民間音樂固有的特性，發(fā)揮音樂教師的帶動作用，以教師為主體，使少數(shù)民族幼兒音樂教育更加有針對性，更加符合幼兒的學(xué)習(xí)需求。讓幼兒產(chǎn)生學(xué)習(xí)民族歌曲的濃厚興趣，提高學(xué)習(xí)民間音樂的動力，更好地了解、學(xué)習(xí)民間音樂。

模型檢測工具的輸入包括兩個部分：形式化描述的安全性性質(zhì)、軟件模型。NuSMV工具支持檢測模型是否滿足LTL描述的安全性屬性。

3　實例分析：電梯控制軟件

電梯在生活中隨處可見，它的安全性與人們的生命財產(chǎn)安全息息相關(guān)。電梯主要由轎廂、門系統(tǒng)、按鈕（內(nèi)外）、電力系統(tǒng)、控制系統(tǒng)等組成，其中電梯的控制是由軟件完成的。

3.1電梯系統(tǒng)危害分析與軟件安全性需求提取

系統(tǒng)危害包括：H1：電梯無命令地移動；H2：電梯運行過程中電梯門沒有關(guān)閉；H3：電梯停在不合適的位置。電梯控制器有兩個個控制行為： CA1：運行電梯（move）； CA2：制動（stop）。

不安全控制行為：UCA1.1：電梯沒有請求時提供運行命令[H1]；UCA1.2：電梯到達請求樓層時提供運行命令[H3]；UCA1.3：電梯運行命令提供過久導(dǎo)致電梯停在不合適的位置[H3]。

過程模型變量主要有：當(dāng)前樓層（cur_floor）、請求樓層（req_floor）、門狀態(tài)（door_state）、運行狀態(tài)（move_state）。明確了控制器模型與模型變量，接著分析不安全控制產(chǎn)生的原因（如表1所示）。

表1　基于過程模型變量組合與上下文分析不安全控制行為產(chǎn)生原因

UCA1.1相關(guān)的安全性需求：

其中：

將安全性需求用LTL描述，如下例SR1,1、SR1,2：

將系統(tǒng)模型與時態(tài)邏輯公式放到NuSMV工具中，表2是電梯運行狀態(tài)模塊模型代碼。move_state定義為一個枚舉類型，可取值有兩個：stop和moving。

表2　電梯運行狀態(tài)轉(zhuǎn)移規(guī)則

分別驗證安全性需求SR1,1、SR1,2SR1,4驗證代碼如下：

SPEC G (cur_floor = req_floor & door_state = closed & move_state = stop -＞ !move_state = moving)

SPEC G (cur_floor = req_floor & door_state = closed & move_state = moving -＞ !move_state = moving)

4　結(jié)束語

本文使用STPA方法對系統(tǒng)進行危害分析，并得到軟件相關(guān)的安全性需求。將這些與軟件相關(guān)安全性映射為形式化邏輯公式，使得我們可以在代碼層對其進行安全性驗證。然而分析過程主要依靠人工分析，下一步需要開發(fā)一些自動化工具。

參考文獻

[1]Leveson N G.Safeware: system safety and computers[M].ACM,1995.

[2]McDermid J A.Issues in developing software for safety critical systems[J].Reliability Engineering & System Safety, 1991,32(1):1-24.

[3]Leveson N G.A new approach to hazard analysis for complex systems[C]//International Conference of the System Safety Society,2003.

[4]Leveson N.Engineering a safer world: Systems thinking applied to safety[M].Mit Press,2011.

[5]Baier C,KATOEN J P.Principles of Model Checking (Representation and Mind Series)[J].2008.

[6]Leveson N.A new accident model for engineering safer systems[J].Safety science,2004,42(4):237-270.