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

王鵬 吳康 閻芳 汪克念 張嘯晨

摘 要：現(xiàn)代安全關鍵系統(tǒng)的功能實現(xiàn)越來越依賴于軟件，這導致軟件的安全性對系統(tǒng)安全至關重要，而軟件的復雜性使得采用傳統(tǒng)安全性分析方法很難捕獲組件交互過程帶來的危險。為保證安全關鍵系統(tǒng)的安全性，提出一種基于系統(tǒng)理論過程分析（STPA）的軟件安全性驗證方法。在安全控制結構基礎上，通過構建帶有軟件過程模型變量的過程模型，細化分析危險行為發(fā)生的系統(tǒng)上下文信息，并以此生成軟件安全性需求。然后通過設計起落架控制系統(tǒng)軟件，采用模型檢驗技術對軟件進行安全性驗證。結果表明，所提方法能夠在系統(tǒng)級層面有效識別出軟件中潛在的危險控制路徑，并可以減少對人工分析的依賴。

關鍵詞：系統(tǒng)理論過程分析方法;軟件安全;形式化;模型檢驗;起落架控制軟件

中圖分類號：TP311.5;V247

文獻標志碼：A

Security verification method of safety critical software

based on system theoretic process analysis

WANG Peng1，2，3*， WU Kang1，3， YAN Fang1，2， WANG Kenian1，2， ZHANG Xiaochen1，2

1.Key Laboratory of Airworthiness Certification Technology for Civil Aviation Aircraft， Tianjin 300300， China;

2.College of Airworthiness， Civil Aviation University of China， Tianjin 300300， China;

3.College of Electronic Information and Automation， Civil Aviation University of China， Tianjin 300300， China

Abstract：

Functional implementation of modern safety critical systems is increasingly dependent on software. As a result， software security is very important to system security， and the complexity of software makes it difficult to capture the dangers of component interactions by traditional security analysis methods. In order to ensure the security of safety critical systems， a software security verification method based on System Theoretic Process Analysis （STPA） was proposed. On the basis of the security control structure， by constructing the process model with software process model variables， the system context information of dangerous behavior occurrence was specified and analyzed， and the software security requirements were generated. Then， through the landing gear control system software design， the software security verification was carried out by the model checking technology. The results show that the proposed method can effectively identify the potential dangerous control paths in the software at the system level and reduce the dependence on manual analysis.

Key words：

System Theoretic Process Analysis （STPA） method; software safety; formalization; model checking; landing gear control software

0?引言

現(xiàn)代安全關鍵電子系統(tǒng)由電子機械密集型向軟件密集型轉變，軟件在實現(xiàn)安全關鍵功能、控制和消除危害方面發(fā)揮著越來越重要的作用。近年來，安全關鍵領域因軟件故障造成的人員傷亡、財產損失等重大災害呈上升趨勢[1]，因此，需要對軟件進行安全性分析[2]，以便識別出安全關鍵系統(tǒng)的軟件中的危險行為，進而可以將危險行為轉化為安全性需求[3-4]，對軟件進行安全性驗證，以確保識別出的危險行為不會發(fā)生。傳統(tǒng)安全性分析技術是將硬件安全分析方法擴展到軟件領域，例如軟件故障樹分析（Software Fault Tree Analysis，SFTA）、軟件失效模式和影響分析（Software Failure Mode and Effects Analysis，SFMEA），是基于傳統(tǒng)鏈式/樹式事故因果模型的安全性分析方法，并且是為過去簡單、松耦合的系統(tǒng)而開發(fā)的，主要集中在故障事件上，而目前與軟件相關的系統(tǒng)危害是由軟件缺陷、軟件需求錯誤和組成系統(tǒng)的不同組件之間不受控制的交互作用造成的，確保系統(tǒng)的安全運行需要充分了解與軟件密切相關的潛在危險，以便在設計中消除它們。

針對傳統(tǒng)安全性分析方法的不足，Leverson等[5]提出了基于系統(tǒng)理論事故模型和過程（Systems Theoretic Accident Model and Processes， STAMP）的安全性分析方法——系統(tǒng)理論過程分析（System Theoretic Process Analysis， STPA）[6-7]，它將事故的潛在原因擴展為動態(tài)控制問題，而不是簡單的部件失效問題。在此基礎上，Thomas[8]提出了一種基于控制結構圖中各控制器的過程模型變量組合的STPA擴展方法，用于識別系統(tǒng)中存在的危險行為。Abdulkhaleq等[9]研究了使用STPA在系統(tǒng)級分析軟件安全性的可行性，并成功應用于汽車巡航控制系統(tǒng)的軟件安全性分析中。

但是STPA的分析過程依賴分析人員的經驗，容易對結果的完整性和客觀性造成影響。形式化方法[10]采用嚴謹?shù)恼Z義，描述STPA分析過程，并且可以運用數(shù)學方法對軟件的安全性進行驗證。

因此，本文在保證充分識別軟件中的危險行為基礎上，考慮減少對人工的依賴，提出一種基于STPA的安全關鍵系統(tǒng)的軟件安全性驗證方法。該方法以安全控制結構為基礎，分析得到危險行為，通過構建軟件過程模型，確定危險行為的過程模型變量組合，根據(jù)形式化定義的分析過程，生成危險行為發(fā)生的系統(tǒng)上下文信息及安全性需求，結合模型檢驗技術[11]，完成對軟件的安全性驗證。本文以起落架控制系統(tǒng)為案例，根據(jù)功能需求設計了起落架控制系統(tǒng)軟件[12]，采用STPA方法提取出軟件安全性需求，借助模型檢驗工具對軟件進行安全性驗證，驗證結果表明了該方法的可行性，并降低人工分析所可能引入錯誤的概率。

1?軟件安全性驗證方法總體架構

為了保證安全關鍵系統(tǒng)的安全，對軟件進行安全性分析時，不能只從軟件本身出發(fā)，必須從系統(tǒng)角度對軟件進行分析，考慮軟件使用過程中軟件與其他組件之間的交互作用，分析軟件可能的工作時序、使用條件、邏輯缺陷對系統(tǒng)造成的不利影響，基于此，本文提出了一種基于STPA的軟件安全性驗證方法。以前三點式收放起落架控制系統(tǒng)（Langding Gear Control System，LGCS）軟件為對象進行安全性驗證。驗證框架如圖1所示。驗證過程主要分為3個步驟：

步驟1?軟件危險行為識別。從系統(tǒng)規(guī)范出發(fā)，確定LGCS軟件失效可能導致的系統(tǒng)級事故與危險，構建軟件安全控制結構，識別軟件中的危險行為。

步驟2?致因分析。基于已確定的潛在危險行為，結合構建的軟件過程模型進行進一步細化分析，確定每個潛在危險行為是如何發(fā)生的，并轉化為相應的軟件安全性需求。

步驟3?軟件安全性驗證。軟件必須根據(jù)已確定的安全需求進行驗證，以確保潛在的危險行為不會發(fā)生，采用形式化的建模方法對軟件的功能需求和安全需求分別進行建模，借助模型檢驗工具，完成對軟件的安全性驗證。

2?軟件危險行為識別

確保系統(tǒng)的安全運行需要充分識別出軟件中的潛在危險行為，以便在軟件設計中消除它們。

2.1?定義系統(tǒng)級事故與危險

在STPA方法中，需要對所有控制行為所可能引發(fā)的系統(tǒng)級事故進行定義，并分析得到導致事故發(fā)生的相關系統(tǒng)危險。軟件中的不恰當控制行為是導致系統(tǒng)事故發(fā)生的重要原因，對軟件的安全性分析需要首先定義與軟件中的控制行為相關的系統(tǒng)級事故。由于起落架引起的事故主要集中在飛機的起飛和降落過程中，因此，本文定義安全性分析場景為飛機的起飛和降落過程。在此場景下，與LGCS的軟件控制器相關的系統(tǒng)級事故為：飛機不能正常降落（A1）、飛機不能正常起飛（A2）。根據(jù)系統(tǒng)級事故分析得到的危險包括：起落架未鎖定（H1）、起落架異常收起（H2）、起落架未放下（H3）。系統(tǒng)級事故及危險映射關系如表1所示。

2.2?構建安全控制結構

在確定系統(tǒng)級事故與危險后，需要分析軟件中可能存在的導致軟件在某種致因場景下對系統(tǒng)進行了危險控制的危險行為，致使系統(tǒng)級事故的發(fā)生。STPA方法中通過構建安全控制結構，分析各組件之間的交互關系，進而得到危險控制行為。本文對起落架系統(tǒng)工作原理和軟件的功能進行分析，構建了圖2所示的安全控制結構圖，包含了LGCS軟件控制器、起落架動作機構、液壓系統(tǒng)、飛行座艙系統(tǒng)。軟件控制器作為人與物理設備之間的交互樞紐，通過接收飛行員指令和飛行狀態(tài)信息，產生對系統(tǒng)的控制信號，分布在系統(tǒng)關鍵部位的傳感器會反饋系統(tǒng)狀態(tài)信息給軟件控制器，軟件控制器處理后傳遞給飛行座艙，告知飛行員當前起落架系統(tǒng)狀態(tài)， 形成了一個包含控制路徑和反饋路徑的閉環(huán)安全控制結構。

2.3?識別危險行為

根據(jù)安全控制結構能夠識別出軟件中可能存在的危險行為，而軟件中潛在的危險行為有可能只有在某些場景下才會導致系統(tǒng)危險，根據(jù)軟件安全性要求，均應被視為潛在危險行為，故作出如下假設：

假設1?飛行員的操作過程無危險性錯誤，且正確處理了系統(tǒng)提示信息，只要軟件提供錯誤信息就會導致系統(tǒng)級事故發(fā)生。

假設2?由于是對軟件的安全性分析，假設其他機械輔助控制方式失效，且來自其他系統(tǒng)和傳感器組件的信息均正常，軟件一旦出現(xiàn)危險行為將會導致系統(tǒng)級事故發(fā)生。

根據(jù)STAMP理論，將安全性問題當作系統(tǒng)控制問題，系統(tǒng)危險發(fā)生是由于對系統(tǒng)的不恰當控制造成的。軟件通過產生不恰當?shù)目刂菩盘枌е孪到y(tǒng)危險。Abdulkhaleq等[13]將STPA方法中的危險行為類型衍生為四種：沒有提供控制信號、提供控制信號、控制信號錯誤執(zhí)行時間、控制信號錯誤作用時間。本文以放下起落架控制信號作為控制行為為例進行說明，給出識別出的軟件中存在的危險行為，所得結果如下所示。

沒有提供導致危險（UCA1）?LGCS控制器沒有提供放下起落架控制信號（H3）。

提供導致危險（UCA2）?LGCS控制器提供放下起落架控制信號，導致起落架解鎖（H1、H2）。

錯誤執(zhí)行時間導致危險（UCA3）?LGCS控制器在起落架艙門打開之前提供放下起落架控制信號（H3）。

錯誤作用時間導致危險（UCA4）?LGCS控制器一直提供放下起落架控制信號，導致起落架無法被鎖定（H1、H2）。

3?致因分析

上述已經識別出了軟件控制器可能發(fā)生的危險行為，通過構建軟件過程模型可以進一步分析軟件危險行為在軟件控制器中是如何發(fā)生的，得到包含LGCS的軟件過程模型變量的軟件危險控制路徑，轉化為相應的軟件安全性需求。在STPA中，該過程通常依賴人工分析完成，容易受到人為因素的影響。因此，本文結合形式化方法，對軟件過程模型的分析過程進行了定義，規(guī)范了分析過程，分析結果將根據(jù)定義生成。

3.1?構建軟件過程模型

識別軟件過程中產生的影響控制行為安全性的變量，并將它們包含在控制結構圖的軟件控制器中，以記錄每個危險行為是如何發(fā)生的，構建了如圖3所示的包含軟件過程模型變量的軟件過程模型。

過程模型包含三種類型的變量（信息）：軟件控制器接收系統(tǒng)外部控制器信息、軟件控制器接收系統(tǒng)內部組件信息、軟件控制器的輸出信息。

這些過程模型變量可以用來細化分析每一個可能發(fā)生的危險控制行為的上下文信息及其控制路徑，并轉化為相應的安全約束。

3.2?形式化致因分析

構建了軟件過程模型后，需要對軟件過程模型進行分析。為了減少人工對軟件過程模型的分析過程，本文對軟件過程模型進行了形式化定義，通過定義四元組形式化描述軟件控制器在系統(tǒng)上下文信息下產生了某種類型的控制行為所導致的結果。四元組定義如下：

定義1?定義四元組（SC、CA、CT、ST）表示軟件控制器（SC） 在系統(tǒng)狀態(tài)下（ST）產生某種控制類型（CT） 的控制行為（CA）。其中：

SC表示能夠產生對系統(tǒng)的控制信號的軟件控制器集合，SC=（sc1，sc2，…，scn）。

CT代表控制行為類型集合，且CT={P，NP，ES，EAT}。其中P表示提供控制信號;NP表示沒有提供控制信號;ES表示控制信號錯誤的時序;EAT表示控制信號錯誤的作用時間。

CA表示軟件控制器產生的對被控對象的控制行為集合，且CA={ca1，ca2，…，can}。

ST表示控制行為發(fā)生時系統(tǒng)上下文信息集合，ST={st1，st2，…，stn}。

定義2?定義四元組UCA=∑（CA，ST）∧CT→H表示軟件控制路徑∑（CA，ST）以CT的控制類型發(fā)生時是否會對系統(tǒng)產生危險，其中∑（CA，ST）和CT滿足∑（CA，ST）×CT=∑ i，j（CA，ST）i·CTj，i為（CA，ST）可能的取值數(shù)，UCA∈U，U=∑ i，j（CA，ST）i·CTj→H，H∈Hazards，Hazards={Yes，No}。

結合上述形式化定義1和定義2，對帶有過程模型變量的起落架軟件過程模型進行形式化分析。其中，定義中的SC表示LGCS的軟件控制器;CA表示軟件控制器中的控制行為，軟件控制器的輸出信息作為軟件的控制行為作用于起落架的內部組件，對于LGCS而言，軟件控制器對起落架的控制行為為extend_EV和retract_EV。影響這些控制行為安全的系統(tǒng)上下文信息ST包含收放手柄的狀態(tài)信息handle={up，down}、飛機當前的飛行狀態(tài)信息flight={take_off，landing}以及監(jiān)控系統(tǒng)內部組件與軟件控制信號的健康信息state={normaly，anormaly};CT表示起落架的四種控制行為類型CT={P，NP，ES，EAT}。

為充分分析危險行為發(fā)生的上下文信息，為每個危險控制行為確定過程模型變量及其可能的組合。每個組合都將在四個控制行為類型中進行評估，以確定控制行為在系統(tǒng)上下文信息中是否是危險。在系統(tǒng)上下文信息中，如果某種控制類型的控制行為發(fā)生導致系統(tǒng)危險，那么控制行為將被認為是危險的，然后分析導致每個危險行為的潛在危險場景及控制路徑。本文是對軟件設計模型進行安全性驗證需要通過安全需求檢測出模型中的危險的狀態(tài)變遷，因此本文通過線性時序邏輯（Linear Temporal Logic， LTL）公式描述危險控制路徑和相應的安全性需求，對軟件設計模型的時態(tài)邏輯進行驗證。本文以收放手柄處于拉下位置，軟件控制器產生extend_EV信號為例進行說明，通過文中給出的定義1可以確定LGCS的軟件控制器中與之對應的關鍵變量，

表3中顯示了控制器產生entend_EV信號，在系統(tǒng)上下文信息ST所包含的關鍵過程模型變量可能的取值組合下，針對不同控制類型CT是否會對系統(tǒng)產生危險，由于以handle=down為例進行說明，表中確定了4種不安全的場景，并組合得到16個可能的結果。參照定義2，可通過LTL公式描述表3中所給出的軟件控制路徑及其對系統(tǒng)所產生的結果，首先可確定定義2中的i取值為4，采用LTL中的邏輯符號“∧”描述CA、ST、CT下的過程模型變量之間的關系;采用“→”符號表明控制行為到控制結果的遷移關系;采用“□”時間符號表示控制信號一直被提供。

表4為CT=P，UCA1的危險路徑及其對應的軟件安全性需求。安全性需求包含了軟件中關鍵的過程模型變量組合，能夠對軟件中的危險行為進行約束。

4?軟件安全性驗證

為了驗證通過STPA方法獲取的軟件安全性需求能夠正確約束軟件的危險行為，本文根據(jù)已有的起落架軟件功能需求設計了起落架軟件，采用的是法國愛斯特爾技術有限公司的安全關鍵的應用開發(fā)環(huán)境（Safty Critical Application Development， SCADE）[14]，一款通過了多個安全關鍵行業(yè)軟件工程標準認證的工具。該工具廣泛應用于安全關鍵領域的軟件建模。SCADE模型結合了Lustre和Esterel兩種形式化同步語言，以嚴格的數(shù)學理論保證設計的完整性和無二義性，集成的KCG代碼生成器能夠保證模型和代碼的一致性，已被廣泛應用于反應式系統(tǒng)的開發(fā)。

4.1?SCADE建模

4.1.1?起落架控制系統(tǒng)軟件建模

根據(jù)LGCS軟件的功能需求設計了如圖4所示的軟件控制器。LGCS軟件控制器接收傳感器的數(shù)據(jù)，對來自前、左、右起落架的組件狀態(tài)信息進行同步，保證對三點式起落架同步控制。同步后的狀態(tài)信息輸入給邏輯控制模塊，邏輯控制模塊根據(jù)狀態(tài)信息執(zhí)行邏輯控制，輸出對起落架組件的控制信號，起落架控制邏輯分為收起落架控制邏輯和放起落架控制邏輯。軟件控制器需要實時監(jiān)控起落架的狀態(tài)與控制信號之間的約束關系是否被滿足，并將監(jiān)控的狀態(tài)信息傳遞給飛行座艙，以便飛行員執(zhí)行相應操作，整個過程涉及到多方系統(tǒng)的交互，都將影響軟件控制器的執(zhí)行過程，因此需要識別出其中的危險交互場景，保證系統(tǒng)的安全。

4.1.2?安全需求建模

對于已經構建完成并通過功能測試的起落架軟件設計模型，需要在安全關鍵的應用開發(fā)環(huán)境（Safty Critical Application Development， SCADE）中建立觀察器模型，對其進行安全性驗證。觀察器模型根據(jù)已有的安全需求建立，由于SCADE中的邏輯建模符號與LTL公式語義相同，可直觀地進行轉換，提高了STPA方法與SCADE建模工具之間的結合效率，以便實現(xiàn)對軟件設計模型的安全性驗證。本文對表4中的軟件安全需求進行建模，將安全需求轉為了SCADE中對起落架控制軟件的觀察器模型，如圖5所示。

4.2?形式化驗證

SCADE的形式化驗證中，用戶不需要編寫傳統(tǒng)驗證流程中大量的測試用例和測試規(guī)程，只需要根據(jù)已有的安全性需求設計出安全屬性，通過SCADE對安全屬性建模，在SCADE中建立形式化驗證工程，自動化實現(xiàn)對設計模型的形式化驗證，驗證框架如圖6所示，分為軟件設計模型和觀察器模型。將軟件設計模型中的關鍵變量作為觀察器模型的輸入，對軟件進行約束。同時，考慮到軟件控制信號發(fā)出后，硬件返回狀態(tài)信息將會隨著變化，因為是對軟件的安全性驗證，所以假設系統(tǒng)硬件均正常，在觀察器模型中需要限定形式化驗證過程中的輸入，以便軟件能夠被正常執(zhí)行。

驗證環(huán)境為一臺搭載Intel Xeon E51620 v4的處理器、3.5GHz主頻、8GB內存的電腦，在該環(huán)境下運行SCADE形式化驗證引擎。

驗證結果表明，軟件設計中存在不符合安全需求的危險行為，并檢測出了潛在的危險行為UCA1，其中圖7（a）為SSR1.4的驗證結果，說明軟件中存在導致UCA1發(fā)生的危險路徑RUCA1.4，并且SCADE工具為SSR1.4生成一個反例，如圖7（b）所示。將反例導入到仿真工程中，通過單步調試搜索軟件設計中的危險路徑。在此之前本文已經分析得到了可能導致UCA1發(fā)生的危險路徑RUCA1.4，實現(xiàn)對危險行為的原因進行定位，可以減少人為分析的工作量。定位后只需分析已給出的導致違反SSR1.4的路徑，反例的仿真結果如圖7（c）所示，反例總共給出了15個周期的交互場景，在第13個周期時，Res4輸出為false，說明此時軟件中存在違反SSR1.4的危險行為，此時關鍵變量取值為{extend_EV=open，handle=down，state=anormaly， flight=take_off}，對比RUCA1.4可知extend_EV信號出現(xiàn)錯誤，有可能導致當飛機處于起飛狀態(tài)并且飛機未離開地面時，起落架異常解鎖，導致事故發(fā)生。該系統(tǒng)級事故發(fā)生是由于提供extend_EV信號導致的，而該信號是在一個交互場景中被異常提供，在進行模擬仿真時很難被發(fā)現(xiàn)，通過本文提供的系統(tǒng)安全性分析方法獲取的安全性需求，結合模型檢驗技術識別出了潛在的致因場景導致軟件危險行為的發(fā)生。根據(jù)發(fā)現(xiàn)的危險原因修改設計后，危險行為被消除，最終驗證通過。

5結語

本文結合民機起落架控制系統(tǒng)的設計過程，對系統(tǒng)安全性分析方法STPA在軟件安全性分析中的應用進行了研究。通過構建軟件過程模型，生成包含軟件過程模型變量的軟件危險控制路徑和安全性需求，結合模型檢驗工具實現(xiàn)自動的安全性驗證。結果表明：1）STPA安全性分析方法，可以在系統(tǒng)級識別出軟件的危險行為，并推導出相應的軟件安全性需求。2）對軟件過程模型的分析過程進行形式化定義，能夠生成包含軟件過程模型變量的軟件危險控制路徑和相應安全性需求。3）結合模型檢驗技術，能夠自動完成對軟件的安全性驗證; 同時，降低了安全性驗證過程中人為因素的影響，提高了分析結果的可靠性。但依然存在部分人工分析過程，需要進一步提高該方法的形式化過程，并開發(fā)相關工具自動化完成分析工作，以及開發(fā)LTL邏輯運算符與SCADE模型符號之間的轉換工具，以實現(xiàn)對安全關鍵系統(tǒng)軟件更高自動化的安全性驗證。

參考文獻 （References）

[1]?黃志球，徐丙鳳，闞雙龍，等. 嵌入式機載軟件安全性分析標準、方法及工具研究綜述[J]. 軟件學報， 2014， 25（2）：200-218. （HUANG Z Q， XU B F， KAN S L， et al. Survey on embedded software safety analysis standards， methods and tools for airborne system [J]. Journal of Software， 2014， 25（2）：200-218.）

[2]?DODD I， HABLI I. Safety certification of airborne software： an empirical study[J]. Reliability Engineering and System Safety， 2012， 98（1）：7-23.

[3]?朱丹江，姚淑珍，譚火彬. 基于場景控制特征的安全性需求分析方法[J]. 北京航空航天大學學報， 2016， 42（11）：2358-2370. （ZHU D J， YAO S Z， TAN H B. Safety requirements analysis method based on control characteristics of scenarios[J]. Journal of Beijing University of Aeronautics and Astronautics， 2016， 42（11）：2358-2370.）