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

Formal Verification Method for Integer Overflow in Aerospace Embedded Software

作　　者：高猛[1,2] 滕俊元 王政 GAO Meng;TENG Jun-Yuan;WANG Zheng(Beijing Institute of Control Engineering,Beijing 100190,China;Beijing Sunwise Information Technology Ltd.,Beijing 100190,China)

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

出　　处：《软件学报》2021年第10期2977-2992,共16页Journal of Software

基　　金：国家自然科学基金(61802017);装备预研领域基金(61400020407)。

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

关 键 词：航天嵌入式软件 整数溢出 有界模型检测 中断驱动型程序 顺序化 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]