使用顯式控制流語言驗(yàn)證匯編程序的方法.pdf

1、隨著程序員和用戶對計(jì)算機(jī)系統(tǒng)軟件和可執(zhí)行程序安全性和正確性的要求不斷提高，程序驗(yàn)證以其可靠而高精確的驗(yàn)證結(jié)果，在計(jì)算機(jī)領(lǐng)域已經(jīng)越來越受歡迎。驗(yàn)證一個(gè)程序具體是指使用正規(guī)的數(shù)學(xué)方法，證明該段程序滿足特定的由其規(guī)范描述的屬性。近年來，為了使得被驗(yàn)證程序的正確性不依賴于龐大復(fù)雜的編譯器的正確性，越來越多的程序驗(yàn)證工作選擇直接在機(jī)器語言或者匯編語言上進(jìn)行。
　　 然而，驗(yàn)證匯編程序具有很大的困難，因?yàn)閰R編語言不具備高級語言中的非常清晰的

2、抽象機(jī)制的結(jié)構(gòu)(如循環(huán)體結(jié)構(gòu)、函數(shù)結(jié)構(gòu)等)，來幫助程序的理解和驗(yàn)證。在匯編語言中，僅有的結(jié)構(gòu)為由一連串順序指令組成以跳轉(zhuǎn)指令結(jié)尾的程序代碼的基本塊。因?yàn)槿狈Y(jié)構(gòu)化的抽象機(jī)制，為了能夠一致地驗(yàn)證各種抽象機(jī)制，已有的匯編語言級程序驗(yàn)證系統(tǒng)只能選擇忽略所有的抽象機(jī)制，使用基本塊作為驗(yàn)證的基本單元，將所有的程序代碼都以延續(xù)傳遞風(fēng)格(Continuation Passing Style，簡稱CPS)來理解和驗(yàn)證。因?yàn)閷Τ绦蛑谐橄髾C(jī)制意義的破壞，C

3、PS風(fēng)格的驗(yàn)證系統(tǒng)很難能夠被用來驗(yàn)證大的軟件系統(tǒng)。另外，CPS邏輯驗(yàn)證系統(tǒng)一般僅能夠驗(yàn)證匯編程序的安全性，卻很難保證它們的部分正確性。
　　 本文提出了上述問題的解決方法，其主要內(nèi)容及貢獻(xiàn)包括：
　　 ·本文提出了一個(gè)驗(yàn)證匯編程序的新方法。該方法能夠直接在匯編級驗(yàn)證程序的部分正確性而不丟失對程序原有機(jī)制的理解。原有匯編級程序驗(yàn)證系統(tǒng)的程序驗(yàn)證步驟為：首先直接在匯編程序?qū)嶋H代碼上為每個(gè)基本塊提供規(guī)范，之后使用系統(tǒng)的推理規(guī)則

4、進(jìn)行驗(yàn)證。在本文的提出的方法中，我們引入顯式控制流語言CFEL(Control-Flow-Explicit Langtrage的簡寫)這個(gè)介于程序規(guī)范和匯編程序?qū)嶋H代碼之間的輔助結(jié)構(gòu)。顧名思義，我們使用CFEL來描述程序的控制流，并在驗(yàn)證時(shí)使用控制流來代表程序本身。CFEL結(jié)構(gòu)簡單卻具有強(qiáng)大的表達(dá)力，能夠描述包括函數(shù)調(diào)用和返回、異常處理、嵌入代碼指針、自修改代碼等各種程序機(jī)制的控制流。在一個(gè)程序?qū)嶋H被驗(yàn)證前，我們首先通過使用CFEL描述

5、各段程序的控制流來輔助程序的驗(yàn)證。而驗(yàn)證所需要的規(guī)范將會(huì)直接提供給CFEL描述的控制流段。
　　 ·在CFEL的基礎(chǔ)上，我們提供的一套結(jié)構(gòu)簡單、模塊化并且適用性廣的具體驗(yàn)證系統(tǒng)TCAP(Trail-Based Certifying Assembly Programming的簡寫)。TCAP的推理規(guī)則用來保證CFEL描述的各個(gè)控制流塊確實(shí)是實(shí)際程序的正確控制流，并且各個(gè)控制流塊的執(zhí)行特性滿足所提供的規(guī)范。帶有各種不同程序抽象機(jī)制的

6、匯編程序可以在TCAP這一個(gè)驗(yàn)證系統(tǒng)中驗(yàn)證，不需要使用不同系統(tǒng)對各個(gè)不同的抽象機(jī)制進(jìn)行驗(yàn)證后將證明想辦法鏈接在一起。因?yàn)镃FEL已經(jīng)描述了程序的控制流信息，TCAP中的規(guī)范以及規(guī)則都相對簡單和易用。本文還提供一些使用TCAP來驗(yàn)證具有各種抽象機(jī)制的實(shí)際程序的例子。
　　 ·本文為TCAP提供了一套基于步指標(biāo)的語義模型。其中步指標(biāo)指的是程序關(guān)心的需要保證安全的程序執(zhí)行步數(shù)。為一套支持多重程序抽象機(jī)制的驗(yàn)證系統(tǒng)提供語義模型是相當(dāng)困難

7、的工作，很多匯編級驗(yàn)證系統(tǒng)也因此選擇使用語法的方法來證明其可靠性。語義模型為驗(yàn)證系統(tǒng)的推理規(guī)則定義具體的意義，從而使得系統(tǒng)更易擴(kuò)展。另外，相比于語法方法，語義方法的模塊性和泛型性也是其非常重要的優(yōu)勢之一，為驗(yàn)證系統(tǒng)提供一個(gè)簡單易懂的語義模型已經(jīng)成為計(jì)算機(jī)理論中很多重要研究工作的主要內(nèi)容。本文中提供的語義模型簡單易懂卻不失強(qiáng)大的表達(dá)力。整個(gè)語義模型基于簡單而直觀的帶有步指標(biāo)的操作語義而不需要任何復(fù)雜理論，卻可以解釋支持包括嵌入代碼指針在內(nèi)