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

2990 Journal of Software 软件学报 Vol.32, No.10, October 2021

主程序 中断服务程序
void main( ){ void ex0_ISR( ){
… …
switch(datapkg){ if ((IntStateReg|0xfb)==0xfb){
case DATAPKG_P4: mwCurrent[0].bytes.high=XBYTE[0x002D];
while (i<32){ mwCurrent[0].bytes.low=XBYTE[0x002E];
i==0; mwPulTemp.word=mwCurrent[0].word;
if (i<31){ S 2:uartSend[2]=mwPulTemp.high;
S 1:uartSend[31]+=uartSend[i]; S 3:uartSend[3]=mwPulTemp.low;
} …
… }
i++; }
}
}
}
Fig.11 A typical example of false alarms
图 11 误报典型样例
4 相关工作

针对源码级整数溢出,已有的检测方法主要包括变量区间运算、污点分析和类型规约、动态分析.
(1) 变量区间运算.Sarkar 等人 [15] 提出了流不敏感的整数溢出分析方法,通过条件判断语句约束变量取值
范围,在遍历抽象语法树的过程中更新子分支下的变量约束条件,通过获得的变量数值范围信息来判
断是否发生整数溢出.Pereira 等人 [16] 提出了分阶段提取变量之间关系操作的约束,在拓扑顺序中分析
强连通分支,以加快变量约束求解的速度;
(2) 污点分析和类型规约.以 IntPatch、Kint、DRIVER 等工具 [6,17,18] 为代表的污点分析及类型规约技术,
通过提取程序中的危险路径,并利用代码插装或约束求解等方法来判定该路径上是否发生整数溢出.
其中,IntPatch 和 Kint 主要检测流入内存分配操作的整数溢出错误;DRIVER 尝试提取程序中所有危
险路径,并采用代码插装的方式来动态判定是否会触发整数溢出;
(3) 动态分析.以 ARCHERR 和 RICH 等工具 [19,20] 为代表的动态分析技术,在程序执行过程中对整数操作
插装变量取值范围的判定来检测整数溢出.其中,ARCHERR 考虑了运行时环境信息对整数算术运算
的影响;RICH 为整数操作语义定义形式化的安全规则,根据类型规则约束插装动态验证代码.
由于航天嵌入式软件控制算法涉及大量的数值型数据以及数学运算,而中断触发的不确定性导致软件可
执行路径分析变得异常复杂,因此上述这些技术具有明显的应用局限性,如存在运行开销大、误报率高等问题.
本文与这些研究的不同在于:根据整数溢出变量特征和中断驱动程序模型提出了针对性的检测方法,能够更有
效地捕获整数溢出错误.
在中断驱动型程序分析与验证基础研究方面,Kroening 等人 [21] 将中断驱动程序转换为对内存的原子读写
访问事件,并将这些访问事件的所有并发交叠状态直接编码为 SAT/SMT 公式,然后使用有界模型检测工具对生
成的公式进行验证.Schlich 等人 [22] 在模型检测时采用偏序约简技术,降低了中断驱动程序验证所要遍历的状态
空间规模.Kidd 等人 [23] 通过线程调度策略将多线程程序转换为顺序化程序,该方法只适用于中断优先级固定的
情况.Wu 等人 [12] 基于数据流依赖对中断驱动程序顺序化,并在抽象解释框架的基础上设计标志量抽象域和语
法等价抽象域来提高顺序化后中断驱动型程序的分析精度.
文献[24]的研究思路与本文较为接近,主要提出将中断并发程序自动序列化为非确定性的顺序程序,然后
将竞争发生的路径条件转换为 SMT 公式,并通过有界模型检测进行验证.但当中断程序的数目和规模较大时,
会产生状态空间爆炸,造成分析无法完成.与该项研究相比,本文作了如下关键技术改进:提出了一种基于干扰
变量的中断驱动程序顺序化方法,引入抽象解释、摘要机制对中断函数特征表示,在保证中断驱动型程序正确
性的同时也有效降低了顺序化后程序规模,并使得目前的模型检测技术能够适用于中断驱动型程序整数溢出
检测.