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

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

Fig.5 A common type of interrupt-driven programs
图 5 一类常见的中断驱动程序
2 基于有界模型检测的整数溢出检测方法

在传统的整数溢出有界模型检测 [7,8] 下,需要将运行时各变量取值信息以及当前运行位置作为程序模型状
态构建状态迁移系统,进而验证系统是否满足整数溢出性质.然而,该方法存在一个显著的问题:模型状态随着
程序规模的扩大而成倍增加,从而产生状态空间爆炸,无法有效地针对大规模软件进行检测.另外,航天嵌入式
软件的特征之一是使用中断作为软件设计常用的模式,而目前的有界模型检测技术大都无法适用于中断驱动
型程序整数溢出检测,因此很难在软件工程实践中直接应用.
本文针对以上问题开展了相关研究工作,首先给出整数溢出有界模型检测执行框架,而框架中的基于整数
溢出变量依赖的程序模型约简技术以及基于干扰变量的中断驱动型程序顺序化将在后续的各节中详细描述.
2.1 整数溢出有界模型检测执行框架

有界模型检测理论的基本思想是:用状态迁移系统 M 表征程序的行为,用模态/时序公式 F 描述程序的性
质,在给定的 k 界限之内检查系统 M 是否满足模态/时序公式 F:若不满足,则表明在界限 k 之内不存在错误;若满
足,则表明存在一条错误执行路径并给出相应的反例.
本文在 Clarke 等人 [7,9] 有界模型检测研究的基础上,基于整数溢出特征提出了基于整数溢出变量依赖的程
序模型约简技术以及基于干扰变量的中断驱动程序顺序化方法,在保证整数溢出分析精度的前提下,尽可能地
提高分析效率.
下面我们给出整数溢出有界模型检测执行的基本框架,如图 6 所示.
(1) 对程序进行约简和顺序化操作.框架中提到的程序模型约简和中断驱动程序顺序化方法将分别在后
续的第 2.2 节和第 2.3 节中进行详细描述;
(2) 将处理后的程序转化为静态单赋值形式 SSA.将程序按指定的界限 k 进行展开并得到相应的控制流
图(control flow graph,简称 CFG),控制流图可以进一步转化为静态单赋值形式.其中,本文中的界限 k
定义为循环执行次数的上界;
(3) 基于断言的属性规约描述整数溢出性质.整数溢出性质属于模型检测特性中的安全性(safty property)
范畴,即:在指定的范围内,给定的状态或事件(本文中指的是整数溢出错误)不会发生.基于断言的属性
规约能够表征程序运行至断言时给定变量取值集合 S,若存在从程序起始位置到断言位置的一条执
行路径,在该执行路径上经过一系列变量定义(即变量写操作),使得最终变量取值不属于集合 S,即发
生整数溢出.针对航天嵌入式软件整数溢出操作,可以依据其算术运算过程插入相应的断言,对变量
取值集合进行刻画,例如:若判断程序是否满足无符号整数加溢出错误,则在程序的位置 l 处插入断言
assert(arg 1 +arg 2 ≥arg 1 )即描述了无符号整数未发生加溢出时变量取值的集合;
(4) 构建逻辑公式,并使用 SMT 求解器求解.将模型各状态之间的转移关系与待验证的整数溢出性质进
行合取操作,构成待求解的公式,通过 SMT 求解器求解 [10] .若有解,则表明存在一条错误执行路径并给
出相应的反例;反之,则表明在界限 k 之内不存在整数溢出错误.