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

Out-of-Bounds Array Access Bug Characteristics in AerospaceEmbedded Software

作　　者：陈睿 于婷婷[1,2] 贾春鹏 李超 高栋栋 江云松 杨孟飞 CHEN Rui;YU Tingting;JIA Chunpeng;LI Chao;GAO Dongdong;JIANG Yunsong;YANG Mengfei(Beijing Sunwise Information Technology Ltd.,Beijing 100190,China;Beijing Institute of Control Engineering,Beijing 100190,China;China Academy of Space Technology,Beijing 100094,China)

机构地区：[1]北京轩宇信息技术有限公司,北京100190 [2]北京控制工程研究所,北京100190 [3]中国空间技术研究院,北京100094

出　　处：《空间控制技术与应用》2021年第2期1-9,共9页Aerospace Control and Application

基　　金：国家自然科学基金资助项目(61802017)。

摘　　要：根据统计,数组越界是航天嵌入式软件开发过程中出现最多且最容易被遗漏的缺陷类型之一.目前自动化检测数组越界多基于抽象解释、符号执行、程序模型检验等方法,这些方法在误报、漏报、可扩展性等方面的表现依赖于软件及缺陷特征.分析了近三年航天嵌入式软件第三方测试中发现的94个数组越界问题,从缺陷模式和缺陷表现形式两方面分析得出10项航天嵌入式软件数组越界缺陷特征,并提出对设计具体检测方法关键的若干启示.进一步基于这些特征和启示探讨了数组越界检测算法针对中断驱动型程序的改进方向.According to statistics,out-of-bounds array access is one of the most common and easily missed bugs in aerospace embedded software. At present,program analysis methods for automatically detecting out-of-bounds array access mostly base on abstract interpretation theory,symbolic execution,model checking and etc. The performances of these methods in false positives,false negatives,and extensibility and so on mainly rely on the characteristics of the software and defects. Therefore,we firstly analyze 94 real world out-of-bounds array access errors in recent 3 years,which are from aerospace embedded software left to the third-party testing part. We carefully examine the bug pattern and manifestation of these bugs,and extract 10 characteristics about the out-of-bounds array access errors in aerospace embedded software,as well as some important implications. According to these characteristics and implications,we explore the improvement of detection methods for out-of-bounds array access with respect to interrupt-driven programs.

关 键 词：航天嵌入式软件 数组越界 程序分析 中断驱动型程序 

分 类 号：TP399[自动化与计算机技术—计算机应用技术]