面向C程序验证的切片执行方法

论文摘要

随着计算机系统的广泛应用,计算机软件的高可信性质受到了越来越多的关注。面向软件源程序的形式验证是保障软件高可信性质的一种有效方法,受到了大量的关注和广泛的研究。但是,由于软件程序逻辑复杂、规模庞大,如何提高软件源程序验证的精度特别是可扩展性仍是当前研究所面临的主要问题。本文提出了一种面向C程序的时序安全性质验证方法,即切片执行方法。它本质上是一种轻量级的符号执行,能够自动抽象出顺序和并发C程序的有限状态模型,并基于模型检验方法进行验证。切片执行融合了程序切片、程序语义抽象、符号化状态表示、反例制导的抽象精化、偏序缩减等多种有效的状态空间缩减技术,大大缩减了抽象模型的状态空间,从而提高了软件源程序形式验证的可扩展性。切片执行的主要特点是面向时序安全性质的验证,能够以接近标准流敏感数据流分析的代价,达到路径敏感程序模拟的验证精度;同时切片执行支持包括循环在内的程序结构,支持全自动的模型抽象和性质验证。切片执行构建在基于变量抽象的程序保守近似语义的基础上,它符号化地执行变量抽象下的相关语句,计算用于描述程序保守近似语义的部分最强后置条件和部分最弱前置条件,抽象出C程序的有限状态模型,并基于模型检验方法验证抽象模型是否满足给定的时序安全性质。基于本文提出的搜索复用框架,切片执行不断根据产生的伪反例路径精化变量抽象的抽象准则,直到性质被验证或找到真实反例路径。面向并发C程序验证,切片执行集成了本文提出的有状态动态偏序缩减方法,大大缩减搜索的状态空间。切片执行还集成了一种轻量级判定过程,用于对C程序验证过程中的验证公式进行高效判定。具体地,本文的创新点包括如下五个方面:1、提出了切片执行的基本概念和方法。基于对程序验证基本规律的分析,我们提出了变量抽象方法,只考虑程序中与待验证性质相关的变量和语句。基于变量抽象,我们定义了部分最强后置条件,进而定义了程序的保守近似语义。基于这两个概念,我们提出了切片执行的概念,它是一种轻量级的符号执行过程。2、提出了面向时序安全性质验证的搜索复用框架并将其应用于切片执行。搜索复用框架也是一种反例路径制导的抽象精化（CEGAR）框架,基于伪反例路径进行模型精化。相比传统的CEGAR框架,搜索复用框架的最大特点是能够在不同精度的抽象模型之间进行充分的信息复用,从而避免了大量不必要的重复搜索,有效降低了验证开销。3、提出了部分最弱前置条件的概念并将其应用于切片执行。部分最弱前置条件是程序保守近似语义的另一种表示方法,同样基于变量抽象定义。在切片执行过程中,可以用部分最弱前置条件部分地取代部分最强后置条件,以生成更弱的一阶逻辑公式来描述抽象模型的同一个状态,从而在不影响模型精度的前提下有效缩减生成模型的状态空间。4、提出了面向有状态模型检验的有状态动态偏序缩减方法,并将其集成到切片执行过程中。我们将切片执行方法扩展到了对并发C程序的验证。为了进一步进行状态空间缩减,我们提出了有状态动态偏序缩减方法,并将其自然地集成到切片执行框架中,用于指导切片执行,使其避免搜索多条具有相同偏序关系的并发进/线程交迭执行路径。我们进行了多个实验,包括两个实用并发程序片段和一个并发SSL程序。实验结果表明,切片执行和有状态动态偏序缩减这两种正交的状态空间缩减方法的集成,大大缩减了并发程序抽象模型的状态空间,特别是降低了验证的空间开销。5、提出了面向切片执行验证公式的轻量级判定过程。我们定义了一类整数线性一阶逻辑判定公式,此类判定公式支持C程序中常用的整数线性运算。我们优化了判定过程,并扩充了对整数除法、取余和位运算的支持。实验表明,扩充后的判定过程能够对面向C程序的切片执行所产生的绝大多数验证公式进行高效判定。在基于SSL程序的切片执行实验中我们发现,采用该判定方法后,验证效率比使用定理证明工具Simplify提高了10.5倍。我们还基于开放源代码的MAGIC项目,实现了基于切片执行的C程序验证工具原型,并基于openssl-0.9.6c等实用程序针对上述每个创新点都进行了实验。我们在实验时采用了与BLAST和MAGIC相同的硬件平台,并针对相同的验证用例,验证了相同的性质集合。经过充分的实验数据对比,我们发现切片执行在验证效率上具有一定的优势。

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 课题研究背景
• 1.1.1 软件的可信性质
• 1.1.2 基于软件源代码的可靠安全性质保证
• 1.2 相关研究工作
• 1.2.1 静态分析方法
• 1.2.2 定理证明方法
• 1.2.3 抽象解释方法
• 1.2.4 模型检验方法
• 1.2.5 谓词抽象方法
• 1.3 课题研究思路
• 1.3.1 相关工作的小结与比较
• 1.3.2 课题研究目标
• 1.3.3 课题研究内容
• 1.3.4 课题技术特色
• 1.4 课题创新点
• 1.5 论文结构
• 第二章 切片执行的基本概念和方法
• 2.1 基本模型和概念
• 2.1.1 C 程序模型和时序安全性质
• 2.1.2 最强后置条件
• 2.2 基于变量抽象的程序保守近似语义
• 2.2.1 变量抽象
• 2.2.2 部分最强后置条件
• 2.3 切片执行
• 2.3.1 切片执行上下文
• 2.3.2 切片执行图
• 2.3.3 讨论
• 2.4 时序安全性质的验证
• 2.4.1 对切片执行图的模型检验
• 2.4.2 切片执行与模型检验的集成
• 2.4.3 抽象准则的精化
• 2.5 验证工具与实验结果
• 2.5.1 验证工具
• 2.5.2 实验结果与分析
• 2.6 相关工作
• 2.7 小结
• 第三章 搜索复用框架及其在切片执行中的应用
• 3.1 面向切片执行的搜索复用框架
• 3.2 基于搜索复用框架的切片执行
• 3.3 可靠状态的确定
• 3.4 实验结果
• 3.5 相关工作
• 3.6 小结
• 第四章 部分最弱前置条件及其在切片执行中的应用
• 4.1 部分最弱前置条件
• 4.2 部分最弱前置条件在切片执行中的应用
• 4.3 避免部分最弱前置条件公式规模的指数增长
• 4.3.1 最弱前置条件公式规模的指数增长问题与解决方法
• 4.3.2 紧凑的部分最弱前置条件表示和计算方法
• 4.4 处理指针与变量别名
• 4.5 实验结果与分析
• 4.6 相关工作
• 4.7 小结
• 第五章 有状态动态偏序缩减方法
• 5.1 并发C 程序模型和无状态动态偏序缩减方法
• 5.1.1 并发C 程序模型
• 5.1.2 无状态动态偏序缩减方法
• 5.2 有状态动态偏序缩减方法
• 5.2.1 交迭信息总结
• 5.2.2 有状态动态偏序缩减方法
• 5.3 有状态动态偏序缩减的实现
• 5.3.1 交迭信息总结的实现
• 5.3.2 基于有状态动态偏序缩减的含圈状态空间遍历过程的实现
• 5.4 实验结果
• 5.5 相关研究工作
• 5.6 小结
• 第六章 并发C 程序的切片执行
• 6.1 并发C 程序模型及其保守近似语义
• 6.1.1 并发C 程序模型
• 6.1.2 变量抽象下的保守近似语义
• 6.2 并发C 程序的基本切片执行
• 6.3 集成无状态动态偏序缩减的切片执行
• 6.3.1 时钟向量
• 6.3.2 集成无状态动态偏序缩减的切片执行
• 6.4 集成有状态动态偏序缩减的切片执行
• 6.4.1 基于时钟向量的有状态动态偏序缩减方法的实现
• 6.4.2 集成有状态动态偏序缩减方法的切片执行过程
• 6.5 建模环境与实验结果
• 6.5.1 并发C 程序建模环境
• 6.5.2 实验结果
• 6.6 相关研究工作
• 6.7 小结
• 第七章 面向切片执行的轻量级判定过程
• 7.1 完备的整数线性公式判定方法
• 7.2 面向C 源代码验证的扩充判定方法
• 7.3 对切片执行产生的一阶逻辑验证公式的判定
• 7.4 验证工具和实验结果
• 7.5 相关工作
• 7.6 小结
• 第八章 结束语
• 8.1 工作总结
• 8.2 研究展望
• 致谢
• 参考文献
• 作者在学期间取得的学术成果