指針邏輯的擴(kuò)展與應(yīng)用.pdf

1、在信息時(shí)代，計(jì)算機(jī)軟件技術(shù)得到了廣泛的應(yīng)用。然而，隨著軟件功能越來越強(qiáng)大，軟件本身也變得愈發(fā)復(fù)雜，軟件的可靠性和安全性越來越難以得到保障。在通常使用的C，C++或者Java語言中，為了使程序能夠高效運(yùn)行，指針或者引用在程序中大量使用。但是指針的靈活使用很容易引起錯(cuò)誤，比如空指針或者懸空指針引用，內(nèi)存泄露等。這些錯(cuò)誤不僅難以發(fā)現(xiàn)，如果一旦發(fā)生可能導(dǎo)致系統(tǒng)崩潰。而且，這些程序漏洞可能被黑客加以利用。另一方面，指針錯(cuò)誤之所以難以被發(fā)現(xiàn)，是因?yàn)?/p>

2、不同指針之間存在可能的別名關(guān)系，即是兩個(gè)語法上不同的名字在運(yùn)行的時(shí)候可能引用同一個(gè)內(nèi)存地址。修改一個(gè)名字對(duì)應(yīng)的值，別的名字所對(duì)應(yīng)的值可能也會(huì)隨之改變，給程序調(diào)試和程序推理帶來很大的困難。因此，帶有指針程序的安全性在軟件安全研究中占有重要位置。 由于指針程序安全研究具有很大的挑戰(zhàn)性，工業(yè)界常用的軟件測(cè)試方法無法完全保證錯(cuò)誤不會(huì)發(fā)生，因而指針程序性質(zhì)證明方法成為當(dāng)前研究熱點(diǎn)。而現(xiàn)有的證明方法，要么需要顯式引入堆或棧等高級(jí)語言語法之外

3、的概念來刻畫程序的運(yùn)行狀態(tài)，要么生成的驗(yàn)證條件太過于復(fù)雜而不能夠自動(dòng)證明，而需要程序員手工證明。堆和棧的描述需要知道確切的內(nèi)存地址，但是具有同構(gòu)結(jié)構(gòu)的堆是不可以區(qū)分的。而無存儲(chǔ)模型方法則克服了上述所有困難，不需要顯式引入堆棧概念，而其良好性質(zhì)保證可以被自動(dòng)機(jī)實(shí)現(xiàn)，因而證明可以自動(dòng)。指針邏輯在本質(zhì)上是基于無存儲(chǔ)模型方法，但是當(dāng)前還具有很多不足。當(dāng)前指針邏輯缺少抽象模型描述，導(dǎo)致了指針邏輯規(guī)則都是由算法風(fēng)格函數(shù)輔助構(gòu)成，這使得難以看清楚指針

4、邏輯本質(zhì)。而且，當(dāng)前指針邏輯支持的指針特征較少，雖然斷言語言支持符號(hào)訪問路徑，用戶自定義謂詞和描述性謂詞，但是其實(shí)現(xiàn)PLCC(V1)(Pointer Logic Certifying Compiler，簡(jiǎn)稱為PLCC，V1表示Version1，后面的V2表示Version2)的推理并不支持。最重要的是，PLCC(V1)生成的驗(yàn)證條件并不能自動(dòng)證明，而需要程序員通過交互式定理證明器COQ來完成證明。 基于上述考慮，本文在訪問路徑相

5、等概念上提出一個(gè)無存儲(chǔ)模型，研究了該模型的各種性質(zhì)，例如右規(guī)則性，前綴閉包性等。同時(shí)，本文專注于無存儲(chǔ)模型上的指針邏輯斷言的良型性，繼而重新闡述了指針邏輯推理規(guī)則。為了使指針邏輯能夠驗(yàn)證更大范圍的程序，本文提出了針對(duì)指針邏輯的框架規(guī)則(frame rule)和函數(shù)調(diào)用規(guī)則。此外，本文在原有指針邏輯基礎(chǔ)上，擴(kuò)展源語言和斷言語言來支持指針?biāo)阈g(shù)，然后在方便模塊化實(shí)現(xiàn)前提下擴(kuò)展指針邏輯規(guī)則來保障指針?biāo)阈g(shù)的安全。原來指針邏輯中的集合是無名集合，而

6、無名集合不能處理含有某些情況下的函數(shù)調(diào)用的程序，因而本文提出帶標(biāo)簽的集合可以適用于任意函數(shù)調(diào)用的驗(yàn)證。在實(shí)現(xiàn)方面，本文根據(jù)無存儲(chǔ)模型性質(zhì)設(shè)計(jì)了實(shí)現(xiàn)指針邏輯規(guī)則的自動(dòng)推理算法，并提出了展開機(jī)制來處理斷言語言支持用戶自定義謂詞和描述性謂詞。最后，本文工作均在PLCC(V2)的前端中實(shí)現(xiàn)。 本文的主要特色和貢獻(xiàn)為： ·本文提出了一個(gè)比已存在無存儲(chǔ)模型更有效更簡(jiǎn)潔的無存儲(chǔ)模型。此模型不僅繼承了已存在無存儲(chǔ)模型的優(yōu)點(diǎn)，而且克服了其

7、冗余多，表示代價(jià)高的缺點(diǎn)。 ·本文完善了指針邏輯，在抽象模型上以一種簡(jiǎn)單更為容易理解的方式重新闡述指針邏輯推理規(guī)則。由于抽象模型沒有傳統(tǒng)無存儲(chǔ)模型的冗余，花費(fèi)代價(jià)大等缺點(diǎn)，因而本文可以發(fā)現(xiàn)以前指針邏輯(Chen et al．，2007a，b)規(guī)則中具有一個(gè)漏洞：以前指針邏輯所定義的no_leak函數(shù)在某些時(shí)候會(huì)將某些正確程序誤認(rèn)為會(huì)出現(xiàn)內(nèi)存錯(cuò)誤而拒絕。本文給出修正此漏洞的規(guī)則，同時(shí)這也反映了建立抽象模型的必要性，因?yàn)橐郧暗闹羔樳?/p>

8、輯規(guī)則是基于一些復(fù)雜的算法風(fēng)格的輔助函數(shù)，并且導(dǎo)致難以看清楚指針邏輯的本質(zhì)。 ·本文擴(kuò)展了指針邏輯。相比擴(kuò)展前的指針邏輯，本文擴(kuò)展了指針邏輯在局部推理的規(guī)則、擴(kuò)展支持在動(dòng)態(tài)數(shù)組上的指針?biāo)阈g(shù)以及利用帶標(biāo)簽的集合來驗(yàn)證任意函數(shù)調(diào)用的擴(kuò)展，這樣指針邏輯就能夠在更大范圍內(nèi)保障程序的安全。 ·本文設(shè)計(jì)了實(shí)現(xiàn)指針邏輯規(guī)則的算法和提出了展開技術(shù)來實(shí)現(xiàn)謂詞推理自動(dòng)化，并將其應(yīng)用到自動(dòng)驗(yàn)證工具PLCC(V2)前端實(shí)現(xiàn)上。相比PLCC(V1