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

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

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

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

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

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

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

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