【摘要】：隨著代碼規(guī)模的增大和系統(tǒng)復(fù)雜性的增加,軟件開發(fā)者意識到依靠人工的方式去維護軟件系統(tǒng)、排除系統(tǒng)錯誤已經(jīng)變得非常困難。形式化方法由于其正確性高、可自動化的特點,已經(jīng)開始被應(yīng)用于大型復(fù)雜的軟件系統(tǒng)中。模型檢驗作為一種廣泛采用的形式化方法,建立在對系統(tǒng)模型的抽象和對性質(zhì)規(guī)約驗證的基礎(chǔ)之上,利用算法對模型的性質(zhì)進(jìn)行驗證;模型檢驗技術(shù)不僅適用于系統(tǒng)開發(fā)前的安全性和可靠性驗證,也適用于系統(tǒng)后期的維護工作。Coccinelle作為基于模型檢驗技術(shù)的代碼搜索和轉(zhuǎn)化工具,主要用于解決系統(tǒng)API庫接口變化引發(fā)的并行演變。它利用描述語言SmPL描述代碼模式,還可以在代碼中搜索軟件錯誤和漏洞,提升代碼質(zhì)量。SmPL能夠理解C程序中的控制邏輯,因此可以精確地在大規(guī)模的程序中搜索C語言的代碼塊。目前SmPL支持條件語句、循環(huán)語句等不同控制結(jié)構(gòu)的模式描述,但是缺少了對do-while循環(huán)結(jié)構(gòu)的支持,這會限制SmPL的表達(dá)能力,影響程序匹配的準(zhǔn)確性。本文針對Coccinelle中缺少的do-while循環(huán)結(jié)構(gòu)進(jìn)行了建模和公式設(shè)計。我們通過對C語言代碼中的do-while循環(huán)結(jié)構(gòu)進(jìn)行建模,抽象為具有通用性的控制流圖。在SmPL中,需要將do-while循環(huán)的控制結(jié)構(gòu)轉(zhuǎn)為CTL公式;通過對do-while的語法定義的補充,完成從代碼到AST,再到CTL公式的轉(zhuǎn)換過程,從而拓展SmPL的表意能力,完善了Coccinelle的控制流功能。本文的成果主要包括:1.我們對拓展后的Coccinelle進(jìn)行了測試,包含了功能測試和性能測試,測試結(jié)果顯示拓展后的Coccinelle可以正確地解析包含復(fù)合控制結(jié)構(gòu)和嵌套結(jié)構(gòu)下的do-while循環(huán)。2.我們利用拓展后的Coccinelle對Linux內(nèi)核中的代碼模式進(jìn)行了調(diào)研,統(tǒng)計了Linux內(nèi)核中do-while結(jié)構(gòu)的數(shù)量和代碼分布情況。還成功地對現(xiàn)實中一個具體的內(nèi)核問題進(jìn)行了驗證,結(jié)果說明本文成果兼具正確性和實用性。
【學(xué)位授予單位】：蘭州大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2019
【分類號】：TP311.52
【圖文】：

大學(xué)碩士學(xué)位論文 完善 Coccinelle 的控制流功能的補丁進(jìn)行修改。occinelle 的實現(xiàn)原理分析上一節(jié)中，我們介紹了如何使用 Coccinelle 去匹配和搜索源代碼細(xì)分析 Coccinelle 實現(xiàn)這一過程的原理。Coccinelle 每次執(zhí)行以 規(guī)則為執(zhí)行單位。每個規(guī)則將對一個或者多個 C 源代碼文件進(jìn)行明了 Coccinelle 轉(zhuǎn)換引擎執(zhí)行的主要步驟。

圖 2-5 函數(shù) SAT，該函數(shù)還調(diào)用了特化函數(shù)pre 、pre 、S TEU和S TAF在這個算法中，SAT 函數(shù)接收模型 和公式Φ作為參數(shù)，遞歸地遍歷在模型中標(biāo)記滿足對應(yīng)公式的狀態(tài)節(jié)點。遞歸地遍歷公式時，通常最底層是原子命題。根據(jù) SAT 函數(shù)，當(dāng)公式中只有原子命題的情況時，它會標(biāo)命題成立的狀態(tài)節(jié)點，返回該狀態(tài)集合。這個狀態(tài)集合將作為函數(shù) SAT 結(jié)果，會上一層 SAT 函數(shù)中執(zhí)行其他運算符的計算。最后狀態(tài)集合之間結(jié)果會作為最終滿足公式Φ的輸出。在圖 2-3 中，Φ中會出現(xiàn)不同的運算符，主要有三類處理方式： 第一類是直接返回結(jié)果，例如 T，⊥以及原子命題。 第二類是遞歸地進(jìn)行處理，例如∧，∨和 運算符。 第三類是調(diào)用函數(shù)pre 、pre 、S TEU和S TAF進(jìn)行處理。對于第二類和第三類情況，算法通常會對公式進(jìn)行一次預(yù)處理，因為輯中，可以用 、∨來表示所有邏輯運算符；而在時序邏輯中，可以用 EX、AF 來表示所有時序運算符。公式 2-2 中包含了運算符的轉(zhuǎn)換關(guān)系。

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 孫書韜,何新華,宮云戰(zhàn),王維鋒;基于自由邊控制流圖的路徑覆蓋分析實現(xiàn)方法[J];裝甲兵工程學(xué)院學(xué)報;1996年03期

2 杜子德;程序控制流圖：一種可觀化的程序設(shè)計工具[J];計算機研究與發(fā)展;1995年12期

3 劉敏;;一個絲織機微機監(jiān)測系統(tǒng)介紹[J];微型機與應(yīng)用;1987年01期

4 羅四維;狄玉來;;具有兩個存儲器的控制流并行計算機結(jié)構(gòu)[J];計算機研究與發(fā)展;1988年03期

5 張雁;林英;;程序控制流圖自動生成的算法[J];計算機與數(shù)字工程;2010年02期

6 沈欽濤;張麗;羅磊;馬俊;余杰;吳慶波;;上下文敏感的控制流完整性保護的改進(jìn)方法[J];計算機科學(xué);2017年11期

7 李金諾;陸育鋒;湯云杰;張開元;;一種基于上下文的精簡控制流圖方法的研究[J];價值工程;2014年29期

8 孫永新;吳家培;閆大順;;基于基本塊標(biāo)識方法的控制流圖生成器設(shè)計[J];計算機應(yīng)用與軟件;2010年05期

9 徐渠;趙洋;袁馳;;一種基于擴展類控制流圖的類測試技術(shù)[J];微電子學(xué)與計算機;2016年01期

10 單永明;一種源程序到控制流圖的自動生成方法[J];小型微型計算機系統(tǒng);1996年10期

相關(guān)會議論文 前3條

1 夏玉輝;張威;萬琳;王洪艷;;一種基于控制流圖的靜態(tài)測試方法[A];第三屆全國軟件測試會議與移動計算、柵格、智能化高級論壇論文集[C];2009年

2 王雅文;宮云戰(zhàn);肖慶;楊朝紅;;區(qū)間運算在軟件缺陷檢測中的應(yīng)用[A];第五屆中國測試學(xué)術(shù)會議論文集[C];2008年

3 萬琳;劉娟;金麗亞;;未初始化變量故障的靜態(tài)分析[A];第四屆中國測試學(xué)術(shù)會議論文集[C];2006年

相關(guān)博士學(xué)位論文 前3條

1 李勇鋼;基于資源訪問控制的控制流劫持檢測與防御研究[D];中國科學(xué)技術(shù)大學(xué);2019年

2 孫強;面向?qū)ο蟪绦虻闹赶蚍治黾夹g(shù)研究[D];上海交通大學(xué);2013年

3 逄龍;多線程程序中關(guān)聯(lián)變量原子性驗證關(guān)鍵技術(shù)研究[D];哈爾濱工業(yè)大學(xué);2015年

相關(guān)碩士學(xué)位論文 前10條

1 趙益民;完善Coccinelle的控制流功能及測試[D];蘭州大學(xué);2019年

2 張浩宇;COTS DSP環(huán)境下JPEG2000的可配置軟加固技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2016年

3 帕爾哈提江·斯迪克;面向二進(jìn)制的控制流攻擊預(yù)防技術(shù)研究[D];西安電子科技大學(xué);2018年

4 王慶然;基于雙核安全處理器架構(gòu)的程序控制流保護策略[D];天津大學(xué);2018年

5 程偉;基于程序控制流的覆蓋率引導(dǎo)模糊測試技術(shù)研究[D];浙江大學(xué);2019年

6 崔晨;固件代碼控制流圖恢復(fù)技術(shù)研究[D];解放軍信息工程大學(xué);2012年

7 蘇振;類C語言程序分片系統(tǒng)的設(shè)計與實現(xiàn)[D];吉林大學(xué);2006年

8 曹厚華;快速程序流分析方法的研究與應(yīng)用[D];大連理工大學(xué);2008年

9 余雙雙;遺傳算法在交互概覽圖測試路徑生成中的應(yīng)用研究[D];重慶大學(xué);2016年

10 周瓚;一種PHP程序自動化缺陷分析工具的設(shè)計與開發(fā)[D];電子科技大學(xué);2014年

本文編號：2741205