軍工高安全軟件數(shù)值型運行時錯誤分析方法*

黃明，詹海潭，張偉，經(jīng)小川，李寧，王瀟茵

(1.中國工程物理研究院，綿陽621900;2.中國航天系統(tǒng)科學(xué)與工程研究院，北京100048)

軍工高安全軟件數(shù)值型運行時錯誤分析方法*

黃明1，詹海潭2，張偉2，經(jīng)小川2，李寧2，王瀟茵2

(1.中國工程物理研究院，綿陽621900;2.中國航天系統(tǒng)科學(xué)與工程研究院，北京100048)

提出一種抽象解釋和有界模型驗證的數(shù)值型運行時錯誤分析方法.利用抽象解釋方法分析程序數(shù)值變量范圍，獲得每個程序點達到不動點的變量初步值范圍信息.根據(jù)待分析的運行時錯誤類型，在相關(guān)需要檢測的程序點處將數(shù)值變量取值信息轉(zhuǎn)化為斷言或假設(shè)形式插入程序中，將帶有斷言和假設(shè)的程序轉(zhuǎn)化為布爾公式，驗證其可滿足性，進而驗證斷言的正確性.實驗證明，該方法與現(xiàn)有方法相比，在精度和效率兩方面都有良好的表現(xiàn).

抽象解釋;有界模型驗證;數(shù)值型運行時錯誤;值范圍分析

0 引言

軍工軟件即使經(jīng)過嚴格的測試，在運行過程中仍然可能并且已經(jīng)出現(xiàn)過非預(yù)期的潛通路、引發(fā)系統(tǒng)不安全狀態(tài)的軟件缺陷.其中，有一類錯誤是在特定的運行時條件下才可能出現(xiàn)的，簡稱“運行時錯誤”.運行時錯誤(run-time error)是程序在不斷的動態(tài)運行過程中產(chǎn)生的錯誤［1］.

所有運行時錯誤類別中，數(shù)組越界、除零操作、負數(shù)開偶次方、整數(shù)和浮點數(shù)的上溢出/下溢出4種運行時錯誤，簡稱“數(shù)值型運行時錯誤”可歸納為程序變量值范圍的分析與驗證.數(shù)值型運行時錯誤的檢查方法多種多樣，主要有人工審查、靜態(tài)分析、動態(tài)測試、形式化分析等，其中形式化分析方法是檢查數(shù)值型運行時錯誤非常有效的方法，包括抽象解釋、模型驗證、定理證明、約束求解等［2］.

大量實驗分析發(fā)現(xiàn)［3-4］抽象解釋和模型驗證方法在數(shù)值型運行時錯誤分析方面都發(fā)揮了作用，但還未達到精度和效率最優(yōu)化.抽象解釋的本質(zhì)是采用抽象域上的計算來代替程序具體對象域上的計算，通過損失精度求得計算上的可行性，因而抽象解釋的方法很難保證分析的精度［5］;模型驗證對于復(fù)雜系統(tǒng)，需要驗證的屬性數(shù)量龐大，可能會導(dǎo)致狀態(tài)空間爆炸，而有界模型檢驗方法避免了無窮系統(tǒng)導(dǎo)致的狀態(tài)空間爆炸，依據(jù)抽象解釋理論分析的完備性和模型檢驗分析的精確性的優(yōu)點，將抽象解釋理論與模型檢驗方法相結(jié)合是目前研究的熱點.

本文在對軍工嵌入式軟件運行時錯誤特點研究的基礎(chǔ)上，充分調(diào)研抽象解釋、模型驗證以及兩者相結(jié)合的現(xiàn)有方法，將基于抽象解釋的值范圍分析和有界模型驗證有機的結(jié)合起來，實現(xiàn)了自動化的高精度、高效率的檢測.通過抽象解釋方法，求得變量的初步值范圍信息，然后依據(jù)要檢查的運行時錯誤類型，在必要的程序點處插入相關(guān)斷言和假設(shè)，最后通過有界模型驗證檢查斷言的可滿足性進而確定該運行時錯誤是否可能發(fā)生.該方法縮小了模型驗證的搜索空間，提高了模型驗證的效率，在數(shù)值型運行時錯分析的精度和效率方面都有良好的表現(xiàn).

1 基于抽象解釋的值范圍分析

基于抽象解釋理論框架下所有計算都是在抽象域上進行，因此抽象域的設(shè)計是抽象解釋理論框架下的關(guān)鍵［6］.本文依據(jù)軟件的特點，設(shè)計了區(qū)間向量抽象域.在區(qū)間抽象域，求解程序的不動點獲得程序的不變量關(guān)系，進而獲得各程序點處每個數(shù)值變量的值范圍信息.

1.1 區(qū)間向量抽象域

充分考慮矩陣運算的分析精度及實用性，根據(jù)矩陣運算特有的運算性質(zhì)和規(guī)律，提出區(qū)間向量抽象域.將矩陣的各行各列分別抽象為一個區(qū)間，形成區(qū)間向量對，所對應(yīng)的元素交集表示矩陣元素［7］.

區(qū)間向量抽象域是在經(jīng)典的區(qū)間抽象域基礎(chǔ)［2］上，針對程序中的數(shù)組變量的表示而進行的擴展.對于給定的矩陣(數(shù)值型二維數(shù)組)A中假設(shè)包含m×n個元素，將實數(shù)矩陣轉(zhuǎn)化為區(qū)間矩陣，矩陣中每一行(列)的n(m)個區(qū)間元素由該n(m)個元素可能取到的最小值和最大值所構(gòu)成的區(qū)間來近似表示.因此，一個矩陣可以由列區(qū)間向量和行區(qū)間向量所組成的區(qū)間向量對來近似表示，其中向量元素是矩陣元素抽象后的形式化表示.

具體函數(shù)γiv是將區(qū)間向量抽象域向具體域具體化的過程，具體化過程是將行、列區(qū)間向量對應(yīng)的區(qū)間元素交集獲得矩陣中的相對應(yīng)的矩陣元素，形式化定義為:

抽象函數(shù)αiv是矩陣具體域向區(qū)間向量抽象域抽象化的過程，是將實數(shù)矩陣轉(zhuǎn)化為區(qū)間矩陣，區(qū)間矩陣的每一行列的所有區(qū)間元素的可能取值的最小值和最大值作為一個區(qū)間，表示該行列所有元素的可能取值的上界，形成區(qū)間向量對來實現(xiàn)矩陣的抽象過程.形式化定義為:

1.2 不動點求解

不動點求解是在程序控制流圖上采用迭代方式求解程序不動點，通常采用Worklist前向分析算法，根據(jù)控制流圖每條語句，使用對應(yīng)的抽象域上的操作算子計算最新結(jié)果，并依據(jù)遷移函數(shù)更新目標(biāo)節(jié)點的抽象值，順序遍歷完控制流上的節(jié)點.

遷移函數(shù)是指程序在執(zhí)行完一條語句之后，程序狀態(tài)發(fā)生的變化在抽象域上所表示的狀態(tài)遷移動作.基于抽象解釋的程序靜態(tài)分析，會在每個程序點創(chuàng)建一個抽象環(huán)境，用X#表示，即把所有程序變量映射到抽象域.

對于程序中矩陣元素的賦值語句A［i］［j］:= expr在抽象環(huán)境X#下，程序狀態(tài)發(fā)生變化，矩陣元素值需要更新，反應(yīng)在區(qū)間向量抽象域中則需要更新區(qū)間向量對中相應(yīng)的元素，賦值遷移函數(shù)形式為:

其中，［expr］#X#表示程序在某程序點對應(yīng)的抽象環(huán)境X#下計算表達式expr所得到的區(qū)間抽象值.

2 有界模型驗證

有界模型驗證把復(fù)雜狀態(tài)機模型及待驗證的屬性轉(zhuǎn)換成布爾表達式和斷言，利用SAT［8-9］工具進行求解以檢測各狀態(tài)的可滿足性.因為其對程序的遞歸調(diào)用層數(shù)和循環(huán)的次數(shù)都設(shè)定上界，這樣程序必然終止，可以將不可判定問題轉(zhuǎn)化為可判定問題，但如何設(shè)定有界模型驗證的上界，特別是對復(fù)雜程序來說，非常困難，設(shè)置過大會影響驗證的效率及準(zhǔn)確性，設(shè)置過小會導(dǎo)致對程序的驗證不全面.上述開展的基于抽象解釋的值范圍分析能在一定程度解決該問題，通過獲取各程序點處數(shù)值變量的初步值范圍信息，以假設(shè)(assume)形式插入程序中，可以指導(dǎo)有界模型驗證時界的設(shè)定，將循環(huán)展開次數(shù)確定在合適的范圍內(nèi).此外，程序中的假設(shè)還可縮小模型驗證時的值范圍搜索空間，進而提高驗證的效率.另一方面，對程序進行基于抽象解釋的值范圍分析后，根據(jù)程序點處數(shù)值變量的初步值范圍信息，可以剔除很多不可能發(fā)生錯誤的程序點，減少程序中插入斷言(assert)的數(shù)目，提高模型驗證的效率.

2.1 斷言和假設(shè)

本文提出依據(jù)待分析的數(shù)值型運行時錯誤類型，在需要檢測的程序點處將通過抽象解釋獲得的數(shù)值變量取值信息轉(zhuǎn)化為斷言或假設(shè)形式插入程序中，斷言作為能夠進行模型檢驗的屬性，而假設(shè)作為模型驗證的限制條件.對4類錯誤類型如何生成斷言和假設(shè)情況進行說明:

(1)除零運算:在進行除法運算的程序點處，判斷除數(shù)取值范圍是否包含0.如果包含則插入不為0的斷言，否則不插入斷言.同時在該程序點處以assume()的形式插入除數(shù)取值信息.

(2)數(shù)組越界:判斷數(shù)組下標(biāo)變量取值范圍是否落于數(shù)組最大界和最小界之內(nèi).如果可能大于上界，則插入小于上界的斷言;如果可能小于下界，則插入大于下界的斷言;否則不插入斷言.同時在該程序點處以assume()形式插入數(shù)組下標(biāo)取值信息.

(3)負數(shù)開偶次方:在進行開偶次方運算的程序點處，判斷被開方數(shù)的取值范圍是否包含負值，如果包含則插入被開方數(shù)為正的斷言，否則不插入斷言.同時在該程序點處以assume()形式插入被開方數(shù)取值信息.

(4)數(shù)值溢出:判斷變量取值范圍是否超過機器最大數(shù)，如果超過則插入小于機器最大數(shù)的斷言，否則不插入斷言.同時在該程序點處以assume()形式插入變量取值信息.

2.2 布爾公式可滿足性驗證

將帶有斷言和假設(shè)的程序轉(zhuǎn)化為布爾公式，包括限制條件和屬性.限制條件為程序的各賦值語句和假設(shè)，屬性為需要驗證的斷言.使用SAT驗證器判斷布爾公式的可滿足性，進而驗證斷言的正確性，若不正確，提供相關(guān)的反例路徑.

3 實例演示

本文以一實例來驗證某程序代碼片段(圖1)是否存在除零操作這類運行時錯誤.

圖1 某程序代碼片段Fig.1Program code snippet

(1)區(qū)間向量抽象域

依據(jù)圖1程序第一行a［3］［3］、b［3］［3］、c［3］［3］的定義，3個二維數(shù)組的抽象函數(shù)如下，通過抽象函數(shù)(參照公式(2))將具體域轉(zhuǎn)換成抽象域: αiv(a［3］［3］)＜［［0.2，0.5］［0.1，0.7］［0.1，0.6］］T，［［0.2，0.4］［0.1，0.7］［0.1，0.6］］＞αiv(b［3］［3］)＜［［0.2，0.6］［0.2，0.4］［0.1，0.5］］T，［［0.3，0.5］［0.2，0.6］［0.1，0.4］］＞αiv(c［3］［3］)＜［［0.0，0.0］［0.0，0.0］［0.0，0.0］］T，［［0.0，0.0］［0.0，0.0］［0.0，0.0］］＞

(2)求解不動點

運用不動點求解迭代算法求解圖1代碼中Line7處c［i］［j］在區(qū)間向量抽象域的取值信息.

Line5處第1次迭代，c［0］［0］∈［－0.3，0.1］，依據(jù)賦值遷移函數(shù)(公式(3))，得到二維數(shù)組c［3］［3］的抽象域表示如下:

循環(huán)結(jié)束之后，可得二維數(shù)組c［3］［3］的抽象域參照公式(1)，將迭代結(jié)束后c［3］［3］的抽象域轉(zhuǎn)換為具體域:

(3)插入斷言和假設(shè)

圖1代碼中Line 10處存在除法運算k=1/c［2］［2］，因而需要檢測該處是否存在除零操作的錯誤，即c［2］［2］的值是否等于0.通過(2)中的迭代計算，可得循環(huán)語句的計算達到不動點時，c［2］［2］的值在區(qū)間［－0.3，0.5］之內(nèi)，因而為了驗證c［2］［2］是否為0只需要在該處插入斷言assert(c［2］［2］＞0.0000001||c［2］［2］＜－0.0000001);同時，可在該程序點處插入c［2］［2］的取值信息assume(－0.3=＜c［2］［2］＜=0.5)，如圖2所示.

圖2 帶有斷言和假設(shè)的程序轉(zhuǎn)化為布爾公式的過程圖Fig.2The course of program with assumption and assertion translating to Boolean

(4)有界模型驗證

將帶有斷言和假設(shè)的程序轉(zhuǎn)化為布爾公式，如圖2所示.然后利用SAT模型驗證器，輸入布爾公式，輸出所有經(jīng)過驗證后的斷言及反例路徑.

1)對圖2中的for循環(huán)體展開，轉(zhuǎn)換成if結(jié)構(gòu)，內(nèi)循環(huán)和外循環(huán)的循環(huán)展開次數(shù)都為3;

2)將圖2中的循環(huán)體中的靜態(tài)獨立程序塊轉(zhuǎn)換成布爾公式，其中，限制條件(C)為程序塊中的各賦值語句和插入的假設(shè)－0.3=＜c［2］［2］＜=0.5，屬性(P)為需要驗證的斷言c［2］［2］＞0.0000001|| c［2］［2］＜－0.0000001;

3)為了驗證屬性P的正確性，首先將屬性P取反;然后將邏輯公式C∧P進行平坦化操作(flattening)，轉(zhuǎn)換為合取范式結(jié)構(gòu)(CNF);最后將CNF輸入驗證器MiniSat判斷公式的可滿足性.若滿足，說明屬性P被違反，也就是說存在某組值違背了屬性P，該斷言不正確，同時生成反例路徑.若不滿足，說明不存在任何一組值違背屬性P，該斷言正確.

4 試驗驗證

作者以抽象解釋和有界模型驗證相結(jié)合的數(shù)值型運行時錯誤分析方法為基礎(chǔ)開發(fā)了C語言程序運行時錯誤分析工具REC(Run-time error checker).為了研究REC與現(xiàn)有分析工具在準(zhǔn)確率和效率之間的差別，選取Astree和CBMC來與之比較.Astree是一個典型的基于抽象解釋的程序分析工具，依托于ENS Paris、CNRS、INRIA發(fā)起的ASTree項目，CBMC是一個典型的有界模型驗證工具，由牛津大學(xué)的系統(tǒng)論證團隊開發(fā)［10］.

本論文實驗對象選取某軟件的4個功能模塊，包括公共功能實現(xiàn)模塊(1489行)、1553功能實現(xiàn)模塊(4039行)、導(dǎo)航控制計算模塊(10503行)、制導(dǎo)任務(wù)功能實現(xiàn)模塊(15162行)，該控制軟件由C語言編寫，采用標(biāo)準(zhǔn)GCC編譯器編譯.實驗環(huán)境使用測試專用機，計算機的處理器為Intel(R)Core (TM)2 Quad CPU、CPU頻率為2.83GHz，內(nèi)存為3.5GB，操作系統(tǒng)為Windows Xp.在該環(huán)境下，采用Astree、CBMC和REC對以上4個功能模塊代碼中的除零操作進行檢測.

表1顯示工具REC、Astree和CBMC對4個程序進行分析的結(jié)果.3個工具的分析總時間分別為165.3min、289.9min和185.1min，CBMC的分析時間最長，Astree的分析時間最短，REC的分析時間居中，與Astree相差不大，比CBMC提高了36%的效率.同時，表1列舉了程序中確認的缺陷數(shù)，工具報告的缺陷數(shù)、誤報的缺陷數(shù)、漏報的缺陷數(shù)等幾個關(guān)鍵的指標(biāo).工具Astree、CBMC和REC的誤報率是65.8%，44.1%和37.1%，漏報率是13.8%、34.5%和24.1%.實驗結(jié)果表明REC工具在分析效率和準(zhǔn)確率方面都有良好表現(xiàn).

表13 種不同工具的分析結(jié)果Tab.1Analysis results with 3 different checkers

5 總結(jié)

本論文提出一種抽象解釋和有界模型驗證相結(jié)合的軟件數(shù)值型運行時錯誤分析方法，對程序進行數(shù)值型運行時錯誤的檢測.本文除零操作運行時錯誤進行了實例演示和相關(guān)實驗，結(jié)果顯示表明該方法在軟件運行時錯誤檢測的精度和效率方面都有明顯提高.

［1］梅宏，王千祥，張路，王戟.軟件分析技術(shù)進展［J］.計算機學(xué)報，2009，32(9):1699-1709.MEI H，WANG Q X，ZHANG L，et al.Software analysis:a road map［J］.Chinese Journal of Computers，2009，32(9):1699-1709.

［2］Cousot P，Cousot R.Abstract interpretation:a unified lattice model for static analysis of programs by construction or approximation of fixpoints［C］//Proceeding of the 4thACM Symposium on Principles of Programming Languages.New York:ACM，1977，238-252.

［3］Gopan D，DiMaio F.A Framework for numeric analysis of array operations［C］//Proceedings of the 32ndACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.New York:ACM，2005，338-350.

［4］侯蘇寧.基于抽象解釋的數(shù)值程序分析技術(shù)研究［D］.長沙:國防科學(xué)技術(shù)大學(xué)，2009.

［5］陳立前，王戟，劉萬偉.基于約束的多面體抽象域的弱接合［J］.軟件學(xué)報，2010，21(11):2711-2724.CHEN L Q，WANG J，LIU W W.Weak join for the constraint-based polyehdra abstract domain［J］.Journal of Software，2010，21(11):2711-2724.

［6］闞雙龍，黃志球，陳哲，徐丙鳳.使用事件自動機規(guī)約的C語言有界模型驗證［J］.軟件學(xué)報，2014，25 (11):2452-2472.KAN S L，HUANG Z Q，CHEN Z，et al.Bounded model checking of C programs using event automaton specifications［J］.Journal of Software，2014，25(11):2452-2472.

［7］李睿，連航，馬世龍，黎濤.基于形式化方法的航空電子系統(tǒng)檢測［J］.軟件學(xué)報，2015，26(2):181-201.LI R，LIAN H，MA S L，et al.Avionics system testing based on formal methods［J］.Journal of Software，2015，26(2):181-201.

［8］Drdobbs.Computing luminaries receive NSF grant to develop modeling tools for complex systems［J］.Dr Dobbs Journal，2009.

［9］王崑聲，詹海潭，經(jīng)小川，李寧，張剛.航天嵌入式軟件運行時錯誤靜態(tài)分析方法［J］.北京理工大學(xué)學(xué)報，2013，33(2):160-165.

［10］吳世堂，李寧，詹海潭.基于區(qū)間向量抽象域的數(shù)值程序分析算法［J］.計算機工程與設(shè)計，2015，36(2): 410-414.

Numerical Runtime Error Check of Aerospace Safety-Critical Software

HUANG Ming1，ZHAN Haitan2，ZHANG Wei2，JING Xiaochuan2，Li Ning2，Wang Xiaoyin2
(1.China Academy of Engineering Physics，Mianyang 621900，China; 2.China Academy of Aerospace Systems Science and Engineering，Beijing 100048，China)

A novel method of numerical runtime error analysis is presented based on abstract interpretation and bounded model checking.Firstly，the scope of program numeric variables is analyzed with abstract interpretation to obtain the variable range information of each program fixed point.Second，based on runtime error type to be analyzed，the value of the variable information is changed into the form of assertions or assumptions.Then the program is inserted at the detected point.Finally，the program is changed with assertions and assumptions into Boolean formula to verify the satisfiability of Boolean formula，and then to verify the correctness of the assertion.Experiment results show that the method has good performance both in terms of accuracy and efficiency compared with the existing methods.

interpretation;bounded model check;numerical runtime error; value analysis

TP311

A

1674-1579(2016)05-0058-06

10.3969/j.issn.1674-1579.2016.05.006

黃明(1972—)，男，高級工程師，研究方向為機械及裝備制造技術(shù);詹海潭(1988—)，男，工程師，研究方向為軟件分析驗證技術(shù);張偉(1978—)，女，研究員，研究方向為軟件安全性技術(shù);經(jīng)小川(1972—)，男，研究員，研究方向為信息安全技術(shù);李寧(1981—)，男，高級工程師，研究方向為信息安技術(shù);王瀟茵(1982—)，女，高級工程師，研究方向為信息安全技術(shù).

*國家自然科學(xué)基金資助項目(91418204).

2016-08-02