软件学报

作者：高猛，滕俊元，王政

单位：高猛，北京控制工程研究所, 北京 100190;北京轩宇信息技术有限公司, 北京 10019011,滕俊元，北京控制工程研究所, 北京 100190;北京轩宇信息技术有限公司, 北京 10019002,王政，北京控制工程研究所, 北京 100190;北京轩宇信息技术有限公司, 北京 10019003

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

基金：国家自然科学基金（61802017）；装备预研领域基金（61400020407）

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

来源：2021年第10期

《软件学报》期刊编辑部

查看软件学报杂志2021年第10期