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

 

中國科學(xué)技術(shù)大學(xué)安徽省211工程院校985工程院校

 

頁數(shù)：111

 

【學(xué)位級別】：博士

 

文章目錄

摘要

ABSTRACT

目錄

表格索引

插圖索引

算法索引

第一章 簡介

    1.1 程序的正確性

    1.2 程序正確性證明

    1.3 程序的錯誤檢測

        1.3.1 軟件測試

        1.3.2 程序分析

    1.4 C程序應(yīng)用的廣泛及重要性

    1.5 研究內(nèi)容及貢獻(xiàn)

        1.5.1 C程序內(nèi)存泄漏檢測

        1.5.2 基于函數(shù)摘要的多錯誤檢測框架

        1.5.3 面向符號執(zhí)行的約束求解優(yōu)化

    1.6 論文組織

第二章 背景介紹

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

        2.1.1 控制流圖

        2.1.2 數(shù)據(jù)流分析

        2.1.3 符號執(zhí)行

        2.1.4 敏感性分析

    2.2 C程序的錯誤模式

        2.2.1 未定義的行為

        2.2.2 常見錯誤模式

    2.3 本章小結(jié)

第三章 內(nèi)存泄漏的自動化檢測

    3.1 簡介

    3.2 相關(guān)工作

    3.3 動機(jī)和示例

        3.3.1 內(nèi)存行為

        3.3.2 結(jié)合路徑敏感性的例子

    3.4 基于內(nèi)存狀態(tài)轉(zhuǎn)移圖的內(nèi)存泄漏檢測

        3.4.1 算法框架

        3.4.2 過程內(nèi)分析

        3.4.3 過程間分析

        3.4.4 示例

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

    3.5 具體實現(xiàn)

        3.5.1 Clang Static Analyzer概述

        3.5.2 內(nèi)存泄漏檢測器

        3.5.3 錯誤報告生成器

    3.6 實驗結(jié)果

        3.6.1 已檢測到的內(nèi)存泄漏

        3.6.2 與其他工具的比較

    3.7 本章小結(jié)

第四章 支持多錯誤檢測的C程序靜態(tài)分析框架

    4.1 簡介

    4.2 示例

    4.3 框架概述

        4.3.1 系統(tǒng)架構(gòu)

        4.3.2 錯誤檢測器

        4.3.3 框架整體算法

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

        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 基于函數(shù)摘要的分析

        4.5.2 基于內(nèi)聯(lián)的過程間分析

    4.6 實驗結(jié)果

        4.6.1 實驗基準(zhǔn)程序

        4.6.2 RQ1：錯誤檢測能力

        4.6.3 RQ2：過程間分析的比較

        4.6.4 RQ3：與Saturn的比較

    4.7 相關(guān)工作

        4.7.1 基于函數(shù)摘要的靜態(tài)錯誤檢測

        4.7.2 基于內(nèi)聯(lián)的程序錯誤檢測

        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 復(fù)雜約束變量賦值重用

        5.2.4 算法復(fù)雜度比較

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

        5.3.1 約束求解器

        5.3.2 基于后驗證的約束求解

        5.3.3 實驗結(jié)果

    5.4 相關(guān)工作

    5.5 本章小結(jié)

第六章 結(jié)束語

    6.1 主要貢獻(xiàn)

    6.2 進(jìn)一步工作

        6.2.1 循環(huán)的分析

        6.2.2 浮點數(shù)的分析

        6.2.3 更多實驗以及工具的改進(jìn)

參考文獻(xiàn)

致謝

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

 

 

參考文獻(xiàn)

 

期刊論文

 

[1]Demand-Driven Memory Leak Detection Based on Flow-and Context-Sensitive Pointer Analysis[J]. 王戟,馬曉東,董威,徐厚峰,劉萬偉.  Journal of Computer Science & Technology. 2009(02)

[2]約束問題求解[J]. 季曉慧,張健.  自動化學(xué)報. 2007(02)