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

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

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

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

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

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