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

高猛 等:航天嵌入式软件整数溢出的形式化验证方法 2987

主程序在第 8 行赋值语句中对全局变量 interfval 进行读访问,中断 ISR 0 对 interfval 进行写访问,因此该程
序干扰变量信息为interfval,tmpval=interfval,8,0,中断 ISR 0 函数摘要表示为0,interfval,[3,3].图 10(b)给出了顺
序化后的程序,该程序引入了干扰位置变量 loc 0 和中断触发标志变量 rand 0 ,并在赋值语句 tmpval=interfval 前插
入了中断 ISR 0 函数摘要.经有界模型检测后,给出了发生整数溢出的路径,即:当 loc 0 为 8、rand 0 为 1、interfval
为 3 时,会导致整数溢出错误.

Fig.10 Sequentialization of an interrupt-driven program
图 10 中断驱动程序顺序化示例
3 实验评估

在本节的实验评估中,我们采用“样例+实例”的验证思路对提出的整数溢出检测方法的性能和效果进行评
估.在样例验证中,使用基准测试程序来验证基于整数溢出变量依赖的程序模型约简技术的有效性.基准测试程
序来源于 SIR(software-artifact infrastructure repository)程序集 [13] ,该程序集是软件研究领域广泛认可的标准验
证程序;在实例验证中,以文献[14]介绍的基准测试程序以及从典型整数溢出实例中选取的两个真实航天领域
嵌入式软件为对象,重点验证中断驱动程序顺序化方法的有效性.实验的硬件环境均配置为 Windows 10 Intel
Core i7- 8550@1.80GHz 8.00GB RAM.
3.1 样例验证

样例验证阶段,选择 SIR 标准验证程序套件中的 4 个软件作为被测程序.被测程序均为顺序化程序,由于其
内置故障并不包含整数溢出,因此需要通过变异注入的方式构造整数溢出错误.被测程序的基本信息以及变异
注入各类整数溢出错误的数量见表 1.
Table 1 Basic information of the program
表 1 被测程序基本信息
被测程序 无符号整数上溢 无符号整数下溢 有符号整数上溢 有符号整数下溢 问题总数 LOC 功能
tcas 1 1 1 1 4 173 飞行器高度隔离
schedule 1 1 2 1 5 412 优先级规划
schedule2 1 1 1 1 4 374 信息度量
printtokens 1 2 2 1 6 726 词法分析

以 tcas 程序为例,表 2 给出了 4 种整数溢出实例,其中,每一个错误包含两行:第 1 行表示变异注入的语句,
第 2 行表示整数溢出语句.