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

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

18 while Worklist and line>0
该算法的目的是找出所有与指定的断言相关语句组成的约束条件.为了证明本文算法的正确性,首先给出
“断言相关语句”定义.
定义 1(断言相关语句). 给定断言 assert(p),与该断言相关语句 s 应满足下列条件之一.
1) s 的左值出现在 p 中;
2) 存在语句 s 1 位于 s 和 assert(p)之间,s 1 与断言 assert(p)相关,且 s 的左值出现在 s 1 的右值中.
采用反证法给出上述算法的正确性证明,即,上述算法既不会遗漏约束条件,也不会输出多余的约束条件.
1) 假设本文算法遗漏了条件 S[n],则:
 assert(p),假设 S[n]C simp ,且 S[n]左值 v 出现在 p 中.由算法定义 6、定义 7vWorklist,由算法定义
11~定义 13如果 vWorklist,则 S[n]C simp ,与假设相反;
 assert(p),假设 S[n]C simp ,且S[m]C simp 满足 S[m]的右值中含有 S[n]的左值 v.由算法定义 16、定义
17vWorklist,由算法定义 11~定义 13如果 vWorklist,则 S[n]C simp ,与假设相反.
综上,可得证.
2) 假设本文算法输出了多余的条件 S[n],则:
assert(p),假设 S[n]C simp 与 assert(p)不相关,C simp 其余条件都与 assert(p)相关,记 S[n]的左值为 v.
由算法定义 11~定义 13vWorklist.
由算法定义 6、定义 7 和定义 16、定义 17必存在以下两种情况之一.
a) v 定义在 assert(p)中;
b) S[m]C simp 满足 v 在 S[m]的右值中出现,且 S[m]与 assert(p)相关.
对于情况 a),由断言相关语句定义 a)S[n]与 assert(p)相关;对于情况 b),由断言相关语句的定义 b)S[n]
与 assert(p)相关.
与假设矛盾,故得证. □
本文算法通过对 SSA 中间表示语句集合进行遍历,根据整数溢出变量传递性和无后效性选取与整数溢出
相关的语句加入约束条件 C simp 中.因此,约简后的验证条件为 C simp P,该约简条件将作为模型检测的输入.图 7
给出了一个从 C 程序到约简后 SSA 形式的转换过程示例,可以看出:约简后不仅降低了程序约束条件 C 的规模,
也不会影响程序执行到断言语句处的状态和性质.

Fig.7 Translation from a C program to its reduction SSA form
图 7 C 程序到约简后 SSA 形式的转换
本文使用 Z3 作为 SMT 求解器 [11] .图 7(d)所展示的 C simp 还包括 x 3 =guard 0 ?x 2 :x 1 的形式,因此需要对公式加
以展开,以便调用 SMT 求解器,如图 8 所示.
图 8(b)中展开得到的析取范式包括具有蕴含关系的单元子句(z 0 >10z 0 >0)及矛盾的子句(z 0 >10z 0 ≤0),本
文暂不考虑具有单元子句之间的约简,直接利用 SMT 求解器完成判定.