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

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2021,32(10):29772992 [doi: 10.13328/j.cnki.jos.006024] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563


航天嵌入式软件整数溢出的形式化验证方法 

1,2
1,2
高 猛 , 滕俊元 , 王 政 1,2
1
(北京控制工程研究所,北京 100190)
2
(北京轩宇信息技术有限公司,北京 100190)
通讯作者: 滕俊元, E-mail: tengjunyuan@sunwiseinfo.com

摘 要: 整数溢出引起的软件系统安全性问题屡见不鲜,已有的模型检测技术由于存在状态空间爆炸、不能有效
支持中断驱动型程序检测等缺点而少有工程应用.结合真实案例,对航天嵌入式软件整数溢出问题的分布和特征进
行了系统性的分析.在有界模型检测技术的基础上,结合整数溢出特征,提出了基于整数溢出变量依赖的程序模型约
简技术;同时,针对中断驱动型程序,结合中断函数特征抽象,提出了基于干扰变量的中断驱动程序顺序化方法.经过
基准测试程序和真实航天嵌入式软件实验,结果表明:该方法在保证整数溢出问题检出率的前提下,不仅能够提高分
析效率,还使得已有的模型检测技术能够适用于中断驱动型程序整数溢出检测.
关键词: 航天嵌入式软件;整数溢出;有界模型检测;中断驱动型程序;顺序化
中图法分类号: TP311

中文引用格式: 高猛,滕俊元,王政.航天嵌入式软件整数溢出的形式化验证方法.软件学报,2021,32(10):29772992. http://
www.jos.org.cn/1000-9825/6024.htm
英文引用格式: Gao M, Teng JY, Wang Z. Formal verification method for integer overflow in aerospace embedded software.
Ruan Jian Xue Bao/Journal of Software, 2021,32(10):29772992 (in Chinese). http://www.jos.org.cn/1000-9825/6024.htm
Formal Verification Method for Integer Overflow in Aerospace Embedded Software

1,2
1,2
GAO Meng , TENG Jun-Yuan , WANG Zheng 1,2
1
(Beijing Institute of Control Engineering, Beijing 100190, China)
2
(Beijing Sunwise Information Technology Ltd., Beijing 100190, China)
Abstract: The security problems of software systems caused by integer overflow are common, while the existing model checking
techniques have few engineering applications due to the shortcomings of state space explosion and failure to support interrupt-driven
program detection. This paper systematically analyzes the distribution and characteristics of integer overflow in aerospace embedded
software through some real cases. On the basis of bounded model checking, a program model reduction technique based on integer
overflow variable dependence is proposed based on the characteristics of integer overflow variables. At the same time, we present a
interference variables dependency sequentialization method for interrupt-driven programs based on the characteristic abstraction of
interrupt functions. The results of benchmark programs and real aerospace embedded software experiments show that this method can not
only improve the analysis efficiency, but also make the existing model checking techniques applicable to integer overflow detection of the
interrupt-driven programs under the premise of guaranteeing the detection rate of integer overflow.
Key words: aerospace embedded software; integer overflow; bounded model checking; interrupt-driven program; sequentialization

我国新一代航天器中广泛采用软件密集系统(software-intensive system),软件在保证航天器安全稳定运行、
可靠完成任务方面起着至关重要的作用.航天器许多关键任务、复杂功能的完成均依赖于软件,软件规模和复

 基金项目: 国家自然科学基金(61802017); 装备预研领域基金(61400020407)
Foundation item: National Natural Science Foundation of China (61802017); Equipment Pre-research Field Fund Project
(61400020407)
收稿时间: 2019-08-12; 修改时间: 2019-10-10, 2020-01-19; 采用时间: 2020-02-28