出具證明編譯器中驗證條件化簡和編譯優(yōu)化的研究.pdf

1、程序驗證用邏輯證明的方法證明程序滿足其規(guī)范，是實現(xiàn)安全性的重要方法。出具證明編譯器(Certifying Compiler)是編譯器與驗證器的結(jié)合。本文描述的出具證明編譯器項目CComp讓用戶給出描述程序正確性的規(guī)范，并在源代碼使用霍爾邏輯風(fēng)格的推理規(guī)則產(chǎn)生驗證條件(Verification Condition，VC)，經(jīng)由證明器證明后產(chǎn)生證明項。然后將源代碼和規(guī)范轉(zhuǎn)化成底層的匯編代碼和其上的規(guī)范，并利用源級證明項生成匯編代碼級證明，最

2、終生成攜帶證明代碼。
　　 CComp由多人協(xié)作完成，本人承擔(dān)項目中的斷言語言設(shè)計以及驗證條件生成和化簡工作。實驗室先前的項目PointerC[4]，過大的驗證條件規(guī)模成為系統(tǒng)性能的瓶頸。因此CComp采用一系列的措施來化簡VC，刪除其中的冗余。
　　 實用的編譯器會包含眾多優(yōu)化，以提高程序執(zhí)行的效率。編譯優(yōu)化是一系列程序變換，對于出具證明編譯中包含規(guī)范的程序，變換前的程序的規(guī)范可能無法正確或充分地描述變換后的程序，為

3、此程序規(guī)范也應(yīng)該隨著代碼優(yōu)化一起轉(zhuǎn)換。目前關(guān)于出具證明編譯器的項目較少研究編譯優(yōu)化的影響，但編譯優(yōu)化是決定出具證明編譯器是否能走向應(yīng)用的關(guān)鍵因素之一。
　　 本文通過分析研究，針對以上兩個重要問題分別提出了相應(yīng)的解決方案，并實現(xiàn)了原型系統(tǒng)驗證方法的合理性。本文的主要貢獻為：
　　 1.為CComp項目設(shè)計了使用分離邏輯描述的斷言語言和其推理規(guī)則，實現(xiàn)了相應(yīng)的驗證條件生成器；設(shè)計并實現(xiàn)了一個重寫系統(tǒng)，實現(xiàn)了驗證條件的化簡，