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

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

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

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

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

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