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

1、隨著軟件逐漸被應(yīng)用到國(guó)家、社會(huì)的更廣、更深的領(lǐng)域中，隨之而來的軟件安全性問題也不容忽視。重要領(lǐng)域、行業(yè)的關(guān)鍵軟件的安全性問題尤為迫切，關(guān)鍵軟件的安全漏洞讓國(guó)家和社會(huì)蒙受了巨大的損失?，F(xiàn)有的保證軟件安全的方法主要依靠軟件測(cè)試，這種方法只能保證經(jīng)測(cè)試的特定情狀不出錯(cuò)，未經(jīng)測(cè)試的或者無法測(cè)試的情況下的行為往往不可知。通過形式化程序的性質(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語言，它保留了C語言的動(dòng)態(tài)存儲(chǔ)管理的特性，便于我們研究存儲(chǔ)安全方面的隱患：同時(shí)我們?cè)O(shè)計(jì)了一種斷言語言方便程序員書寫安全規(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à)的謂詞，且指針斷言中的指針變量可以用整型斷言中的變量來精確地描述其在堆中的偏移，能夠描述更復(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)證明通過計(jì)算滿足同種性質(zhì)的指針的閉包集合是否等價(jià)來證

5、明指針蘊(yùn)含斷言的前后件是否等價(jià)，從而得到指針斷言的證明。此外我們還設(shè)計(jì)實(shí)現(xiàn)了一個(gè)定理檢查器，它從文件中讀取我們產(chǎn)生的攜證明代碼，經(jīng)詞法、語法分析無誤的程序，進(jìn)一步較驗(yàn)其證明和代碼的合法性。這樣我們不但提供了一種對(duì)產(chǎn)生的攜證明代碼機(jī)器自動(dòng)檢查的方法，還將編譯器模塊排除出信任基礎(chǔ)，增強(qiáng)了系統(tǒng)的可信性。同時(shí)我們通過代表性的示例程序?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è)新