科技發(fā)展日新月異,計算機(jī)的應(yīng)用越來越普及,使得程序隨處可見,其應(yīng)用場景十分廣泛,小到手機(jī)應(yīng)用、智能家電控制系統(tǒng)和門禁系統(tǒng)等,大到交通控制系統(tǒng)、高鐵列車控制系統(tǒng)和衛(wèi)星通信系統(tǒng)等。人們的安全意識也逐步提高,對于程序的安全性和可靠性的要求也越來越高。如何保障程序的安全性和提高可靠性一直以來是軟件技術(shù)發(fā)展與應(yīng)用的核心問題之一。本文主要從靜態(tài)程序驗證領(lǐng)域?qū)Τ绦蛟创a進(jìn)行分析。其工作流程首先通過底層虛擬機(jī)(Low Level Virtual Machine,LLVM)將源代碼轉(zhuǎn)換成與語言無關(guān)的中間表示,并對中間表示進(jìn)行優(yōu)化和提升,轉(zhuǎn)化成靜態(tài)單賦值形式;其次使用有界模型檢測技術(shù)實現(xiàn)程序有限次數(shù)的循環(huán)展開;然后通過語義分析將中間表示轉(zhuǎn)化成等價的基于SMT-lib2規(guī)范的公式;最后調(diào)用可滿足性模理論(Satisfiability Modulo Theories,SMT)求解器驗證解析后的公式集合的正確性。本文的主要貢獻(xiàn)有三個方面:首先實現(xiàn)了基于LLVM的中間表示的基本塊狀態(tài)遷移系統(tǒng)的有界模型檢測方法,避免了對源代碼的直接驗證,通過有界模型檢測實現(xiàn)循環(huán)展開,通過語義分析實現(xiàn)數(shù)據(jù)流編碼,通過構(gòu)造遷移關(guān)系實現(xiàn)...

【文章頁數(shù)】：64 頁

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

【文章目錄】：
摘要
abstract
第1章 引言
    1.1 研究背景和意義
    1.2 研究現(xiàn)狀
    1.3 主要工作
    1.4 論文結(jié)構(gòu)
    1.5 本章小結(jié)
第2章 相關(guān)技術(shù)
    2.1 形式驗證
    2.2 有界模型檢測
    2.3 LLVM
        2.3.1 中間表示
        2.3.2 指令集
        2.3.3 靜態(tài)單賦值形式
    2.4 控制流分析
        2.4.1 控制流圖
        2.4.2 支配關(guān)系
        2.4.3 后支配關(guān)系
        2.4.4 控制依賴關(guān)系
    2.5 SMT求解器
    2.6 本章小結(jié)
第3章 基于狀態(tài)遷移的程序驗證方法
    3.1 生成中間表示
    3.2 有限次循環(huán)展開
        3.2.1 循環(huán)展開預(yù)處理
        3.2.2 循環(huán)展開
    3.3 遷移系統(tǒng)構(gòu)造
        3.3.1 基本塊
        3.3.2 基本塊遷移關(guān)系構(gòu)造
        3.3.3 指令構(gòu)造
    3.4 測試用例生成公式
    3.5 實驗分析
    3.6 本章小結(jié)
第4章 基于狀態(tài)遷移的程序驗證方法改進(jìn)
    4.1 遷移系統(tǒng)構(gòu)造
        4.1.1 基本塊表示
        4.1.2 指令分析
    4.2 測試用例生成公式
    4.3 實驗分析
    4.4 本章小結(jié)
第5章 基于控制依賴關(guān)系的程序驗證方法
    5.1 拓?fù)渑判?br>    5.2 控制依賴關(guān)系
    5.3 遷移系統(tǒng)構(gòu)造
        5.3.1 控制流表示
        5.3.2 指令分析
    5.4 測試用例生成公式
    5.5 實驗分析
    5.6 本章小結(jié)
第6章 總結(jié)與展望
    6.1 本文主要成果
    6.2 本文的創(chuàng)新點
    6.3 本文的不足
    6.4 將來的工作
參考文獻(xiàn)
致謝



本文編號：3833174