現(xiàn)代社會,軟件已經(jīng)成為最重要的基礎設施之一,在很多行業(yè)中發(fā)揮著不可或缺的作用。同時,軟件的安全性也越來越受人們的重視。軟件測試作為保障軟件可靠性的重要手段之一,一直以來都是國內(nèi)外科研人員的研究熱點。動態(tài)符號執(zhí)行技術是軟件測試領域的前沿技術,從誕生以來一直受人們的廣泛關注。國內(nèi)外研究人員基于動態(tài)符號執(zhí)行技術開發(fā)了很多實用的軟件測試工具,KLEE就是其中的佼佼者。然而,KLEE只能對單線程程序進行符號執(zhí)行。鑒于此,瑞典洛桑聯(lián)邦理工學院的Stefan Bucur與其合作伙伴在KLEE的基礎上開發(fā)了并行符號執(zhí)行工具Cloud9,實現(xiàn)了對多線程程序的符號執(zhí)行。但是Cloud9在對多線程程序進行符號執(zhí)行時沒有考慮線程交錯調(diào)度問題,不能完全探索多線程程序的所有路徑。因此,本文在Cloud9的基礎上,設計并實現(xiàn)了可以覆蓋所有路徑分支的一般多線程符號執(zhí)行框架,并在此基礎上,提出了基于斷言制導的多線程符號執(zhí)行方法。本文的主要貢獻包括以下三點:在研究了符號執(zhí)行基本理論和Cloud9對多線程程序符號執(zhí)行的方法的基礎上,給出了可以覆蓋所有路徑分支的一般多線程程序符號執(zhí)行框架,從三個方面來講述:首先,對多線程符號... 

【文章來源】：西安電子科技大學陜西省 211工程院校 教育部直屬院校

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

【學位級別】：碩士

【文章目錄】：
摘要
ABSTRACT
縮略語對照表
第一章 緒論
    1.1 研究背景與意義
    1.2 國內(nèi)外研究現(xiàn)狀
    1.3 研究內(nèi)容和組織結構
        1.3.1 研究內(nèi)容
        1.3.2 組織結構
第二章 相關理論與技術
    2.1 動態(tài)符號執(zhí)行概述
        2.1.2 動態(tài)符號執(zhí)行基本流程
        2.1.3 動態(tài)符號執(zhí)行各模塊介紹
        2.1.4 動態(tài)符號執(zhí)行面臨的挑戰(zhàn)
    2.2 KLEE概述
        2.2.1 解釋模塊
        2.2.2 符號表示模塊
        2.2.3 約束求解模塊
        2.2.4 路徑選擇模塊
        2.2.5 錯誤檢測模塊
    2.3 Cloud9概述
    2.4 本章小結
第三章 基于斷言制導的多線程符號執(zhí)行的設計
    3.1 一般多線程符號執(zhí)行
        3.1.1 多線程程序的描述
        3.1.2 廣義交錯圖
        3.1.3 算法描述
    3.2 基于斷言制導的多線程符號執(zhí)行
        3.2.1 主要思想
        3.2.2 算法描述
        3.2.3 最弱前置條件的計算
        3.2.4 b-PP結點的謂詞摘要
        3.2.5 i-PP結點的謂詞摘要
        3.2.6 基于謂詞摘要的冗余執(zhí)行修剪
        3.2.7 謂詞摘要的優(yōu)化
    3.3 本章小結
第四章 基于斷言制導的多線程符號執(zhí)行的實現(xiàn)
    4.1 方法實現(xiàn)的流程框架
    4.2 符號執(zhí)行模塊
    4.3 謂詞摘要計算模塊
        4.3.1 遞歸過程的實現(xiàn)
        4.3.2 結點分類的實現(xiàn)
        4.3.3 狀態(tài)更新的實現(xiàn)
        4.3.4 謂詞摘要生成的實現(xiàn)
    4.4 冗余執(zhí)行修剪模塊
    4.5 本章小結
第五章 實驗與結果分析
    5.1 實驗環(huán)境介紹
    5.2 實驗測試
    5.3 實驗結果分析
    5.4 本章小結
第六章 總結與展望
    6.1 總結
    6.2 展望
參考文獻
致謝
作者簡介


【參考文獻】：
期刊論文
[1]計算機軟件中安全漏洞檢測技術的應用[J]. 陳楷.  數(shù)字技術與應用. 2010(07)
[2]淺談代碼安全質(zhì)量保障中的模糊測試技術[J]. 鄧承志,朱衛(wèi)東.  信息網(wǎng)絡安全. 2009(02)
[3]基于污點分析的源代碼脆弱性檢測技術[J]. 孔德光,鄭烇,帥建梅,陳超,葛瑤.  小型微型計算機系統(tǒng). 2009(01)
[4]軟件安全漏洞的靜態(tài)檢測技術[J]. 張林,曾慶凱.  計算機工程. 2008(12)

碩士論文
[1]基于動態(tài)符號執(zhí)行的MSVL程序模型檢測理論與方法[D]. 卜康康.西安電子科技大學 2015



本文編號：3264606