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

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]，所以程序是否存在数组越界是不可判定的,导致检测此问题缺少有效的通用算法. 另一方面由于无法通过代码本身推测程序使用环境，使用静态分析检测软件时往往会因为对环境进行过度近似，导致产生大量误报.

受软件及缺陷特征……