基于插樁和布爾邏輯的運行時程序驗證框架

李業華，顧乃杰，張穎楠，彭 飛

(1.中國科學技術大學計算機科學與技術學院，合肥 230027；2.安徽省計算與通訊軟件重點實驗室，合肥 230027；3.中國科學技術大學中國科學院沈陽計算技術研究所網絡與通信聯合實驗室，合肥 230027)

1 概述

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

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

Saturn[2,4-5]是由美國 Stanford大學開發的一個用于靜態檢查大型軟件系統屬性的項目。Saturn定義了一門邏輯語言 Calypso[5]來描述屬性約束集。該屬性約束集定義系統的特征和屬性。本文提出的RPAL語言參考了 Calypso語言的設計。但 RPAL在 Calypso的句子、謂詞和事實等語法元素基礎上擴展了事實操作集，大大增強了事實管理模型。相比Calypso，RPAL是動態語言而不是符號語言，支持完整的類型系統和對象管理。因此分析程序的語義變得更加清晰，大大減少因為分析程序的類型錯誤導致的分析結果錯誤。

RPA使用獨立的事實倉庫管理驗證過程中的中間和最終事實結論。事實倉庫建模為命名事實棧集合，支持比Saturn更靈活的事實管理操作。

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

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

2 運行時程序驗證框架

RPA是一個用于驗證和分析運行時程序屬性的工具框架。完整的RPA系統包括RPA核心和RPAL擴展。其中RPA核心包括RPAL語言、RPAL語言解析器和 RPA程序驗證虛擬機 3個部分，而RPAL擴展則包括各種擴展謂詞庫。

2.1 基本驗證流程

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

圖1 RPA運行時程序驗證的流程

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

(1)第1階段是感應器安放階段，主要根據RPAL分析程序刻畫的程序屬性執行程序插樁工作。插樁后的目標軟件每一次執行將會額外地輸出狀態信息記錄文件。

(2)在第 2階段，RPA會啟動目標程序執行，結束后把合法的RPAL分析程序和狀態信息記錄文件作為RPA虛擬機的輸入，啟動分析過程。

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

2.2 系統框架

RPA核心實現包括RPAL解析器和RPA虛擬機。RPAL解析器負責分析RPAL分析程序的輸入，準備好基本的驗證環境。RPA虛擬機則在解析器準備的驗證環境基礎上執行系統的驗證分析工作。圖2給出了RPA的主要框架。

圖2 RPA系統框架

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

3 RPAL動態邏輯語言

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

3.1 概念和元素

運行時軟件規范由獨立完整的句子組成。每一個獨立完整的句子斷言了運行時程序的某一行為或屬性。句子由謂詞組成。謂詞是基本斷言單位，帶有特定的語義，斷言一個基本事實。

RPAL句子支持布爾合取和布爾非等邏輯表達式。多個RPAL句子之間是布爾析取關系。這些布爾表達式的文字就是謂詞。下面是RPAL句子和謂詞的數學定義。

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

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

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

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

定義2 謂詞P定義為：

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

RPAL既支持斷言謂詞以斷言運行時程序點上特定性質，也支持事實添加謂詞和事實查詢謂詞以實現事實推理。事實推理是 RPA的另外一個重要特性。事實推理能力使得 RPA在分析驗證運行時程序的同時根據句子定義的推理規則發現新的事實。這些新發現的事實可以作為后續推理的中間結論保存在事實倉庫。程序分析結束后所有保留在事實倉庫中的事實成為整個驗證的結論保存到外部數據文件，以供用戶查詢分析。

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

定義句子：

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

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

3.2 RPAL分析程序組成

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

4 程序驗證框架的實現

RPA程序驗證框架的實現主要包括RPAL語言解析器和RPA虛擬機的實現。本文主要討論RPA虛擬機的實現。3個RPA上的術語如表2所示。

表2 術語定義

RPA虛擬機定義了RPAL分析程序運行的環境，處理所有底層的輸入輸出工作。更重要的是，RPA虛擬機負責調度RPAL分析程序的句子執行，使得用戶定義的運行時程序規范能夠正確而系統地與軟件的某次具體執行相比較，實施具體的事實推理。

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

圖3 虛擬指令映射與事實倉庫示意圖

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

4.1 程序插樁

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

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

RPA的插樁管理模塊整合了 PDTOOLKIT[13]工具包和 Pin[14]動態插樁工具。PDTOOLKIT項目的DUCTAPE開發庫為RPA提供結構化地分析高級語言(C/C++/Fortran)的接口。使用 DUCTAPE，插樁管理器可方便地定位目標源碼插樁點。

4.2 句子調度

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

每一次更新謂詞狀態之后，RPA虛擬機會嘗試調度句子執行。RPA虛擬機調度器調度過程分為2個階段：預處理階段和調度階段。虛擬機在預處理階段的主要任務是估算句子里謂詞的滿足性。當虛擬機發現句子里所有謂詞都可能滿足的時候，該句子被標記為待調度并添加到待調度句子集合。同一時刻有可能存在多個標記為待調度執行的句子。這種情況下虛擬機在調度階段需要計算待調度句子之間的依賴關系，確定句子的執行順序。如果出現循環依賴，虛擬機報告調度錯誤并停止RPA系統。

預處理階段的結果是當前可調度的句子集合S。事實上，句子之間可能存在事實依賴關系，見定義3。

定義 3 若句子 S1的執行會產生事實 F，句子 S2滿足的前提是存在事實F，則S2事實依賴于S1。

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

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

雖然上述例子沒有產生任何錯誤，但句子 11有可能引起句子循環。假設上述例子中，被func2調用的func1內部再次遞歸調用func2。這時句子11和句子6成為待執行句子，但是句子11和句子6形成句子循環。

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

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

第3事實謂詞Finfunc的參數是第2謂詞的輸出，與第1謂詞參數同名卻對應不同對象。這種形式不存在句子循環。這種依賴稱為偽事實依賴，這種形式稱為偽句子循環。

綜上所述，RPA句子調度算法可分 3個階段：(1)第1階段為預處理階段，以事實名為關鍵字建立依賴關系，去掉偽句子循環。(2)第2階段使用拓撲排序算法計算待執行句子的執行次序。若排序過程中發現環，則進入第3階段，否則算法結束。(3)調度器在第3階段匹配相互依賴的事實對象間的參數，確定句子循環是否存在。若存在則報告錯誤并退出檢測，否則更新句子依賴關系并返回第2階段。

5 實驗結果與分析

RPA的其中一個目標就是幫助代碼閱讀者理解現有系統。本文通過一個實際的例子來展示如何用RPAL編寫實際的運行時程序分析程序，并且給出該例子的驗證結果。該例子使用了 FCAM 謂詞擴展庫。

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

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

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

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

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

6 結束語

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

(1)現有 RPA謂詞擴展庫不足，只能支持函數調用模型和簡單的變量值跟蹤模型；

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

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

[1]梁 睿.基于運行時驗證的 AOP程序檢測框架研究[D].蘭州: 蘭州大學, 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.