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

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

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

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

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


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

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



本文編號(hào)：3264606