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

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

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

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

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

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

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

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

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