支持用戶自定義謂詞的自動定理證明的研究.pdf

1、隨著計算機學(xué)科的迅猛發(fā)展，計算機軟件正逐漸演化成為人們學(xué)習(xí)生活中的一個龐大的體系。另一方面，軟件的安全形勢非常嚴(yán)峻，尤其隨著移動計算的日益普及，對未受信源提供代碼的安全執(zhí)行問題也慢慢浮現(xiàn)出來。軟件的安全性成為關(guān)注的重點，在軟件安全性的研究中，軟件滿足特定安全策略的證明方法是目前國內(nèi)外研究的熱點之一。
　　 出具證明編譯器是軟件安全的一個重要研究方向，程序員在源碼上添加其屬性描述形成程序規(guī)范，驗證條件生成器對程序規(guī)范推理演算生成驗

2、證條件，接著由自動定理證明器對驗證條件求解并生成證明，最后將編譯器將生成的可執(zhí)行文件與證明并輸出，代碼消費方可以使用自己信任的證明檢查器來檢查該證明的正確性。不難發(fā)現(xiàn)，自動定理證明器在出具證明編譯器內(nèi)部發(fā)揮了非常重要的作用。
　　 CComp是我們實驗室先前的一個研究項目，是一個能證明部分指針程序正確性的出具證明編譯器。在先前工作的基礎(chǔ)上，本文在其源級做了擴展，通過添加自定義謂詞機制來增強斷言語言的表達(dá)能力。用戶通過定義一些謂詞

3、來幫助描述程序的歸納性質(zhì)，并且通過提供這些謂詞所滿足性質(zhì)的等式，來支持出具證明編譯器自動完成這些程序性質(zhì)的證明。這意味著出具證明編譯器可以證明的性質(zhì)將更加豐富靈活。
　　 本文的研究內(nèi)容主要有：為添加的自定義謂詞機制重新設(shè)計斷言語言，要求斷言語言是基于分離邏輯設(shè)計的，并且為項目組所設(shè)計的出具證明編譯器補充設(shè)計并實現(xiàn)一個自動定理證明器，以支持自定義謂詞。本文的貢獻(xiàn)是解決了如何利用用戶提供的謂詞定義及相關(guān)引理，依據(jù)特定的推理規(guī)則，形

4、成自動定理證明算法的問題。
　　 本文首先介紹了本課題的研究背景和研究現(xiàn)狀，接著簡單介紹了本課題的項目基礎(chǔ)CComp及其流程。本文接著介紹了源級框架下的程序規(guī)范，驗證條件生成器依據(jù)程序語義對程序推理生成驗證條件，斷言語言上的推理規(guī)則，支持自定義謂詞及相關(guān)引理的自動定理證明器等。最后介紹了兩個證明實例和總結(jié)。
　　 本文工作的意義在于，通過對支持用戶自定義謂詞的出具證明編譯器中自動定理證明搜索策略的探索研究，擴展了出具證明