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

南京航空航天大學 讓 濤

?

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

南京航空航天大學 讓 濤

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

【關鍵詞】軟件安全性；安全性驗證；系統理論危害分析；模型檢測

1　引言

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

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

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

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

2.1系統危害分析與軟件安全性需求提取

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

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

或

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

2.2軟件安全性驗證

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

表示運行路徑上的所有狀態。

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

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

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

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

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

3.1電梯系統危害分析與軟件安全性需求提取

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

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

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

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

UCA1.1相關的安全性需求：

其中：

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

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

表2　電梯運行狀態轉移規則

分別驗證安全性需求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　結束語

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

參考文獻

[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.