一個(gè)出具證明編譯器系統(tǒng)的設(shè)計(jì)與實(shí)現(xiàn).pdf

1、隨著軟件逐漸被應(yīng)用到國(guó)家、社會(huì)的更廣、更深的領(lǐng)域中，隨之而來(lái)的軟件安全性問(wèn)題也不容忽視。重要領(lǐng)域、行業(yè)的關(guān)鍵軟件的安全性問(wèn)題尤為迫切，關(guān)鍵軟件的安全漏洞讓國(guó)家和社會(huì)蒙受了巨大的損失。現(xiàn)有的保證軟件安全的方法主要依靠軟件測(cè)試，這種方法只能保證經(jīng)測(cè)試的特定情狀不出錯(cuò)，未經(jīng)測(cè)試的或者無(wú)法測(cè)試的情況下的行為往往不可知。通過(guò)形式化程序的性質(zhì)，并給出形式化證明的方法，被稱之為形式化程序驗(yàn)證，這種方法是提高軟件安全性的一個(gè)有效途徑，且前人已經(jīng)取得了豐

2、碩的成果。 程序驗(yàn)證方法能夠從理論上保證軟件不發(fā)生程序中禁止的錯(cuò)誤，而出具證明編譯器技術(shù)結(jié)合了編譯器技術(shù)和程序驗(yàn)證方法，它作為驗(yàn)證編譯器的一個(gè)重要分支，在生成目標(biāo)代碼同時(shí)，給出目標(biāo)代碼對(duì)應(yīng)的安全證明。出具證明編譯器的出現(xiàn)降低了形式化程序驗(yàn)證的開銷，它能夠(半)自動(dòng)地給出形式化的證明。 本實(shí)驗(yàn)室前期也完成了一個(gè)出具證明編譯器的原型系統(tǒng)，但它不能夠自動(dòng)產(chǎn)生證明，這個(gè)缺陷極大的制約了其功用性和實(shí)用性，因此我們?cè)谖∏捌谠拖到y(tǒng)

3、的經(jīng)驗(yàn)后，重新設(shè)計(jì)的一個(gè)出具證明的編譯器。新的編譯器處理一個(gè)類C的PointerC語(yǔ)言，它保留了C語(yǔ)言的動(dòng)態(tài)存儲(chǔ)管理的特性，便于我們研究存儲(chǔ)安全方面的隱患：同時(shí)我們?cè)O(shè)計(jì)了一種斷言語(yǔ)言方便程序員書寫安全規(guī)范。出具證明的編譯器除了完成傳統(tǒng)的代碼編譯和代碼發(fā)射外，還將源級(jí)的安全規(guī)范翻譯到目標(biāo)級(jí)。在目標(biāo)級(jí)包含一個(gè)驗(yàn)證系統(tǒng)，該驗(yàn)證系統(tǒng)中的驗(yàn)證條件產(chǎn)生器根據(jù)翻譯得到的安全規(guī)范，生成程序?qū)?yīng)的驗(yàn)證條件，驗(yàn)證條件包括整型斷言和指針斷言兩類：其中整型斷言

4、是機(jī)器模型上變量值的約束關(guān)系謂詞，指針斷言是關(guān)于指針表示信息是否等價(jià)的謂詞，且指針斷言中的指針變量可以用整型斷言中的變量來(lái)精確地描述其在堆中的偏移，能夠描述更復(fù)雜的性質(zhì)。目標(biāo)級(jí)驗(yàn)證系統(tǒng)中還包括一個(gè)定理證明器，它能夠自動(dòng)地產(chǎn)生兩種驗(yàn)證條件的證明：整型斷言的自動(dòng)證明主要借助于一個(gè)整數(shù)謂詞自動(dòng)證明算法和一個(gè)將目標(biāo)機(jī)器模型上的寄存器變量、棧變量和堆變量范化成一種符號(hào)化變?cè)乃惴ǎ恢羔様嘌缘淖詣?dòng)證明通過(guò)計(jì)算滿足同種性質(zhì)的指針的閉包集合是否等價(jià)來(lái)證

5、明指針蘊(yùn)含斷言的前后件是否等價(jià)，從而得到指針斷言的證明。此外我們還設(shè)計(jì)實(shí)現(xiàn)了一個(gè)定理檢查器，它從文件中讀取我們產(chǎn)生的攜證明代碼，經(jīng)詞法、語(yǔ)法分析無(wú)誤的程序，進(jìn)一步較驗(yàn)其證明和代碼的合法性。這樣我們不但提供了一種對(duì)產(chǎn)生的攜證明代碼機(jī)器自動(dòng)檢查的方法，還將編譯器模塊排除出信任基礎(chǔ)，增強(qiáng)了系統(tǒng)的可信性。同時(shí)我們通過(guò)代表性的示例程序?qū)ο到y(tǒng)可用性進(jìn)行了實(shí)驗(yàn)評(píng)測(cè)，實(shí)驗(yàn)結(jié)果也在本文末尾給出。本文介紹的系統(tǒng)實(shí)現(xiàn)了一個(gè)可信計(jì)算框架，這是對(duì)程序驗(yàn)證的一個(gè)新