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

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

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

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