陳立前， 吳國福， 姜加紅

1. 國防科技大學計算機學院， 湖南 長沙 410073 2. 國防科技大學空天科學學院， 湖南 長沙 410073 3. 北京跟蹤與通信技術研究所， 北京 海淀 100095

0 引 言

隨著我國衛(wèi)星、大運載火箭、載人航天、探月計劃的發(fā)展，航天嵌入式軟件的規(guī)模和復雜程度日益增大，系統(tǒng)并發(fā)性不斷增強，軟件系統(tǒng)變得日趨龐大和難以駕馭，軟件系統(tǒng)中潛在的缺陷也越來越難以檢測、定位和控制[1].軟件故障已成為航天系統(tǒng)失敗的重要因素[2].源代碼級程序錯誤仍是航天嵌入式軟件中最突出的問題之一，數(shù)組越界、算術溢出、被零除、空指針解引用、數(shù)據(jù)競爭等問題仍經常發(fā)生.

靜態(tài)分析是一種在編譯時通過分析程序源代碼來推斷程序運行時性質的程序分析技術，是檢測代碼缺陷、提高代碼安全性與可靠性的一種重要技術.盡管程序分析是一類不可判定問題，然而通過適當?shù)某橄?，靜態(tài)分析能夠構造程序行為的某種近似，并得出有意義的分析結果.程序靜態(tài)分析的目標是在程序運行前盡可能多地發(fā)現(xiàn)其中隱含的錯誤，以提高程序的可靠性和安全性.對于一些常見的源代碼級程序錯誤，雖已有較成熟商業(yè)化靜態(tài)分析工具(如Coverity、Klocwork、Parasoft等)支持其檢測，但是這些工具主要基于語法規(guī)則、缺陷模式等開展分析，程序語義信息利用不夠，且對于航天嵌入式軟件中常見的中斷并發(fā)機制、浮點運算、面向可靠性的容錯設計等代碼特征和要素考慮不夠，因此這些工具還不能很好地適用于航天嵌入式軟件的分析.

為此，本文首先將分析航天嵌入式軟件代碼特征及常見錯誤.在此基礎上，介紹適合于航天嵌入式軟件錯誤檢測的靜態(tài)分析技術，包括抽象解釋、符號執(zhí)行、數(shù)據(jù)競爭檢測等.這些靜態(tài)分析技術都通過不同方式自動分析并利用了程序的語義信息.

1 航天嵌入式軟件代碼特征及常見錯誤

航天嵌入式軟件對可靠性要求非常高，軟件開發(fā)過程有嚴格的評審環(huán)節(jié)，軟件設計考慮容錯與冗余設計，軟件編碼實現(xiàn)遵循嚴格的安全編程規(guī)范.遵循嚴格的編程規(guī)范，使用程序語言的安全子集編程，從某些方面規(guī)避了程序錯誤的引入，也簡化了程序分析的難度，如無需考慮遞歸函數(shù)、非結構化程序結構(goto語句)等.但是，航天嵌入式軟件中也有一些特征和要素，也給程序分析帶來了挑戰(zhàn).

航天嵌入式軟件在本質上都是基于物理模型的，需要實現(xiàn)導航、姿軌控等模塊，因此不可避免地會包含大量數(shù)值計算，涉及許多整型、浮點型變量及其上的運算，從而容易導致除以零、整數(shù)溢出、浮點溢出等運行時錯誤[1].在涉及姿態(tài)軌道控制的功能實現(xiàn)方面，航天軟件會大量使用浮點運算.這些計算模塊的源數(shù)據(jù)來自敏感器模數(shù)(AD)轉換后的數(shù)據(jù)，如果不對數(shù)據(jù)的有效性進行檢查，數(shù)據(jù)處理過程中可能出現(xiàn)非法浮點數(shù)等問題，導致整個系統(tǒng)數(shù)據(jù)錯誤.同時，由于浮點數(shù)的有限二進質制表示，在處理極小數(shù)時，可能產生除以零的問題，導致無法得到正確結果.浮點的誤差累積可能對結果的計算精度造成較大影響.

為了更好封裝數(shù)據(jù)，航天嵌入式軟件會大量使用數(shù)組、結構體、聯(lián)合體等數(shù)據(jù)結構，從而容易出現(xiàn)初始化不完全、數(shù)組越界等數(shù)據(jù)使用問題.航天嵌入式軟件大部分使用C語言編程，程序代碼中會大量使用指針，經常會使用指針訪問內存絕對地址、數(shù)組、結構體或傳遞函數(shù)參數(shù)等.指針的使用增加了編程實現(xiàn)的靈活性，但C語言中指針不受約束，指針訪問可能超出所定義內存區(qū)域范圍，造成越界訪問，導致不相干數(shù)據(jù)被破壞、函數(shù)調用堆棧被覆蓋等嚴重問題.

航天嵌入式軟件功能復雜，往往采用多任務(多進程)設計，并且其執(zhí)行會受外部中斷源的影響.多任務調度、中斷處理帶來的并發(fā)可能導致數(shù)據(jù)競爭、數(shù)據(jù)訪問原子性違反等問題.數(shù)據(jù)競爭問題僅在特定外部環(huán)境和輸入下才會出現(xiàn)，難以測試、調試和復現(xiàn)，問題遺漏率較高，是航天嵌入式軟件可信性保障中最迫切需要解決的問題之一.

航天嵌入式軟件中可能包含符合設計的無限循環(huán)(如用于事件處理、采集數(shù)據(jù)等).但是，不符合預期設計的無限循環(huán)可能給系統(tǒng)帶來嚴重的后果.代碼設計邏輯不當會導致在某些條件下對循環(huán)變量進行更改，導致無法滿足循環(huán)退出條件.程序進入無限循環(huán)后，可能導致系統(tǒng)崩潰或者長時間占用CPU無法為其他模塊服務.

航天嵌入式軟件中往往融入三模冗余等容錯技術來提高系統(tǒng)的可靠性.比如，為了防止外空間高能粒子對RAM數(shù)據(jù)造成的翻轉破壞，對關鍵數(shù)據(jù)采用三取二的方式，即數(shù)據(jù)保存三份副本，使用時采用三取二的表決方式得到正確的值.數(shù)據(jù)保存三份副本，新數(shù)據(jù)產生時需要同步更新三份數(shù)據(jù)，可能由于人為疏忽造成數(shù)據(jù)更新不同步，帶來關鍵數(shù)據(jù)錯誤等問題.因此，需要從代碼層面檢查同時更新了三份數(shù)據(jù)以及表決程序本身代碼實現(xiàn)的正確性.此外，看門狗程序、數(shù)據(jù)緩沖模塊(乒乓存儲、環(huán)形緩存等)、數(shù)字濾波器等航天嵌入式軟件中常見模塊的正確性，也需要保證.

2 面向航天嵌入式軟件的抽象解釋技術

抽象解釋是一種對程序語義進行可靠近似的通用理論，可用于構造和逼近程序不動點，為靜態(tài)分析提供了一個通用的框架[3].基于抽象解釋的靜態(tài)程序分析框架一般包括編譯前端、不動點求解器和抽象域庫三個模塊.編譯前端主要負責將源程序建模成遷移系統(tǒng)，不動點求解器通過迭代的方式調用抽象域的操作來計算程序不變式，而抽象域庫一方面為靜態(tài)分析過程中需處理的值、表達式、約束等元素提供統(tǒng)一的數(shù)據(jù)類型，另一方面為區(qū)間抽象域、八邊形抽象域、多面體抽象域等抽象域的域操作提供了通用的接口.

上世紀九十年代末，基于抽象解釋的靜態(tài)分析工具已被用來識別導致阿麗亞娜5號火箭失效的程序錯誤和類似錯誤[4].近年來，基于抽象解釋的靜態(tài)分析工具在工業(yè)界大規(guī)模嵌入式軟件尤其是航空航天嵌入式軟件的分析與驗證中得到了成功應用[5-6].

PolySpace是最早采用抽象解釋的商業(yè)化靜態(tài)分析工具之一.目前，其產品Polyspace Code Prover，支持形式化地證明軟件中不存在嚴重的運行時錯誤(如不存在溢出、除以零、數(shù)組訪問越界等運行時錯誤)；其產品Polyspace Bug Finder，能夠檢查編碼規(guī)則、安全標準、代碼質量指標，并能發(fā)現(xiàn)嵌入式軟件代碼中的運行時錯誤、并發(fā)問題、安全漏洞等缺陷[7].最近，Alenia Aermacchi公司開發(fā)了符合DO-178B A級認證的 M-346教練機飛行控制系統(tǒng)自動駕駛儀軟件.在該自動駕駛儀軟件的開發(fā)和認證過程中，該公司使用了Polyspace靜態(tài)分析工具來檢查代碼中是否存在運行時錯誤，確保符合 MISRA C編碼標準，并為DO-178B A 級認證的取證提供了證據(jù)[8].

Cousot等[5]基于抽象解釋開發(fā)了程序靜態(tài)分析工具ASTREE，并以航空航天嵌入式安全關鍵軟件系統(tǒng)作為主要研究對象，分析和驗證這些軟件系統(tǒng)的一些關鍵性質，并自動檢測其中的運行時錯誤[6].這些錯誤包括數(shù)組越界、算術溢出、除以零等.ASTREE被成功應用于空客A340(約13.2萬行C 代碼)、A380(約35 萬行C代碼)等系列飛機的飛行控制軟件的分析，并實現(xiàn)了“零誤報”[9].在航天領域，ASTREE證明了歐空局“儒勒·凡爾納”號自動貨運飛船ATV (Automated Transfer Vehicle) 的自動對接軟件(約19萬行C代碼)不含運行時錯誤[10].最近，作為ASTREE的并發(fā)擴展版本，Miné等[11]基于抽象解釋開發(fā)了面向并發(fā)程序分析的商業(yè)化靜態(tài)分析工具AstreeA，并實際應用于空客飛行系統(tǒng)軟件的分析，被分析程序的最大規(guī)模達到百萬行C代碼.

NASA開發(fā)了基于抽象解釋的C程序運行時錯誤檢查工具C Global Surveyor(CGS)[12]，并成功地應用于Mars Path-Finder(13.5萬行代碼)、Deep Space One(28萬行代碼)、Mars Exploration Rover(65萬行代碼)等NASA的火星探測項目的軟件質量保證.CGS重點檢查C程序的三種運行時錯誤：訪問未初始化變量、訪問空指針、數(shù)組越界訪問.經過針對NASA軟件的優(yōu)化，其誤報率被控制在10%左右.同時CGS利用多處理器平臺支持對程序的并行分析，從而進一步提高了其可擴展性.

另外，Goubault等[13]基于抽象解釋開發(fā)了用來分析浮點程序中舍入誤差的傳播情況并發(fā)現(xiàn)舍入誤差的階及其源頭的靜態(tài)分析工具Fluctuat，并在ATV自動貨運飛船的監(jiān)控與安全保障單元(MSU)軟件等工業(yè)界航空航天控制軟件的分析與驗證中也得到了成功應用[10].

3 面向航天嵌入式軟件的符號執(zhí)行技術

符號執(zhí)行技術使用符號化的值(而非具體值)作為輸入，來(抽象)執(zhí)行程序.這樣，每次(抽象)執(zhí)行就可以覆蓋具有相同執(zhí)行路徑的多個輸入，分析器可以搜集每次執(zhí)行對應的路徑約束，然后通過約束求解器求解得到可觸發(fā)該路徑的具體輸入值.總體而言，相比抽象解釋符號執(zhí)行可以避免誤報.符號執(zhí)行發(fā)現(xiàn)的錯誤對應一條真實可行的路徑，從而可以生成觸發(fā)該錯誤的測試用例.符號執(zhí)行技術最初在上世紀70年代提出，但是當時的硬件和算法能力尚不夠，所以應用受限.近年來，隨著SAT和SMT求解技術的快速發(fā)展、相關判定算法的研究進展以及現(xiàn)代計算機運算速度的提升，符號執(zhí)行在越來越多的實際場景中變得適用可行，成為近十余年的研究熱點之一.基于符號執(zhí)行技術構建的分析工具和測試工具也逐漸被工業(yè)界所采納并使用.目前，比較著名的符號執(zhí)行工具有KLEE、SAGE、Pex、SPF、DART、CUTE、S2E、Cloud9等.

符號執(zhí)行技術對程序的路徑空間進行遍歷，是一種路徑敏感的分析技術，因此分析精度高.但是，當被分析程序具有較大規(guī)模時，符號執(zhí)行面臨路徑空間爆炸問題.為了提高符號執(zhí)行的可擴展性和效率，近年來，研究人員開展了大量研究，并提出了多種優(yōu)化技術.其中，將符號執(zhí)行與具體執(zhí)行相結合(稱為concolic execution)的思想的提出，對推動符號執(zhí)行的發(fā)展起了重要作用.Godefroid、Sen等人提出了動態(tài)符號執(zhí)行(dynamic symbolic execution)技術，將具體執(zhí)行(如隨機測試)和靜態(tài)符號執(zhí)行方法結合起來，使用具體執(zhí)行中的信息輔助符號執(zhí)行，增加覆蓋率，并能減少符號執(zhí)行的約束求解開銷.動態(tài)符號執(zhí)行有效緩解了第三方庫源碼不可見、復雜路徑條件(如非線性表達式、超越函數(shù)等)超出約束求解器能力范圍等靜態(tài)符號執(zhí)行面臨的挑戰(zhàn)性問題.

Java PathFinder(JPF)是美國NASA開發(fā)的面向Java字節(jié)碼程序的分析和驗證工具[14].該工具最早是基于模型檢驗思想設計的，用于檢測并發(fā)程序中的數(shù)據(jù)競爭、死鎖等問題.早期的JPF，將Java代碼翻譯為Promela代碼，然后使用模型檢驗工具SPIN來檢驗性質，并應用于航空領域實時操作系統(tǒng)DEOS的驗證中[15].后來，該工具逐漸引入靜態(tài)分析的思想，采用基于符號執(zhí)行的方法對軟件進行分析和驗證[16].JPF是NASA航天器控制軟件驗證的重要工具，如勇氣號、機遇號火星探測器的控制軟件都采用JPF進行了分析和驗證.

4 面向航天嵌入式軟件的數(shù)據(jù)競爭檢測技術

隨著航天軟件并發(fā)性不斷增強，數(shù)據(jù)訪問沖突問題已成為航天嵌入式軟件質量保障中最迫切需要解決的問題之一[17].數(shù)據(jù)訪問沖突是指多個并發(fā)執(zhí)行流(如任務、中斷、線程)對同一數(shù)據(jù)單元進行同時讀寫、且其中至少有一個操作是寫操作.由于數(shù)據(jù)訪問沖突中涉及的兩次訪問之間的次序不可確定，程序可能會因此產生異常行為，嚴重時甚至會導致軟件或系統(tǒng)失效.這類問題的產生是由于航天器的不同器件之間、多個并發(fā)運行的軟件之間存在復雜的數(shù)據(jù)交互，如果同步、互斥機制安排不當，很容易產生數(shù)據(jù)競爭、原子性破壞等數(shù)據(jù)訪問沖突問題，從而導致軟件和系統(tǒng)故障.已往的航天嵌入式軟件研制經驗表明，數(shù)據(jù)競爭問題僅在特定外部環(huán)境和輸入下才會出現(xiàn)，難以測試、調試和復現(xiàn)，問題遺漏率較高.同時，因為這類問題涉及到并發(fā)軟件之間的復雜交疊和時序關系，所以其檢測比較困難.基于模型檢驗和符號執(zhí)行的Java PathFinder(JPF)、基于抽象解釋的靜態(tài)分析工具AstreeA都支持多線程程序的數(shù)據(jù)競爭檢測.

航天嵌入式軟件的典型并發(fā)特征是中斷驅動.由于中斷導致的數(shù)據(jù)競爭問題，曾經導致多起系統(tǒng)故障，比如某衛(wèi)星帆板驅動線路盒轉角跳變導致控制偏差[18].據(jù)中國空間技術研究院軟件產品保證中心統(tǒng)計，在航天器總裝測試(AIT.)階段發(fā)現(xiàn)的軟件質量問題中，約80%都與中斷密切相關[18]，這已經成為影響我國航天任務完成的技術障礙.因此，研究針對中斷并發(fā)、中斷與任務共存相關數(shù)據(jù)競爭分析方法和工具具有重要現(xiàn)實意義.中斷驅動型軟件包含常規(guī)任務、中斷處理函數(shù)等成分，是一種特殊的并發(fā)軟件.一方面，中斷驅動型軟件的分析面臨一般并發(fā)程序的共性問題，即因為狀態(tài)的并發(fā)組合導致的整體狀態(tài)空間爆炸問題；另一方面，與一般的多線程程序不同，因為中斷觸發(fā)的不確定性和中斷控制的動態(tài)性，中斷驅動型程序的執(zhí)行過程，需要進行特殊的語義解釋.

除了航天領域，汽車電子領域的軟件也常常包含中斷.Schwarz等[19]提出了一種針對中斷驅動型程序的數(shù)據(jù)競爭檢測方法，其主要針對汽車電子領域使用天花板協(xié)議(priority ceiling protocal)的中斷程序.其主要思想是在抽象解釋框架下，使用任務與中斷間的全局不變式，并基于該不變式計算共享變量的資源鎖，然后通過資源鎖來判定程序中是否存在數(shù)據(jù)競爭，并開發(fā)了工具Goblint[20].目前，Goblint已成功應用于OSEK程序、Linux設備驅動程序等程序的數(shù)據(jù)競爭檢測和鎖錯誤檢測.

5 國內航天嵌入式軟件靜態(tài)分析工具研究

近年來，國內學術界和工業(yè)界在將靜態(tài)分析技術與工具應用于航天嵌入式軟件的質量保證方面開展了不少研究.尤其，國內航天軟件評測部門采用靜態(tài)分析技術也開發(fā)了一些面向航天軟件的靜態(tài)分析工具，并在實際航天軟件進行了應用，為航天軟件質量保證提供了有力支撐.北京軒宇信息技術有限公司研發(fā)的C/C++靜態(tài)缺陷檢測工具Sunwise SpecChecker支持安全編碼標準符合性檢查、運行時缺陷檢測和代碼質量度量等，采用跨函數(shù)、跨中斷的抽象解釋技術對程序進行高效的并發(fā)語義分析，除了支持如空指針、未初始化變量、數(shù)組越界、除零錯、整數(shù)溢出等運行時錯誤的檢測，還支持中斷數(shù)據(jù)訪問沖突缺陷的檢測.該公司研制的針對C語言程序的單元與集成測試平臺Sunwise AUnit，采用了動態(tài)符號執(zhí)行和約束求解技術來加速C程序測試用例的快速生成，提高了測試效率.這些工具已經在中國空間技術研究院全面應用，促進了型號軟件質量，并推廣至航空、電力等多個領域[21].王崑聲等[22]針對航天嵌入式軟件提出了一種基于屬性模型的運行時錯誤靜態(tài)分析方法，并開發(fā)了相應的工具，在航天嵌入式軟件上開展了實驗.

在航天嵌入式軟件數(shù)據(jù)競爭檢測方面，吳學光等[17]針對多重中斷航天嵌入式C程序開展了數(shù)據(jù)競爭及原子性檢測相關研究，并開發(fā)了多重中斷環(huán)境下數(shù)據(jù)競爭和原子性檢查工具MIDAC.該工具支持共享變量分析、數(shù)據(jù)競爭檢測、原子性違反檢測等.進一步，WU等[23]在有界模型檢驗框架下提出了一種面向多任務、多中斷嵌入式軟件的數(shù)據(jù)競爭檢測方法，將可能產生數(shù)據(jù)競爭的路徑條件編碼為SAT/SMT公式，然后通過判斷公式的不可滿足性來消除數(shù)據(jù)競爭誤報.進一步，WU等[24]提出了基于順序化的中斷驅動型程序的數(shù)值性質分析方法，將中斷驅動型程序順序化為帶非確定性的順序程序，然后使用面向順序程序的數(shù)值性質分析方法來分析順序化中斷驅動型程序，以檢查中斷驅動型程序中的數(shù)值相關運行時錯誤，并在真實航天軟件上開展了實驗.陳睿等[18]以航天嵌入式軟件數(shù)據(jù)競爭案例庫為基礎，經過系統(tǒng)分析，提出了刻畫有害中斷數(shù)據(jù)競爭的7種缺陷模式，并針對其中最常見且最難解決的單變量訪問序模式，提出一種支持過程間分析、中斷并發(fā)分析的高效檢測方法，設計并實現(xiàn)了相應的檢測工具SpaceDRC，在多個航天重點型號中進行了應用.進一步，陳睿等[25]設計開發(fā)了航天嵌入式軟件中斷數(shù)據(jù)訪問沖突基準測試集程序RaceBench，對SpaceDRC工具進行了評估.

表1 典型靜態(tài)分析技術及其在航天嵌入式軟件中的適用方面與可改進方面Tab.1 Static analysis techniques and its applications to aerospace embedded software

6 結 論

本文首先分析了航天嵌入式軟件的代碼特征及常見錯誤.在此基礎上，介紹了適合于航天嵌入式軟件錯誤檢測的靜態(tài)分析技術，包括抽象解釋、符號執(zhí)行、數(shù)據(jù)競爭檢測等.然后，介紹了國內近年來在面向航天嵌入式軟件的靜態(tài)分析技術與工具方面的研究進展.表1給出了本文主要介紹的抽象解釋、符號執(zhí)行兩種典型靜態(tài)分析技術及其優(yōu)缺點，以及在航天嵌入式軟件中的適用方面與可改進方面.限于篇幅,本文只是簡述了面向航天嵌入式軟件的一部分靜態(tài)分析技術及其進展[26].

雖然近年來國內在面向航天嵌入式軟件的靜態(tài)分析技術與工具方面取得了不少進展，未來需要進一步研究和開發(fā)適合于航天嵌入式軟件特征、支持領域關鍵模塊(如數(shù)據(jù)緩沖區(qū)等)、面向更多類型性質與缺陷、面向航天嵌入式軟件未來發(fā)展方向(如多核等)的靜態(tài)分析技術與工具，為載人航天、探月工程和衛(wèi)星等國家重大科技專項中的軟件質量保障提供支撐.