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

 

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

 

頁(yè)數(shù)：111

 

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

 

文章目錄

摘要

ABSTRACT

目錄

表格索引

插圖索引

算法索引

第一章 簡(jiǎn)介

    1.1 程序的正確性

    1.2 程序正確性證明

    1.3 程序的錯(cuò)誤檢測(cè)

        1.3.1 軟件測(cè)試

        1.3.2 程序分析

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

    1.5 研究?jī)?nèi)容及貢獻(xiàn)

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

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

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

    1.6 論文組織

第二章 背景介紹

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

        2.1.1 控制流圖

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

        2.1.3 符號(hào)執(zhí)行

        2.1.4 敏感性分析

    2.2 C程序的錯(cuò)誤模式

        2.2.1 未定義的行為

        2.2.2 常見(jiàn)錯(cuò)誤模式

    2.3 本章小結(jié)

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

    3.1 簡(jiǎn)介

    3.2 相關(guān)工作

    3.3 動(dòng)機(jī)和示例

        3.3.1 內(nèi)存行為

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

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

        3.4.1 算法框架

        3.4.2 過(guò)程內(nèi)分析

        3.4.3 過(guò)程間分析

        3.4.4 示例

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

    3.5 具體實(shí)現(xiàn)

        3.5.1 Clang Static Analyzer概述

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

        3.5.3 錯(cuò)誤報(bào)告生成器

    3.6 實(shí)驗(yàn)結(jié)果

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

        3.6.2 與其他工具的比較

    3.7 本章小結(jié)

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

    4.1 簡(jiǎn)介

    4.2 示例

    4.3 框架概述

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

        4.3.2 錯(cuò)誤檢測(cè)器

        4.3.3 框架整體算法

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

        4.4.1 抽象區(qū)域

        4.4.2 抽象值

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

        4.4.4 程序狀態(tài)

    4.5 過(guò)程間符號(hào)執(zhí)行

        4.5.1 基于函數(shù)摘要的分析

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

    4.6 實(shí)驗(yàn)結(jié)果

        4.6.1 實(shí)驗(yàn)基準(zhǔn)程序

        4.6.2 RQ1：錯(cuò)誤檢測(cè)能力

        4.6.3 RQ2：過(guò)程間分析的比較

        4.6.4 RQ3：與Saturn的比較

    4.7 相關(guān)工作

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

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

        4.7.3 模塊化的指針?lè)治?/div>

本文編號(hào)：168299