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

1、現(xiàn)今計算機和互聯(lián)網(wǎng)技術(shù)的迅速發(fā)展不僅帶來了具有更強計算能力的計算機、更加便捷的信息交流方式，而且也對計算機軟件的安全性和可靠性提出了更高的要求。目前軟件安全性的保證主要是依靠程序設(shè)計者自身的能力以及軟件測試。在軟件開發(fā)過程中使用形式化方法進行程序驗證是提高軟件安全性的一個有效途徑。 出具證明編譯器是近些年來結(jié)合程序設(shè)計和程序驗證技術(shù)所出現(xiàn)的研究方向。作為驗證編譯研究的一個分支，出具證明編譯器的主要設(shè)計思想是整個系統(tǒng)能夠在編譯獲得

2、目標代碼的同時也為這些目標代碼生成用于說明目標代碼滿足某些程序性質(zhì)的證明。 本文所介紹的工作基于我們的出具證明編譯器原型系統(tǒng)項目，是我們進行出具證明編譯研究的一次嘗試。原型系統(tǒng)的設(shè)計和實現(xiàn)主要涉及到編譯器技術(shù)、基于Hoare邏輯的程序驗證技術(shù)等。此外，為了更好地考察與動態(tài)存儲管理相關(guān)的程序性質(zhì)，我們不僅在源語言的設(shè)計中保留了指針類型以及動態(tài)存儲管理的語句，而且也設(shè)計了指針邏輯。 本文重點介紹了出具證明編譯器原型系統(tǒng)中主要

3、功能模塊的實現(xiàn)，這些模塊包括位于原型系統(tǒng)前端的驗證條件生成器，位于后端的代碼生成器和證明生成器。文中不僅描述了這些模塊所使用的數(shù)據(jù)結(jié)構(gòu)的設(shè)計以及它們各自的工作流程，而且也對設(shè)計和實現(xiàn)這些模塊的過程中的經(jīng)驗進行了總結(jié)。同時，由于目標代碼級程序性質(zhì)證明框架的實現(xiàn)使用了定理證明輔助工具Coq，因此原型系統(tǒng)在設(shè)計和實現(xiàn)的過程中也加入了與Coq系統(tǒng)接口問題的考慮。 通過整個原型系統(tǒng)的構(gòu)建，我們初步解決了出具證明編譯中的若干問題，特別是源語