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

秦 楠，馬 亮，黃 銳

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

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

0 引言

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

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

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

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

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

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

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

3）軟件安全控制行為建模。針對軟件實現(xiàn)的系統(tǒng)控制功能，對軟件的安全性控制過程進行抽象，構(gòu)建軟件安全控制行為邏輯的狀態(tài)圖模型，并將其自動轉(zhuǎn)化為形式化語言。

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

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

2 軟件安全性分析建模

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

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

在系統(tǒng)理論中，系統(tǒng)被視為層次化的控制結(jié)構(gòu)，每層系統(tǒng)通過對下層系統(tǒng)施加約束實現(xiàn)控制［6］。安全控制結(jié)構(gòu)描述了系統(tǒng)各組件之間的交互關(guān)系，定義如下：

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

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

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

定義3狀態(tài)組合表。令CAi為控制器COi向執(zhí)行器ATi發(fā)出的控制行為，令PMV=∪(P1，P2，…，Pn)是一組過程模型變量，每個過程模型變量Pi具有Vi個變量值。每個過程模型的狀態(tài)都會對安全性造成影響，對于每一個控制行為，需要分析其在n 個過程模型不同狀態(tài)組合下是否危險?；谝韵碌仁娇梢陨蛇^程模型變量的狀態(tài)組合表TSC：

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

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

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

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

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

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

2）狀態(tài)轉(zhuǎn)移條件由不安全控制行為的相應(yīng)安全約束決定。

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

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

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

3 軟件安全性需求驗證

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

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

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

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

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

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

在2.2 節(jié)分析的基礎(chǔ)上，本文提出了將描述系統(tǒng)控制行為邏輯的狀態(tài)圖模型自動轉(zhuǎn)換為形式化模型的方法，基本步驟如下，部分算法如算法1所示。

步驟1 將樹形狀態(tài)圖的根節(jié)點作為輸入，創(chuàng)建SMV 模型的主模塊。

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

步驟3 用當前狀態(tài)節(jié)點的所有變量來創(chuàng)建子模塊的參數(shù)列表。

步驟4 對當前節(jié)點的狀態(tài)轉(zhuǎn)移進行解析，并創(chuàng)建當前狀態(tài)節(jié)點與其他狀態(tài)的轉(zhuǎn)移關(guān)系的真值表。

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

算法1 生成SMV模型。

輸入 安全控制行為模型的樹型結(jié)構(gòu)圖Ttd，STPA 數(shù)據(jù)模型DataModel，樹型結(jié)構(gòu)圖節(jié)點a。

輸出：SMV模型SMVi。

4 安全性需求分析與驗證方法的應(yīng)用

4.1 系統(tǒng)級分析

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

表1 某發(fā)射控制系統(tǒng)的系統(tǒng)級危險Tab.1 System-level accidents of a launch control system

根據(jù)系統(tǒng)工作流程及相關(guān)組件，建立如圖3 的系統(tǒng)安全控制結(jié)構(gòu)模型，通過識別系統(tǒng)控制和交互進一步分析潛在的不安全控制行為。

4.2 軟件安全性需求分析

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

圖3 某武器發(fā)射控制系統(tǒng)安全控制結(jié)構(gòu)Fig.3 Safety control structure of a weapon launch control system

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

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

在已有研究［14］基礎(chǔ)上，結(jié)合某武器發(fā)射控制系統(tǒng)實際，進一步完善設(shè)備指示燈狀態(tài)變量，并添加傳感器接收航行器狀態(tài)信號情況的過程模型變量，建立如圖4 所示的帶有過程模型的控制結(jié)構(gòu)。

圖4 帶有過程模型的控制結(jié)構(gòu)Fig.4 Control structure with process model

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

1）設(shè)備1 指示燈，擁有4 個狀態(tài)，分別為黃燈、綠燈、紅燈和熄滅狀態(tài)；

2）設(shè)備2 指示燈，擁有4 個狀態(tài)，分別為黃燈、綠燈、紅燈和熄滅狀態(tài)；

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

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

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

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

4.3 軟件安全性驗證

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

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

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

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

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

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

圖6 NuSMV驗證結(jié)果Fig.6 NuSMV verification results

5 結(jié)語

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