基于攜帶證明的代碼的垃圾收集過程驗(yàn)證.pdf

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

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

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

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

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

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