航天嵌入式软件数组越界缺陷特征研究

陈 睿， 于婷婷*， 贾春鹏， 李 超， 高栋栋， 江云松， 杨孟飞

1. 北京轩宇信息技术有限公司, 北京 100190 2. 北京控制工程研究所, 北京 100190 3. 中国空间技术研究院, 北京 100094

0 引 言

嵌入式软件在航天器控制系统中的地位不断提高，其可信性要求远高于一般软件.然而由于嵌入式软件及其运行环境的特殊性，一些常见缺陷，如数组越界、除零错、未初始化内存等仍是航天嵌入式软件面临的关键可信问题.其中,根据统计,数组越界是近两年航天嵌入式软件开发过程中出现最多、最容易被遗漏的运行时缺陷.当数组越界发生在对关键数据的访问时,往往会出现非预期的行为，导致严重的安全性问题[1].如何高效检测航天嵌入式软件的数组越界问题是亟待解决的难题之一.

目前对安全性具有极高要求的系统多使用基于抽象解释[2-8]、符号执行[9-13]、程序模型检验[14-16]等的数组越界检测方法.在工业中得到一定应用的检测工具主要有基于抽象解释技术的PolySpace[8]、Astree[4]、CGS[5]、IKOS[6],以及基于符号执行技术的KLEE[12]、S2E[13]等.然而这些工具在实际应用时存在过多误报与漏报，仍需依赖大量的人工测试.这是由于任何程序分析技术都不能完全判定程序的任意不平凡性质[17]，所以程序是否存在数组越界是不可判定的,导致检测此问题缺少有效的通用算法. 另一方面由于无法通过代码本身推测程序使用环境，使用静态分析检测软件时往往会因为对环境进行过度近似，导致产生大量误报.

受软件及缺陷特征的影响,同样的方法应用在不同领域、不同类别的程序中效果差异很大.而航天嵌入式软件具有受中断副作用影响、通过I/O数据与外设频繁交互等鲜明的领域特征.结合领域特征、缺陷特征以及常见缺陷模式进行针对性的分析是解决具体领域具体问题的有效方法.如何基于缺陷及航天嵌入式软件特征，选取合适的环境近似策略，并对检测方法进行针对性优化，是实现尽可能减少误报的同时保证召回率的关键.

为了能够针对航天嵌入式软件提出有效的数组越界检测方法，降低数组越界在实际工程中的遗漏,本文对航天嵌入式软件数组越界问题展开缺陷特征实证研究.研究使用了近三年航天嵌入式软件第三方测试中检测出存在数组越界问题的94个真实案例.这些案例来源于航天器控制系统、航天器综合电子系统等各类航天嵌入式软件，均为开发方经过多方测试依然遗漏的问题,代表了实际工程中最难解决的问题类型. 本文从数组越界模式以及数组越界表现形式两个维度对这些案例进行系统分析,提取出表1所示的10个非常有代表性的航天嵌入式软件数组越界特征.通过分析这些特征, 总结了对确定缺陷检测方法和具体分析策略具有重要作用的启示(见表1)，对进一步探索数组越界检测算法的改进方向奠定基础. 结合特征与启示, 讨论数组越界检测算法针对航天嵌入式软件的改进方向.

表1 真实案例中数组越界特征与启示Tab.1 Characterizations and implications of out-of-bounds array access bugs in real world cases

表2 数组越界模式定义Tab.2 Definitions of out-of-bounds array access pattern

1 研究方法

1.1 缺陷集

本文以2017年到2020年中国空间技术研究院型号软件第三方评测问题库、第三方评测遗漏问题库和软件问题案例库作为缺陷来源.这些软件覆盖了近几年我国研制和发射的各类空间飞行器中的关键嵌入式软件，主要包括航天器控制软件、航天器综合电子软件、航天器中央数据单元软件以及各类遥测遥控软件等.

本文通过“数组越界”、“下标溢出”等关键词在缺陷管理库中进行搜索和挖掘，经过人工分析和确认筛选出案例库中全部数组越界问题共计94个，来自86个不同的软件版本.其中人工确认部分会逐个进行问题单分析,并结合源代码，确定为需要修改的程序问题.这些问题均为第三方测试阶段,甚至更晚阶段发现的数组越界问题,都是开发方经过各类测试依然遗漏的问题,代表了实际工程中最难解决的问题类型.

1.2 特征分类

为了给将来的数组越界研究提供引导，本文从数组越界模式和数组越界表现形式两个维度对上述案例进行分析，收集并研究数组越界特征.重点讨论如下几个问题：

研究问题1：数组越界最常见的模式是什么

研究问题2：航天嵌入式软件有什么程序特征？

研究问题3：数组下标与几个变量相关联？

研究问题4：数组下标与哪种运算相关？

研究问题5：数组下标的来源是什么,受什么影响？

(1)关于数组越界模式的研究将围绕研究问题1展开.基于越界原因,数组越界模式可分为五类，包括常量下标越界、变量下标越界、下标临界、不一致定义和其他.详细的模式定义可见表2.

(2)关于数组越界表现形式的研究将围绕研究问题2、3、4、5展开.通过分析这些航天嵌入式软件中数组越界问题的具体表现,重点关注航天嵌入式软件的程序规模与程序类型，以及与数组下标相关的变量、运算、函数等的分布情况.

1.3 有效性

与其余实证研究工作类似,特征研究的有效性主要与所研究案例、所使用缺陷和研究方法的代表性相关.

关于研究案例的代表性,本文所研究的案例都是用C编写的航天嵌入式软件,是此类软件中最广泛应用的编程语言.这些软件来源于近三年的中国空间技术研究院第三方评测问题库、第三方评测遗漏问题库和北京控制工程研究所软件问题案例库,覆盖了我国80%以上星(船、器)载嵌入式软件.

关于所使用的缺陷的代表性,本文所使用的缺陷是从上述软件中收集的全部数组越界问题,具有很好的代表性和说明问题的能力.

关于研究方法,本文分析了所使用案例及缺陷的所有相关信息，涵盖多个版本的源代码、第三方测试分析及程序员修改反馈等.

2 数组越界模式研究

在检测软件缺陷时，面对不同的数组越界模式通常需要采取不同的检测方法.首先基于研究问题1(数组越界最常见的模式是什么？)展开研究.表3为统计的数组越界模式分布情况，依照研究方法所述可将数组越界模式划分为5类，其具体分类与定义已在表2中给出.

表3 数组越界模式分布Tab.3 Distribution of out-of-bounds array access pattern

特征1:大多数(77.7%)数组越界问题都属于变量下标越界模式.启示:检测此类问题需要应用程序分析方法进行全面分析./*例1:变量下标越界*/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作为数组flameSucFlag[3]的下标,取值为-1时会造成数组越界*/}

特征1可以从表3中分析得出，这主要由于程序中很多作为数组下标的变量或者来源于各种运算、循环计数、外部函数、I/O数据等或者会受到它们的影响,程序员们往往会忽略掉判断这些变量的取值范围.比如例1中,数组busdata_buf[CanBusNum][250]的取值有可能等于3,经过运算之后temp的取值则为-1,接下来temp作为数组flameSucFlag的下标则会造成数组越界.这些问题看似简单，但是在实际检测中却难以被发现,是最为常见和棘手的数组越界模式.由于下标变量来源及关系的复杂性,检测这类问题需要用到符号执行、抽象解释等程序分析方法进行全面分析.

特征2:一定数量的(20.2%)数组越界问题属于常量下标越界模式、下标临界模式和不一致定义模式.启示:这些缺陷模式较为简单,可以通过模式匹配进行检测.

除去大量因未对数组下标预先做取值范围判断而造成的数组越界,研究表明还有相当一定比例的数组越界属于常量下标越界模式(4.3%)，下标临界模式(13.8%)和不一致定义模式(2.1%).其中下标临界模式更为常见，这种情况多是由于程序员们在访问长度为n的数组时,忽略了数组范围为0～n-1,误以为n也是数组的有效下标. 常量下标越界大多由于数组定义时未能预先考虑是否满足使用要求.而数组定义范围不一致则是由于程序员们在多个文件皆声明了同一个数组, 定义存在一些差异导致同一数组长度不一致,这种情况在后续访问数组时极易造成数组越界.比如例2中,在头文件中定义数组ramData的大小为2048,而在canDataParse-define.c文件中定义ramData的大小却为2014.这3类缺陷模式都非常简单,可以直接通过模式匹配进行检测.

*例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];/*数组A_GD_RF_SCX长度为561 int,即为2244char*/if(type==0x0000000C) memset((void*) & A_GD_RF_SCX,0,4488);/*memset长度为4488,超过数组A_GD_RF_SCX长度,引起数组越界*/}

此外,还有少数(2.1%)数组越界问题的成因不属于上述情况,比如例3所示的memset长度超出数组定义范围也会造成数组越界,类似的还有strcpy等函数超范围访问引起数组越界.

3 数组越界表现形式研究

具有数组越界问题的数组和程序在表现形式上的特征对缺陷检测技术的研究具有重要意义,根据不同特征可以更有针对性地选取检测方法，探讨具体改进策略.接下来将按照研究方法所述从数组越界表现形式这个维度探寻航天嵌入式软件中该缺陷的特征.根据这些特征,讨论关于数组越界检测方法的启示,为后面探索现存检测方法的改进方向奠定基础.

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

为了更好地刻画和理解航天嵌入式软件的数组越界问题,首先需要了解航天嵌入式软件的程序特点,以及它们的软件规模.明确了这些问题,才能从中得到关于航天嵌入式软件检测技术的启示,更有针对性地探讨此类程序数组越界检测方法的前进方向.

特征3:所有程序均为中断驱动型程序.启示:检测方法应支持对中断的处理.

研究发现,所有程序都是中断驱动型程序(特征3),数组下标取值中受到中断副作用影响的程序占总量的22.3%.比如例4中数组retSum就会受中断副作用影响. CNT作为一个全局变量当大于等于10000时，主程序会产生一个警告，并对数组retSum的下标做加一操作.然而由于中断影响，CNT达到数值后可能会执行中断程序而被重置为0,这导致主程序不能产生警告,数组retSum的下标也不能做加一操作.

/*例4:中断*/void CheckFunc(){ while(1){ if(CNT>=10000) assert(retSum[temp++]); /*若CNT大于等于10000,则*/}void interrupt CheckFunc(void){ CNT++; if(CNT>10000) CNT=0; /*若中断执行到CNT>10000,则CNT会被置0*/}

因为使用中断是航天嵌入式软件最主要的特征之一,故而在检测此类软件时需要支持对中断的处理.然而由于软件特征、编码规范、开发习惯等因素,数组下标受中断副作用影响的程序比例却比较低.由于中断驱动型程序精确分析的开销很大,结合特征3，可知在精准性、效率和可靠性的取舍中,效率和可靠性对于程序的整体分析更为重要.

特征4:单文件规模小,跨文件的数值引用关系少.启示:对于航天嵌入式软件,程序分析无需跨翻译单元,无需考虑大规模程序,也可以取得较好的效果.

对比非嵌入式软件,航天嵌入式软件单文件代码行数较少,95.7%的文件不超过5000行,86.2%的文件不超过2000行,仅4.3%的数组下标越界检测需要进行跨文件的数值分析.这主要源于航天嵌入式软件单文件功能需求少、跨文件交互少的特点.故而对于此类软件，程序检测时不需要考虑大规模程序，也不需要跨翻译单元分析.

3.2 数组下标与几个变量相关联？

如前文所述，数组越界模式中分布最为广泛的是未判断作为数组下标变量的取值范围.若要更好地检测这类数组越界问题,首先需要了解数组下标与变量之间的关联情况.当涉及到变量之间的关联情况，数量级的信息是最为重要的，所以接下来关心的重点是数组下标关联变量的数量分布.

特征5:几乎所有数组下标与不多于4个变量存在关联关系.启示:程序分析需要考虑变量间关系,但数组下标与其他变量间的关系并不复杂,无需进行复杂的变量间关系分析.

将数组下标所包含的变量称为下标包含变量,并将下标包含变量和与下标包含变量有运算关系的变量称为下标关联变量. 例5中，数组InsBufTwo的下标包含变量为j和subInsCnt,下标关联变量则为j、subInsCnt、inslen和temp.由此可知，数组InsBuffTwo的下标关联变量的个数为4个.

/*例5:关联变量*/void main(){ inslen = temp & 0xFF; subInsCnt = 0; for (j = 0; j < inslen; j++) { InsBufTwo[j + subInsCnt] = InsBuf[j] subInsCnt = subInsCnt + 1; }}

图1所示为下标关联变量的分布图.由分布图可知，72.3%的数组下标存在1～2个关联变量,并且数组下标关联变量一般不多于4个(根据图1统计图,下标关联变量大于5的数组个数为0).这表明在做相关程序分析时需要考虑变量间的关系，但与此同时，因为数组下标与其他变量之间的关系并不复杂，所以可以不需要进行复杂的变量间关系分析.

图1 下标关联变量分布图Fig.1 Distribution of related variables for index variables

3.3 数组下标与哪种运算相关？

除去讨论数组下标与变量的关联问题,要分析数组下标变量取值范围,还要考虑数组下标与运算的关联.比如例1是运算时未判断变量范围造成的数组越界.那么需要讨论如下问题：数组下标与何种运算相关？了解航天嵌入式软件中数组下标的关联运算的构成,对于探索数组越界的检测方法会产生很有价值的启示.

特征6:数组下标相关运算中超过90%的运算为线性运算.启示:分析方法不需要精确处理非线性关系,简化非线性运算对分析精度不会产生很大影响.

将数组下标关联变量涉及的运算称为下标相关运算.分析发现航天嵌入式软件中下标相关运算只有少量的非线性运算(仅有9.6%), 90.4%的运算为线性运算.其中赋值运算占54.1%,加减运算占18.8%,逻辑运算占17.7%,乘除运算占5.9%(除法占1.2%),位域运算占3.5%.

既然数组下标相关运算中非线性运算很少,那么在对航天嵌入式软件的数组越界分析中不需要精确处理非线性关系,可以在一定程度内简化非线性运算,并且不会对数组越界的分析精度产生很大的影响.

特征7:数组下标相关运算中几乎不存在浮点转换运算.启示:在数组越界检测中,可以忽略所有浮点运算,将所有浮点数看作任意值,在检测精度不会受到很大影响的同时可以有更高的效率.

所研究的问题中没有浮点数到数组下标相的转换,也即数组下标的相关运算中几乎不存在浮点转换运算.那么在检测数组越界缺陷时,可以忽略掉所有的浮点运算,将所有浮点数看作任意值,检测精度不会受到很大影响,反而可以得到更好的效率.

3.4 数组下标的来源是什么，受什么影响？

要分析数组下标变量取值范围,还需要考虑数组下标的来源.所以本节将讨论如下问题：数组下标多来源于什么？受什么影响比较大？

特征8:部分(22.3%)数组下标受函数参数影响.启示:数组越界检测需要使用上下文敏感的程序分析方法.

研究问题中，数组下标受函数参数影响的程序占22.3%,但函数调用层数不深,通常不多于4层.这意味着对航天嵌入式软件进行数组越界检测时,需要使用上下文敏感的程序分析方法来分析函数对数组下标所造成的影响.

特征9:近半数(40.4%)数组下标受外部I/O数据影响.启示:对外部I/O数据的取值、时序进行建模可以大大提高静态分析精度.

嵌入式程序的输入几乎全部来自于总线数据，I/O数据在程序中的表现为:来源于绝对地址、每次读取的值可能不同、每次写入的影响不能确定、读取到的值的变化不能通过程序判断.研究发现I/O数据参与数组下标运算的程序占40.4%.会产生这种情况因为嵌入式软件主要特点之一是使用大量总线数据作为输入.例6中,cmdlen的取值受函数Read1553BMem的调用结果,而Read1553BMem的数据来自I/O数据.

由于大量程序的数组下标会受到I/O数据影响,而I/O数据具有不确定性和时间相关性,在相关检测时,若能对对外部I/O数据的取值、时序进行精准可靠的建模,则可以大大提高航天嵌入式软件静态分析精度.

特征10:超过一半(68.1%)数组下标受循环计数 或其相关变量影响.启示:分析方法必须支持高效的循环程序处理,同时分析方法需要具有处理循环变量与下标关联变量关系的能力

研究表明,68.1%的程序中数组下标来自于循环体内循环计数或其相关变量,且循环次数可能很大.比如例7中当i循环计数到取值150时,作为数组PRoffset的下标会造成数组越界(PRoffset长度为150).

由于航天嵌入式软件中数组下标与循环变量的高相关性与循环次数的高上限,在选取数组越界检测方法的时候,能否高效的处理循环、能否较精确的描述循环变量与数组下标关联变量的关系是选择的重要依据.

4 特征研究对改进检测方法的探讨

本章在特征研究和启示的辅助下，探讨数组越界检测算法针对航天嵌入式软件的改进方向.为了简化表述, 对于具体特征将使用表1中的特征简称代替.

根据函数参数使用特征(特征8)，航天嵌入式软件数组检测需要使用上下文敏感的程序分析方法.根据程序规模特征(特征4),对于航天嵌入式软件无需做跨文件分析.结合这两个特征可以确定:以文件为单位,使用函数内联方式的过程间分析是航天嵌入式软件数组越界检测的最佳方法.

若考虑基于抽象解释的缺陷检测方法，根据关联变量特征(特征5)与运算操作特征(特征6),使用凸抽象域,并使用变量关联作为变量分组依据可以在航天嵌入式软件数组越界检测中获得较好的性能和准确率.并且由于循环计数影响特征(特征10)，航天嵌入式软件中68.1%的数组下标与循环变量相关,且循环次数可能很大,能否高效的处理循环、能否较精确的描述循环变量与数组下标的关系是抽象域选择的重要依据.由于浮点转换运算特征 (特征7), 航天嵌入式软件几乎没有浮点运算结果到数组下标的转换,在数组越界检测中,忽略所有浮点运算,将所有浮点数看作任意值,在检测精度不会受到过多影响的同时可以获得更好的效率.

使用中断是航天嵌入式软件最主要的特征之一,几乎所有程序都为中断驱动型程序(特征3),检测方法必须支持对中断的处理.然而由于软件特征、编码规范、开发习惯等因素,数组下标受中断副作用影响的程序比例仅为22.3%.由于中断驱动型程序精确分析开销很大,对于整体分析而言,相较于精确性,效率和可靠性更为重要.同时,根据I/O数据使用特征(特征9),在分析中考虑I/O数据将大大提高航天嵌入式软件静态分析精度.由于I/O数据的不确定性和时间相关性,如何如何尽可能精准地刻画I/O数据的取值和行为是提升嵌入式软件值分析精确性的关键问题.

5 相关工作

数组越界缺陷实证研究：缺陷实证研究近年成为软件工程研究的热点,比较著名的工作有LU等[18]针对真实并发缺陷的实证研究,CHEN等[19]针对中断数据竞争缺陷的实证研究，以及ISLAM等[20]针对深度学习程序缺陷的实证研究.此类工作多是为了从程序缺陷特征出发研究现存检测工具以及主流检测技术的优劣势，对探索应用于特定缺陷、特定领域检测方法的改进方向起重要的指导作用.

目前已有一些关于数组越界缺陷实证研究的工作，然而都面向一般开源软件，并且聚焦安全漏洞相关的缓冲区溢出缺陷，不能体现航天嵌入式软件中数组越界的缺陷特征.WILANDER等[21]使用20个缓冲区溢出的程序缺陷对4个检测缓冲区溢出的动态分析工具做了实证分析.他们的研究发现即使最好的工具也只能检测50%的问题,并且其中有6个类型不能被任何工具检测出.

FANG等[22]对缓冲区溢出缺陷做了实证研究来分析现存的检测工具和方法.他们发现多数检测都使用了模糊测试方法,却很少使用静态检测方法.

在最近的工作中,YE等[23]分别对63个真实项目中的100个缓冲区溢出缺陷版本和修复版本进行分析,展开了关于缓冲区溢出静态检测工具的实证研究.并且比较了Fortify, Checkmarx和Splint等工具的检测效率(efficiency)和有效性(effectiveness).他们的研究结果为后续相关检测方法提供了一些启示.

DUDINA[24]分析了一些流行的缓冲区溢出测试集以及从实际应用程序中提取的缺陷片段,从而研究静态分析器难以发现的缺陷类型.他的研究表明过程间分析、路径敏感分析和循环处理是必不可少的检测技术.基于此工作,他认为在现有基础上改进字符串处理,并与污点分析相结合是未来的改进方向.

不同于上述工作，本文是已知首个针对嵌入式软件中的数组越界开展的实证研究，主要目的是探索静态检测方法在检测数组越界缺陷时的改进方向.本文分析的数组越界案例都来源于真实的航天嵌入式软件,能够真正从实际出发得出针对中断驱动型程序的重要启示.

数组越界检测研究：目前存在很多静态数组越界检测工具[5,6,8,25-27],其中应用比较广泛的商业工具Polyspace具备理论上无漏报的优点,但可扩展性低.Coverity[27]可以支持百万行级别的代码分析,却存在大量误报.CGS是NASA Ames研究中心针对火星探测任务嵌入式软件开发的数组越界检测工具,该工具在火星车软件上取得了比商业工具更好的精度和召回率，但是能处理程序的规模仅为20万行.

近年研究者们进行了一些新的探索.SHAO等[28]研究了现存的缓冲区溢出检测技术,并提出了缓冲区溢出检测领域未来的3个改进方向:对二进制代码进行分析,结合机器学习算法进行分析以及综合利用多种技术进行分析.GAO等[29]提出了一种基于污点分析的数组越界的静态检测方法, 并实现了一个可以在Windows和 Linux操作系统上运行的自动化静态分析工具—Carraybound.但由于库函数等原因,该工具存在一些误报和漏报.

本文的研究更多是从航天嵌入式软件的数组越界特征出发,为面向此类软件,检测数组越界缺陷提供有效的改进导向.

6 结 论

数组越界仍然是近几年航天嵌入式软件中的关键可信问题.现有数组越界检测工具和方法应用于航天嵌入式软件存在误报过多且漏报过多的问题. 目前检测数组越界的方法多基于模型检测、抽象解释、符号执行等,这些算法都需要依赖于软件及缺陷的特征.通过特征研究结果来针对性改善数组越界检测算法是降低误报率和漏报率的有效方法.本文分析了近三年来航天嵌入式软件第三方测试中检测出存在数组越界问题的94个真实案例,得出航天嵌入式软件数组越界问题的10个特征. 通过分析这些特征，提出了确定程序分析方法和具体分析策略的启示.并进一步探讨了数组越界检测算法的改进方向.本文是已知首个针对真实嵌入式软件的数组越界缺陷特征研究.

下一步将基于本文研究结果，设计基于干扰分析的中断程序分析方法,并实现具有低误报率和漏报率的航天嵌入式软件数组越界检测工具.