安全關(guān)鍵系統(tǒng)的?？臻g分析研究

陳高鋒，湯小明

(1.楊凌職業(yè)技術(shù)學(xué)院，陜西 楊凌 712100;2.西北工業(yè)大學(xué)自動化學(xué)院，陜西 西安 710072)

0 引言

根據(jù)民機適航標(biāo)準(zhǔn)DO-178B的規(guī)定，航空電子系統(tǒng)安全等級分為5級［1］。最高級別為安全關(guān)鍵級別，該級別的一個系統(tǒng)故障會引起飛機墜毀和人員傷亡。對于這樣的系統(tǒng)，不僅要保證系統(tǒng)開發(fā)生命周期的嚴(yán)格可控外，還需要進(jìn)行非?？量痰南到y(tǒng)分析，如時間分析、系統(tǒng)端到端延遲分析、通信分析以及空間分析等［2，7，12］。

近年來，對于航空電子系統(tǒng)來說，由于硬件的快速發(fā)展，特別是處理器速度的快速提升，各大飛機制造商(如波音和空客)從降低系統(tǒng)成本、能耗、重量以及空間等因素出發(fā)，紛紛要求或采納綜合模塊化的航空電子體系結(jié)構(gòu)(IMA)。

綜合模塊化航空電子系統(tǒng)要求能夠?qū)⑦^去獨立的多個具有不同安全關(guān)鍵級別的子系統(tǒng)綜合到單一的硬件平臺［11］。相對傳統(tǒng)計算機，該體系要求幾乎全新的系統(tǒng)設(shè)計、驗證與分析理論和技術(shù)。而支撐該體系的核心是具備時間、空間分區(qū)的操作系統(tǒng)軟件。

(1)時間分析方面。由于航空電子系統(tǒng)屬于強實時安全關(guān)鍵系統(tǒng)，其正確性不僅依賴于程序的邏輯，還依賴于程序的時間特性。某一任務(wù)必須在指定的時間范圍內(nèi)完成，否則會導(dǎo)致時限缺失(Missed Deadline)。一個時間缺失可能會引起系統(tǒng)的失效，而且對于這種故障類型，一般是由于離線或靜態(tài)時間分析的不足而引起，因此在產(chǎn)品運行時很難排除或恢復(fù)系統(tǒng)。如何對新的分區(qū)體系的航空電子系統(tǒng)進(jìn)行時間分析，目前國內(nèi)外還處在研究階段［4］。

(2)空間分析方面。一個由于存儲空間異常引起的系統(tǒng)故障，系統(tǒng)開發(fā)或維護(hù)人員很難從失效特征直接判斷到根原因。如圖1所示，一般故障的發(fā)生會經(jīng)歷故障(Fault)、錯誤(Error)、失效(Failure)3個階段。故障是失效的根原因(Root Cause)，錯誤表示系統(tǒng)出現(xiàn)持續(xù)的不期望的行為、條件或狀態(tài)，失效表示系統(tǒng)或部件不能滿足正常的規(guī)范或需求。由故障到錯誤的延遲稱為故障延遲(Fault Latency)，由錯誤到失效的延遲稱為錯誤延遲(Error Latency)。對于存儲異常，系統(tǒng)的故障處理機制一般只是觸發(fā)系統(tǒng)段異常(segmentation fault)，之后提供一個 Coredump功能。Coredump能夠?qū)⑾到y(tǒng)出現(xiàn)故障前的狀態(tài)進(jìn)行保存。然而，對于存儲異常，如棧溢出故障，系統(tǒng)的失效現(xiàn)場一般離真正的故障點差的很遠(yuǎn)。

圖1 故障-錯誤-失效模型

另外，存儲空間異常通常會引起整個系統(tǒng)崩潰，對于安全關(guān)鍵系統(tǒng)，系統(tǒng)的實效往往會引起墜機或人員傷亡。因此，安全關(guān)鍵系統(tǒng)空間分析的重要性是顯而易見的。

由于系統(tǒng)?？臻g的分析涉及系統(tǒng)動態(tài)運行狀態(tài)，而且目前航空電子系統(tǒng)領(lǐng)域多使用實時操作系統(tǒng)，操作系統(tǒng)的動態(tài)調(diào)度以及系統(tǒng)中中斷觸發(fā)的不確定性再次增加了對于系統(tǒng)?？臻g分析的難度。

1 系統(tǒng)棧空間分析

目前，商用操作一般都要求用戶在創(chuàng)建任務(wù)時指定任務(wù)對棧的需求大小。如圖2和圖3顯示實時操作系統(tǒng)VxWorks和QNX的任務(wù)創(chuàng)建函數(shù)，它們在任務(wù)創(chuàng)建時都要求用戶指定棧的大小。一般情況下操作系統(tǒng)或其分析工具并不能提供準(zhǔn)確的棧需求量，因此嵌入式軟件設(shè)計人員僅僅是通過局部變量使用情況進(jìn)行估算，并沒有考慮處理器體系、編譯器、中斷以及其它任務(wù)搶占等因素。由此非常容易造成棧溢出的故障。對于堆棧溢出故障，有可能出現(xiàn)系統(tǒng)崩潰(crash)或掛起(hung)，從而造成災(zāi)難性后果。

圖2 VxWorks中任務(wù)創(chuàng)建對?？臻g的需求

圖3 QNX中任務(wù)創(chuàng)建對棧空間的需求

棧的分析是安全關(guān)鍵系統(tǒng)驗證的重要組成部分，安全棧最大使用量的計算是棧分析的重要方式［6］，可以通過靜態(tài)分析或動態(tài)分析的方法得到。

在用戶設(shè)計中，如果沒有進(jìn)行確定的?？臻g分析，一般都會預(yù)留足夠大的閑余空間，而且既使是留了很大的空間，也并不能證明系統(tǒng)?？臻g是可靠了。實際上，中斷的觸發(fā)在程序的任何點都可能發(fā)生。本文論述一種方法，該方法能夠綜合考慮中斷的影響。由于該分析方法是基于目標(biāo)代碼，而非高級語言程序，因此同時考慮處理器和編譯器對棧的影響。

針對不同的程序設(shè)計方法，中斷對棧的影響會不同。因此，將現(xiàn)有系統(tǒng)抽象為下面2種假設(shè)。

假設(shè)1:程序由主程序和中斷服務(wù)程序組成。中斷不允許嵌套，也不允許搶占。棧的安全上限(Stack bound)可以由式(1)計算:

其中，depth(i)表示由中斷或函數(shù)i使用棧的最大量;inti表示中斷i。且有:

假設(shè)2:程序由主程序和中斷服務(wù)程序組成。中斷不允許自身嵌套，允許搶占。也即系統(tǒng)中只允許最多一個中斷服務(wù)程序?qū)嵗\行。棧的安全上限(Stack bound)可以由式(3)計算:

目前大多數(shù)系統(tǒng)都符合假設(shè)2程序的假設(shè)條件，但是由于嵌入式系統(tǒng)很少遇到像式(3)使用的最壞情況，所以，式(1)的計算過于樂觀，而式(3)的計算過于悲觀。因此，如何對程序及中斷分析，從而得到安全的棧最壞使用深度(Worst Case Stack Depth，WCSD)是本文要論述的重點。

1.1 綜合中斷影響的棧分析過程

對?？臻g的分析需要對匯編代碼進(jìn)行分析，同時與處理器體系相關(guān)。為此引入一種對程序的抽象方式，中斷搶占圖(Interrrupt Preemption Graph，IPG)。

中斷搶占圖是一種采用對目標(biāo)碼進(jìn)行數(shù)據(jù)流分析(結(jié)合控制流)的方法，得到程序中可能引發(fā)的中斷強占關(guān)系圖。從而可以分析中斷對系統(tǒng)棧的影響。結(jié)合程序調(diào)用可以分析軟件全局棧。

中斷搶占圖是一個帶權(quán)值的有向圖。每一個邊代表中斷搶占，而權(quán)值代表該搶占的中斷服務(wù)程序?qū)５男枨蟆?/p>

圖4表示在假設(shè)1下程序的中斷搶占圖。其中，中斷1對系統(tǒng)棧的單獨貢獻(xiàn)為12，中斷2對系統(tǒng)棧的單獨貢獻(xiàn)為25，中斷3對系統(tǒng)棧的單獨貢獻(xiàn)為7。圖5表示假設(shè)2對應(yīng)的中斷搶占圖，該圖表示打開所有中斷的情況。

圖4 假設(shè)1對應(yīng)的IPG

圖5 假設(shè)2對應(yīng)的IPG

棧的分析主要是對程序數(shù)據(jù)流的分析，因此需要分析出在一定輸入情況下，經(jīng)過對程序的符號執(zhí)行(Symbolic Execution)，分析出程序運行后數(shù)據(jù)的狀態(tài)。如圖6所示，在程序運行后需要知道寄存器R0和R1的狀態(tài)。

為此需要對程序進(jìn)行建模。假設(shè)安全關(guān)鍵系統(tǒng)中沒有遞歸調(diào)用和中斷自身嵌套，因此需要跟蹤程序中斷屏蔽寄存器(Interrupt Mask Register)來分析程序點的棧需求情況，并且為程序PC寄存器、通用寄存器和中斷相關(guān)的I/O寄存器進(jìn)行建模。

圖6 數(shù)據(jù)流的變化過程

目標(biāo)代碼或匯編代碼分析器設(shè)計中，一個重要的問題是針對不同的處理器體系設(shè)計每條指令的抽象版本［5］。為此引入位格圖(Bitwise Lattices)，圖 7顯示了1位寄存器的位格圖，在該圖中，1位可能的值為1、0或不能確定⊥。

圖7 1位位格圖

基于位格圖定義了 4種操作:and、or、xor和merge，如圖8所示。

圖8 位格圖上的操作

其中merge操作用來對控制流路徑進(jìn)行合并操作，例如if-then-else結(jié)構(gòu)的程序，可以看出分析程序采用了保守的操作方式來合并2個分支。

基于以上的位格圖及其操作，就可以分析程序的執(zhí)行過程。例如:如果 A=0b11001100，B=0bXXXX1111，則有:

根據(jù)IPG，通過反向(從葉子節(jié)點到根節(jié)點)遍歷IPG圖就可以得到系統(tǒng)的WCSD，中斷i的WCSD算法如下:

其中，depth(i)表示由中斷 i對棧的最大貢獻(xiàn)量;depth(i，j)表示在某程序點，中斷j使能時，中斷i對棧的最大貢獻(xiàn)量。

對于如PowerPC體系的處理器，其復(fù)位中斷為1號中斷，因此系統(tǒng)的 WCSD=WCSD(1);對于AVR處理器，其復(fù)位中斷為0號中斷，則系統(tǒng) WCSD=WCSD(0)。

在操作系統(tǒng)的設(shè)計中，除了使用高級語言，如C、C++、Perl等，還使用匯編代碼和in-line函數(shù)。在操作系統(tǒng)中使用in-line函數(shù)，一般具有2個目的:

(1)減少堆棧使用，不需要壓棧返回地址，標(biāo)志寄存器以及函數(shù)參數(shù)。

(2)提高執(zhí)行效率，程序不需要彈壓棧操作，被調(diào)函數(shù)與調(diào)用函數(shù)在同一個執(zhí)行環(huán)境中，以及可以更好地利用處理器寄存器等。

1.2 系統(tǒng)設(shè)計對棧的考慮

可以從以上的WCSD計算算法得出，如果IPG圖中有循環(huán)出現(xiàn)，如圖9所示，則使得該算法無法終止和WCSD的求解不確定。循環(huán)IPG使得棧安全的證明變得非常困難，因此在程序設(shè)計中需要避免出現(xiàn)導(dǎo)致循環(huán)IPG。

圖9 帶循環(huán)的IPG

循環(huán)IPG是由于中斷嵌套引起的，或者說前一個中斷還沒有結(jié)束，后一個中斷已經(jīng)開始運行，因此在安全關(guān)鍵系統(tǒng)設(shè)計中，為了保證系統(tǒng)棧深度的確定性，最好不要使用中斷嵌套。如果由于特殊需要如時鐘中斷，則在系統(tǒng)設(shè)計中需要非常小心地設(shè)計，以保證當(dāng)中斷強占時仍然能保證系統(tǒng)最大棧使用的確定性，如中斷函數(shù)可重入性、最大嵌套深度確定等。

此外，IPG圖中如果中斷過度被搶占(IPG圖的深度很大)時，需要進(jìn)行優(yōu)化設(shè)計。因為中斷的過度搶占會使系統(tǒng)任務(wù)相應(yīng)變慢，同時由于中斷的搶占破壞了程序的局部性，增加Cache實效(Cache missing)的可能性。

圖10 帶中斷的FCOS_domain_get_id調(diào)用圖

2 系統(tǒng)棧分析實例

目前，業(yè)界可以使用的棧分析工具主要有Utah大學(xué)的 Stacktool［6］和 Absint公司的 StackAnalyzer［8］。StackAnalyzer是商用軟件，支持多種主流處理器類型;Stacktool是一款開源的棧分析工具，目前僅支持Atmel(AVR交叉工具鏈)處理器。本節(jié)論述的系統(tǒng)棧分析是基于開源工具Stacktool進(jìn)行的。為了分析代碼，需要對體系結(jié)構(gòu)相關(guān)的代碼進(jìn)行改寫，主要是保留壓棧和彈棧的代碼，以及改變中斷相關(guān)寄存器的操作和指令，刪除其它匯編代碼。在對被分析代碼的修改過程中，盡量采用保守的方式，即如果對某個中斷屏蔽位不是非常確定其為0或為1，都強行將其置為0。

本節(jié)主要論述對安全關(guān)鍵操作系統(tǒng)FCOS［2-4］的棧分析過程。FCOS通過APEX接口向上層應(yīng)用提供服務(wù)，APEX接口是由航空電子標(biāo)準(zhǔn)ARINC653規(guī)定的分區(qū)操作系統(tǒng)為應(yīng)用提供的一個功能集［9］。APEX接口提供如分區(qū)管理函數(shù)、進(jìn)程管理函數(shù)、時間管理函數(shù)、分區(qū)間/分區(qū)內(nèi)通信函數(shù)以及健康監(jiān)控函數(shù)等，如表1所示。

表1 APEX接口

為了表述的簡便，以GET_PARTITION_STATUS函數(shù)的子函數(shù)FCOS_domain_get_id()的棧分析為例，論述棧分析過程。圖10顯示了FCOS_domain_get_id()的調(diào)用圖(Call graph)，可以看出該調(diào)用圖與常見的調(diào)用圖不太一樣，多了一些可能會搶占FCOS_domain_get_id()的函數(shù)或中斷。

圖11 函數(shù)FCOS_domain_get_id的棧分析報告

采用棧分析工具對函數(shù)FCOS_domain_get_id()分析后，得到如圖11的分析報告。其中正常使用的棧量表示該函數(shù)本身使用的棧大小，而最壞情況使用的棧大小表示綜合考慮全系統(tǒng)后的情況。另外，表2還列出了部分APEX接口的棧分析報告。

表2 FCOS函數(shù)棧分析

3 結(jié)束語

對于安全關(guān)鍵強實時系統(tǒng)，如飛行控制系統(tǒng)、發(fā)動機控制系統(tǒng)、醫(yī)療設(shè)備等，系統(tǒng)的空間分析變得非常重要，其分析結(jié)果直接影響到系統(tǒng)設(shè)計和系統(tǒng)驗證。特別是當(dāng)系統(tǒng)像綜合模塊化航空電子系統(tǒng)，需要綜合多個傳統(tǒng)的子系統(tǒng)與一個單一的硬件平臺時，系統(tǒng)的空間分析將直接關(guān)系到系統(tǒng)的整體規(guī)劃和綜合。同時由于系統(tǒng)集成商需要同時集成多個提供商的子系統(tǒng)，因此對空間分析的需求變得非常必要。本文論述一種系統(tǒng)?？臻g分析方法，并采用該方法對安全關(guān)鍵操作系統(tǒng)FCOS的?？臻g進(jìn)行分析。

［1］Vance Hilderman，Tony Baghai.Avionics Certification:A Complete Guide to DO-178B(Software)，DO-254(Hardware)［Z］.Avionics Communications Inc.，2007.

［2］Tang Xiaoming，Zhu Zhiqiang，Chen Nong.A safety critical operating system towards partitioning arichecture［C］//Proceedings of International Conference on Pacific Asian A-viation and Aerospace.2010.

［3］Tang Xiaoming，Zhao Yuting，Li Yinjuan，et al.A strongly partitioned operating system model for data link networks［C］//Proceedings of the 5th International Conference on Wireless Algorithms，Systems，and Applications.2010:274-281.

［4］Tang Xiaoming，Zhang Xinguo.Timing analysis of safety critiacl operating system FCOS［C］//Proceeding of International Conference on System and Networking on Education.2011.

［5］John Regehr，Alastair Reid.HOIST:A system for automatically deriving static analyzers for embedded systems［C］//Proceedings of Proceedings of the 11th International Conference on Architectural Support for Programming Languages and Operating Systems.2004:133-143.

［6］John Regehr，Alastair Reid，Kirk Webb.Eliminating stack overflow by abstract interpretation［J］.ACM Transactions on Embedded Computing Systems，2005，4(4):751-778.

［7］Legrand J，Singhoff F，Nana L，et al.About bounds of buffers shared by periodic tasks:The IRMA project［C］//Proceedings of the 15th Euromicro International Conference of Real Time Systems.2003.

［8］Absint.StackAnalyzer:Stack Usage Analysis［DB/OL］.http://www.absint.com/stackanalyzer/，2013-08-09.

［9］ARINC 653，Avionics Application Standard Software Interface［S］.

［10］Reinhold Heckmann，Christian Ferdinand.Verifying safety-critical timing and memory-usage properties of embedded software by abstract interpretation［C］//Proceedings of the Conference on Design，Automation and Test in Europe.2005:618-619.

［11］湯小明，李引娟，程農(nóng).VxWorks在飛行管理系統(tǒng)中的應(yīng)用研究［J］.計算機工程與設(shè)計，2011，32(3):52-56.

［12］湯小明，蘇羅輝，宋科璞.飛行管理系統(tǒng)AADL建模與分析［J］.計算機技術(shù)與發(fā)展，2010，20(3):91-94.

［13］武華，劉軍偉.基于 VxWorks的多任務(wù)程序設(shè)計［J］.計算機技術(shù)與發(fā)展，2010，21(9):163-166.

［14］程斐，苗克堅，王瑞敏.QNX與VxWorks的特性分析和實時性能測試［J］.計算機工程與設(shè)計，2008，29(18):4734-4735，4739.