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

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

Fig.1 Distributions trend of integer overflow
图 1 4 类整数溢出分布趋势

1.2 整数溢出特征分析
1) 整数溢出变量分析
这里所谓的整数溢出变量是指与整数溢出操作存在数据依赖关系的变量,符合数据流依赖性关系,即具有
传递性和无后效性的特点.
a. 传递性.对于整数溢出操作 T,若操作数为变量 a 和 b,则整数溢出操作 T 依赖于变量 a 和 b.若变量 a、
b 在整数溢出操作前进行了定义(即变量写操作)或条件判断,记为
a=g(m i )?func(m j ):func(m k ),b=g(n i )?func(n j ):func(n k ),
其中,m i 、m j 、m k 、n i 、n j 、n k 为变量集合,则整数溢出操作 T 也依赖于集合 m i 、m j 、m k 、n i 、n j 、n k
中的变量,即整数溢出数据依赖关系具有传递性;
b. 无后效性.假设在程序起始点到整数溢出点 T 的任一条执行路径上的某一整数溢出变量为 m,则变量
m 的值信息仅取决于该路径上最近时刻该变量的定义,而与其他时刻变量 m 的定义无关.
图 2(a)给出了整数溢出变量传递性的示例,其中,程序第 5 行为整数溢出操作,操作数为 m 2 和 m 1 .而 m 2 的取
值依赖于变量 b 和 c,m 1 的取值依赖于变量 a 和 c,因此,变量 a、b、c、m 1 、m 2 称为整数溢出变量.图 2(b)给出
了整数溢出变量 a、b、c、m 1 、m 2 之间的依赖关系.
1 unsigned int a,b,c,m 1,m 2,rec; a c b
2 a=2; b=3; c=4;
3 m 1=c-a; m 1 m 2
4 m 2=c-b;
5 rec=m 2-m 1; rec=m 2-m 1
(a) (b)
Fig.2 Example: Transitivity of integer overflow variables
图 2 示例:整数溢出变量的传递性
图 3 给出了整数溢出变量无后效性的示例,其中,程序第 6 行为整数溢出操作,操作数为 a 和 b.而变量 a 的
值仅取决于第 5 行的赋值操作,与第 2 行的赋值操作无关;变量 b 的值仅取决于第 3 行的赋值操作.
1 unsigned int a,b,c,rec;
2 a=2;
3 b=3;
4 c=4;
5 a=c;
6 rec=b-a;
Fig.3 Example: No aftereffect of integer overflow variables
图 3 示例:整数溢出变量的无后效性