基于攜帶證明的代碼的垃圾收集過程驗證.pdf

1、使用Java和C＃等安全的程序設(shè)計語言編寫的程序能夠完全避免一些在傳統(tǒng)程序設(shè)計語言編寫的程序中經(jīng)常出現(xiàn)的安全漏洞，從而提高軟件的可靠性。然而，這類安全語言的眾多安全特性都依賴于其運行環(huán)境，特別是垃圾收集機(jī)制的正確性和安全性。不幸的是，垃圾收集算法通常難于設(shè)計和正確地實現(xiàn)。同時，垃圾收集器和用戶程序的交互過程也往往相當(dāng)復(fù)雜而易出錯。因此，為了提高使用垃圾收集機(jī)制的程序設(shè)計語言的安全性和可靠性，勢必需要對垃圾收集過程的安全性和正確性進(jìn)行嚴(yán)格

2、的研究。 本文工作使用基于Hoare邏輯的匯編語言級形式程序驗證框架，對垃圾收集器的安全性和正確性，以及垃圾收集器與多種用戶程序，特別是類型化匯編語言的交互過程的安全性進(jìn)行了嚴(yán)格的形式驗證。本文工作基于攜帶證明的代碼技術(shù)，所有的驗證都在計算機(jī)輔助定理證明工具COQ中實現(xiàn)為計算機(jī)可檢查的證明。這樣，垃圾收集器和用戶程序就能夠被構(gòu)造為一個完整的攜帶安全性證明的軟件包，方便地通過互聯(lián)網(wǎng)和其他渠道進(jìn)行發(fā)布。 第一部分工作驗證了兩

3、種典型垃圾收集器的匯編語言實現(xiàn)。該工作使用分離邏輯風(fēng)格的代碼規(guī)范語言給出了停止式標(biāo)記-清掃垃圾收集器和基于初始快照的Yuasa漸進(jìn)式垃圾收集器的安全規(guī)范，并使用Hoare風(fēng)格的程序邏輯和推理方法證明了垃圾收集器滿足其安全規(guī)范。 第二部分工作從單獨驗證垃圾收集器工作存在的不足出發(fā)，提出并實現(xiàn)了一種通用的驗證垃圾收集器和用戶程序交互過程的方法。其核心思想是使用類似抽象數(shù)據(jù)類型的技術(shù)將垃圾收集器對用戶程序的接口及其驗證抽象起來，使得用

4、戶程序的驗證無需再關(guān)心垃圾收集器的具體實現(xiàn)，并方便用戶程序驗證和垃圾收集器驗證的鏈接。 最后一部分工作研究了類型安全的垃圾收集過程。給出了一種為基礎(chǔ)的類型化匯編語言提供驗證的垃圾收集過程的方法，它基于一個開放式的匯編語言級程序邏輯，并使用了第二部分工作的主要思想，將垃圾收集器的細(xì)節(jié)從類型化匯編語言的類型系統(tǒng)中抽象出去，簡化了類型化匯編語言的設(shè)計。 同時，本文還討論了這些工作在計算機(jī)輔助定理證明工具CoQ中的實現(xiàn)，以及在這

5、些實現(xiàn)中設(shè)計和發(fā)展的一些提高證明效率的方法和技術(shù)。本文工作的主要貢獻(xiàn)和創(chuàng)新包括：1)基于匯編語言層次的一個攜帶證明程序的驗證框架，首次成功地驗證了多種垃圾收集算法的匯編級實現(xiàn)代碼，以及它們和用戶程序的交互過程；2)提出了一種基于抽象數(shù)據(jù)類型技術(shù)的通用方法，能夠?qū)占?、用戶程序以及它們的交互過程進(jìn)行簡潔且嚴(yán)格的驗證；3)首次成功地解決了在最小被信任計算基礎(chǔ)的前提下為類型化匯編語言提供類型安全的垃圾收集過程這一熱點研究問題；4)基于分

6、離邏輯技術(shù)，首次成功地從單個內(nèi)存單元開始構(gòu)造了標(biāo)記一清掃式垃圾收集器的具體內(nèi)存規(guī)范。 這些研究工作對減小安全程序設(shè)計語言的被信任計算基礎(chǔ)進(jìn)行了有益的嘗試一一使用形式程序驗證技術(shù)，攜帶基礎(chǔ)證明的垃圾收集過程就可以被排除出安全程序設(shè)計語言的被信任計算基礎(chǔ)。同時，它們也為匯編語言級程序的形式驗證，特別是為攜帶證明的代碼的技術(shù)的應(yīng)用積累了重要的理論和實踐經(jīng)驗。而隨著這類技術(shù)的進(jìn)步，更多被信任的軟件就可以經(jīng)過驗證而被排除出系統(tǒng)的被信任計算