基于程序局部性引導的有界模型檢測優(yōu)化方法

王舜，杜曄，韓臻，劉吉強

?

基于程序局部性引導的有界模型檢測優(yōu)化方法

王舜，杜曄，韓臻，劉吉強

（北京交通大學智能交通數(shù)據(jù)安全與隱私保護技術北京市重點實驗室，北京 100044）

基于多種模型檢測方法組合的復合檢測方式是當前軟件模型檢測領域開展研究的熱點之一。在當前的研究中，提高檢測的規(guī)模和檢測的對象復雜程度的關鍵在于如何有效處理抽象的擴張和收縮。證明通過對程序模式或驗證信息的利用可以加快狀態(tài)空間的探索速度。面向有界模型檢測（BMC）加速方法展開研究，使用程序中額外的信息和知識對其處理以協(xié)助檢測器刪除冗余和無效的狀態(tài)。在對程序局部性進行定義的基礎上，對其加速性進行討論，提出一種加速有界檢測的方法和一種改進策略，對算法進行了詳細描述，并通過實驗驗證了方法在檢測效率和性能上的優(yōu)越性。

模型檢測；BMC；軟件檢測；局部性；優(yōu)化

1 引言

軟件模型檢測是提高軟件可靠性的一種非常重要的方法。在工業(yè)環(huán)境中，一些對于軟件可靠性要求高的安全苛求系統(tǒng)已大量地使用這種方法。軟件模型檢測是基于程序的形式化理論發(fā)展出的一種技術，它的基本思想是對當前需要檢測程序的整體狀態(tài)空間進行遍歷，從而尋找其中是否包含問題狀態(tài)。對于使用基本的遍歷思想來檢測程序的方法來講，狀態(tài)空間爆炸使它在很小的程序上都會耗盡其所有的運算和存儲資源，因此，這種檢測方法并不具備成規(guī)模的實用性。

針對上述問題，現(xiàn)代的軟件模型檢測方法使用了多重的優(yōu)化策略來緩解，這些策略可以按照枚舉型和推理型來進行分類[1,2]，2種類型分別體現(xiàn)了具象和抽象的邏輯思想。而隨著研究的進展和深入，很多新的研究使用了同時綜合2種方法特征的混合策略。特別是隨著近年來各種各樣的方法被陸續(xù)提出，研究者逐漸發(fā)現(xiàn)，區(qū)分和指導各種方法的根本不同在于如何使用源代碼中的信息來引導狀態(tài)空間的搜索。當然與之相對地，還可以通過表象對軟件模型檢測的方法進行分類，例如，模型檢測算法是否有界。

有界模型檢測器（BMC）是一種常見的和使用廣泛的軟件模型檢測工具。在近幾年的相關研究中，已經(jīng)有不少基于其思想的成熟的實現(xiàn)，如文獻[3~7]。使用有界模型檢測器對程序進行檢測的實踐可能會因為使用了不合適的參數(shù)而導致檢測無法完成或檢測失敗。同時，由于其原理的制約，這種檢測方法也無法直接對整個程序的狀態(tài)空間進行檢測。從這個角度來講，阻礙有界模型檢測對大規(guī)模代碼進行檢測的障礙之一在于缺乏一種有效的將代碼分解為可以檢測的片段并且自動引導檢測器來進行檢驗的方法。

SAT求解問題是另一個更加基礎的研究領域，需要求解的SAT問題同樣是類似的會引起狀態(tài)爆炸的NP完全問題。在這個研究領域中，前向—后向搜索是常用的加速求解的方法之一，而最為經(jīng)典的SAT前向—后向搜索算法的實現(xiàn)則是DPLL算法[8]。這種算法的核心思想是，在遍歷搜索時記憶和學習關于邏輯樹的結構信息，并使用這個信息來指導新一輪的搜索。在整個SAT求解器的研究領域中，大量的優(yōu)化方法都采用了類似的思路為指導，也就是使用在有限的搜索中發(fā)現(xiàn)的信息來縮減后續(xù)的搜索樹，或選擇最優(yōu)的后續(xù)搜索?；谙闰炐畔⒌膯l(fā)式算法[9~12]是另一類常用的優(yōu)化方法。與前一類方法相比，它最大的不同是并不能保證總是有效。但是相對地，啟發(fā)式算法在狀態(tài)空間的規(guī)模和邏輯復雜度快速增長的情況下是一種更有潛力的方法。

最后，程序在設計和運行中具有一個非常本質和重要的特征，即程序的局部性。在調研中，當前模型檢測領域并沒有相關研究聚焦在程序的局部性和模型檢測的優(yōu)化結合以及程序的局部性對模型檢測加速的可能性上。因此，本文主要研究聚焦以上層面。首先，本文給出了一種可能的程序局部性形式化定義，然后，設計了一個策略來對程序進行劃分，并提出了一種算法自動化地使用這種劃分來指導有界模型檢測器的自動運行，最后，通過實驗驗證了本文方法在加速有界模型檢測器對程序的檢測上具有較為明顯作用。

2 相關工作

近年來，大量的研究關注和聚焦了模型檢測和模型檢測的相關算法和應用。其中，基于邏輯的枚舉和基于邏輯的推理是2種重要的類型。在這些研究中，最為活躍和引人注目的部分集中在以下2個方向：1) 基于推理的模型檢測方法，包括基于符號演算的模型檢測方法；2) 不同模型檢測方法的可組裝性的研究。

其中，第一類研究方向使用歸結原理和插值規(guī)則通過定理證明的方法[13~15]來進行模型檢測。另外，還有一些研究設計并實現(xiàn)了一類框架[16~19]，并在這類框架下實現(xiàn)了基于前向—后向搜索的遍歷式模型檢測方法。這類方法的基本思想是將目標狀態(tài)空間簡化為一類抽象狀態(tài)空間，并在其上進行檢測。在這類框架之上，文獻[20,21]設計了一種懶惰方法，它是針對狀態(tài)展開的優(yōu)化，使算法在展開狀態(tài)時不需要一次性完全展開，而是按照需要展開必要的層數(shù)，從而避免狀態(tài)空間一次性展開過大。最后，文獻[22~24]的研究則著眼于設計和實施一套全新的軟件模型檢測方法。

第二類研究方向中包含了一類構建通用的模型檢測方法基礎的理論以及其相關的實現(xiàn)，它們都基于一套可以嵌入和組合大量不同方法的基礎框架之上。文獻[25~30]是其中非常重要的組成部分。它們建立了一個稱為CPA的模型檢測框架。這個框架實際上是一個基于格的狀態(tài)抽象，在這個抽象之上，使用融合、加強以及停止運算符來將各種算法組合在一起。除了這些工作以外，文獻[31]使用了另一種上近似和下近似結合的方法來對不同的模型檢測方法進行組合。

本文方法是一類組合方法，但是其手段并非直接組合已有的方法，而是結合第一類的研究和第二類的研究，提出一種基于新的局部性啟發(fā)式檢測加速方法。

3 基本模型

3.1 程序模型

為了簡化問題的分析和討論，本文使用一個簡單程序模型來表示需要檢測輸入的程序抽象。這個模型是一個基于簡單命令式程序語言的擴展，使用這個模型可以描述C語言的邏輯結構，而其他的細節(jié)則直接交給BMC工具處理即可。

一個簡單命令式程序包含了一系列的操作符，這些操作符包括：賦值操作符、假設操作符、整形變量。簡單命令式程序的描述細節(jié)可以參考文獻[1]。這里對簡單命令式程序進行一個擴展，使其可以滿足對本文形式化描述的要求，其包含了一些額外的程序結構：函數(shù)、分支、循環(huán)。它可以通過分支循環(huán)展開和函數(shù)嵌入的方式很容易地轉換回經(jīng)典的簡單命令式程序。實際上，可以通過這個擴展給基礎定義添加一些高級結構。

一個帶條件語句的命令式程序可以轉換為一個簡單命令式程序，這個轉換可以通過合取條件變量（以中的元素為變量的布爾表達式）與賦值表達式來獲得。

循環(huán)語句的處理比條件語句要稍微復雜一些。首先對需要轉換的循環(huán)語句設定一個展開層數(shù)限制，然后展開這個循環(huán)為順序程序。如果循環(huán)在到達限制前沒有展開完畢，則停止在展開限制處（圖1為一個簡單的例子）。這個展開實際上是一種懶惰（lazy）的循環(huán)展開方式。使用這種方法可以在一定程度上阻止可能的狀態(tài)空間發(fā)生爆炸問題。而在循環(huán)展開以后，可能會遺留下一個未被展開的循環(huán)體，這個尾巴可以被表示為一個特殊的節(jié)點，它被標記為尚未被轉換和翻譯。這也是一個在懶惰策略中常用的技巧。函數(shù)的翻譯和循環(huán)的翻譯類似，但是更為簡單直接。一個函數(shù)既可以被展開成一段平坦的程序片段，同時也可以不翻譯。在形式化的語言表達中，可以采用一個函數(shù)集合去統(tǒng)一地表示2種翻譯方法。

上面所述的描述方式可以表示一個具體的程序。這個具體的程序模型描述了一個程序精確的運行特性，但是它的狀態(tài)集通常都十分巨大甚至難以使用有限的描述來表示。如果使用這個較為接近底層的模型去指導一個狀態(tài)空間的搜索，難免會遇到困難和失敗。因此，需要一個更加抽象的模型去描述一個更小以及更有限的狀態(tài)空間。

3.2 抽象可達圖

3.3 有界模型檢測

有界模型檢測（BMC）只檢測步以內的可達性，其形式化的表達如下。

其中，表示初始狀態(tài)集合，表示程序的轉換關系集合，前方下標是轉換關系索引，表示程序不變的屬性集合，這些屬性需要在程序的整個執(zhí)行期中保證不被違反。一個有界模型檢測方法的工作過程就是對這個命題進行驗證，證明它恒為真或找到一個使它為假的證明。如果一個有界模型檢測方法找到了一個使命題為假的證明，這個證明肯定可以應用在原始的程序中，使程序也有一條相應的在這個賦值下的路徑，這條路徑通常被稱為反例。如果反例存在，那它一定是充分的。但是當這個有界模型檢測方法給出了一個恒為真的證明時，這個證明卻不足以說明整個原始程序的安全是充分的。所以，有界模型檢測方法是一種下近似的驗證方法。這樣的有界模型檢測可以保證整個驗證過程一定能在一定步驟后停止，無論它檢測的程序是什么結構。因此，這種方法配合其他一些優(yōu)化方法對于檢測實用的程序非常有效。

有界模型檢測的基本算法框架如算法1所示。這種方法需要配合使用一個SAT或SMT求解器來作為內部的核心組件。一個基本的有界模型檢測算法也可以看作是符號模型檢測算法添加一個界限的產(chǎn)物。

算法1 有界模型檢測的基本算法

輸出 如果程序安全則輸出SAFE，如果程序檢測逾越邊界則輸出UNKNOWN，否則輸出UNSAFE

步數(shù)設置為0

while 工作列表非空 do

步數(shù)加1

if 步數(shù)大于，則返回 UNKNOWN

為工作集添加元素的像

if 可達集在錯誤點非空，則返回 UNSAFE

否則，返回SAFE

如果把有界模型檢測算法看作是對程序模型的樹型遍歷，那么很顯然，這種方法使用的是深度優(yōu)先策略。

4 程序局部性定義與局部性模型描述

局部性又被稱為參考局部性或者局部性原理，是計算機工程領域的一個重要的原理。這個原理描述了計算機系統(tǒng)在數(shù)據(jù)訪問和程序執(zhí)行的過程中會大概率地優(yōu)先訪問或者執(zhí)行上一個訪問位置附近的相關數(shù)據(jù)，對于指導計算機工程上的很多問題的優(yōu)化方案有重要的作用。在局部性中，2種重要的類型分別是時間局部性和空間局部性。時間局部性描述了在一段連續(xù)的時間片段中，特定的數(shù)據(jù)或位置會被頻繁地訪問。相似地，空間局部性描述了數(shù)據(jù)的訪問會經(jīng)常地發(fā)生在相距很近的地方。在很多啟發(fā)式算法中，局部性是指導優(yōu)化內在原理。

當前的程序設計語言給予了程序設計人員強大的能力，這個能力體現(xiàn)在程序中就是程序的多維度上的自由度。具體來講，例如，在面向對象的程序設計（OOP）范式中，2個重要的自由度是繼承和包含關系。另一個重要的例子是，在堆棧式語言編碼的程序當中，2個重要的維度是深度和廣度。程序的局部性在這2個例子中就可以體現(xiàn)在它們的自由維度上。在每一個維度上，程序本身都具有依賴這個維度的局部性。形式化地，這些局部性可以體現(xiàn)在相關程序的語法和語義的鄰接關系上。在這里將要給出一個基于擴展版本的簡單命令程序的局部性的定義。首先，需要先介紹幾個前置概念。

在分層抽象可達圖中，節(jié)點的有向連接體現(xiàn)了程序執(zhí)行序列的方向。實際上，分層抽象可達圖是一個二維視角下程序流語義的展現(xiàn)。

在分層抽象可達圖中，量化的距離定義不妨借鑒經(jīng)典的距離表達方法，即曼哈頓距離來表示。在這個前提下，可以進一步定義一個曼哈頓抽象可達圖為一種分層抽象可達圖，其中，每一層都是一個由分支、循環(huán)或函數(shù)節(jié)點展開得到的子抽象可達圖。在曼哈頓抽象可達圖中，每一層的子分支，循環(huán)和函數(shù)都默認不被展開。在這個抽象可達圖上，可以比較方便地定義距離，同時，程序語法和語義上的信息也被有效地保留了下來。

假設1一個程序的執(zhí)行路徑會有較大概率選擇局部性強的路徑。

本文給出的假設1是合理的。首先，其符合程序員的編程直覺。使用局部性較強的路徑更加容易設計邏輯連貫的程序，因為在處理邏輯的連接時，需要進行的額外記憶將會降低。其次，局部性符合計算機體系結構的基本原理，程序在執(zhí)行時選擇局部性較強的路徑會節(jié)約計算機運算的時間資源和空間資源。

為了將程序的局部性性質應用到傳統(tǒng)的有界模型檢測算法中去，原始的算法需要進行一定的擴展，從而使它可以接受和處理現(xiàn)代程序設計語言中蘊含的特定的因果關系。具體地，就是讓原始的有界模型檢測算法可以接受和處理來自廣度方向上的局部性信息。有界模型檢測算法是一個典型的深度優(yōu)先搜索算法，這個算法只接受具體的符號化程序作為輸入，然后按照這個程序的運行路徑進行搜索和計算。綜上所述，本文的程序局部性的定義是包含抽象狀態(tài)的，因此，有界模型檢測算法并不能直接應用在其上。特別地，如果搜索方向是廣度優(yōu)先，那么在執(zhí)行過程中將會有很大概率碰到抽象狀態(tài)。所以需要讓有界模型檢測算法可以處理一些抽象狀態(tài)。

不翻譯函數(shù)（uninterpreted function）是SAT求解領域里的一個重要的理論模型。這個模型擴展了SAT求解器的能力，使它可以處理的邏輯范圍不僅限于命題邏輯[32]。不翻譯函數(shù)的基本理念是使用一個不展開的符號來表示一組命題，而這組命題中的符號被當作這個符號的參數(shù)來處理。這樣一來，這個不展開的符號就符合了一般函數(shù)的定義，而它的值就是這組命題計算式的合取。這種表示方式可以跳過對這組計算式的原地求值（on-site evaluation），從而形成一個懶惰求值的節(jié)點。因此，可以仿照不翻譯函數(shù)的形式邏輯來表示本文的抽象可達圖中的抽象部分。

定義7 不翻譯函數(shù)的擴展邏輯。一個定義了不翻譯函數(shù)的擴展邏輯包含以下語法。

這種擴展邏輯利用了不翻譯函數(shù)的能力并且可以處理多重返回值以及各種各樣的二元關系運算符。它可以將程序片段轉換成邏輯公式使特定的SAT或SMT求解器得以求解。對應地，它也可以將程序變?yōu)榭杀籅MC接受的抽象程序。

5 局部性引導的BMC算法

本節(jié)將會討論如何使用局部性來指導有界模型檢測算法。先從設計和實現(xiàn)一個簡單的、使用局部性策略的算法開始，接著討論一個添加了更多優(yōu)化的版本。

5.1 基礎算法

直接使用程序的局部性來指導有界模型檢測算法可以通過計算目標程序的2個節(jié)點間的局部性度量來實現(xiàn)。這個想法相對比較易于實現(xiàn)，同時又易于理解。通過搜索當前節(jié)點到錯誤點的局部度量可以獲得一個整體局部性。反復進行搜索便可以得到一個迭代更新的局部性參考。

與原始的有界模型檢測算法類似，每一輪有界模型檢測算法的運行并不是完全覆蓋整個程序的狀態(tài)集。但對比傳統(tǒng)的算法，本文算法可以降低在深度或廣度方向上的運行消耗。另外，將一個大型的有界模型檢測搜索拆分成數(shù)個較小檢測可以增加檢測的靈活性，使檢測可以在有限的空間下對更大型的狀態(tài)空間執(zhí)行搜索。

函數(shù)是遞歸逐層檢測程序的抽象可達圖的方法。其他一些參數(shù)的定義如下。

是分層抽象可達圖的有序列表。

用來獲取抽象可達圖的根元素的函數(shù)。

是一個獲取目標程序后置操作的迭代器。

是一個獲取抽象可達圖中父節(jié)點的函數(shù)。

是一個獲取抽象可達圖中子節(jié)點的函數(shù)。

是一個使用擴展邏輯將節(jié)點變?yōu)閷某橄蠊?jié)點的函數(shù)。

是一個獲取分層抽象可達圖當前層的節(jié)點的迭代器。

是一個從目標抽象可達圖的節(jié)點上獲取其所包含的具體狀態(tài)的函數(shù)。這些狀態(tài)包括所選擇節(jié)點在深度或廣度方向上的狀態(tài)。如果深度或廣度方向沒有在參數(shù)上被指定，那么就直接獲取節(jié)點在所有方向上的具體狀態(tài)，這時，這個函數(shù)與函數(shù)互逆。

是一個統(tǒng)計集合內元素個數(shù)的函數(shù)。

是一個獲得節(jié)點和路徑間具有因果關系的所有節(jié)點的集合。

是獲取當前節(jié)點沿特定方向到錯誤點的路徑。

算法2 基礎算法

輸出 如果程序安全則輸出SAFE，否則輸出UNSAFE

初始化結果為UNKNOWN，抽象狀態(tài)為空

調用函數(shù)創(chuàng)建分層，賦值給

while 結果是UNKNOWN do

調用函數(shù)(,(),)并把結果傳遞給檢測結果和

for 對于集合的元素 do

對元素調用函數(shù)

返回結果

函數(shù)創(chuàng)建分層ARG():

初始化為

for 對于程序執(zhí)行的各步驟 do

if 該步驟符合曼哈頓條件 then

調用函數(shù)(,)并給其結果賦值為該步驟調用函數(shù)的返回值。

否則，調用函數(shù)()并為其結果賦值為該步驟調用函數(shù)的返回值

函數(shù)(,,)：

調用函數(shù)分別計算廣度方向上的距離和深度上的距離，并求二者之差t

設置探索方向為深度

ift大于1 then

設置探索方向為廣度

調用函數(shù)((,當前探索方向),, 1)并賦值給結果

else if 結果是UNKNOW then

初始化和為空

for 集合(,)的元素 do

調用函數(shù)(, 當前元素,)并將結果賦值給和

if取值為UNKNOWN then 將合并入

返回(UNKNOWN,)

否則，返回SAFE

函數(shù)(,):

if 方向是深度方向 then

返回((,last()))

否則返回((,last()))

5.2 改進算法

算法3 改進算法

輸出 如果程序安全則輸出SAFE，否則，輸出UNSAFE

調用函數(shù)創(chuàng)建分層ARG()并將結果賦予

調用函數(shù)分別計算廣度方向上的距離和深度上的距離，并求二者之差t

設置探索方向為深度

if 結果為UNSAFE then

返回 (UNSAFE,)

else if 結果為UNKNOWN then

初始化，為空

初始化為真

for 集合(,)的元素 do

if取值為UNSAFE then 將合并入

否則返回SAFE

在整個改進的算法中，參考了反例引導的抽象—精煉模型檢測方法（counterexample-guided abstraction-refinement）中的反例引導思想。通過提取每次有界模型檢測器獲取的一個證明來加強算法中的局部性尋找，從而使局部性引導過程的搜索空間可以被有效限制，并且避免了一些重復的狀態(tài)遍歷。這種做法可以加強在局部性尋找失敗時的算法效率。

6 實驗設計與性能分析

本文方法使用有界模型檢測工具作為內部的實現(xiàn)核心，這個工具本身具有獨立地檢測軟件可靠性的能力。綜上所述，本文的目標是針對傳統(tǒng)的有界模型檢測工具的一個改進和優(yōu)化。將優(yōu)化方法實施在一個現(xiàn)有的有界模型檢測器上而不是使用一個定制的檢測器具有多重優(yōu)勢。其中之一是，現(xiàn)有的模型檢測器除了實施基本的有界模型檢測算法以外，同時還考慮了多種與模型檢測和程序分析相關的優(yōu)化措施。使用現(xiàn)有的模型檢測工具可以充分地利用領域里已經(jīng)實施的相關優(yōu)化方法，從而可以獲得更佳的性能表現(xiàn)。另外一點是，使用現(xiàn)有的工具可以充分利用其對于程序的表達和處理的能力，從而可以使方法能夠應對更多樣和復雜的樣本。

通過對現(xiàn)有各種有界模型檢測工具進行考察發(fā)現(xiàn)，其中很多工具并不能很好地分析和處理實際的代碼片段，例如代碼具有復雜的循環(huán)結構、跳轉、指針或內存操作。在部分有界模型檢測工具中，對這些結構的檢測體現(xiàn)為直接跳過或出現(xiàn)誤報或者提示錯誤并拒絕，因此本文實驗還需要對測試樣本進行篩選，以去除不良用例。

實驗使用了來自SV-COMP和其他項目中的工業(yè)代碼作為測試用的樣本。這些樣本中包含了規(guī)模不一的代碼片段。其中，最長的代碼片段長度為1 762行，最短的片段長度為341行。使用這個長度范圍內的片段是因為短于這個長度的片段有界模型檢測工具可以很快地完成代碼的檢查，無法區(qū)分本文所述方案的優(yōu)越性；而長于最長片段的代碼將會導致內部的有界模型檢測工具出現(xiàn)錯誤中止，從而使比較產(chǎn)生系統(tǒng)性誤差。在測試樣本中，除了代碼長度不同，代碼的類型也有所區(qū)別。樣本中的代碼包含順序代碼、分支代碼、循環(huán)代碼、跳轉代碼、指針及內存操作代碼。所檢查的程序安全性屬性包含可達、不可達、控制邏輯以及一些訪問相關的屬性。

大多有界模型檢測器最大的問題都是對指針和內存的支持不完整，導致實際生產(chǎn)中的代碼難以進行有效的檢測。通過大量的研究和測試發(fā)現(xiàn)，LLBMC[33]對于工業(yè)代碼的支持最為完整，同時因為其使用了顯式內存分析，它對代碼規(guī)模的支持也很強大。同時根據(jù)SV-COMP[34]的測試結果顯示，其在整個模型檢測業(yè)界也具有很好的性能表現(xiàn)?；谶@些研究，在測試中使用LLBMC作為算法中有界模型檢測器的實現(xiàn)。

本文實驗平臺配置如下。Intel Core 2，4核8線程處理器，64 GB物理內存以及64位Ubuntu 12.04操作系統(tǒng)。保留測試代碼中的各種瑕疵以及不好的編程范式，從而使其更加貼近真實的生產(chǎn)中會產(chǎn)生的代碼。同時，也使程序員在編寫代碼時遺留在程序中的局部性得以保留。實驗分為2個部分，第一個部分將實驗樣本按照代碼規(guī)模從低到高分為5個階梯。因為代碼的行數(shù)與其復雜程度具有一定的關系但又不是嚴格的線性關系，使用這種階梯式的分類方法可以更好地體現(xiàn)出代碼復雜程度的演進。第二個部分將代碼按照其邏輯類型分為4個大類。使用這個分類的目的是觀察程序的邏輯類型對算法的影響。

本文實驗并未涉及比較算法在空間上的復雜度差異，其原因是本文方法涉及多次使用檢測工具，其內存消耗包括了多次的預分配和其他支持庫的共享部分與單一使用不具備可比性。同時，本文用以比較的其他算法來自不同框架，其本身內存分配和回收機理不同，也會造成結果的說明性不佳。

實驗使用的測試樣本代碼總共有115段，來自于其他測試樣例和一些實際項目中的典型代碼片段。在實驗的第一個部分中，按照大約200行代碼為一塊對這些代碼進行分片。

單獨使用LLBMC以及2種算法在這些分片上運行的時間消耗比較如表1所示。其中所列的時間是代碼檢測的平均時間。通過比較可以發(fā)現(xiàn)，本文所述的算法在規(guī)模較小的程序檢測中體現(xiàn)出更高的時間消耗。這是因為本文方案對代碼進行了多次掃描，這種掃描造成了潛在的時間消耗。同時，本文使用的方法具有一個啟動過載，這個因素同樣影響了時間消耗。在規(guī)模較大的代碼檢測中，本文方法展現(xiàn)出了優(yōu)勢。

表1 算法時間消耗比較

第二部分實驗結果如表2所示。其中，數(shù)據(jù)代表當前類別在所列算法的檢測中成功返回并返回正確結果的數(shù)量。在前面實驗中已經(jīng)發(fā)現(xiàn)當代碼規(guī)模增大到一定程度時，傳統(tǒng)的有界模型檢測器已無法完成針對代碼的檢測。因此也將代碼規(guī)模限制在這個邊界的附近，從而可以獲得具有比較意義的結果。在第二部分的實驗中也可以發(fā)現(xiàn)，LLBMC在各個類型的代碼中均有檢測失敗的案例。由于給LLBMC設置了無限長的代碼展開，所以這種檢測失敗基本上都是由于狀態(tài)空間過大所引起。本文的2種方案在其上表現(xiàn)很好，這是由于本文方法將模型檢測空間進行了有效限制。

表2 算法成功檢測數(shù)量比較

從實驗結果可以看到，本文方法在LLBMC上可以有效地運行并成功地對相對大規(guī)模的代碼進行檢測，比單純的有界模型檢測算法在規(guī)模上更加強壯，同時在相對較大的規(guī)模代碼上具有一定的時間優(yōu)勢。當然，在實驗中也發(fā)現(xiàn)了在不同的代碼片段上有一定的不穩(wěn)定性。這個現(xiàn)象的原因可能是代碼的局部性在不同的代碼片段上的強弱程度表現(xiàn)不一，這也同時說明了實現(xiàn)屬于一種啟發(fā)式的算法實例。

7 結束語

本文提出了局部性在模型檢測方法中應用的可能性，在描述了形式化定義的基礎之上提出了對應的算法，并通過實驗驗證了其有效性。該方法實際上屬于一種上近似的算法，通過獲取一種局部性的上近似來對目標程序模型的狀態(tài)空間進行分片，然后使用有界模型檢測工具來完成狀態(tài)子空間的檢測。算法理論上可以結合各種有界模型檢測算法，具有可擴展性，同時也具有結合其他模型檢測算法的潛力。在未來的研究中，可以進一步地探討將本文算法嵌入其他模型檢測算法中或將其他模型檢測算法嵌入本文算法中的可能性。

[1] JHALA R, MAJUMDAR R. Software model checking[J]. ACM Computing Surveys. 2009, 41(4): 1-54.

[2] BJORNER N, MCMILLAN K, RYBALCHENKO A. On solving universally quantified horn clauses[C]//The International Symposium on Static Analysis. 2013: 105-125.

[3] CLARKE E, KROENING D, LERDA F. A tool for checking ansi-c programs[C]//The 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2004: 168-176.

[4] CORDEIRO L, LISCHER B, MARQUES S J. SMT-based bounded model checking for embedded ANSIC software[J]. IEEE Transactions on Software Engineering, 2012, 38(4): 137-148.

[5] YANG Z, GANAI M K, GUPTA A, et al. Efficient SAT-based bounded model checking for software verification[J]. Theoretical Computer Science, 2008, 404 (3) : 256-274.

[6] MERZ F, FALKE S, SINZ C. LLBMC: bounded model checking of C and C++ programs using a compiler IR[C]//The International Conference on Verified Software: Theories, Tools, Experiments. 2012: 146-161.

[7] MORSE J, CORDEIRO D, NICOLE D, et al. Handling unbounded loops with ESBMC 1.20[C]//The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2013: 619-622.

[8] DAVIS M, LOGEMANN G, LOVELAND D. A machine program for theorem-proving[J]. Communications of the ACM, 1967, 5(5): 394-397.

[9] HOOKER J N, VINAY V. Branching rules for satisfiability[J]. Journal of Automated Reasoning, 1995 , 15 (3) :359-383.

[10] LI C M, ANBULAGAN A. Heuristics based on unit propagation for satisfiability problems[C]//The 15th International Joint Conference on Artificial Intelligence. 1997 :366-371.

[11] MOURA D, BJORNER N. Z3: an efficient SMT solver[C]//The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2008: 337-340.

[12] LIU L, KONG W, ANDO T. A survey of acceleration techniques for SMT-based bounded model checking[C]//The International Conference on Computer Sciences and Applications. 2013: 554-559.

[13] HENZINGER T A, JHALA R, MAJUMDAR R, et al. Abstractions from proofs[J]. ACM SIGPLAN Notices, 2004 , 39 (1) :232-244.

[14] JHALA R, MCMILLAN K L. Array abstractions from proofs[C]//The International Conference on Computer Aided Verification. 2004: 232-244.

[15] MCMILLAN K L. Lazy abstraction with interpolants[C]//The International Conference on Computer Aided Verification. 123-136.

[16] GULAVANI B S, RAJAMANI S K. Counterexample driven refinement for abstract interpretation[C]//The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2006: 474-488.

[17] FLANAGAN C, QADEER S. Predicate abstraction for software verification[J]. ACM SIGPLAN Notices, 2002, 37 (1) :191-202.

[18] KOMURAVELLI A, GURFINKEL A, CHAKI S. Automatic abstraction in SMT-based unbounded software model checking[C]//The International Conference on Computer Aided Verification. 2013: 846-862.

[19] APEL S, BEYER D, FRIEDBERGER K. Domain types: abstract- domain selection based on variable usage[C]//The International Conference on Hardware and Software: Verification and Testing. 2013: 262-278.

[20] BEYER D, HENZINGER T A, THEODULOZ G. Lazy shape analysis[C]//International Conference on Computer Aided Verification. 2006: 532-546.

[21] HENZINGER T A, JHALA R, MAJUMDAR R, et al. Lazy abstraction[J]. ACM SIGPLAN Notices, 2002, 37(1): 58-70.

[22] BRADLEY A R. SAT-based model checking without unrolling[C]//The International Conference on Verification, Model Checking, and Abstract Interpretation. 2011: 70-87.

[23] RRADLEY A R, MANNA Z. Checking safety by inductive generalization of counterexamples to induction[C]//The International Conference on Formal Methods in Computer Aided Design. 2007: 173-180.

[24] CHAKI S, CLARKE E M, GROCE A, et al. Modular verification of software components in C[J]. IEEE Transactions on Software Engineering, 2004 , 30 (6) :388-402.

[25] BEYER D, KEREMOGLU M E. CPAchecker: a tool for configurable software verification[C]//The International Conference on Computer Aided Verification. 2011:184-190.

[26] BEYER D, LEMBERGER T. Symbolic execution with CEGAR[M]// Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. Springer International Publishing, 2016.

[27] BEYER D, DANGL M, WENDLER P. Boosting K-induction with Continuously-refined Invariants[M]//Computer Aided Verification. Springer International Publishing, 2015: 622-640.

[28] BEYER D, LOWE S. Interpolation for value analysis[J]. Software-Engineering and Management, 2015: 73-74.

[29] BEYER D, WENDLER P. Reuse of verification results[C]//The International Symposium on Model Checking Software. 2013: 1-17.

[30] BEYER D, LOWE S. Explicit-State software model checking based on CEGAR and interpolation[C]//The International Conference on Fundamental Approaches to Software Engineering. 2013: 146-162.

[31] ALBARGHOUTHI A, GURFINKEL A, CHECHIK M. From Under-Approximations to Over-Approximations and Back[C]//The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2012: 157-172.

[32] KROENING D, STRICHMAN O. Decision procedures: an algorithmic point of view[M]. Springer Publishing Company, 2008.

[33] SINZ C, MERZ F, FALKE S. LLBMC: a bounded model checker for LLVM’s intermediate representation[C]//The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2012: 542-544.

[34] BEYER D. Status report on software verification[C]//The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2014: 373-388.

Locality-guided based optimization method for bounded model checker

WANG Shun, DU Ye, HAN Zhen, LIU Jiqiang

Beijing Key Laboratory of Security and Privacy in Intelligent Transportation, Beijing Jiaotong University, Beijing 100044, China

For software model checking, approaches that combine with different kind of verification methods are now under research. The key to improve scale and complexity of verifiable software is handling the method for abstraction widening and strengthening wisely and precisely. To archive that, using extra knowledge that extracted from programming pattern or learned through verifying procedure to help eliminate the redundant state has been proved effective. Definition of program locality was given. It took the important role in accelerating software verification, then the strategy was raised and an algorithm was implemented to take advantage of program locality. This method exploits the features of modern BMC (bounded model checker) and scales up the capability of its power in large scale and comprehensive software modules.

model checking, BMC, software verification, locality, optimization

TP311.1

A

10.11959/j.issn.1000-436x.2018050

2017-06-14；

2018-01-11

北京高校青年英才計劃基金資助項目（No.YETP0548）；國家自然科學基金資助項目（No.61672092）

Beijing Higher Education Young Elite Teacher Project (No.YETP0548), The National Natural Science Foundation of China (No.61672092)

王舜（1988-），男，陜西西安人，北京交通大學博士生，主要研究方向為形式化方法、程序分析技術、信息安全等。

杜曄（1978-），男，黑龍江哈爾濱人，博士，北京交通大學副教授、博士生導師，主要研究方向為網(wǎng)絡安全、態(tài)勢感知、軟件可靠性分析與評估等。

韓臻（1962-），男，浙江寧波人，北京交通大學教授、博士生導師，主要研究方向為可信計算、系統(tǒng)安全、保密技術等。

劉吉強（1973-），男，山東海陽人，北京交通大學教授、博士生導師，主要研究方向為密碼學、可信計算、隱私保護技術等。