航天嵌入式軟件數(shù)組越界缺陷特征研究

陳 睿， 于婷婷*， 賈春鵬， 李 超， 高棟棟， 江云松， 楊孟飛

1. 北京軒宇信息技術(shù)有限公司, 北京 100190 2. 北京控制工程研究所, 北京 100190 3. 中國空間技術(shù)研究院, 北京 100094

0 引 言

嵌入式軟件在航天器控制系統(tǒng)中的地位不斷提高，其可信性要求遠(yuǎn)高于一般軟件.然而由于嵌入式軟件及其運(yùn)行環(huán)境的特殊性，一些常見缺陷，如數(shù)組越界、除零錯(cuò)、未初始化內(nèi)存等仍是航天嵌入式軟件面臨的關(guān)鍵可信問題.其中,根據(jù)統(tǒng)計(jì),數(shù)組越界是近兩年航天嵌入式軟件開發(fā)過程中出現(xiàn)最多、最容易被遺漏的運(yùn)行時(shí)缺陷.當(dāng)數(shù)組越界發(fā)生在對(duì)關(guān)鍵數(shù)據(jù)的訪問時(shí),往往會(huì)出現(xiàn)非預(yù)期的行為，導(dǎo)致嚴(yán)重的安全性問題[1].如何高效檢測(cè)航天嵌入式軟件的數(shù)組越界問題是亟待解決的難題之一.

目前對(duì)安全性具有極高要求的系統(tǒng)多使用基于抽象解釋[2-8]、符號(hào)執(zhí)行[9-13]、程序模型檢驗(yàn)[14-16]等的數(shù)組越界檢測(cè)方法.在工業(yè)中得到一定應(yīng)用的檢測(cè)工具主要有基于抽象解釋技術(shù)的PolySpace[8]、Astree[4]、CGS[5]、IKOS[6],以及基于符號(hào)執(zhí)行技術(shù)的KLEE[12]、S2E[13]等.然而這些工具在實(shí)際應(yīng)用時(shí)存在過多誤報(bào)與漏報(bào)，仍需依賴大量的人工測(cè)試.這是由于任何程序分析技術(shù)都不能完全判定程序的任意不平凡性質(zhì)[17]，所以程序是否存在數(shù)組越界是不可判定的,導(dǎo)致檢測(cè)此問題缺少有效的通用算法. 另一方面由于無法通過代碼本身推測(cè)程序使用環(huán)境，使用靜態(tài)分析檢測(cè)軟件時(shí)往往會(huì)因?yàn)閷?duì)環(huán)境進(jìn)行過度近似，導(dǎo)致產(chǎn)生大量誤報(bào).

受軟件及缺陷特征的影響,同樣的方法應(yīng)用在不同領(lǐng)域、不同類別的程序中效果差異很大.而航天嵌入式軟件具有受中斷副作用影響、通過I/O數(shù)據(jù)與外設(shè)頻繁交互等鮮明的領(lǐng)域特征.結(jié)合領(lǐng)域特征、缺陷特征以及常見缺陷模式進(jìn)行針對(duì)性的分析是解決具體領(lǐng)域具體問題的有效方法.如何基于缺陷及航天嵌入式軟件特征，選取合適的環(huán)境近似策略，并對(duì)檢測(cè)方法進(jìn)行針對(duì)性優(yōu)化，是實(shí)現(xiàn)盡可能減少誤報(bào)的同時(shí)保證召回率的關(guān)鍵.

為了能夠針對(duì)航天嵌入式軟件提出有效的數(shù)組越界檢測(cè)方法，降低數(shù)組越界在實(shí)際工程中的遺漏,本文對(duì)航天嵌入式軟件數(shù)組越界問題展開缺陷特征實(shí)證研究.研究使用了近三年航天嵌入式軟件第三方測(cè)試中檢測(cè)出存在數(shù)組越界問題的94個(gè)真實(shí)案例.這些案例來源于航天器控制系統(tǒng)、航天器綜合電子系統(tǒng)等各類航天嵌入式軟件，均為開發(fā)方經(jīng)過多方測(cè)試依然遺漏的問題,代表了實(shí)際工程中最難解決的問題類型. 本文從數(shù)組越界模式以及數(shù)組越界表現(xiàn)形式兩個(gè)維度對(duì)這些案例進(jìn)行系統(tǒng)分析,提取出表1所示的10個(gè)非常有代表性的航天嵌入式軟件數(shù)組越界特征.通過分析這些特征, 總結(jié)了對(duì)確定缺陷檢測(cè)方法和具體分析策略具有重要作用的啟示(見表1)，對(duì)進(jìn)一步探索數(shù)組越界檢測(cè)算法的改進(jìn)方向奠定基礎(chǔ). 結(jié)合特征與啟示, 討論數(shù)組越界檢測(cè)算法針對(duì)航天嵌入式軟件的改進(jìn)方向.

表1 真實(shí)案例中數(shù)組越界特征與啟示Tab.1 Characterizations and implications of out-of-bounds array access bugs in real world cases

表2 數(shù)組越界模式定義Tab.2 Definitions of out-of-bounds array access pattern

1 研究方法

1.1 缺陷集

本文以2017年到2020年中國空間技術(shù)研究院型號(hào)軟件第三方評(píng)測(cè)問題庫、第三方評(píng)測(cè)遺漏問題庫和軟件問題案例庫作為缺陷來源.這些軟件覆蓋了近幾年我國研制和發(fā)射的各類空間飛行器中的關(guān)鍵嵌入式軟件，主要包括航天器控制軟件、航天器綜合電子軟件、航天器中央數(shù)據(jù)單元軟件以及各類遙測(cè)遙控軟件等.

本文通過“數(shù)組越界”、“下標(biāo)溢出”等關(guān)鍵詞在缺陷管理庫中進(jìn)行搜索和挖掘，經(jīng)過人工分析和確認(rèn)篩選出案例庫中全部數(shù)組越界問題共計(jì)94個(gè)，來自86個(gè)不同的軟件版本.其中人工確認(rèn)部分會(huì)逐個(gè)進(jìn)行問題單分析,并結(jié)合源代碼，確定為需要修改的程序問題.這些問題均為第三方測(cè)試階段,甚至更晚階段發(fā)現(xiàn)的數(shù)組越界問題,都是開發(fā)方經(jīng)過各類測(cè)試依然遺漏的問題,代表了實(shí)際工程中最難解決的問題類型.

1.2 特征分類

為了給將來的數(shù)組越界研究提供引導(dǎo)，本文從數(shù)組越界模式和數(shù)組越界表現(xiàn)形式兩個(gè)維度對(duì)上述案例進(jìn)行分析，收集并研究數(shù)組越界特征.重點(diǎn)討論如下幾個(gè)問題：

研究問題1：數(shù)組越界最常見的模式是什么

研究問題2：航天嵌入式軟件有什么程序特征？

研究問題3：數(shù)組下標(biāo)與幾個(gè)變量相關(guān)聯(lián)？

研究問題4：數(shù)組下標(biāo)與哪種運(yùn)算相關(guān)？

研究問題5：數(shù)組下標(biāo)的來源是什么,受什么影響？

(1)關(guān)于數(shù)組越界模式的研究將圍繞研究問題1展開.基于越界原因,數(shù)組越界模式可分為五類，包括常量下標(biāo)越界、變量下標(biāo)越界、下標(biāo)臨界、不一致定義和其他.詳細(xì)的模式定義可見表2.

(2)關(guān)于數(shù)組越界表現(xiàn)形式的研究將圍繞研究問題2、3、4、5展開.通過分析這些航天嵌入式軟件中數(shù)組越界問題的具體表現(xiàn),重點(diǎn)關(guān)注航天嵌入式軟件的程序規(guī)模與程序類型，以及與數(shù)組下標(biāo)相關(guān)的變量、運(yùn)算、函數(shù)等的分布情況.

1.3 有效性

與其余實(shí)證研究工作類似,特征研究的有效性主要與所研究案例、所使用缺陷和研究方法的代表性相關(guān).

關(guān)于研究案例的代表性,本文所研究的案例都是用C編寫的航天嵌入式軟件,是此類軟件中最廣泛應(yīng)用的編程語言.這些軟件來源于近三年的中國空間技術(shù)研究院第三方評(píng)測(cè)問題庫、第三方評(píng)測(cè)遺漏問題庫和北京控制工程研究所軟件問題案例庫,覆蓋了我國80%以上星(船、器)載嵌入式軟件.

關(guān)于所使用的缺陷的代表性,本文所使用的缺陷是從上述軟件中收集的全部數(shù)組越界問題,具有很好的代表性和說明問題的能力.

關(guān)于研究方法,本文分析了所使用案例及缺陷的所有相關(guān)信息，涵蓋多個(gè)版本的源代碼、第三方測(cè)試分析及程序員修改反饋等.

2 數(shù)組越界模式研究

在檢測(cè)軟件缺陷時(shí)，面對(duì)不同的數(shù)組越界模式通常需要采取不同的檢測(cè)方法.首先基于研究問題1(數(shù)組越界最常見的模式是什么？)展開研究.表3為統(tǒng)計(jì)的數(shù)組越界模式分布情況，依照研究方法所述可將數(shù)組越界模式劃分為5類，其具體分類與定義已在表2中給出.

表3 數(shù)組越界模式分布Tab.3 Distribution of out-of-bounds array access pattern

特征1:大多數(shù)(77.7%)數(shù)組越界問題都屬于變量下標(biāo)越界模式.啟示:檢測(cè)此類問題需要應(yīng)用程序分析方法進(jìn)行全面分析./*例1:變量下標(biāo)越界*/void loadCode(unsigned int CanBusNum){flameSucFlag[3];temp = (unsigned int)(2-busdata_buf[CanBusNum][250]);/* busdata_buf[CanBusNum] 可能等于3,那么temp ==(un-signed int) (-1)*/flameSucFlag[temp] =(flameSucFlag[temp]) | ((unsigned int) 1<<(busdata_buf[CanBusNum][250]));/* temp作為數(shù)組flameSucFlag[3]的下標(biāo),取值為-1時(shí)會(huì)造成數(shù)組越界*/}

特征1可以從表3中分析得出，這主要由于程序中很多作為數(shù)組下標(biāo)的變量或者來源于各種運(yùn)算、循環(huán)計(jì)數(shù)、外部函數(shù)、I/O數(shù)據(jù)等或者會(huì)受到它們的影響,程序員們往往會(huì)忽略掉判斷這些變量的取值范圍.比如例1中,數(shù)組busdata_buf[CanBusNum][250]的取值有可能等于3,經(jīng)過運(yùn)算之后temp的取值則為-1,接下來temp作為數(shù)組flameSucFlag的下標(biāo)則會(huì)造成數(shù)組越界.這些問題看似簡(jiǎn)單，但是在實(shí)際檢測(cè)中卻難以被發(fā)現(xiàn),是最為常見和棘手的數(shù)組越界模式.由于下標(biāo)變量來源及關(guān)系的復(fù)雜性,檢測(cè)這類問題需要用到符號(hào)執(zhí)行、抽象解釋等程序分析方法進(jìn)行全面分析.

特征2:一定數(shù)量的(20.2%)數(shù)組越界問題屬于常量下標(biāo)越界模式、下標(biāo)臨界模式和不一致定義模式.啟示:這些缺陷模式較為簡(jiǎn)單,可以通過模式匹配進(jìn)行檢測(cè).

除去大量因未對(duì)數(shù)組下標(biāo)預(yù)先做取值范圍判斷而造成的數(shù)組越界,研究表明還有相當(dāng)一定比例的數(shù)組越界屬于常量下標(biāo)越界模式(4.3%)，下標(biāo)臨界模式(13.8%)和不一致定義模式(2.1%).其中下標(biāo)臨界模式更為常見，這種情況多是由于程序員們?cè)谠L問長(zhǎng)度為n的數(shù)組時(shí),忽略了數(shù)組范圍為0～n-1,誤以為n也是數(shù)組的有效下標(biāo). 常量下標(biāo)越界大多由于數(shù)組定義時(shí)未能預(yù)先考慮是否滿足使用要求.而數(shù)組定義范圍不一致則是由于程序員們?cè)诙鄠€(gè)文件皆聲明了同一個(gè)數(shù)組, 定義存在一些差異導(dǎo)致同一數(shù)組長(zhǎng)度不一致,這種情況在后續(xù)訪問數(shù)組時(shí)極易造成數(shù)組越界.比如例2中,在頭文件中定義數(shù)組ramData的大小為2048,而在canDataParse-define.c文件中定義ramData的大小卻為2014.這3類缺陷模式都非常簡(jiǎn)單,可以直接通過模式匹配進(jìn)行檢測(cè).

*例2:不一致定義*//*canDataParse-define.h*/ extern unsigned char ramData[2048];/*canDataParse-define.c*/ unsigned char ramData[2014];/*例3:memset*/void McBSP1_ISR(void){signed int A_GD_RF_SCX[561];/*數(shù)組A_GD_RF_SCX長(zhǎng)度為561 int,即為2244char*/if(type==0x0000000C) memset((void*) & A_GD_RF_SCX,0,4488);/*memset長(zhǎng)度為4488,超過數(shù)組A_GD_RF_SCX長(zhǎng)度,引起數(shù)組越界*/}

此外,還有少數(shù)(2.1%)數(shù)組越界問題的成因不屬于上述情況,比如例3所示的memset長(zhǎng)度超出數(shù)組定義范圍也會(huì)造成數(shù)組越界,類似的還有strcpy等函數(shù)超范圍訪問引起數(shù)組越界.

3 數(shù)組越界表現(xiàn)形式研究

具有數(shù)組越界問題的數(shù)組和程序在表現(xiàn)形式上的特征對(duì)缺陷檢測(cè)技術(shù)的研究具有重要意義,根據(jù)不同特征可以更有針對(duì)性地選取檢測(cè)方法，探討具體改進(jìn)策略.接下來將按照研究方法所述從數(shù)組越界表現(xiàn)形式這個(gè)維度探尋航天嵌入式軟件中該缺陷的特征.根據(jù)這些特征,討論關(guān)于數(shù)組越界檢測(cè)方法的啟示,為后面探索現(xiàn)存檢測(cè)方法的改進(jìn)方向奠定基礎(chǔ).

3.1 航天嵌入式軟件有什么程序特征？

為了更好地刻畫和理解航天嵌入式軟件的數(shù)組越界問題,首先需要了解航天嵌入式軟件的程序特點(diǎn),以及它們的軟件規(guī)模.明確了這些問題,才能從中得到關(guān)于航天嵌入式軟件檢測(cè)技術(shù)的啟示,更有針對(duì)性地探討此類程序數(shù)組越界檢測(cè)方法的前進(jìn)方向.

特征3:所有程序均為中斷驅(qū)動(dòng)型程序.啟示:檢測(cè)方法應(yīng)支持對(duì)中斷的處理.

研究發(fā)現(xiàn),所有程序都是中斷驅(qū)動(dòng)型程序(特征3),數(shù)組下標(biāo)取值中受到中斷副作用影響的程序占總量的22.3%.比如例4中數(shù)組retSum就會(huì)受中斷副作用影響. CNT作為一個(gè)全局變量當(dāng)大于等于10000時(shí)，主程序會(huì)產(chǎn)生一個(gè)警告，并對(duì)數(shù)組retSum的下標(biāo)做加一操作.然而由于中斷影響，CNT達(dá)到數(shù)值后可能會(huì)執(zhí)行中斷程序而被重置為0,這導(dǎo)致主程序不能產(chǎn)生警告,數(shù)組retSum的下標(biāo)也不能做加一操作.

/*例4:中斷*/void CheckFunc(){ while(1){ if(CNT>=10000) assert(retSum[temp++]); /*若CNT大于等于10000,則*/}void interrupt CheckFunc(void){ CNT++; if(CNT>10000) CNT=0; /*若中斷執(zhí)行到CNT>10000,則CNT會(huì)被置0*/}

因?yàn)槭褂弥袛嗍呛教烨度胧杰浖钪饕奶卣髦?故而在檢測(cè)此類軟件時(shí)需要支持對(duì)中斷的處理.然而由于軟件特征、編碼規(guī)范、開發(fā)習(xí)慣等因素,數(shù)組下標(biāo)受中斷副作用影響的程序比例卻比較低.由于中斷驅(qū)動(dòng)型程序精確分析的開銷很大,結(jié)合特征3，可知在精準(zhǔn)性、效率和可靠性的取舍中,效率和可靠性對(duì)于程序的整體分析更為重要.

特征4:單文件規(guī)模小,跨文件的數(shù)值引用關(guān)系少.啟示:對(duì)于航天嵌入式軟件,程序分析無需跨翻譯單元,無需考慮大規(guī)模程序,也可以取得較好的效果.

對(duì)比非嵌入式軟件,航天嵌入式軟件單文件代碼行數(shù)較少,95.7%的文件不超過5000行,86.2%的文件不超過2000行,僅4.3%的數(shù)組下標(biāo)越界檢測(cè)需要進(jìn)行跨文件的數(shù)值分析.這主要源于航天嵌入式軟件單文件功能需求少、跨文件交互少的特點(diǎn).故而對(duì)于此類軟件，程序檢測(cè)時(shí)不需要考慮大規(guī)模程序，也不需要跨翻譯單元分析.

3.2 數(shù)組下標(biāo)與幾個(gè)變量相關(guān)聯(lián)？

如前文所述，數(shù)組越界模式中分布最為廣泛的是未判斷作為數(shù)組下標(biāo)變量的取值范圍.若要更好地檢測(cè)這類數(shù)組越界問題,首先需要了解數(shù)組下標(biāo)與變量之間的關(guān)聯(lián)情況.當(dāng)涉及到變量之間的關(guān)聯(lián)情況，數(shù)量級(jí)的信息是最為重要的，所以接下來關(guān)心的重點(diǎn)是數(shù)組下標(biāo)關(guān)聯(lián)變量的數(shù)量分布.

特征5:幾乎所有數(shù)組下標(biāo)與不多于4個(gè)變量存在關(guān)聯(lián)關(guān)系.啟示:程序分析需要考慮變量間關(guān)系,但數(shù)組下標(biāo)與其他變量間的關(guān)系并不復(fù)雜,無需進(jìn)行復(fù)雜的變量間關(guān)系分析.

將數(shù)組下標(biāo)所包含的變量稱為下標(biāo)包含變量,并將下標(biāo)包含變量和與下標(biāo)包含變量有運(yùn)算關(guān)系的變量稱為下標(biāo)關(guān)聯(lián)變量. 例5中，數(shù)組InsBufTwo的下標(biāo)包含變量為j和subInsCnt,下標(biāo)關(guān)聯(lián)變量則為j、subInsCnt、inslen和temp.由此可知，數(shù)組InsBuffTwo的下標(biāo)關(guān)聯(lián)變量的個(gè)數(shù)為4個(gè).

/*例5:關(guān)聯(lián)變量*/void main(){ inslen = temp & 0xFF; subInsCnt = 0; for (j = 0; j < inslen; j++) { InsBufTwo[j + subInsCnt] = InsBuf[j] subInsCnt = subInsCnt + 1; }}

圖1所示為下標(biāo)關(guān)聯(lián)變量的分布圖.由分布圖可知，72.3%的數(shù)組下標(biāo)存在1～2個(gè)關(guān)聯(lián)變量,并且數(shù)組下標(biāo)關(guān)聯(lián)變量一般不多于4個(gè)(根據(jù)圖1統(tǒng)計(jì)圖,下標(biāo)關(guān)聯(lián)變量大于5的數(shù)組個(gè)數(shù)為0).這表明在做相關(guān)程序分析時(shí)需要考慮變量間的關(guān)系，但與此同時(shí)，因?yàn)閿?shù)組下標(biāo)與其他變量之間的關(guān)系并不復(fù)雜，所以可以不需要進(jìn)行復(fù)雜的變量間關(guān)系分析.

圖1 下標(biāo)關(guān)聯(lián)變量分布圖Fig.1 Distribution of related variables for index variables

3.3 數(shù)組下標(biāo)與哪種運(yùn)算相關(guān)？

除去討論數(shù)組下標(biāo)與變量的關(guān)聯(lián)問題,要分析數(shù)組下標(biāo)變量取值范圍,還要考慮數(shù)組下標(biāo)與運(yùn)算的關(guān)聯(lián).比如例1是運(yùn)算時(shí)未判斷變量范圍造成的數(shù)組越界.那么需要討論如下問題：數(shù)組下標(biāo)與何種運(yùn)算相關(guān)？了解航天嵌入式軟件中數(shù)組下標(biāo)的關(guān)聯(lián)運(yùn)算的構(gòu)成,對(duì)于探索數(shù)組越界的檢測(cè)方法會(huì)產(chǎn)生很有價(jià)值的啟示.

特征6:數(shù)組下標(biāo)相關(guān)運(yùn)算中超過90%的運(yùn)算為線性運(yùn)算.啟示:分析方法不需要精確處理非線性關(guān)系,簡(jiǎn)化非線性運(yùn)算對(duì)分析精度不會(huì)產(chǎn)生很大影響.

將數(shù)組下標(biāo)關(guān)聯(lián)變量涉及的運(yùn)算稱為下標(biāo)相關(guān)運(yùn)算.分析發(fā)現(xiàn)航天嵌入式軟件中下標(biāo)相關(guān)運(yùn)算只有少量的非線性運(yùn)算(僅有9.6%), 90.4%的運(yùn)算為線性運(yùn)算.其中賦值運(yùn)算占54.1%,加減運(yùn)算占18.8%,邏輯運(yùn)算占17.7%,乘除運(yùn)算占5.9%(除法占1.2%),位域運(yùn)算占3.5%.

既然數(shù)組下標(biāo)相關(guān)運(yùn)算中非線性運(yùn)算很少,那么在對(duì)航天嵌入式軟件的數(shù)組越界分析中不需要精確處理非線性關(guān)系,可以在一定程度內(nèi)簡(jiǎn)化非線性運(yùn)算,并且不會(huì)對(duì)數(shù)組越界的分析精度產(chǎn)生很大的影響.

特征7:數(shù)組下標(biāo)相關(guān)運(yùn)算中幾乎不存在浮點(diǎn)轉(zhuǎn)換運(yùn)算.啟示:在數(shù)組越界檢測(cè)中,可以忽略所有浮點(diǎn)運(yùn)算,將所有浮點(diǎn)數(shù)看作任意值,在檢測(cè)精度不會(huì)受到很大影響的同時(shí)可以有更高的效率.

所研究的問題中沒有浮點(diǎn)數(shù)到數(shù)組下標(biāo)相的轉(zhuǎn)換,也即數(shù)組下標(biāo)的相關(guān)運(yùn)算中幾乎不存在浮點(diǎn)轉(zhuǎn)換運(yùn)算.那么在檢測(cè)數(shù)組越界缺陷時(shí),可以忽略掉所有的浮點(diǎn)運(yùn)算,將所有浮點(diǎn)數(shù)看作任意值,檢測(cè)精度不會(huì)受到很大影響,反而可以得到更好的效率.

3.4 數(shù)組下標(biāo)的來源是什么，受什么影響？

要分析數(shù)組下標(biāo)變量取值范圍,還需要考慮數(shù)組下標(biāo)的來源.所以本節(jié)將討論如下問題：數(shù)組下標(biāo)多來源于什么？受什么影響比較大？

特征8:部分(22.3%)數(shù)組下標(biāo)受函數(shù)參數(shù)影響.啟示:數(shù)組越界檢測(cè)需要使用上下文敏感的程序分析方法.

研究問題中，數(shù)組下標(biāo)受函數(shù)參數(shù)影響的程序占22.3%,但函數(shù)調(diào)用層數(shù)不深,通常不多于4層.這意味著對(duì)航天嵌入式軟件進(jìn)行數(shù)組越界檢測(cè)時(shí),需要使用上下文敏感的程序分析方法來分析函數(shù)對(duì)數(shù)組下標(biāo)所造成的影響.

特征9:近半數(shù)(40.4%)數(shù)組下標(biāo)受外部I/O數(shù)據(jù)影響.啟示:對(duì)外部I/O數(shù)據(jù)的取值、時(shí)序進(jìn)行建?？梢源蟠筇岣哽o態(tài)分析精度.

嵌入式程序的輸入幾乎全部來自于總線數(shù)據(jù)，I/O數(shù)據(jù)在程序中的表現(xiàn)為:來源于絕對(duì)地址、每次讀取的值可能不同、每次寫入的影響不能確定、讀取到的值的變化不能通過程序判斷.研究發(fā)現(xiàn)I/O數(shù)據(jù)參與數(shù)組下標(biāo)運(yùn)算的程序占40.4%.會(huì)產(chǎn)生這種情況因?yàn)榍度胧杰浖饕攸c(diǎn)之一是使用大量總線數(shù)據(jù)作為輸入.例6中,cmdlen的取值受函數(shù)Read1553BMem的調(diào)用結(jié)果,而Read1553BMem的數(shù)據(jù)來自I/O數(shù)據(jù).

由于大量程序的數(shù)組下標(biāo)會(huì)受到I/O數(shù)據(jù)影響,而I/O數(shù)據(jù)具有不確定性和時(shí)間相關(guān)性,在相關(guān)檢測(cè)時(shí),若能對(duì)對(duì)外部I/O數(shù)據(jù)的取值、時(shí)序進(jìn)行精準(zhǔn)可靠的建模,則可以大大提高航天嵌入式軟件靜態(tài)分析精度.

特征10:超過一半(68.1%)數(shù)組下標(biāo)受循環(huán)計(jì)數(shù) 或其相關(guān)變量影響.啟示:分析方法必須支持高效的循環(huán)程序處理,同時(shí)分析方法需要具有處理循環(huán)變量與下標(biāo)關(guān)聯(lián)變量關(guān)系的能力

研究表明,68.1%的程序中數(shù)組下標(biāo)來自于循環(huán)體內(nèi)循環(huán)計(jì)數(shù)或其相關(guān)變量,且循環(huán)次數(shù)可能很大.比如例7中當(dāng)i循環(huán)計(jì)數(shù)到取值150時(shí),作為數(shù)組PRoffset的下標(biāo)會(huì)造成數(shù)組越界(PRoffset長(zhǎng)度為150).

由于航天嵌入式軟件中數(shù)組下標(biāo)與循環(huán)變量的高相關(guān)性與循環(huán)次數(shù)的高上限,在選取數(shù)組越界檢測(cè)方法的時(shí)候,能否高效的處理循環(huán)、能否較精確的描述循環(huán)變量與數(shù)組下標(biāo)關(guān)聯(lián)變量的關(guān)系是選擇的重要依據(jù).

4 特征研究對(duì)改進(jìn)檢測(cè)方法的探討

本章在特征研究和啟示的輔助下，探討數(shù)組越界檢測(cè)算法針對(duì)航天嵌入式軟件的改進(jìn)方向.為了簡(jiǎn)化表述, 對(duì)于具體特征將使用表1中的特征簡(jiǎn)稱代替.

根據(jù)函數(shù)參數(shù)使用特征(特征8)，航天嵌入式軟件數(shù)組檢測(cè)需要使用上下文敏感的程序分析方法.根據(jù)程序規(guī)模特征(特征4),對(duì)于航天嵌入式軟件無需做跨文件分析.結(jié)合這兩個(gè)特征可以確定:以文件為單位,使用函數(shù)內(nèi)聯(lián)方式的過程間分析是航天嵌入式軟件數(shù)組越界檢測(cè)的最佳方法.

若考慮基于抽象解釋的缺陷檢測(cè)方法，根據(jù)關(guān)聯(lián)變量特征(特征5)與運(yùn)算操作特征(特征6),使用凸抽象域,并使用變量關(guān)聯(lián)作為變量分組依據(jù)可以在航天嵌入式軟件數(shù)組越界檢測(cè)中獲得較好的性能和準(zhǔn)確率.并且由于循環(huán)計(jì)數(shù)影響特征(特征10)，航天嵌入式軟件中68.1%的數(shù)組下標(biāo)與循環(huán)變量相關(guān),且循環(huán)次數(shù)可能很大,能否高效的處理循環(huán)、能否較精確的描述循環(huán)變量與數(shù)組下標(biāo)的關(guān)系是抽象域選擇的重要依據(jù).由于浮點(diǎn)轉(zhuǎn)換運(yùn)算特征 (特征7), 航天嵌入式軟件幾乎沒有浮點(diǎn)運(yùn)算結(jié)果到數(shù)組下標(biāo)的轉(zhuǎn)換,在數(shù)組越界檢測(cè)中,忽略所有浮點(diǎn)運(yùn)算,將所有浮點(diǎn)數(shù)看作任意值,在檢測(cè)精度不會(huì)受到過多影響的同時(shí)可以獲得更好的效率.

使用中斷是航天嵌入式軟件最主要的特征之一,幾乎所有程序都為中斷驅(qū)動(dòng)型程序(特征3),檢測(cè)方法必須支持對(duì)中斷的處理.然而由于軟件特征、編碼規(guī)范、開發(fā)習(xí)慣等因素,數(shù)組下標(biāo)受中斷副作用影響的程序比例僅為22.3%.由于中斷驅(qū)動(dòng)型程序精確分析開銷很大,對(duì)于整體分析而言,相較于精確性,效率和可靠性更為重要.同時(shí),根據(jù)I/O數(shù)據(jù)使用特征(特征9),在分析中考慮I/O數(shù)據(jù)將大大提高航天嵌入式軟件靜態(tài)分析精度.由于I/O數(shù)據(jù)的不確定性和時(shí)間相關(guān)性,如何如何盡可能精準(zhǔn)地刻畫I/O數(shù)據(jù)的取值和行為是提升嵌入式軟件值分析精確性的關(guān)鍵問題.

5 相關(guān)工作

數(shù)組越界缺陷實(shí)證研究：缺陷實(shí)證研究近年成為軟件工程研究的熱點(diǎn),比較著名的工作有LU等[18]針對(duì)真實(shí)并發(fā)缺陷的實(shí)證研究,CHEN等[19]針對(duì)中斷數(shù)據(jù)競(jìng)爭(zhēng)缺陷的實(shí)證研究，以及ISLAM等[20]針對(duì)深度學(xué)習(xí)程序缺陷的實(shí)證研究.此類工作多是為了從程序缺陷特征出發(fā)研究現(xiàn)存檢測(cè)工具以及主流檢測(cè)技術(shù)的優(yōu)劣勢(shì)，對(duì)探索應(yīng)用于特定缺陷、特定領(lǐng)域檢測(cè)方法的改進(jìn)方向起重要的指導(dǎo)作用.

目前已有一些關(guān)于數(shù)組越界缺陷實(shí)證研究的工作，然而都面向一般開源軟件，并且聚焦安全漏洞相關(guān)的緩沖區(qū)溢出缺陷，不能體現(xiàn)航天嵌入式軟件中數(shù)組越界的缺陷特征.WILANDER等[21]使用20個(gè)緩沖區(qū)溢出的程序缺陷對(duì)4個(gè)檢測(cè)緩沖區(qū)溢出的動(dòng)態(tài)分析工具做了實(shí)證分析.他們的研究發(fā)現(xiàn)即使最好的工具也只能檢測(cè)50%的問題,并且其中有6個(gè)類型不能被任何工具檢測(cè)出.

FANG等[22]對(duì)緩沖區(qū)溢出缺陷做了實(shí)證研究來分析現(xiàn)存的檢測(cè)工具和方法.他們發(fā)現(xiàn)多數(shù)檢測(cè)都使用了模糊測(cè)試方法,卻很少使用靜態(tài)檢測(cè)方法.

在最近的工作中,YE等[23]分別對(duì)63個(gè)真實(shí)項(xiàng)目中的100個(gè)緩沖區(qū)溢出缺陷版本和修復(fù)版本進(jìn)行分析,展開了關(guān)于緩沖區(qū)溢出靜態(tài)檢測(cè)工具的實(shí)證研究.并且比較了Fortify, Checkmarx和Splint等工具的檢測(cè)效率(efficiency)和有效性(effectiveness).他們的研究結(jié)果為后續(xù)相關(guān)檢測(cè)方法提供了一些啟示.

DUDINA[24]分析了一些流行的緩沖區(qū)溢出測(cè)試集以及從實(shí)際應(yīng)用程序中提取的缺陷片段,從而研究靜態(tài)分析器難以發(fā)現(xiàn)的缺陷類型.他的研究表明過程間分析、路徑敏感分析和循環(huán)處理是必不可少的檢測(cè)技術(shù).基于此工作,他認(rèn)為在現(xiàn)有基礎(chǔ)上改進(jìn)字符串處理,并與污點(diǎn)分析相結(jié)合是未來的改進(jìn)方向.

不同于上述工作，本文是已知首個(gè)針對(duì)嵌入式軟件中的數(shù)組越界開展的實(shí)證研究，主要目的是探索靜態(tài)檢測(cè)方法在檢測(cè)數(shù)組越界缺陷時(shí)的改進(jìn)方向.本文分析的數(shù)組越界案例都來源于真實(shí)的航天嵌入式軟件,能夠真正從實(shí)際出發(fā)得出針對(duì)中斷驅(qū)動(dòng)型程序的重要啟示.

數(shù)組越界檢測(cè)研究：目前存在很多靜態(tài)數(shù)組越界檢測(cè)工具[5,6,8,25-27],其中應(yīng)用比較廣泛的商業(yè)工具Polyspace具備理論上無漏報(bào)的優(yōu)點(diǎn),但可擴(kuò)展性低.Coverity[27]可以支持百萬行級(jí)別的代碼分析,卻存在大量誤報(bào).CGS是NASA Ames研究中心針對(duì)火星探測(cè)任務(wù)嵌入式軟件開發(fā)的數(shù)組越界檢測(cè)工具,該工具在火星車軟件上取得了比商業(yè)工具更好的精度和召回率，但是能處理程序的規(guī)模僅為20萬行.

近年研究者們進(jìn)行了一些新的探索.SHAO等[28]研究了現(xiàn)存的緩沖區(qū)溢出檢測(cè)技術(shù),并提出了緩沖區(qū)溢出檢測(cè)領(lǐng)域未來的3個(gè)改進(jìn)方向:對(duì)二進(jìn)制代碼進(jìn)行分析,結(jié)合機(jī)器學(xué)習(xí)算法進(jìn)行分析以及綜合利用多種技術(shù)進(jìn)行分析.GAO等[29]提出了一種基于污點(diǎn)分析的數(shù)組越界的靜態(tài)檢測(cè)方法, 并實(shí)現(xiàn)了一個(gè)可以在Windows和 Linux操作系統(tǒng)上運(yùn)行的自動(dòng)化靜態(tài)分析工具—Carraybound.但由于庫函數(shù)等原因,該工具存在一些誤報(bào)和漏報(bào).

本文的研究更多是從航天嵌入式軟件的數(shù)組越界特征出發(fā),為面向此類軟件,檢測(cè)數(shù)組越界缺陷提供有效的改進(jìn)導(dǎo)向.

6 結(jié) 論

數(shù)組越界仍然是近幾年航天嵌入式軟件中的關(guān)鍵可信問題.現(xiàn)有數(shù)組越界檢測(cè)工具和方法應(yīng)用于航天嵌入式軟件存在誤報(bào)過多且漏報(bào)過多的問題. 目前檢測(cè)數(shù)組越界的方法多基于模型檢測(cè)、抽象解釋、符號(hào)執(zhí)行等,這些算法都需要依賴于軟件及缺陷的特征.通過特征研究結(jié)果來針對(duì)性改善數(shù)組越界檢測(cè)算法是降低誤報(bào)率和漏報(bào)率的有效方法.本文分析了近三年來航天嵌入式軟件第三方測(cè)試中檢測(cè)出存在數(shù)組越界問題的94個(gè)真實(shí)案例,得出航天嵌入式軟件數(shù)組越界問題的10個(gè)特征. 通過分析這些特征，提出了確定程序分析方法和具體分析策略的啟示.并進(jìn)一步探討了數(shù)組越界檢測(cè)算法的改進(jìn)方向.本文是已知首個(gè)針對(duì)真實(shí)嵌入式軟件的數(shù)組越界缺陷特征研究.

下一步將基于本文研究結(jié)果，設(shè)計(jì)基于干擾分析的中斷程序分析方法,并實(shí)現(xiàn)具有低誤報(bào)率和漏報(bào)率的航天嵌入式軟件數(shù)組越界檢測(cè)工具.