Page 6 - 《软件学报》2021年第10期

2978 Journal of Software 软件学报 Vol.32, No.10, October 2021

杂度呈几何级增长,这种特点和趋势在空间站、载人航天、深空探测等重大航天工程中尤为凸显.同时,航天器
属于典型的安全苛求系统,对软件可靠性和安全性有极高的要求,软件一旦发生失效,将会导致任务失败或人员
伤亡.
航天器控制功能涉及大量复杂的数学运算,其运算结果的正确性作为航天器可靠性和安全性的关键部分,
不仅取决于算法所对应的数学模型的正确描述,也取决于运算过程的正确性.受计算机内存和 CPU 等硬件环境
的限制,软件中变量和数据只能使用有限字节,意味着变量和数据的取值范围是有严格要求的,运算结果一旦失
真,即使是精心设计的算法,也无法正确实现相关功能.
整数溢出错误是导致软件运算结果出错的重要原因之一,由其引发的事故也屡见不鲜.1996 年,欧洲 Ariane
[1]
[1]
5 火箭爆炸灾难 ;2004 年,Comair 航空公司航班停飞事故 等等.国际权威漏洞披露组织 CVE(common
vulnerabilities and exposures)在 2007 年发布的年度报告中,将整数漏洞(integer-based vulnerability)列为威胁软
[2]
件安全的第二大类漏洞 ,其中,整数溢出错误最为常见.MITRE 也在 2011 年的报告中,将整数溢出错误列为“25
[3]
个最危险的软件错误”之一 .据中国空间技术研究院软件产品保证中心统计,近 10 年,因整数溢出引发的航天
器在轨质量问题就有 3 例;在航天器总装测试(A.I.T.)阶段发现的在研质量问题中,约 8%都与整数溢出密切相
关,仅 2019 年就发生了 2 起整数溢出导致的质量问题.
航天嵌入式软件通常采用中断驱动机制实现被控对象的控制算法,若直接使用面向顺序程序的整数溢出
检测技术来分析航天嵌入式软件,分析结果将不正确;而使用面向多线程程序的整数溢出检测技术来分析航天
嵌入式软件,分析结果误报率较高、适用性不好.另外,由于控制算法涉及大量的数值型数据以及数学运算,且中
断触发的不确定性导致软件可执行路径分析变得异常复杂,以危险路径分析为主的整数溢出检测方法也存在
运行开销大、分析精度不高等问题.因此,目前主流的整数溢出检测方法都无法有效应用.
本文以航天嵌入式软件真实整数溢出案例为基础,对嵌入式软件整数溢出分布及特征进行了系统分析,提
出了基于整数溢出变量依赖的程序模型约简技术;针对中断驱动型程序,提出了基于干扰变量的中断驱动程序
顺序化方法,使得现有模型检测技术能够有效地对中断驱动型程序的整数溢出问题进行检测;最后,通过实验验
证本文方法的有效性.
本文第 1 节基于航天嵌入式软件整数溢出真实案例对整数溢出分布和特征进行分析和总结.第 2 节结合整
数溢出特征给出整数溢出有界模型检测方法.第 3 节给出实验评估结果.第 4 节介绍相关研究工作.第 5 节对全
文进行总结,并对未来研究方向进行初步探讨.

1 航天嵌入式软件整数溢出特征研究

[4]
针对整型溢出案例进行研究,不仅能够补充理论基础,还能为整数溢出检测方法提供有效的指导意见 .
[6]
[5]
Dietz 等人 针对 spec 2000 中的整数溢出问题,从故意使用和未定义操作两个角度进行了分析;Wang 等人 从
Linux 内核使用出发,对整数溢出问题进行了系统性研究.
本节选取 2010 年~2019 年航天嵌入式软件评测过程中发现的 75 个整数溢出真实案例作为研究对象(这些
整数溢出案例可以通过 https://github.com/JunYuanTeng/Case-Set 下载),分析其分布趋势,并从整数溢出变量、数
学运算、循环和递归操作和中断使用方式上进行深入讨论,以更全面地认识航天嵌入式软件整数溢出特征.
1.1 整数溢出分布趋势
整数溢出的表现形式一般可以分为如下 4 类:无符号整数上溢、无符号整数下溢、有符号整数上溢、有符
号整数下溢,这 4 类整数溢出错误在本文所研究的航天嵌入式软件 75 个典型实例中均会存在.图 1 描述了 4 类
整数溢出错误的百分比堆积柱状图.其中,横坐标记录整数溢出错误发现的年份和总数,纵坐标表示每类整数溢
出错误的分布比例,柱状图上的数字表示 4 类整数溢出错误的数量.
总体来说,无符号整数上溢和下溢是整数溢出的主要部分,占比达 81.3%;其次是有符号整数上溢,占比达
16%;有符号整数下溢数目最少.从逐年的数量趋势来看,无符号整数上溢和下溢都占有绝大部分的比例.