【摘要】：隨著計(jì)算機(jī)技術(shù)的不斷發(fā)展,軟件已經(jīng)融入到人們的日常生活和工作生產(chǎn)中,而隨著軟件規(guī)模和復(fù)雜度的不斷攀升,軟件的質(zhì)量依舊不盡如人意,由此造成的問題對于安全攸關(guān)的領(lǐng)域威脅極大。提高軟件的可信度是大勢所趨,其中基于演繹推理的形式化驗(yàn)證方法就是主要研究方向之一。本課題組設(shè)計(jì)并開發(fā)了安全C語言驗(yàn)證器,它是一款基于演繹推理的C語言程序驗(yàn)證工具,采用了霍爾邏輯和形狀圖邏輯。形狀系統(tǒng)是安全C語言驗(yàn)證器對于形狀圖邏輯的實(shí)現(xiàn),用于完成堆指針相關(guān)程序語句的演算,并限制程序能夠使用的易變數(shù)據(jù)結(jié)構(gòu)及其相關(guān)操作。本工作針對形狀系統(tǒng)中存在的不足,實(shí)施了一系列改進(jìn)和擴(kuò)展。第一,擴(kuò)展了形狀系統(tǒng)的演算操作。通過為節(jié)點(diǎn)定位演算擴(kuò)展角標(biāo)表達(dá)式相關(guān)的操作規(guī)則,把該演算擴(kuò)展到適用于帶角標(biāo)的指針訪問路徑的場合,解決原本指針訪問路徑抽象表述能力不足的問題。此外,本工作還通過函數(shù)調(diào)用窗口的概念,細(xì)化和實(shí)現(xiàn)了形狀圖邏輯中最復(fù)雜的函數(shù)調(diào)用規(guī)則,使得形狀系統(tǒng)能支持帶函數(shù)調(diào)用語句的驗(yàn)證。第二,改進(jìn)了形狀圖的構(gòu)造方法。形狀圖構(gòu)造方法用于從描述堆指針性質(zhì)的符號斷言構(gòu)造等價(jià)的形狀圖,以便形狀系統(tǒng)能夠根據(jù)構(gòu)造得到的形狀圖對堆指針操作語句進(jìn)行演算。本工作為該方法引入了內(nèi)置形狀謂詞,用以簡化和復(fù)用部分?jǐn)嘌悦枋?并對不同類型的斷言施加明確的操作語義,使得形狀系統(tǒng)可以正確還原斷言描述的形狀圖,并發(fā)現(xiàn)斷言中的錯(cuò)誤。此外,本工作還引入了自定義謂詞到內(nèi)置形狀謂詞的推斷方法,以盡可能規(guī)避內(nèi)置形狀謂詞引入后造成的冗余表述的問題。第三,引入了形狀檢查方法。形狀檢查方法用以檢查程序使用的易變數(shù)據(jù)結(jié)構(gòu)是否符合安全C語言的相關(guān)限定。為表示檢查操作的不同嚴(yán)格程度,本工作為形狀檢查方法引入不同的形狀級別,并通過形狀分割、形狀分析和形狀推斷這三個(gè)階段分解由易變數(shù)據(jù)結(jié)構(gòu)中不同指針域帶來的復(fù)雜性。另外,本工作還通過實(shí)現(xiàn)顯式形狀檢查和隱式形狀檢查,簡化形狀檢查方法的使用。通過本文工作,擴(kuò)展后的形狀系統(tǒng)可以處理表述能力更強(qiáng)、更為復(fù)雜的描述形狀圖的斷言,能夠支持含有函數(shù)調(diào)用的程序的演算,并且能夠靈活便捷地完成對于易變數(shù)據(jù)結(jié)構(gòu)是否符合形狀定義的檢查,最終使得形狀系統(tǒng)的功能和性能得到改善。
【學(xué)位授予單位】：中國科學(xué)技術(shù)大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2018
【分類號】：TP311.52
【圖文】：

形狀圖是對于程序執(zhí)行過程中易變數(shù)據(jù)結(jié)構(gòu)狀態(tài)的圖形化描述，它通過有逡逑向圖的形式描述程序中聲明的堆指針變量和堆內(nèi)存中數(shù)據(jù)結(jié)構(gòu)節(jié)點(diǎn)指針域的指逡逑向情況，但并不關(guān)心節(jié)點(diǎn)的數(shù)據(jù)域。如圖２．３所示，在形狀圖的表述中，存在６種逡逑不同類型的形狀圖節(jié)點(diǎn)［３７］：聲明節(jié)點(diǎn)用于指代程序中聲明的堆指針變量，顯示逡逑為圓形節(jié)點(diǎn)；ＮＵＬＬ節(jié)點(diǎn)用于描述Ｃ語言中的ＮＵＬＬ字面量，顯示為含Ｎ的虛逡逑線矩形，若存在指針指向ＮＵＬＬ節(jié)點(diǎn)，即該指針的值為ＮＵＬＬ；懸空節(jié)點(diǎn)用于描逡逑述懸空的內(nèi)存塊，顯示為含Ｄ的虛線矩形，若存在指針指向懸空節(jié)點(diǎn)，即該指逡逑針懸空；結(jié)構(gòu)節(jié)點(diǎn)用于指代動(dòng)態(tài)分配的結(jié)構(gòu)體內(nèi)存塊，顯示為實(shí)線矩形；濃縮節(jié)逡逑點(diǎn)用于描述指定數(shù)量的結(jié)構(gòu)節(jié)點(diǎn)的折疊，顯示為灰底實(shí)線矩形，其中ｅ為描述數(shù)逡逑量的表達(dá)式，ａ為關(guān)于ｅ的約束斷言，引入濃縮節(jié)點(diǎn)主要用以簡化形狀圖的表述逡逑（如減少節(jié)點(diǎn)的數(shù)量）并提升其抽象表述能力；謂詞節(jié)點(diǎn)用于指代具備特定謂詞逡逑性質(zhì)的內(nèi)存塊

限制程序能夠使用的易變數(shù)據(jù)結(jié)構(gòu)種類及相關(guān)操作的目的，當(dāng)前的形狀系統(tǒng)能逡逑夠支持５種形狀類別：單向鏈表、循環(huán)單向鏈表、雙向鏈表、循環(huán)雙向鏈表和二逡逑叉樹。形狀系統(tǒng)演算操作的主要對象即形狀圖，實(shí)現(xiàn)中通過如圖２．５所示的類繼逡逑承體系完成對于不同節(jié)點(diǎn)的表述，其中ＢａｓｅＮｏｄｅ是所有節(jié)點(diǎn)的抽象基類，包含逡逑適用于所有節(jié)點(diǎn)類型的操作接口，ＣｏｎｄｅｎｓｅＮｏｄｅ則是繼承自ＳｔｒｕｃｔＮｏｄｅ，其在后逡逑者的基礎(chǔ)上，還包含與長度信息相關(guān)的成員變量。逡逑ＢａｓｅＮｏｄｅ逡逑邐邐邐邋ｉ邐１逡逑Ｔ邐丨ＤｅｃＫＮｏｄｅ：聲明節(jié)點(diǎn)逡逑邐Ｉ邐１邐１邐｜邋ＳｔｍｃｔＮｏｄｅ：結(jié)構(gòu)節(jié)點(diǎn)邋；逡逑ＤｅｃｉＮｏｄｅ邐ＳｔｍｃｔＮｏｄｅ邐ＤａｎｇｌｉｕｇＮｏｄｅ邋｜邋Ｃ°ｎｄｅｉｉｓｅＮｏｄｅ：濃縮＂ｐ邋點(diǎn)邋｜逡逑邐邋邐邋邐！邋ＰｒｅｄｉｃａｔｅＮｏｄｅ：謂詞節(jié)點(diǎn)邐｜逡逑Ｓ邐＊ＮｕｌｌＮｏｄｅ：邋ＮＵＬＬ節(jié)點(diǎn)逡逑邐Ｊ邐邐邐１邐．Ｉ邐邐邋；ＤａｉｉｇｌｉｎｇＮｏｄｅ：懸空節(jié)點(diǎn)邋｜逡逑ＰｒｅｄｉｃａｔｅＮｏｄｅ邋ＣｏｎｄｅｎｓｅＮｏｄｅ邋ＮｕｌｌＮｏｄｅ邐！逡逑圖２．５形狀圖節(jié)點(diǎn)的類繼承體系逡逑原型形狀系統(tǒng)初步實(shí)現(xiàn)了形狀圖邏輯中所述的除函數(shù)調(diào)用之外的演算規(guī)則，逡逑但在實(shí)現(xiàn)層面上對于系統(tǒng)的子模塊并未作出明確的劃分。本研宄在實(shí)現(xiàn)過程中逡逑對形狀系統(tǒng)的實(shí)現(xiàn)做了重構(gòu)

【參考文獻(xiàn)】

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

1 宋艷輝;李兆鵬;陳意云;;指針類型遞歸函數(shù)前后形狀圖的自動(dòng)推斷[J];小型微型計(jì)算機(jī)系統(tǒng);2014年04期

2 李兆鵬;張昱;陳意云;;A Shape Graph Logic and A Shape System[J];Journal of Computer Science & Technology;2013年06期

3 張志天;李兆鵬;陳意云;劉剛;;一個(gè)程序驗(yàn)證器的設(shè)計(jì)和實(shí)現(xiàn)[J];計(jì)算機(jī)研究與發(fā)展;2013年05期

4 劉剛;陳意云;張志天;;循環(huán)不變形狀圖的自動(dòng)推斷[J];電子技術(shù);2011年08期

5 單錦輝,姜瑛,孫萍;軟件測試研究進(jìn)展[J];北京大學(xué)學(xué)報(bào)(自然科學(xué)版);2005年01期

6 陳火旺,王戟,董威;高可信軟件工程技術(shù)[J];電子學(xué)報(bào);2003年S1期

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

1 楊晨;安全C語言的驗(yàn)證條件證明器的設(shè)計(jì)與實(shí)現(xiàn)[D];中國科學(xué)技術(shù)大學(xué);2017年

2 李為勝;安全C語言的設(shè)計(jì)與實(shí)現(xiàn)[D];中國科學(xué)技術(shù)大學(xué);2016年

3 李云龍;安全C語言形狀系統(tǒng)的設(shè)計(jì)與實(shí)現(xiàn)[D];中國科學(xué)技術(shù)大學(xué);2016年

4 馮峰;安全C語言的驗(yàn)證條件生成器的設(shè)計(jì)與實(shí)現(xiàn)[D];中國科學(xué)技術(shù)大學(xué);2016年

本文編號：2734670