基于系統理論過程分析的軟件安全性需求分析與驗證方法

秦 楠，馬 亮，黃 銳

（海軍潛艇學院，山東青島 266199）

（?通信作者電子郵箱qinnanqtxy@126.com）

0 引言

隨著計算機軟件技術的發展，現代復雜系統逐漸由機械、電子密集型向軟件密集型轉變，與之相關的軟件安全性問題也日益凸顯。大量涉及軟件的系統事故［1］表明，從系統層面探究安全關鍵系統的安全性問題機理，結合系統功能自動生成軟件安全性需求，并設計合理的軟件安全性驗證方法已成為迫切需要解決的問題［2-4］。目前，安全性分析普遍采用的故障樹分析（Fault Tree Analysis，FTA）、故障模式影響及危害性分析（Failure Mode and Effects Analysis，FMEA）等傳統分析方法都是基于事件鏈的事故致因模型［5］。這些方法依然從硬件失效的角度看待軟件問題，將軟件安全性問題局限于軟件自身的不可靠因素，忽略了軟件需求缺陷、系統交互等潛在的深層次原因，難以適用于軟件密集型系統的安全性分析。

為了克服傳統事件鏈致因模型及安全性分析方法的局限性，Leveson［6］在系統論和控制論基礎上，提出新的安全性分析方法——系統理論過程分析（System Theoretic Process Analysis，STPA）。國內外針對該方法做了大量研究：文獻［7］提出不安全控制行為的生成算法，實現了STPA過程的部分自動化；文獻［8］將STPA方法與模型檢測技術相結合，并成功運用于汽車巡航控制系統的軟件安全性分析中。國內學者也在此方向開展探索，文獻［5］將STPA 致因分析與形式化方法結合，借助安全關鍵的應用開發環境（Safety Critical Application Development，SCADE）工具對起落架控制系統軟件進行形式化驗證，降低了分析過程中人為因素的影響；文獻［9］運用STPA 方法對平交道口控制系統進行安全需求分析，借助XSTAMPP 軟件，得到安全需求的形式化表達；文獻［10］運用STPA 方法對大飛機的除冰系統進行分析，得到軟件安全性設計需求，但是結果為自然語言。現有研究表明，使用STPA 方法進行軟件安全性分析時仍然面臨著以下挑戰：1）分析得到的安全性需求為自然語言，影響分析結果的完整性和客觀性；2）分析過程依賴人工或其他工具，分析效率低；3）缺乏較為完整的需求分析與驗證方法。

本文在STPA 技術基礎上，提出一種集圖形建模、形式建模和形式驗證于一體的軟件安全性分析方法，進一步提高分析過程的自動化程度。通過STPA分析得到軟件安全性需求，并自動生成安全需求的形式化表達式；根據系統控制行為邏輯，構建軟件安全控制行為的狀態圖模型，并將其自動轉化為形式化模型；借助模型檢驗工具完成軟件安全性驗證，結合某武器發射控制系統實例驗證方法的可行性。

1 軟件安全性需求分析與驗證方法框架

為了保證軟件密集型系統的安全性，必須從系統層面查找軟件安全性薄弱環節和問題機理，挖掘深層次的軟件安全性問題。在傳統STPA分析方法的基礎上，本文提出了一種軟件安全性需求分析與驗證方法，以某武器發射控制系統軟件為研究對象進行安全性驗證。方法總體框架如圖1 所示，主要實施步驟如下：

1）軟件安全性需求分析。根據整個系統功能組成，進行系統級事故與危險分析，并構建系統的分層控制結構模型，通過過程模型分析，確定潛在的軟件不安全控制行為，進一步提煉出軟件安全性需求。

2）軟件安全性需求的形式化規約。利用算法將分析得到的軟件安全性需求自動轉化為用線性時序邏輯語言描述的形式化表達式。

3）軟件安全控制行為建模。針對軟件實現的系統控制功能，對軟件的安全性控制過程進行抽象，構建軟件安全控制行為邏輯的狀態圖模型，并將其自動轉化為形式化語言。

4）軟件安全性驗證。借助模型檢查工具，采用形式化方法，完成對軟件安全性屬性的驗證。

圖1 基于STPA的軟件安全性需求分析與驗證方法框架Fig.1 Framework of software safety requirement analysis and verification method based on STPA

2 軟件安全性分析建模

通過過程分析，得到軟件安全性需求，并明確軟件安全性控制行為邏輯，這是進行安全性驗證的基礎。形式化方法具有語義嚴謹、數學基礎完備的特點［11］，為提高分析結果的可靠性，本文采用形式化語言對分析過程進行定義。

2.1 軟件安全性需求分析建模

在系統理論中，系統被視為層次化的控制結構，每層系統通過對下層系統施加約束實現控制［6］。安全控制結構描述了系統各組件之間的交互關系，定義如下：

定義1安全控制結構。將安全控制結構表示為五元組（CO，CA，AT，SE，CP）。其中：CO={CO1，CO2，…，COi}，代表一個或多個控制受控過程的軟件控制器，某一控制器COi可以表示為二元組COi=（CA，PM），CA是控制行為的集合，PM 是過程模型；AT是執行控制行為的執行器，SE是傳感器，負責傳遞受控過程狀態的反饋信息；CP是由控制器控制的一組受控過程。

過程模型是安全控制結構中受控過程假定狀態的模型，用于描述變量及變量之間的關系，以及受控過程狀態更改的邏輯。通過過程模型分析，可以識別出不安全控制行為，進而得到安全需求。為實現分析過程的自動化，規范分析過程，本文對過程模型分析做如下定義。

定義2過程模型。過程模型PM 是用于描述受控過程CP 假定狀態的模型，主要包含過程模型變量（Process Model Variable，PMV）及變量間的關系，當前狀態以及狀態轉移的邏輯。在控制結構圖中，過程模型通常作為控制器內部狀態的一部分。過程模型變量是一組影響控制行為CA 安全性的關鍵變量P 及其狀態S，其中P=∪(P1=v1，P2=v2，…，Pn=vn)，P1和Pn是控制器COi的過程模型變量及其值v1和vn。

定義3狀態組合表。令CAi為控制器COi向執行器ATi發出的控制行為，令PMV=∪(P1，P2，…，Pn)是一組過程模型變量，每個過程模型變量Pi具有Vi個變量值。每個過程模型的狀態都會對安全性造成影響，對于每一個控制行為，需要分析其在n 個過程模型不同狀態組合下是否危險。基于以下等式可以生成過程模型變量的狀態組合表TSC：

其中：×是笛卡兒乘積運算符，i是過程模型變量，n是過程模型變量的總數，狀態組合表是過程模型變量值之間的笛卡兒積。在實際分析中，將通過算法自動生成過程模型變量的組合集，并對生成的結果成對覆蓋，以最小化組合集的數量。

定義4 不安全控制行為。通過上述步驟分析每一個不安全行為的組合，剔除無危險的組合，進一步識別出不安全控制行為（Unsafe Control Action，UCA），用四元組（CA，CS，TSC，CT）表示，CA是不安全控制行為，CS=∪(P1=v1，P2=v2，…，Pn=vn)是CA 的相關過程模型變量的一組關鍵組合，TSC是控制行為CA 是否不安全的狀態組合信息，CT 是提供控制行為CA 的狀態組合類型：任何時間、過早或過晚。其中，“過早”或“過晚”的具體時間需要在自動生成的基礎上根據系統具體情況人工修改。例如，在文中某武器發射控制系統分析案例里，“過晚”是指解脫制動的動作時間必須控制在1.5 s內，否則發射能量已經注入，可能出現武器卡管的嚴重安全性事故，因此，系統判定為“過晚”。

2.2 軟件安全性控制行為建模

安全性控制行為模型（Safe Control Behavior Model，SCBM）主要包括對軟件安全性有影響的控制行為、相應的安全需求及影響系統狀態遷移的過程模型變量。模型結構可以用三元組（PMV，TS，CA）表示。PMV是一組安全關鍵過程模型變量；CA是安全控制行為的集合；TS是從安全需求中提取的狀態轉移條件集合，每個狀態轉移TSi都用語法TS=EV[SR]/TC表示。EV是導致狀態轉移TSi的輸入事件，SR是由不安全控制行為得到的相應安全性約束條件，它是一個限制TSi狀態轉移的布爾條件，TC是當布爾表達式有效時將執行的操作。

Simulink Stateflow 是基于有限狀態機理論的圖形化建模工具，具有直觀性強、支持仿真等優點，已經在工業界得到廣泛應用［12］。本文針對某武器發射系統功能特點，提出了系統控制行為邏輯模型的概念，并通過Stateflow實現了模型的構建。在模型中，通過entry、during和exit等不同類型的操作，可以更改軟件控制器的狀態，以及相應狀態下的過程模型變量值。通過過程模型變量值對當前的狀態轉移條件進行檢驗，并確定系統的后續遷移狀態。狀態轉移條件由分析得到的安全性需求確定。圖2 說明了如何將控制器的內部過程模型變量及其控制行為映射到安全控制行為模型中，具體規則如下所示：

1）軟件安全性控制行為模型應包括軟件控制器所有狀態下的過程模型變量：PMV ?SC∈SCBM，SC代表控制器狀態的集合。

2）狀態轉移條件由不安全控制行為的相應安全約束決定。

3）軟件控制器的所有過程模型變量都必須在模型中進行聲明。

4）在模型中定義名為controlAction 的枚舉類型變量，該變量包含軟件控制器的所有控制行為。軟件控制器進入當前狀態時產生的控制行為由controlAction變量提供。

圖2 過程模型變量及控制行為到安全性控制行為模型的映射規則Fig.2 Mapping rules of process model variables and control behaviors into safety control behavior model

3 軟件安全性需求驗證

3.1 安全性需求的形式化表達

傳統STPA 分析結果為自然語言，在解讀中可能存在歧義，同時，為了使用模型檢查工具進行形式化驗證，需要將分析得到的安全性需求用形式化語言表示。線性時序邏輯（Linear Temporal Logic，LTL）是為實現計算機程序形式化驗證而提出的一種規范表示法［13］，已被廣泛用于表達安全屬性。

若安全需求SRi對于所有路徑的執行結果都為True，那么它可以用以下LTL公式表示：

式（2）表示當系統安全需求為：當CS=∪(P1=v1，P2=v2，…，Pn=vn)時，該系統必須（或不得）提供控制行為CAi。基于以上定義，通過將過程模型分析得到的不安全狀態組合的布爾表達式轉換為LTL表達式，可以將STPA分析得到的軟件安全需求自動轉換為形式化規范語言，實現轉換的算法見文獻［14］。在該方法的基礎上，本文進一步提出軟件安全控制行為模型的概念。針對狀態圖模型難以直接被模型檢測工具驗證的問題，提出一種將軟件安全控制行為模型自動轉換為形式化模型的方法，借助成熟的模型檢測工具對軟件安全需求進行形式化驗證，進一步降低人工分析的影響。

3.2 安全控制行為模型的形式化描述

欲利用模型檢查工具對經過形式化處理的安全需求和系統安全控制行為模型進行驗證，需要將狀態圖模型轉換為符號模型驗證工具（Symbolic Model Verifier，SMV）語言描述的形式化模型。可擴展標記語言（Extensible Markup Language，XML）具有規范統一、互操作性強、可擴展等優點，為了方便實現轉換，首先將STPA 數據模型和Stateflow 數據模型分別導出為XML 格式。通過解析狀態圖模型的XML，生成安全控制行為模型的樹形狀態圖（Transition Tree Diagram，TTD），圖中的每個節點代表一種狀態。

在2.2 節分析的基礎上，本文提出了將描述系統控制行為邏輯的狀態圖模型自動轉換為形式化模型的方法，基本步驟如下，部分算法如算法1所示。

步驟1 將樹形狀態圖的根節點作為輸入，創建SMV 模型的主模塊。

步驟2 將根節點局部變量的數據類型映射到SMV 數據類型中，并為每個子節點聲明一個子模塊。

步驟3 用當前狀態節點的所有變量來創建子模塊的參數列表。

步驟4 對當前節點的狀態轉移進行解析，并創建當前狀態節點與其他狀態的轉移關系的真值表。

步驟5 把所有模塊生成的SMV 規范作為字符串保存到堆棧對象中，并把STPA 數據中的LTL 表達式添加到主模塊末。

算法1 生成SMV模型。

輸入 安全控制行為模型的樹型結構圖Ttd，STPA 數據模型DataModel，樹型結構圖節點a。

輸出：SMV模型SMVi。

4 安全性需求分析與驗證方法的應用

4.1 系統級分析

某武器發射控制系統是包括航行器、發射裝置、發控設備、軟件和人員等組成的能完成規定發射任務的綜合體，是一個集中指揮、綜合控制的復雜系統［14］。執行發射任務之前，航行器被固定在發射管中，“制止”狀態傳感器接通。下達發射指令后，系統檢查準備完畢，開始傳遞發射信號，當設備1 綠色狀態指示燈亮起，信號傳向設備2 且該設備綠色指示燈亮起后，發射模塊接收信號并操縱驅動裝置解脫對航行器的制動，使其在發射能量作用下出管。某武器發射控制系統的系統級事故主要包括：對人員造成嚴重傷害或死亡（A-1）、裝備損壞（A-2）、無法完成發射任務（A-3），系統級危險及其關聯的系統級事故，如表1所示。

表1 某發射控制系統的系統級危險Tab.1 System-level accidents of a launch control system

根據系統工作流程及相關組件，建立如圖3 的系統安全控制結構模型，通過識別系統控制和交互進一步分析潛在的不安全控制行為。

4.2 軟件安全性需求分析

在發射過程中，人員操作和發射控制系統軟件高度交互，控制行為頻繁。本文以系統對航行器“解脫制動”這一典型控制行為例，開展軟件安全性需求分析。

圖3 某武器發射控制系統安全控制結構Fig.3 Safety control structure of a weapon launch control system

STPA 方法將不安全控制行為分為4 類：1）未提供控制導致危險；2）提供控制導致危險；3）過早/過晚提供控制或者控制順序錯誤導致危險；4）控制行為持續時間過長或者過早停止導致危險。針對“解脫航行器制動”這一控制行為中的四類不安全控制行為逐一進行分析評估，如表2所示。

表2 解脫航行器制動的不安全控制行為Tab.2 Unsafe control behaviors of releasing the aircraft brake

在已有研究［14］基礎上，結合某武器發射控制系統實際，進一步完善設備指示燈狀態變量，并添加傳感器接收航行器狀態信號情況的過程模型變量，建立如圖4 所示的帶有過程模型的控制結構。

圖4 帶有過程模型的控制結構Fig.4 Control structure with process model

解脫制動控制行為擁有4個過程模型變量：

1）設備1 指示燈，擁有4 個狀態，分別為黃燈、綠燈、紅燈和熄滅狀態；

2）設備2 指示燈，擁有4 個狀態，分別為黃燈、綠燈、紅燈和熄滅狀態；

3）制動裝置，擁有3 個狀態，分別為完全提起、完全落下和中間狀態（卡滯）。

4）傳感器接收航行器狀態信號情況，擁有兩種狀態，分別是正常和故障。

每個過程模型的狀態都會對安全性造成影響，對于每一個控制行為，需要分析其在4 個過程模型不同狀態組合下是否危險。過程模型變量的狀態組合總數理論上為4×4×3×2=96 個，通過算法對生成的結果成對覆蓋（Pairwise），以最小化組合數量；同時剔除無危險的組合，最終得到30 種危險組合，由此得到30 條用自然語言描述的安全需求。因篇幅限制，生成的部分狀態組合表如表3所示。

表3 解脫航行器制動控制行為的部分狀態組合示例Tab.3 Some examples of state combinations of releasing the aircraft brake

4.3 軟件安全性驗證

通過分析得到了某武器發射控制系統的安全需求，但是其結果為自然語言。為了避免在解讀中存在歧義，影響分析效果，并且為了在下一步工作中使用模型檢查器進行形式化驗證，用上文中提出的算法將其轉換為LTL表達式，部分安全需求及相應的LTL表達式如表4所示。

表4 安全需求及相應的LTL表達式示例Tab.4 Examples of safety requirements and the corresponding LTL expressions

其中，SR1.27 表達式意為在一號設備指示燈為綠色、二號設備指示燈為紅色，制動裝置呈制止狀態且狀態傳感器工作正常的情況下，不允許提供解脫制動動作，這與系統安全要求一致。

借助Simulink Stateflow 工具來描述安全控制結構圖中過程模型變量之間的關系以及軟件控制行為對安全性的影響，如圖5所示。

圖5 軟件安全控制行為的Stateflow模型Fig.5 Stateflow model of software safety control behaviors

將系統安全控制行為模型轉換為SMV 語言，并運行模型檢查工具NuSMV 對生成的SMV 文件進行驗證。NuSMV 是基于二進制決策圖的符號模型驗證工具，支持LTL模型檢查，目前已廣泛應用于有窮狀態遷移系統分析［15］。NuSMV 版本為2.6.0，驗證過程耗時0.6 s。經驗證，所有的LTL 公式都得到滿足，沒有產生反例，這是因為構建的安全控制行為模型是根據分析得出的軟件安全性需求構建的，部分驗證結果如圖6所示。

圖6 NuSMV驗證結果Fig.6 NuSMV verification results

5 結語

本文研究STPA方法在軟件安全性分析中的應用，并結合某武器發射控制系統進行驗證。結果表明：1）通過對軟件安全性需求分析過程進行形式化定義，并將安全性需求自動轉化為形式化規范表達式，可以彌補傳統STPA方法分析結果為自然語言的缺陷，得到較為完備的軟件安全性需求。2）使用狀態圖模型對系統安全控制行為進行描述，并將其自動轉化為形式化模型，能夠實現STPA方法的形式化擴展。3）運用模型檢測工具對安全控制行為模型進行驗證，可以進一步實現分析過程的自動化，提高方法的分析效率。在未來工作中，將嘗試開展針對安全性的軟件測試方案的研究，進一步提高安全性需求分析與驗證的針對性和可靠性。