作者简介

黄晨,女,博士,高级工程师。曾负责并参与多个国家重点工程航天器软件的第三方评测,参与多项院标的编写和制定,以及嵌入式软件数据访问冲突分析,基于模型测试技术等多方面的研究工作,并在相关方面发表多篇论文。

 

摘要:以星载嵌入式软件作为被测对象,研究C语言程序中常见多发问题,解析问题机理形成缺陷模式库,采用静态分析工具SpecChecker对抽样代码进行快速检测,根据工具检测结果,对工具和缺陷模式给出改进建议。采用工具自动化检测代码缺陷能够高效、准确定位问题,避免人为因素引入的问题遗漏,为航天软件的高可靠性、高安全性提供有力保障和支持。


关键词:嵌入式软件;缺陷模式;静态分析;自动化检测

 

1、引 

 

在高质量、高安全性的航天产品中,软件占据了越来越重的比例,从需求分析阶段,到软件研制,各级测试过程中,都需要尽量避免软件问题的发生。一方面从设计上规避,一方面对软件产品进行充分的测试,尽可能早的发现隐藏在软件中的缺陷,避免将软件问题带到卫星上天,造成严重的后果和损失。

 

软件测试是有效发现软件缺陷的重要方法之一,嵌入式软件测试按照是否执行被测系统,将测试类型分为静态测试和动态测试。静态测试不需要编译执行源程序,对源程序进行词法语法、编程规范、数据流、控制流、度量等分析,获取程序的结构和特性,利用形式化方法验证、证明程序是否符合安全规则,能够较为全面的获取程序的特征。动态测试需要通过获取程序的动态信息来分析软件的缺陷,如分析程序的内存状态、覆盖率和执行结果,更有利于理解程序的动态行为特征。

 

很多代码缺陷产生于程序运行过程中,具有隐蔽性和不可预见性,比如数组越界,动态存储分配,内存溢出,指针非法引用,类型不一致的隐式转换等,这些错误都是在编译阶段不能被编译器检查发现的错误。在大规模,复杂度极高的软件中,完全依赖于人工检查方式可能会因为人为等主观原因造成问题被遗漏无法发现。将现有常见多发问题形成缺陷模式库植入工具中,由工具自动化检测代码缺陷,能够高效提升测试效率,避免问题重复发生,减轻测试人员工作量。

    

本文以星载嵌入式软件作为被测对象,研究C语言嵌入式软件常见多发问题,根据缺陷原因和严重等级对规则分类,逐条解析典型规则的问题机理,采用静态分析工具SpecChecker对抽样代码进行快速检测,分析工具检测结果,并对工具和缺陷模式库给出改进建议。

 

2、缺陷模式库规则分析

2.1 规则分类

2.1.1 按照错误类别分类

为了进一步研究软件错误发生的机理,分布情况,针对C语言典型缺陷模式库中的规则,按照规则检查类型对其进行分类。

(1) 数值检查:除零错误、数组越界。

(2) 指针使用检查:空指针解引用。

(3) 数据流检查:变量定义未使用就再次赋值。

(4) 控制流检查:if elseif分支语句末尾缺少else分支。

(5) 初始化检查:使用前未初始化变量。

(6) 类型转换检查:数据类型不一致引入的隐式类型转换。

(7) 操作符使用不当检查:关系表达式、逻辑表达式、条件判断语句中的控制表达式禁止为赋值表达式“=”、使用连续的比较运算,可能导致代码执行逻辑与预期不符。

 

2.1.2   按照严重程度分类

根据故障出现可能引起的错误严重程度,对软件或者系统造成影响的严重程度,给每条规则定义了优先级高、中、低的属性。

(1) 重要:除零错误;数组越界;空指针解引用。

(2) 中等:使用前未初始化变量;数据类型不一致引入的隐式类型转换;关系表达式、逻辑表达式、条件判断语句中的控制表达式禁止为赋值表达式“=”;使用连续的比较运算,可能导致代码执行逻辑与预期不符。

(3) 轻微:if elseif分支语句末尾缺少else分支;变量定义未使用就再次赋值。

 

2.2 规则解析

2.2.1 数值检查

错误发生在不断运行过程中,称为运行时错误,一旦程序中出现该类型错误,会导致计算得到的实际结果与预期结果完成不同,甚至引发计算机复位。数值检查作为运行时错误检查的重要检查内容,会出现在某些特定的运行条件下,即便是经过严格测试的程序,仍有可能存在非预期的浅通路,引发软件不安全问题。

 

(1)数组越界

通过数组的下标来得到数组内指定索引的元素,称作对数组的访问。如果一个数组定义为n个元素,它占用一块连续的内存空间,对n个元素(下标为0n-1)的访问都合法,如果对这n个之外的元素(如下标n)进行访问,访问到的是其它变量,是非法的,称为越界。数组越界在运行时的表现是不确定的,可能不会造成严重后果,也有可能导致程序崩溃。因此在使用数组时一定要检查访问是否越界,以保证程序的正确性。代码示例见表1

 

1 数组越界代码示例

(2)除零错误

出现除零操作时会导致计算结果为一个极大值,超过数据类型能够表示的最大范围,就会发生溢出,计算机程序对于溢出的防护处理可能是计算机复位。因此代码中将整数和浮点数作为分母时都应该进行保护,防止除零后数据溢出的异常情况发生。代码示例见表2

表2 除零错误代码示例


2.2.2 空指针解引用

空指针解引用是一种常见的动态内存错误。指针变量可以指向堆地址、静态变量和空地址单元,当引用指向空地址单元的指针变量时,就会产生空指针引用故障,导致不可预见的错误,系统崩溃或者异常复位。因此,在解引用指针前,应先判断是否为NULL,如果是NULL则不要解引用。代码示例见表3。

表3 空指针解引用代码示例


2.2.3 变量定义未使用就再次赋值

这条规则属于数据流分析规则,主要关注变量值的操作逻辑是否合理正确,如果不符合逻辑,就有可能隐藏代码问题。代码示例见表4。

表4  变量定义未使用就再次赋值代码示例表


2.2.4 if elseif分支语句末尾缺少else分支

这条规则属于控制流分析规则,主要关注程序的结构。需要在代码解析的基础上提取程序的控制流信息,程序的控制流用于决定分配给变量的特定值可能传播到程序的哪些部分。如果存在某条路径中变量值与预期不一致,就有可能隐藏代码问题。代码示例见表5。

 

5 if elseif分支语句末尾缺少else分支代码示例表

 

2.2.5 使用未初始化变量

程序在执行过程中变量位于内存中,内存中供用户使用的存储空间分为三部分:程序区、静态存储区、动态存储区。全局变量全部存储在静态存储区;动态存储区主要存放:函数的形参、自动变量(没有加static的局部变量)、函数调用的现场保护和返回值。在使用动态存储区变量前如果未对其赋初值就直接使用,由于变量值不确定,可能会发生无法预知的错误。代码示例见表6。

 

表6 使用未初始化变量代码示例表

 

 

2.2.6   数据类型不一致引入的隐式类型转换

当赋值变量与被赋值变量类型不相同时,需要进行数据类型转换的相关检查规则。一般情况下,数据的类型的转换通常是由编译系统自动进行的,不需要人工干预,这种类型转换称为隐式类型转换。但如果程序要求一定要将某一类型的数据转换为另外一种类型,则可以利用强制类型转换运算符进行转换,这种强制转换过程称为显式转换。

图1  编译器自动提升规则


C语言编译器数据类型提升规则可以归纳为从长度小的数据类型向长度大的数据类型提升,称为向上转换;反之,称为向下转换。编译器自动转换规则见图1所示。

 

如果出现向上隐式类型转换,两个数据进行加法运算时,小数对应到大数有效位数超出有效数据位数,会导致小数无法加到大数上,造成计算结果存在精度损失。

 

如果出现向下隐式类型转换,大范围变量的数据值超出了小范围变量的能够表示的有效范围,编译器会根据数据值在内存中的表示形式经过转换后,将高位数据截断丢弃造成转换结果错误,因此编译器不允许隐式向下转换,如果必须要这么做,需要使用显式的方法,使用显式的方法也会存在问题,比如两个数据相加得到的计算结果可能出现向上舍入或者向下舍入的情况。

 

例如,将高精度double类型变量转换成float类型变量需要增加强制类型转换。double型向float型转换为向下转换,C语言编译器无法自动执行向下转换的操作,因此需要采用显式类型转换的方式,将double类型变量显式转换为float类型变量。代码示例见表7

 

7 类型转换代码示例表


2.2.7  操作符使用不当

(1)关系表达式、逻辑表达式、条件判断语句中的控制表达式禁止为赋值表达式“=”

在上述表达式中如果使用赋值号会导致条件判断结果始终为真,代码执行逻辑与预期要求不符。代码示例见表8

 

8 某些表达式中禁止使用赋值表达式代码示例表

(2)使用连续的比较运算,可能导致代码执行逻辑与预期不符。

比如连续的比较操作为:1<a<5,不论变量a为什么值,该比较操作的结果始终为真。代码示例见表9。

 

表9  使用连续比较运算的代码示例表


3、代码抽样及结果分析


采用代码抽样的方法验证和分析静态分析工具SpecChecker对缺陷模式库中规则的检查情况SpecChecker是一款具有检查编程规范、故障缺陷分析和共享数据变量分析等功能的静态分析工具。使用该工具的故障缺陷分析功能对随机抽样代码进行检查,给出工具分析结果,对工具和规则提出建议,明确代码设计时的注意事项。

 

3.1 抽样代码情况及指标

抽样20w代码嵌入式C代码,处理器类型有C51GCCDSP,选择以下几个指标作为对工具的衡量指标,以工具发现问题为核心指标。

(1)工具提示:工具提示出违反某规则的总数;

(2)确认为问题:工具提示违反规则位置,经人工确认确实存在程序问题;

(3)工具误报:工具提示违反规则位置,经人工确认不存在违反规则或者任何错误;

(4)工具漏报:代码违反规则要求,工具未给出提示。

 

3.2 工具分析结果

表10  缺陷模式检查结果


3.3 建议

根据表10结果,从几个方面:漏报规则、误报规则、定位准确规则、提示性信息规则、代码改进规则、未检出规则几个方面给出改进建议。

 

(1)漏报规则:工具能够较好的发现整数为0做分母的除零错误,准确率较高,但是未能检出分母为浮点数0.0的情况。在需求分析、代码设计阶段应考虑分母是否可能为零,如果可能为零,应进行除零保护。

 

(2)误报规则:工具对于变量赋值后未使用再次赋值存在一定程度的误报,该条规则给出了较多提示性内容,但并未发现真正的程序问题。建议工具对于局部变量定义时赋初值后未使用再次赋值的情况不进行提示。规则描述中也可更进一步明确什么场景下的代码逻辑是存在缺陷的。

 

(3)定位准确规则:工具对于数组越界使用未初始化变量关系表达式、逻辑表达式、条件判断语句中的控制表达式禁止为赋值表达式“=””使用连续的比较运算,可能导致代码执行逻辑与预期不符,检查结果较为准确。

 

(4)提示性信息规则:“if elseif分支语句末尾缺少else分支未发现出现实质性问题,一般情况下需要结合代码的处理逻辑分析是否存在问题。

 

(5)代码改进规则:double类型数据转换为float类型出现问题的大多数情况是存在一定程度的数据精度损失,会造成计算结果存在一定的误差,建议代码不进行这类操作。

 

(6)未检出规则:目前未见空指针解引用的错误发生,一旦发生后果比较严重可能造成计算机复位,开发和测试人员应引起重视,避免代码中存在指针未判断是否为空就直接使用的情况出现。

 

 

4、结论


本文选择了缺陷模式库中的7类典型缺陷模式,逐条解析问题发生机理,给出错误、正确代码示例,随机抽取测试代码,使用静态分析工具SpecChecker进行检测,相比较单一植入错误代码的方式,代码缺陷更加多样性,能够更为有效的验证工具检查的完备性和可靠性,也更容易暴露出工具存在的缺陷。另一方面,通过结果分析对规则进行合理性、有效性验证,修改、删除无效规则,增加有效规则,对缺陷模式库的改进提供数据支持。

 

航天嵌入式软件的多发、常见问题的收集和汇总将会是一个长期的过程,目前正朝着工具检测的自动化方面飞快发展。收集缺陷规则形成缺陷模式库,采用静态工具自动检测错误,相比较人工检查能够更叫高效、准确的发现问题,避免人为经验不足或者其他主观原因导致的问题遗漏;也可以有效解决因为动态测试输入条件不充分导致问题无法暴露出来的潜在可能;采用静态工具自动化查错应作为测试流程中的一个重要测试环节,对现有测试流程的完善和改进也起到了促进作用。




-End-




2020年02月13日

小系统,大协作,做好战“疫情”报官
基于FPGA的RapidIO接口仿真验证实现方法

上一篇

下一篇

嵌入式软件缺陷模式静态分析方法

本网站由阿里云提供云计算及安全服务 Powered by CloudDream