航天嵌入式软件整数溢出的形式化验证方法
CSTR:
作者:
作者单位:

作者简介:

高猛(1982-),男,高级工程师,CCF专业会员,主要研究领域为软件可靠性,嵌入式软件测试,模型检测.
滕俊元(1985-),男,高级工程师,主要研究领域为软件形式化验证,嵌入式软件测试.
王政(1986-),男,博士,高级工程师,主要研究领域为软件形式化建模,分析与验证,基于模型的设计.

通讯作者:

滕俊元,E-mail:tengjunyuan@sunwiseinfo.com

中图分类号:

TP311

基金项目:

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


Formal Verification Method for Integer Overflow in Aerospace Embedded Software
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61802017); Equipment Pre-research Field Fund Project (61400020407)

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    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.

    参考文献
    相似文献
    引证文献
引用本文

高猛,滕俊元,王政.航天嵌入式软件整数溢出的形式化验证方法.软件学报,2021,32(10):2977-2992

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2019-08-12
  • 最后修改日期:2020-01-19
  • 录用日期:
  • 在线发布日期: 2021-10-09
  • 出版日期: 2021-10-06
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号