C程序静态分析与错误检测 优秀博士毕业论文

  随着计算机技术的快速发展和普及,软件系统已经成为这个社会不可缺少的一部分。与此同时,软件质量的问题也日益突出,特别的,对于用C语言编写的软件,其中一部分是应用于安全攸关的领域如银行、航天、航空等,一个软件错误就可能引起灾难性的后果。静态程序分析是提高软件质量的一种有效手段,然而静态分析工具在对实际程序分析时会产生一定的误报和漏报,前者导致耗费大量的精力在错误报告的手工确认上,后者则导致无法发现潜在的程序错误,这两个问题是限制静态分析工具在实际中广泛使用的主要原因。而误报和漏报的产生的根源在于静态分析的精确性和可伸缩性。本文围绕静态分析工具的精确性和可伸缩性开展了如下研究工作：·c程序内存泄漏检测：内存泄漏是C程序中常见的编程错误,特别对于需要长时间运行的服务端软件,内存泄漏会导致服务端软件运行性能下降,甚至崩溃。学术界已提出多种基于静态分析的检测方法,但是这些方法对程序做了一定程度的抽象,导致精度丢失,从而增加了分析的误报率和漏报率。针对该问题,本文提出了一个内存状态转移模型用于检测程序的内存泄漏,该模型相比其他方法能够更为全面地捕捉动态内存在程序分析过程中的状态变化。为了支持跨过程分析,本文还提出了一种更精确的函数摘要的表示方法,相比于内联的方法既保持了一定的分析精度又提高了分析的速度。该方法已实现在一个原型工具Melton中。通过实验,Melton在多个使用广泛的开源软件（如OpenSSH）中找到了数十个之前未被发现的内存泄漏,并得到开发者的确认和修复。·支持多错误检测的静态分析框架：本文提出了一个支持多种程序错误检测的静态分析框架,并实现了一个静态分析工具Canalyze。Canalyze在对实际程序分析的过程中找到了上百个之前尚未被发现的程序错误,并得到开发者的确认。另外,为了提高静态分析工具Canalyze的可伸缩性,提出了一种精确的基于函数摘要的分析方法,并实现在工具Canalyze中,与基于函数内联的方法比较提高了2到3倍的分析速度。·面向符号执行的约束求解优化：符号执行一般采用SMT （Satisfiability Modulo Theories）求解器进行约束求解,然而SMT求解器的求解时间代价过高。针对该问题,本文提出了一个轻量级的基于赋值重用和后验证的约束求解框架。赋值重用是在符号分析的过程中重用历史求解过的约束集的可满足赋值,来加快当前的求解过程；后验证方法则是采用一个轻量级的求解器求解程序中的约束,然后再采用SMT求解器对可疑的路径进行后验证。这些优化策略在保持求解精度的情况下,提升了上百倍的运行速度。 

 

中国科学技术大学安徽省211工程院校985工程院校

 

页数：111

 

【学位级别】：博士

 

文章目录

摘要

ABSTRACT

目录

表格索引

插图索引

算法索引

第一章 简介

    1.1 程序的正确性

    1.2 程序正确性证明

    1.3 程序的错误检测

        1.3.1 软件测试

        1.3.2 程序分析

    1.4 C程序应用的广泛及重要性

    1.5 研究内容及贡献

        1.5.1 C程序内存泄漏检测

        1.5.2 基于函数摘要的多错误检测框架

        1.5.3 面向符号执行的约束求解优化

    1.6 论文组织

第二章 背景介绍

    2.1 静态程序分析

        2.1.1 控制流图

        2.1.2 数据流分析

        2.1.3 符号执行

        2.1.4 敏感性分析

    2.2 C程序的错误模式

        2.2.1 未定义的行为

        2.2.2 常见错误模式

    2.3 本章小结

第三章 内存泄漏的自动化检测

    3.1 简介

    3.2 相关工作

    3.3 动机和示例

        3.3.1 内存行为

        3.3.2 结合路径敏感性的例子

    3.4 基于内存状态转移图的内存泄漏检测

        3.4.1 算法框架

        3.4.2 过程内分析

        3.4.3 过程间分析

        3.4.4 示例

        3.4.5 本方法的优势及潜在的优化

    3.5 具体实现

        3.5.1 Clang Static Analyzer概述

        3.5.2 内存泄漏检测器

        3.5.3 错误报告生成器

    3.6 实验结果

        3.6.1 已检测到的内存泄漏

        3.6.2 与其他工具的比较

    3.7 本章小结

第四章 支持多错误检测的C程序静态分析框架

    4.1 简介

    4.2 示例

    4.3 框架概述

        4.3.1 系统架构

        4.3.2 错误检测器

        4.3.3 框架整体算法

    4.4 基于区域的过程内分析

        4.4.1 抽象区域

        4.4.2 抽象值

        4.4.3 存储,环境和约束守卫

        4.4.4 程序状态

    4.5 过程间符号执行

        4.5.1 基于函数摘要的分析

        4.5.2 基于内联的过程间分析

    4.6 实验结果

        4.6.1 实验基准程序

        4.6.2 RQ1：错误检测能力

        4.6.3 RQ2：过程间分析的比较

        4.6.4 RQ3：与Saturn的比较

    4.7 相关工作

        4.7.1 基于函数摘要的静态错误检测

        4.7.2 基于内联的程序错误检测

        4.7.3 模块化的指针分析

        4.7.4 一般性的模块化分析

    4.8 本章小节

第五章 面向符号执行的轻量级约束求解框架

    5.1 简介

    5.2 基于赋值重用的约束求解优化

        5.2.1 符号执行中的约束求解

        5.2.2 全变量赋值重用

        5.2.3 复杂约束变量赋值重用

        5.2.4 算法复杂度比较

    5.3 基于后验证的约束求解优化

        5.3.1 约束求解器

        5.3.2 基于后验证的约束求解

        5.3.3 实验结果

    5.4 相关工作

    5.5 本章小结

第六章 结束语

    6.1 主要贡献

    6.2 进一步工作

        6.2.1 循环的分析

        6.2.2 浮点数的分析

        6.2.3 更多实验以及工具的改进

参考文献

致谢

在读期间发表的学术论文与取得的研究成果

 

 

参考文献

 

期刊论文

 

[1]Demand-Driven Memory Leak Detection Based on Flow-and Context-Sensitive Pointer Analysis[J]. 王戟,马晓东,董威,徐厚峰,刘万伟.  Journal of Computer Science & Technology. 2009(02)

[2]约束问题求解[J]. 季晓慧,张健.  自动化学报. 2007(02)