一種出具證明編譯器中匯編級(jí)斷言和證明的生成方法.pdf

1、隨著計(jì)算機(jī)科學(xué)的迅速發(fā)展，軟件規(guī)模日益龐大?，F(xiàn)在人們在考慮軟件執(zhí)行效率的同時(shí)，也越來越關(guān)注其安全性(Safety)。高可信軟件的研究致力于使用前沿的技術(shù)和工具來提高計(jì)算機(jī)軟件的安全性。程序驗(yàn)證是一種構(gòu)建高可信軟件的方法，它的原理是使用數(shù)學(xué)方法來嚴(yán)格證明程序行為符合其預(yù)定規(guī)范，從而保證程序的安全性。程序驗(yàn)證可以對(duì)源代碼進(jìn)行，也可以對(duì)匯編代碼進(jìn)行。源代碼級(jí)別的驗(yàn)證更易于程序員的理解和參與，但是由于普通編譯器的低可靠性，編譯器不能保證由經(jīng)過驗(yàn)

2、證的源代碼(Certified Source Code)生成的匯編代碼仍然滿足預(yù)定的安全規(guī)范。匯編級(jí)別的驗(yàn)證雖然能保證生成的匯編代碼的安全性，但是如果是手工編寫匯編代碼、書寫斷言、交互式完成證明，則代價(jià)過高，開發(fā)效率低。因此一種比較理想的方法是在源代碼級(jí)別進(jìn)行驗(yàn)證，然后通過出具證明編譯器(Certifying Compiler)自動(dòng)生成經(jīng)過驗(yàn)證的匯編代碼。
　　 本文首先介紹了國內(nèi)外基于程序性質(zhì)證明的軟件安全的相關(guān)研究以及出具

3、證明編譯的研究，然后介紹筆者所參與的項(xiàng)目CComp的整體框架模型：CComp是一個(gè)類C語言的出具證明編譯器原型，它在將帶有規(guī)范標(biāo)注的源代碼編譯成匯編代碼的同時(shí)，還能產(chǎn)生匯編代碼滿足相應(yīng)規(guī)范的Coq可檢查證明，從而保證匯編代碼的安全性。
　　 該出具證明編譯器包括：編譯器前端、源級(jí)驗(yàn)證條件生成器、源級(jí)自動(dòng)定理證明器、匯編代碼生成器、匯編級(jí)斷言生成器、匯編級(jí)證明生成器以及匯編級(jí)驗(yàn)證框架。本文的主要工作集中在后而三個(gè)部分，主要研究如何