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

根据统计,数组越界是航天嵌入式软件开发过程中出现最多且最容易被遗漏的缺陷类型之一.目前自动化检测数组越界多基于抽象解释、符号执行、程序模型检验等方法,这些方法在误报、漏报、可扩展性等方面的表现依赖于软件及缺陷特征.分析了近三年航天嵌入式软件第三方测试中发现的94个数组越界问题,从缺陷模式和缺陷表现形式两方面分析得出10项航天嵌入式软件数组越界缺陷特征,并提出对设计具体检测方法关键的若干启示.进一步基于这些特征和启示探讨了数组越界检测算法针对中断驱动型程序的改进方向.

Out-of-Bounds Array Access Bug Characteristics in Aerospace Embedded Software

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.