李業(yè)華，顧乃杰，張穎楠，彭 飛

(1.中國科學(xué)技術(shù)大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，合肥 230027；2.安徽省計(jì)算與通訊軟件重點(diǎn)實(shí)驗(yàn)室，合肥 230027；3.中國科學(xué)技術(shù)大學(xué)中國科學(xué)院沈陽計(jì)算技術(shù)研究所網(wǎng)絡(luò)與通信聯(lián)合實(shí)驗(yàn)室，合肥 230027)

1 概述

程序驗(yàn)證作為保證軟件正確性的一項(xiàng)重要技術(shù)得到了學(xué)術(shù)界的廣泛關(guān)注。研究人員在20世紀(jì)60年代便開始了有關(guān)程序驗(yàn)證理論和方法的研究，開發(fā)出很多針對特定軟件漏洞的檢測和驗(yàn)證工具[1-3]。運(yùn)行時驗(yàn)證技術(shù)驗(yàn)證軟件執(zhí)行路徑是否滿足一定的特征和規(guī)范，它比靜態(tài)驗(yàn)證更加貼近軟件系統(tǒng)的實(shí)現(xiàn)和執(zhí)行。這種方法觀察和驗(yàn)證的是軟件運(yùn)行時的行為，并不需要分析軟件所有可能的行為。所以運(yùn)行時驗(yàn)證的復(fù)雜度不會隨著軟件規(guī)模和復(fù)雜性的增加有顯著變化[1]。

本文提出一種運(yùn)行時程序驗(yàn)證框架RPA，以驗(yàn)證和分析運(yùn)行時程序的行為屬性，設(shè)計(jì)一門基于布爾邏輯的動態(tài)邏輯語言RPAL，以刻畫運(yùn)行時程序行為，還實(shí)現(xiàn)了該語言的虛擬機(jī)。RPA在虛擬機(jī)之上執(zhí)行用戶指定的感應(yīng)器安放，并收集運(yùn)行時程序狀態(tài)信息，執(zhí)行精確的屬性分析和驗(yàn)證。感應(yīng)器是程序狀態(tài)暴露代碼的形象表述，將使用程序插樁技術(shù)自動植入到目標(biāo)程序的執(zhí)行代碼中，完全免去為了分析軟件行為而手工添加狀態(tài)輸出代碼的工作。

Saturn[2,4-5]是由美國 Stanford大學(xué)開發(fā)的一個用于靜態(tài)檢查大型軟件系統(tǒng)屬性的項(xiàng)目。Saturn定義了一門邏輯語言 Calypso[5]來描述屬性約束集。該屬性約束集定義系統(tǒng)的特征和屬性。本文提出的RPAL語言參考了 Calypso語言的設(shè)計(jì)。但 RPAL在 Calypso的句子、謂詞和事實(shí)等語法元素基礎(chǔ)上擴(kuò)展了事實(shí)操作集，大大增強(qiáng)了事實(shí)管理模型。相比Calypso，RPAL是動態(tài)語言而不是符號語言，支持完整的類型系統(tǒng)和對象管理。因此分析程序的語義變得更加清晰，大大減少因?yàn)榉治龀绦虻念愋湾e誤導(dǎo)致的分析結(jié)果錯誤。

RPA使用獨(dú)立的事實(shí)倉庫管理驗(yàn)證過程中的中間和最終事實(shí)結(jié)論。事實(shí)倉庫建模為命名事實(shí)棧集合，支持比Saturn更靈活的事實(shí)管理操作。

Saturn中的分析以函數(shù)為基本分析單位，跨函數(shù)范圍的分析相對困難，需要借助函數(shù)總結(jié)來實(shí)現(xiàn)。RPA作為一個運(yùn)行時驗(yàn)證框架，可以使用簡單而通用的布爾邏輯直觀地定義軟件行為特性。

在分布式系統(tǒng)檢錯領(lǐng)域，Pip[6]、D3S[7]均定義一門系統(tǒng)描述語言以刻畫節(jié)點(diǎn)間的通信行為。MaceMC[3]是建立在Mace[8]分布式系統(tǒng)開發(fā)框架上的基于模型檢測的程序驗(yàn)證工具。同樣使用模型檢測技術(shù)的有MODIST[9]、CrystalBall[10]。另外，文獻(xiàn)[1]提出了一個面向切面程序的程序運(yùn)行時驗(yàn)證框架。該框架采用線性時序邏輯語言LTL[11]作為系統(tǒng)描述語言，不需要獨(dú)立的虛擬機(jī)支持。該框架只接受AspectJ程序，可以利用添加切面的方法把運(yùn)行時驗(yàn)證的任務(wù)以新切面的形式整合到目標(biāo)軟件中。而 RPA的驗(yàn)證面向可執(zhí)行的二進(jìn)制程序，比該框架更靈活，適用性更廣。

2 運(yùn)行時程序驗(yàn)證框架

RPA是一個用于驗(yàn)證和分析運(yùn)行時程序?qū)傩缘墓ぞ呖蚣?。完整的RPA系統(tǒng)包括RPA核心和RPAL擴(kuò)展。其中RPA核心包括RPAL語言、RPAL語言解析器和 RPA程序驗(yàn)證虛擬機(jī) 3個部分，而RPAL擴(kuò)展則包括各種擴(kuò)展謂詞庫。

2.1 基本驗(yàn)證流程

RPA定義了一門形式語言RPAL來描述運(yùn)行時軟件的行為和屬性。這樣的一個用RPAL語言表達(dá)的合法描述稱為運(yùn)行時軟件的規(guī)范，在實(shí)現(xiàn)上稱為RPAL分析程序。RPA運(yùn)行時程序驗(yàn)證的流程如圖1所示，RPA執(zhí)行的驗(yàn)證分析依賴于2個輸入：RPAL分析程序和運(yùn)行時程序的狀態(tài)信息。

圖1 RPA運(yùn)行時程序驗(yàn)證的流程

為了收集必需的運(yùn)行時狀態(tài)以支撐驗(yàn)證工作，RPA需要在系統(tǒng)分析之前利用插樁技術(shù)往目標(biāo)軟件植入狀態(tài)暴露的代碼。所以，RPA的整個分析過程分為2個階段：

(1)第1階段是感應(yīng)器安放階段，主要根據(jù)RPAL分析程序刻畫的程序?qū)傩詧?zhí)行程序插樁工作。插樁后的目標(biāo)軟件每一次執(zhí)行將會額外地輸出狀態(tài)信息記錄文件。

(2)在第 2階段，RPA會啟動目標(biāo)程序執(zhí)行，結(jié)束后把合法的RPAL分析程序和狀態(tài)信息記錄文件作為RPA虛擬機(jī)的輸入，啟動分析過程。

第2階段結(jié)束后，分析結(jié)論會輸出到外部文件。用戶使用RPA結(jié)論查看工具查看和分析驗(yàn)證結(jié)果。

2.2 系統(tǒng)框架

RPA核心實(shí)現(xiàn)包括RPAL解析器和RPA虛擬機(jī)。RPAL解析器負(fù)責(zé)分析RPAL分析程序的輸入，準(zhǔn)備好基本的驗(yàn)證環(huán)境。RPA虛擬機(jī)則在解析器準(zhǔn)備的驗(yàn)證環(huán)境基礎(chǔ)上執(zhí)行系統(tǒng)的驗(yàn)證分析工作。圖2給出了RPA的主要框架。

圖2 RPA系統(tǒng)框架

具體描述如下：(1)內(nèi)存管理器管理 RPA系統(tǒng)所有內(nèi)存資源的申請和釋放。(2)程序信息管理模塊管理目標(biāo)軟件的信息。(3)插樁管理模塊調(diào)用多種現(xiàn)有插樁工具(PDTOOLKIT[12-13]、Pin[14])進(jìn)行源碼和運(yùn)行時插樁。(4)模型層包含謂詞擴(kuò)展的實(shí)現(xiàn)。這些謂詞擴(kuò)展定義了程序驗(yàn)證所基于的基本分析模型。(5)程序邏輯分析器實(shí)現(xiàn)句子調(diào)度分析算法，執(zhí)行系統(tǒng)的驗(yàn)證分析。該模塊的分析過程利用模型層的分析模型實(shí)現(xiàn)。

3 RPAL動態(tài)邏輯語言

RPAL是一門動態(tài)邏輯語言。用戶使用RPAL語言編寫分析程序，刻畫運(yùn)行時軟件的行為特性。所以，RPAL分析程序也可理解為運(yùn)行時軟件的規(guī)范。本節(jié)討論RPAL的主要元素、相關(guān)概念和關(guān)鍵特性。

3.1 概念和元素

運(yùn)行時軟件規(guī)范由獨(dú)立完整的句子組成。每一個獨(dú)立完整的句子斷言了運(yùn)行時程序的某一行為或?qū)傩?。句子由謂詞組成。謂詞是基本斷言單位，帶有特定的語義，斷言一個基本事實(shí)。

RPAL句子支持布爾合取和布爾非等邏輯表達(dá)式。多個RPAL句子之間是布爾析取關(guān)系。這些布爾表達(dá)式的文字就是謂詞。下面是RPAL句子和謂詞的數(shù)學(xué)定義。

定義 1 句子定義為具有不定參數(shù)個數(shù)的布尓函數(shù) S：

其中， Pi（1≤ i≤m）是具有ni個參數(shù)的布爾函數(shù)，句子S的 謂詞 ；Sin=｛xik|1 ≤i≤ m, 1≤ k ≤ ni｝是 句子S的輸入。上述定義為了書寫方便省去了包含布爾非的謂詞項(xiàng)。事實(shí)上布爾非可以在任何謂詞前使用。

句子S的執(zhí)行或者估值定義為對函數(shù)S（ P1, P2, ···,Pm）求值。同樣地，謂詞P的執(zhí)行或者估值定義為對函數(shù) P（ x, x2,… , xn）求值。滿足句子S定義為S的估值為真。同樣地，滿足謂詞 P定義為 P的估值為真。

謂詞是構(gòu)成句子的最小單位，用于表達(dá)特定約束。謂詞除了估值得到滿足性結(jié)果外，還可以有多個輸出。精化謂詞P的定義后得到定義2。

定義2 謂詞P定義為：

其中，1 ≤ k ≤ n,1 ≤ l ≤ m ；ik是P的輸入；Ol是P的輸出。

RPAL既支持?jǐn)嘌灾^詞以斷言運(yùn)行時程序點(diǎn)上特定性質(zhì)，也支持事實(shí)添加謂詞和事實(shí)查詢謂詞以實(shí)現(xiàn)事實(shí)推理。事實(shí)推理是 RPA的另外一個重要特性。事實(shí)推理能力使得 RPA在分析驗(yàn)證運(yùn)行時程序的同時根據(jù)句子定義的推理規(guī)則發(fā)現(xiàn)新的事實(shí)。這些新發(fā)現(xiàn)的事實(shí)可以作為后續(xù)推理的中間結(jié)論保存在事實(shí)倉庫。程序分析結(jié)束后所有保留在事實(shí)倉庫中的事實(shí)成為整個驗(yàn)證的結(jié)論保存到外部數(shù)據(jù)文件，以供用戶查詢分析。

RPAL句子可以通過把一個謂詞的輸出作為另外一個謂詞的輸入來形成更完整的斷言。謂詞使用舉例如表 1所示，其中包括定義斷言謂詞 P、Q、R以及事實(shí)查詢謂詞F。

定義句子：

句子S斷言了函數(shù)father調(diào)用過之后，函數(shù)func每一次調(diào)用的時候，變量v1的值不能為100。其中，“～”是RPAL中布爾非符號。

由此可見，如果 RPA能提供靈活而豐富的基本謂詞集合，工程師便可以靈活地表達(dá)特定模型下有關(guān)運(yùn)行時程序行為屬性的任意斷言。事實(shí)上，支持靈活的謂詞擴(kuò)展正是 RPA設(shè)計(jì)上的一個重要的原則。研究者和工程師只要為 RPA設(shè)計(jì)并實(shí)現(xiàn)支持各種運(yùn)行時驗(yàn)證模型的謂詞庫便可把 RPA的功能拓展到更加廣闊的驗(yàn)證領(lǐng)域中。一般來說一套謂詞庫支持一種特定的分析模型，包含基本謂詞實(shí)現(xiàn)，還有擴(kuò)展對象類型的定義。本文的工作除了實(shí)現(xiàn) RPA核心外，還包括一個RPAL謂詞擴(kuò)展庫FCAM。FCAM支持函數(shù)調(diào)用分析模型和基本的變量值跟蹤模型。

3.2 RPAL分析程序組成

與通用的編程語言不同，RPAL更像是一門聲明語言，沒有條件和循環(huán)等流控制語句。RPAL以句子的形式定義運(yùn)行時程序的屬性和約束，以及條件滿足時事實(shí)的操作，而不是定義 RPA體如何執(zhí)行系統(tǒng)的分析檢測。一個合法的RPAL程序應(yīng)該由類型定義、變量賦值和運(yùn)算語句、事實(shí)謂詞定義和句子集合組成。最終有效的運(yùn)行時程序規(guī)范的定義，以及事實(shí)的推理規(guī)則由且僅由程序中定義的句子組成。

4 程序驗(yàn)證框架的實(shí)現(xiàn)

RPA程序驗(yàn)證框架的實(shí)現(xiàn)主要包括RPAL語言解析器和RPA虛擬機(jī)的實(shí)現(xiàn)。本文主要討論RPA虛擬機(jī)的實(shí)現(xiàn)。3個RPA上的術(shù)語如表2所示。

表2 術(shù)語定義

RPA虛擬機(jī)定義了RPAL分析程序運(yùn)行的環(huán)境，處理所有底層的輸入輸出工作。更重要的是，RPA虛擬機(jī)負(fù)責(zé)調(diào)度RPAL分析程序的句子執(zhí)行，使得用戶定義的運(yùn)行時程序規(guī)范能夠正確而系統(tǒng)地與軟件的某次具體執(zhí)行相比較，實(shí)施具體的事實(shí)推理。

虛擬指令映射與事實(shí)倉庫示意圖如圖3所示。

圖3 虛擬指令映射與事實(shí)倉庫示意圖

合法的 RPAL分析程序傳遞到 RPA系統(tǒng)之后，理論上，RPA會在目標(biāo)執(zhí)行流每條指令之后檢查所有句子是否均滿足。句子在執(zhí)行的時候可以發(fā)現(xiàn)新事實(shí)，去掉已有事實(shí)，和檢查特定事實(shí)是否存在。實(shí)際上 RPA的實(shí)現(xiàn)并不是在目標(biāo)執(zhí)行流每條指令之后都執(zhí)行檢查，而是在數(shù)量非常少的關(guān)鍵節(jié)點(diǎn)執(zhí)行檢查。RPA會在第1階段使用插樁技術(shù)自動往關(guān)鍵節(jié)點(diǎn)中插入感應(yīng)器。在第2階段，這些感應(yīng)器輸出作為虛擬指令被 RPA虛擬機(jī)捕捉，識別后句子映射到 RPAL分析程序的具體句子(見圖 3)。接著句子在虛擬機(jī)上被調(diào)度執(zhí)行。

4.1 程序插樁

放置感應(yīng)器是整個 RPA系統(tǒng)實(shí)現(xiàn)正確而全面檢測的基礎(chǔ)步驟。RPA通過源碼插樁技術(shù)向目標(biāo)軟件的源碼插入合法感應(yīng)器代碼。這些代碼段隨后會跟軟件其他源碼文件一起編譯鏈接。感應(yīng)器代碼的主要任務(wù)是按照虛擬指令的格式往外部文件寫入該插入點(diǎn)上被觀察變量的值。感應(yīng)器就是一個到多個這樣的值組成的集合，反映目標(biāo)系統(tǒng)某方面的狀態(tài)信息。一個虛擬指令可以容納任意個感應(yīng)器。一個感應(yīng)器可以包含任意個觀察值。

正確的程序插樁需要2個步驟：查找插樁點(diǎn)和插入插樁代碼。RPA核心向謂詞實(shí)現(xiàn)提供了一個統(tǒng)一而靈活的插樁模塊。謂詞實(shí)現(xiàn)只要向插樁模塊提供插樁點(diǎn)特征信息和待插入的虛擬指令即可完成一次插樁。

RPA的插樁管理模塊整合了 PDTOOLKIT[13]工具包和 Pin[14]動態(tài)插樁工具。PDTOOLKIT項(xiàng)目的DUCTAPE開發(fā)庫為RPA提供結(jié)構(gòu)化地分析高級語言(C/C++/Fortran)的接口。使用 DUCTAPE，插樁管理器可方便地定位目標(biāo)源碼插樁點(diǎn)。

4.2 句子調(diào)度

在RPA中，程序驗(yàn)證過程是由虛擬指令驅(qū)動的。RPA虛擬機(jī)順序地從狀態(tài)信息記錄中讀取虛擬指令，然后通過句子映射找到對應(yīng)的句子，用感應(yīng)器信息更新謂詞內(nèi)部狀態(tài)。本文定義這樣的過程為一次虛擬指令的執(zhí)行。

每一次更新謂詞狀態(tài)之后，RPA虛擬機(jī)會嘗試調(diào)度句子執(zhí)行。RPA虛擬機(jī)調(diào)度器調(diào)度過程分為2個階段：預(yù)處理階段和調(diào)度階段。虛擬機(jī)在預(yù)處理階段的主要任務(wù)是估算句子里謂詞的滿足性。當(dāng)虛擬機(jī)發(fā)現(xiàn)句子里所有謂詞都可能滿足的時候，該句子被標(biāo)記為待調(diào)度并添加到待調(diào)度句子集合。同一時刻有可能存在多個標(biāo)記為待調(diào)度執(zhí)行的句子。這種情況下虛擬機(jī)在調(diào)度階段需要計(jì)算待調(diào)度句子之間的依賴關(guān)系，確定句子的執(zhí)行順序。如果出現(xiàn)循環(huán)依賴，虛擬機(jī)報(bào)告調(diào)度錯誤并停止RPA系統(tǒng)。

預(yù)處理階段的結(jié)果是當(dāng)前可調(diào)度的句子集合S。事實(shí)上，句子之間可能存在事實(shí)依賴關(guān)系，見定義3。

定義 3 若句子 S1的執(zhí)行會產(chǎn)生事實(shí) F，句子 S2滿足的前提是存在事實(shí)F，則S2事實(shí)依賴于S1。

如果句子A事實(shí)依賴于B，那么A滿足的前提是B被執(zhí)行。這種情況下RPA句子調(diào)度算法應(yīng)得到先B后A的句子執(zhí)行順序。然而，RPAL程序員可以定義這樣一套句子集合。在某種情況下句子 A和句子 B之間相互依賴。這種情況稱為句子循環(huán)。句子循環(huán)是禁止的，理論上這樣的句子集合定義經(jīng)修改可得到合法的沒有相互依賴的句子集。一個包含句子循環(huán)的例子如下：

假設(shè)目標(biāo)程序存在這樣的一個調(diào)用序列func1()->func2()->func1()。RPA 虛擬機(jī)會在函數(shù)func1和func2的起始行插入2個虛擬指令：VI1，VI2。RPA在讀取VI1的時候，行4的call謂詞狀態(tài)被更新，虛擬機(jī)進(jìn)入預(yù)處理階段。預(yù)處理結(jié)束后行4的句子被標(biāo)記為待調(diào)度狀態(tài)。由于該句子是唯一待調(diào)度句子，所以不存在依賴問題。句子4執(zhí)行后句子3會接著被行 4的Finfunc事實(shí)添加操作喚醒執(zhí)行。另外句子 6第1個謂詞標(biāo)記為滿足。當(dāng)func1調(diào)用func2時，句子6被喚醒執(zhí)行。這時雖然句子11第2謂詞call也同時被更新，但第一事實(shí)謂詞Finfunc不滿足，所以句子 11不被調(diào)度。句子6執(zhí)行的結(jié)果是 Finfunc(f2)被添加到事實(shí)倉庫。繼而標(biāo)記句子 8和11的第一謂詞滿足性為真。最后func2遞歸調(diào)用func1時，句子8、句子4和句子3會標(biāo)記為待調(diào)度并相繼執(zhí)行。這種情況下句子8和句子4之間并不存在事實(shí)的依賴關(guān)系，所以執(zhí)行次序可交換。

雖然上述例子沒有產(chǎn)生任何錯誤，但句子 11有可能引起句子循環(huán)。假設(shè)上述例子中，被func2調(diào)用的func1內(nèi)部再次遞歸調(diào)用func2。這時句子11和句子6成為待執(zhí)行句子，但是句子11和句子6形成句子循環(huán)。

RPA句子還可能存在這樣的形式：

Finfunc(F), call([F]), +Finfunc(F);

第3事實(shí)謂詞Finfunc的參數(shù)是第2謂詞的輸出，與第1謂詞參數(shù)同名卻對應(yīng)不同對象。這種形式不存在句子循環(huán)。這種依賴稱為偽事實(shí)依賴，這種形式稱為偽句子循環(huán)。

綜上所述，RPA句子調(diào)度算法可分 3個階段：(1)第1階段為預(yù)處理階段，以事實(shí)名為關(guān)鍵字建立依賴關(guān)系，去掉偽句子循環(huán)。(2)第2階段使用拓?fù)渑判蛩惴ㄓ?jì)算待執(zhí)行句子的執(zhí)行次序。若排序過程中發(fā)現(xiàn)環(huán)，則進(jìn)入第3階段，否則算法結(jié)束。(3)調(diào)度器在第3階段匹配相互依賴的事實(shí)對象間的參數(shù)，確定句子循環(huán)是否存在。若存在則報(bào)告錯誤并退出檢測，否則更新句子依賴關(guān)系并返回第2階段。

5 實(shí)驗(yàn)結(jié)果與分析

RPA的其中一個目標(biāo)就是幫助代碼閱讀者理解現(xiàn)有系統(tǒng)。本文通過一個實(shí)際的例子來展示如何用RPAL編寫實(shí)際的運(yùn)行時程序分析程序，并且給出該例子的驗(yàn)證結(jié)果。該例子使用了 FCAM 謂詞擴(kuò)展庫。

該例子的實(shí)際系統(tǒng)——Haproxy[15]是一個提供TCP和HTTP代理服務(wù)的高速網(wǎng)絡(luò)負(fù)載均衡器，具有高可靠性、高可用性和功能強(qiáng)等特點(diǎn)。Haproxy內(nèi)部處理每一個 HTTP session的主函數(shù)是 process_session。process_session的實(shí)現(xiàn)是一個巨大的狀態(tài)機(jī)，包括非常多底層I/O接口狀態(tài)的判斷和轉(zhuǎn)移。利用一般的代碼閱讀工具輔助理解變得非常困難。這時候，RPA工具既能幫助系統(tǒng)分析者驗(yàn)證系統(tǒng)運(yùn)行時的行為，也能根據(jù)分析者制定的推理策略自動發(fā)現(xiàn)事實(shí)得出結(jié)論。Haproxy處理session的相關(guān)函數(shù)如下：

一個斷言在process_session函數(shù)調(diào)用期間的例子如下，在process_session所有子函數(shù)調(diào)用之外session的狀態(tài)(session->flag)不會改變的 RPAL分析程序片段。

process_session函數(shù)一方面負(fù)責(zé)建立和關(guān)閉鏈接、IO錯誤檢查，另一方面調(diào)用多個 HTTP包分析函數(shù)分析HTTP報(bào)文。session_accept函數(shù)在新HTTP session到來時調(diào)用，負(fù)責(zé)session結(jié)構(gòu)的初始化。本例子將要展示RPA在謂詞擴(kuò)展FCAM支持下跟蹤堆變量值的能力。對于Saturn等只支持靜態(tài)分析的系統(tǒng)來講，實(shí)現(xiàn)正確動態(tài)堆變量值的跟蹤和分析非常的困難。然而 RPA卻非常適合觀察分析堆變量和跨函數(shù)調(diào)用的程序邏輯。

以上所示 RPAL程序中，行 18的句子斷言若http_wait_for_request函數(shù)被調(diào)用，則添加空事實(shí)集合到默認(rèn)事實(shí)棧，然后在該集合里面添加事實(shí)：在函數(shù)http_wait_for_request內(nèi)部。行20斷言當(dāng)這個函數(shù)返回的時候彈出棧頂事實(shí)集。本例子的默認(rèn)事實(shí)棧用作標(biāo)識運(yùn)行時程序當(dāng)前所在的子函數(shù)調(diào)用。行22～行24使用另個命名事實(shí)棧 sess標(biāo)識 process_session的調(diào)用。行 26～行 28讀取 session.c文件第 17行上變量s->flag的值，并把該值保存在事實(shí)對象 Fval中。值得注意的是Haproxy在每一個新 session到來時在內(nèi)存堆上動態(tài)申請變量s->flag的空間。行29～行31指定在session_free函數(shù)調(diào)用之后去掉Fval事實(shí)標(biāo)記。行33～行35的句子是本RPA分析程序最關(guān)鍵的句子。它斷言了當(dāng)變量 s->flag值改變時控制流不會在http_wait_for_request函數(shù)調(diào)用內(nèi)部。

如果 Haproxy的某次執(zhí)行滿足上述斷言，那么RPA運(yùn)行后會產(chǎn)生包含事實(shí) Fsucceed的結(jié)論。由于s->flag的修改遍布process_session函數(shù)的整個調(diào)用過程，因此最終的測試結(jié)果是失敗的，RPA輸出空結(jié)論集。

6 結(jié)束語

本文提出了一個基于程序插樁和布爾邏輯的運(yùn)行時程序驗(yàn)證框架RPA。RPA定義了基于布爾邏輯的動態(tài)邏輯語言RPAL。用戶使用RPAL刻畫軟件運(yùn)行時的行為和屬性后，RPA可自動并系統(tǒng)地對軟件進(jìn)行插樁，執(zhí)行驗(yàn)證和推理。本文給出了一個實(shí)際的例子，顯示了RPAL框架可作為實(shí)際軟件開發(fā)后期的驗(yàn)證和測試工具，承擔(dān)軟件正確性驗(yàn)證的任務(wù)。作為一個基本的驗(yàn)證框架，RPA仍然存在不足的地方。這主要表現(xiàn)在：

(1)現(xiàn)有 RPA謂詞擴(kuò)展庫不足，只能支持函數(shù)調(diào)用模型和簡單的變量值跟蹤模型；

(2)RPA插樁模塊支持的程序插樁方法有待擴(kuò)充，以支持從源碼到二進(jìn)制代碼，再到運(yùn)行時程序的插樁能力。

下一步的工作是設(shè)計(jì)謂詞擴(kuò)展庫以支持完整的變量跟蹤模型，并完善RPA框架。

[1]梁 睿.基于運(yùn)行時驗(yàn)證的 AOP程序檢測框架研究[D].蘭州: 蘭州大學(xué), 2009.

[2]Aiken A, Bugrara S, Dillig I, et al.Saturn Project[EB/OL].[2012-03-01].http://saturn.stanford.edu.

[3]Killian C, Anderson J W, Jhala R, et al.Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code[C]//Proc.of NSDI’07.Cambridge, USA: [s.n.],2007.

[4]Aiken A, Bugrara S, Dillig I, et al.An Overview of the Saturn Project[C]//Proc.of PASTE’07.San Diego, USA:[s.n.], 2007.

[5]Aiken A, Bugrara S, Dillig I, et al.The Saturn Program Analysis System[EB/OL].[2012-03-01].http://saturn.stanford.edu.

[6]Reynolds P, Killian C, Wiener J L, et al.Pip: Detecting the Unexpected in Distributed Systems[C]//Proc.of NSDI’06.San Jose, USA: [s.n.], 2006.

[7]Liu Xuezheng, Guo Zhenyu, Wang Xi, et al.D3S: Debug Deployed Distributed System[C]//Proc.of NSDI’08.San Francisco, USA: [s.n.], 2008.

[8]Killian C E, Anderson J W, Braud R.Mace: Language Support for Building Distributed Systems[C]//Proc.of PLDI’07.San Diego, USA: [s.n.], 2007.

[9]Yang Junfeng, Chen Tisheng, Wu Ming, et al.MODIST:Transparent Model Checking of Unmodified Distributed Systems[C]//Proc.of NSDI’09.Boston, USA: [s.n.],2009.

[10]Yabandeh M, Knezevic N, Kostic D, et al.CrystalBall:Predicting and Preventing Inconsistencies in Deployed Distributed Systems[C]//Proc.of NSDI’09.Boston, USA:[s.n.], 2009.

[11]Pnueli A.The Temporal Logic of Programs[C]//Proc.of the 18th IEEE Symposium on Foundation of Computer Science.[S.l.]: IEEE Computer Society, 1977.

[12]Shende S S, Malony A D.The Tau Parallel Performance System[J].International Journal of High Performance Computing Applications, 2006, 20(2): 287-311.

[13]Shende S S, Malony A D.Pdtoolkit Project[EB/OL].[2012-03-01].http://www.cs.uoregon.edu/Research/tau/do wnloads.php.

[14]Luk Chi-Keung, Cohn R, Muth R, et al.Pin: Building Customized Program Analysis Tools with Dynamic Instrumentation[C]//Proc.of PLDI’05.Chicago, USA:[s.n.], 2005.

[15]Tarreau W.Haproxy Project: The Reliable, High Performance TCP/HTTP Load Balancer[EB/OL].[2012-03-01].http://haproxy.1wt.eu.