隨著計算機技術的快速發(fā)展和普及,軟件系統(tǒng)已經成為這個社會不可缺少的一部分。與此同時,軟件質量的問題也日益突出,特別的,對于用C語言編寫的軟件,其中一部分是應用于安全攸關的領域如銀行、航天、航空等,一個軟件錯誤就可能引起災難性的后果。靜態(tài)程序分析是提高軟件質量的一種有效手段,然而靜態(tài)分析工具在對實際程序分析時會產生一定的誤報和漏報,前者導致耗費大量的精力在錯誤報告的手工確認上,后者則導致無法發(fā)現潛在的程序錯誤,這兩個問題是限制靜態(tài)分析工具在實際中廣泛使用的主要原因。而誤報和漏報的產生的根源在于靜態(tài)分析的精確性和可伸縮性。本文圍繞靜態(tài)分析工具的精確性和可伸縮性開展了如下研究工作：·c程序內存泄漏檢測：內存泄漏是C程序中常見的編程錯誤,特別對于需要長時間運行的服務端軟件,內存泄漏會導致服務端軟件運行性能下降,甚至崩潰。學術界已提出多種基于靜態(tài)分析的檢測方法,但是這些方法對程序做了一定程度的抽象,導致精度丟失,從而增加了分析的誤報率和漏報率。針對該問題,本文提出了一個內存狀態(tài)轉移模型用于檢測程序的內存泄漏,該模型相比其他方法能夠更為全面地捕捉動態(tài)內存在程序分析過程中的狀態(tài)變化。為了支持跨過程分析,本文還提出了一種更精確的函數摘要的表示方法,相比于內聯的方法既保持了一定的分析精度又提高了分析的速度。該方法已實現在一個原型工具Melton中。通過實驗,Melton在多個使用廣泛的開源軟件（如OpenSSH）中找到了數十個之前未被發(fā)現的內存泄漏,并得到開發(fā)者的確認和修復。·支持多錯誤檢測的靜態(tài)分析框架：本文提出了一個支持多種程序錯誤檢測的靜態(tài)分析框架,并實現了一個靜態(tài)分析工具Canalyze。Canalyze在對實際程序分析的過程中找到了上百個之前尚未被發(fā)現的程序錯誤,并得到開發(fā)者的確認。另外,為了提高靜態(tài)分析工具Canalyze的可伸縮性,提出了一種精確的基于函數摘要的分析方法,并實現在工具Canalyze中,與基于函數內聯的方法比較提高了2到3倍的分析速度。·面向符號執(zhí)行的約束求解優(yōu)化：符號執(zhí)行一般采用SMT （Satisfiability Modulo Theories）求解器進行約束求解,然而SMT求解器的求解時間代價過高。針對該問題,本文提出了一個輕量級的基于賦值重用和后驗證的約束求解框架。賦值重用是在符號分析的過程中重用歷史求解過的約束集的可滿足賦值,來加快當前的求解過程；后驗證方法則是采用一個輕量級的求解器求解程序中的約束,然后再采用SMT求解器對可疑的路徑進行后驗證。這些優(yōu)化策略在保持求解精度的情況下,提升了上百倍的運行速度。 

 

中國科學技術大學安徽省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 面向符號執(zhí)行的約束求解優(yōu)化

    1.6 論文組織

第二章 背景介紹

    2.1 靜態(tài)程序分析

        2.1.1 控制流圖

        2.1.2 數據流分析

        2.1.3 符號執(zhí)行

        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 基于內存狀態(tài)轉移圖的內存泄漏檢測

        3.4.1 算法框架

        3.4.2 過程內分析

        3.4.3 過程間分析

        3.4.4 示例

        3.4.5 本方法的優(yōu)勢及潛在的優(yōu)化

    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程序靜態(tài)分析框架

    4.1 簡介

    4.2 示例

    4.3 框架概述

        4.3.1 系統(tǒng)架構

        4.3.2 錯誤檢測器

        4.3.3 框架整體算法

    4.4 基于區(qū)域的過程內分析

        4.4.1 抽象區(qū)域

        4.4.2 抽象值

        4.4.3 存儲,環(huán)境和約束守衛(wèi)

        4.4.4 程序狀態(tài)

    4.5 過程間符號執(zhí)行

        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 基于函數摘要的靜態(tài)錯誤檢測

        4.7.2 基于內聯的程序錯誤檢測

        4.7.3 模塊化的指針分析

        4.7.4 一般性的模塊化分析

    4.8 本章小節(jié)

第五章 面向符號執(zhí)行的輕量級約束求解框架

    5.1 簡介

    5.2 基于賦值重用的約束求解優(yōu)化

        5.2.1 符號執(zhí)行中的約束求解

        5.2.2 全變量賦值重用

        5.2.3 復雜約束變量賦值重用

        5.2.4 算法復雜度比較

    5.3 基于后驗證的約束求解優(yōu)化

        5.3.1 約束求解器

        5.3.2 基于后驗證的約束求解

        5.3.3 實驗結果

    5.4 相關工作

    5.5 本章小結

第六章 結束語

    6.1 主要貢獻

    6.2 進一步工作

        6.2.1 循環(huán)的分析

        6.2.2 浮點數的分析

        6.2.3 更多實驗以及工具的改進

參考文獻

致謝

在讀期間發(fā)表的學術論文與取得的研究成果

 

 

參考文獻

 

期刊論文

 

[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)