基于證據自動機的軟件回歸驗證

賈尚坤,賀 飛

(清華大學 軟件學院, 北京 100084)(*通信作者電子郵箱 hefei@tsinghua.edu.cn)

0 引言

為了保障軟件的正確性與魯棒性,傳統的方法是通過一系列功能與性能相關的測試發現軟件的問題與缺陷。然而,測試方法只能在整個系統或相關功能實現后進行,無法在軟件的需求或設計階段預見系統潛在的問題。另外,測試方法不可能包含所有情況的測試用例,因此無法證明系統不存在缺陷,也無法證明它滿足特定的屬性。而驗證方法則恰好可以解決上述問題。軟件的形式化驗證[1]指的是在軟件系統的抽象數學模型上應用形式化的證明,驗證系統滿足或違反相應的規約和屬性,以確保軟件的正確性。用于建模系統的數學對象包括有限狀態機、Petri網、時間自動機等,而形式化的證明方法則在數理邏輯、自動機、圖論等數學理論基礎之上對系統進行分析與驗證。形式化驗證主要包含定理證明和模型檢測兩種途徑,其中后者由于輕量級和完全自動化在工業界得到了廣泛應用。

多版本迭代是當前軟件開發的普遍狀況。為了節約軟件開發的資金、人力、時間等投入,軟件公司需要用盡可能少的版本迭代為軟件增加更多的新特性。然而,軟件在對自身功能進行擴展的同時,可能會與已有功能產生沖突而引發錯誤,這一現象被稱為“回歸”[2]。為了避免回歸,文獻[3]中首先提出了回歸測試的概念,即用一組覆蓋面盡可能大的回歸測試用例對軟件的新版本進行檢測,報告任何可能出現的新漏洞。但由于回歸測試不可能包含所有的測試用例,因此無法保證所有的新漏洞在軟件發布前都能被提前發現而得到解決。因此,為了確保軟件的安全性與可靠性,需要在軟件的研發進程中引入程序驗證方法。考慮到鄰近版本之間往往有較多的相似性,如果將這些版本視為不同軟件分別進行驗證,將會浪費掉大量的共享信息,從而影響驗證效率。為了利用鄰近版本之間的共享信息,學者又提出了回歸模型檢測[4]與回歸驗證[5]的概念。最初回歸驗證指的是證明相關聯程序的等價性,即:程序P1與P2的任意可終止的執行若具有相同的輸入,則運行結束后將得到相同的返回值。后來人們用回歸驗證表示將形式化驗證技術應用到連續檢測的開發版本中,利用鄰近版本之間的共享信息驗證程序屬性。

而對于證據(witness),最開始更多被用來描述驗證工具在系統違反驗證屬性時生成的錯誤路徑,它們在復現系統的錯誤中扮演了“見證人”的角色。后來證據的含義得到擴展,指的是軟件驗證工具在驗證完成后生成的一個驗證結果輔助文件,用來對驗證程序進行再檢驗,進而確定程序是否如驗證結果所說滿足或違反其驗證屬性[6],如圖1所示。證據需要有統一的格式,這樣不僅方便不同驗證工具的交互,也有助于證據文件的可讀性與可視化。目前在國際軟件驗證大賽(Competition on Software Verification, SV-COMP)上采用的證據文件格式為GraphML(一種可擴展標記語言),其中定義了一個非確定有限自動機,即證據自動機。自動機的節點表示一個程序位置(對應程序計數器的一個值),自動機的邊表示控制流從邊的起點到終點時程序執行的操作(對應一條程序語句),整個證據自動機刻畫了程序的大致結構。圖2給出了一個證據自動機的示例,自動機每個節點上的編號對應一個程序位置,而每條邊除了對應的程序語句之外,還包含起始行號、偏移量等相關的定位信息。

圖1 證據文件的生成與檢驗Fig. 1 Generation and validation of witness files

圖2 證據自動機示例Fig. 2 Example of witness automata

根據驗證結果的不同(不考慮超時等未知驗證結果),證據分為正確證據(correctness witness)[7]與違反證據(violation witnesss)[8]兩類,分別表示程序滿足或違反其驗證屬性。二者的內涵也有所不同,正確證據包含了程序驗證得到的循環不變式,而違反證據記錄了程序驗證過程中到達錯誤狀態的反例路徑信息。由于回歸驗證的關鍵在于鄰近版本之間的共享信息,因此基于證據自動機的回歸驗證的主要目標是提取并重用證據文件中的共享信息。對于鄰近版本的程序而言,若均滿足驗證屬性,則相同或相近程序位置處成立的不變式很可能相差不大;而若均違反驗證屬性,前一版本的反例路徑在后一版本中未必有效,即使有效也未必導向錯誤狀態。因此,基于證據自動機的回歸驗證主要指的是提取并重用之前版本正確證據中的循環不變式,對多版本程序進行回歸驗證。

歷屆國際軟件驗證大賽都要求所有參賽工具提供能夠復現驗證結果的證據文件,從SV-COMP 2015開始規定了反例文件的格式并要求為屬性違反提供違反證據[9],從SV-COMP 2017開始規定了正確文件的格式并要求為屬性滿足提供正確證據[10]。但大多數能生成證據文件的驗證工具并不能利用證據文件中的信息,截至SV-COMP 2017只有可配置程序分析檢測工具(Configurable Program Analysis checker, CPAchecker)和終極自動機驗證工具(Ultimate Automizer, UAutomizer)被選為證據文件的檢驗工具[10]。由于UAutomizer對證據文件中循環不變式的利用效率偏低[7],因此本文在CPAchecker源代碼的基礎上實現回歸驗證功能。CPAchecker是一個應用可配置程序分析(configurable program analysis)框架[11]整合各種軟件分析與驗證技術的開源工具[12],可以通過命令行或Eclipse插件運行。

1 證據預處理

對于多版本程序而言,即便鄰近版本的程序結構也會存在一定的差異,因此上一個版本的證據文件并不能直接應用到下一個版本的驗證中。為了利用之前版本證據自動機中的不變式信息,需要對證據文件進行相應的預處理。預處理大致可以分為兩個部分:影響域分析與證據文件生成。整個預處理過程如圖3所示。證據預處理的相關實現已被整合到CPAchecker源碼中。

圖3 證據預處理Fig. 3 Witness preprocessing

1.1 影響域分析

影響域分析的目的在于確定版本變動對原證據文件中不變式的影響。不受影響的不變式可以直接重用,而受影響的不變式在新版程序中可能仍然成立,需要進一步檢驗。影響域分析分為三步:比較新舊程序、生成混合程序、得到影響結果。

比較新舊程序主要用到了Linux系統中的diff命令:

diff -b -B -H -n old.c new.c

其中:-b用于忽視空格字符;-B用于忽視空白行;-H用于提高大文件比較的速度;-n用于修改輸出格式。通過調用diff命令比較新舊版本程序的文本差異,并將比較結果重定向到差異文件diff.txt中。diff.txt包含了新版程序相對于舊版程序增加和刪除的語句信息,例如對于diff.txt中的以下內容:

a6 1

int c=a+b;

d12 2

其中:a和d分別表示增加和刪除。a和d后面的第一個數字表示舊版程序的行號;第二個數字表示增加或刪除的代碼行數,若為增加還會在后面附加具體的語句。

生成混合程序通過將原證據文件old-witness與差異文件diff.txt的信息綜合到舊版程序old.c中,得到用于影響域分析的混合程序mix.c。old-witness的信息主要指證據自動機節點上的循環不變式。由圖2可知,自動機節點可以通過其入邊與出邊在程序中定位,因而可以將節點上的不變式作為布爾表達式插入到相應的程序位置。之后將diff.txt中的新增語句插入混合程序,并且在新增語句和刪除語句前加上影響標注:

/*@ impact pragma stmt; */

由混合程序mix.c調用Frama-C的影響域分析插件即可得到版本變動語句對原證據文件中不變式的影響結果。Frama-C是一個面向大規模C程序驗證的源碼分析平臺[13],通過整合相關插件實現各種分析與驗證功能。通過圖形界面或命令行調用Frama-C的影響域分析插件,可以分析帶有影響標注的語句對其他語句的影響。調用該插件的具體命令如下:

frama-c -impact-pragma -impact-print

-impact-log r:impact.txt -val-initialized-locals mix.c

-impact-pragma后接函數名表示在相應的函數中檢測影響標注。由于影響標注在所有函數中都可能出現,因此需要調用CPAchecker的相關接口getAllFunctionNames獲取程序所有的函數名。又因為CPAchecker在生成證據自動機時會對程序進行預處理,從混合程序看來自動機節點上不變式中的變量在相應的程序位置處可能尚未初始化,如果直接對這樣的程序進行影響域分析將無法得到正確的影響結果,因此需要用-val-initialized-locals選項對所有的局部變量進行初始化。影響域分析的結果保存在文件impact.txt中。

1.2 證據文件生成

得到影響域分析結果之后,未受影響的不變式可以直接重用。而由于受影響的不變式在新版程序中可能仍然成立,需要將其寫入用于進一步檢驗的新證據文件new-witness。生成new-witness的目的是如果之后的版本迭代不改變程序結構,可以直接將new-witness作為驗證后面版本的輸入,從而省去證據預處理過程。

生成new-witness之前,需要從原證據文件old-witness中提取受影響不變式的相關信息,包括不變式的內容、所屬的節點編號、在程序中的作用域以及與所屬節點相關聯的邊。邊上的代碼行號關系到不變式在新證據自動機中的定位,而由于版本變動,舊版程序的代碼行號在新版程序中也會相應變化。因此,需要對行號進行相應的轉換,轉換方法如算法1所示。

算法1 新舊代碼行號轉換。

輸入 舊版程序代碼行數len,新舊版本差異文件diff.txt。

輸出 整型數組oldToNew[],數組下標和相應的元素值分別表示舊版程序及其在新版程序中對應的代碼行號(均從0開始)。

1)

新建一個大小為len的整型數組oldToNew[],并將其每一項初始化為0

2)

對于diff.txt中的每一行diffline:

3)

解析diffline,得到變動類型type、行號number與行數count

4)

if (type==′d′)

5)

oldToNew[number-1] -=count

6)

else

7)

oldToNew[number]+=count

8)

diff.txt繼續向后讀取count行

9)

intlastIndex=0

10)

for (inti=1;i

11)

oldToNew[i]+=oldToNew[i-1]+1

12)

for (inti=len-1;i>=0; --i)

13)

if (oldToNew[i]>=0)

14)

lastIndex=oldToNew[i]

15)

else

16)

oldToNew[i]=lastIndex

預處理過程改寫了CPAchecker的接口writeProofWitness,在得到不變式相關信息之后,可以由該接口將其寫入新證據文件。對于原證據文件中一條與不變式所屬節點相關聯的邊,找出它經過行號轉換后在新證據自動機中對應的邊,若二者的控制條件一致,則在新證據自動機中的對應節點上附加相應的不變式信息。然后通過合并冗余節點及其不變式,得到最終的新證據自動機,再調用CPAchecker中GraphML構造器GraphMlBuilder的appendTo方法生成新證據文件new-witness。new-witness刻畫了新版程序的大致結構,因而可以應用到新版程序的驗證中。

2 回歸驗證過程

對新版程序進行回歸驗證的關鍵在于提取并重用原證據文件中的不變式信息。不受版本變動影響的不變式可以直接重用,而受影響的不變式則需要在新證據文件中檢驗通過后才能重用。檢驗新證據文件及驗證新版程序的回歸驗證算法基于CPAchecker中用輔助不變式增強的k-歸納(k-induction)算法。

2.1 k-induction及其增強

k-induction最初作為有限狀態遷移系統基于可滿足性判定的一種驗證技術,被用于硬件設計與轉移關系的驗證[14]。后來k-induction技術逐漸應用到軟件分析與驗證領域,如直接內存訪問競爭分析[15]、同步程序分析[16]與嵌入式軟件驗證[17]等。

對于一個表示程序的狀態遷移系統,s和s′為其中的兩個狀態變量,I(s)表示s為初始狀態,T(s,s′)表示存在s到s′的狀態轉移,P(s)表示程序的安全屬性P在s上成立。給定一個任意的正整數k,分兩步說明k-induction的驗證過程。

為了用k-induction證明程序,首先需要驗證P在從初始狀態s1出發k步內可達的所有狀態s1,s2, …,sk上均成立,也就是式(1)不可滿足:

(1)

接下來,還需要驗證只要P在任意k個連續狀態sn,sn+1, …,sn+k-1上成立,P在第k+1個狀態sn+k上就一定成立,也就是式(2)不可滿足:

(2)

由上述兩步即可驗證程序的正確性。若式(1)可以滿足,則程序違反其驗證屬性;若式(2)可以滿足,則在當前k值下無法驗證程序(程序可能滿足或違反其驗證屬性)。

k-induction驗證是歸納方法在軟件驗證中的應用,連續k+1個狀態可以看作程序循環的k次展開。當k=1時,k-induction退化為標準歸納方法,且隨著k的增大,式(2)的歸納假設隨之不斷增強,從而使證明變得更容易。但若要使用k-induction,程序的安全屬性P必須滿足相應的可歸約性(即式(2)不可滿足),否則在當前k值下無法驗證程序。

為了將k-induction推廣到一般程序,Beyer等[18]提出了用輔助不變式增強的k-induction算法。具體來說,就是用與k-induction算法并行的不變式生成算法為程序生成不斷強化的循環不變式,在k-induction的每輪驗證中用當前已知的不變式Inv增強式(2)的歸納假設,也就是改為證明式(3)不可滿足:

(3)

CPAchecker總的k-induction驗證流程如下:1)首先初始化一個較小的k值，以當前的k值為界,調用有界模型檢測(bounded model checking)算法驗證式(1)的可滿足性,若其可滿足,則發現了一條程序的錯誤路徑,結束驗證；2)若式(1)不可滿足,則在當前已知不變式的輔助下驗證式(3)的可滿足性,若其不可滿足,則程序正確性得證；3)若式(3)可以滿足,且在前面的驗證過程中并行算法生成了更強的不變式,則在新不變式的輔助下重新驗證式(3)的可滿足性；4)若式(3)始終可以滿足,則說明在當前k值與輔助不變式下無法驗證程序的正確性，此時CPAchecker會增大k值進行下一輪驗證,直到得出驗證結果或超時為止。

2.2 基于不同不變式生成策略的回歸驗證

CPAchecker通過用不斷強化的不變式增強k-induction的歸納假設以驗證程序的正確性。但如果k-induction驗證的不是程序的安全屬性,而是一些不變式的候選(如證據自動機中待檢驗的不變式),將驗證成立的候選作為輔助不變式提供出去,則k-induction本身也可以作為不變式生成算法。

用CPAchecker的原有配置即可并行兩個k-induction算法,其中一個k-induction(下稱“從KI”)為另一個k-induction(下稱“主KI”)提供輔助不變式,而后者負責驗證程序的正確性。該配置取程序所有到達錯誤狀態的控制流路徑的否定作為從KI的候選不變式[18]。每當從KI成功證明一條候選不變式λ,從KI就將λ加入輔助不變式提供給主KI以增強主KI的歸納假設;同時λ作為從KI的已知不變式,在從KI驗證其他候選不變式時也會增強從KI的歸納假設。隨著k不斷增大,從KI證明的候選不變式不斷增多,提供給主KI的輔助不變式也不斷增強。

在上述配置的基礎上,提取新證據文件中受版本變動影響的不變式加入從KI的候選不變式,用證據預處理得到的不受影響的不變式增強主KI的歸納假設,即可實現基于證據自動機的回歸驗證,如圖4所示。除了原有配置的候選不變式,此過程主要用證據自動機中的不變式信息增強主KI的歸納假設,但證據文件包含的不變式可能不足以輔助程序驗證[7]。因此,只用從KI生成輔助不變式的回歸驗證可能得不到足夠強的歸納假設。

圖4 基于證據自動機的回歸驗證Fig. 4 Regression verification based on witness automata

除了k-induction之外,CPAchecker還可用可配置程序分析算法(Configurable Program Analysis Algorithm, CPAAlgorithm)[19]執行數據流分析生成輔助不變式。CPAAlgorithm通過廣度優先搜索維護可達抽象狀態的集合,動態更新每個狀態上的不變式,在每次迭代結束后將所有狀態上不變式的析取與當前不變式的合取作為輔助不變式提供給主KI。由于CPAAlgorithm應用了動態精度調整,在迭代過程中會不斷增加重要程序變量的數目和表達式的嵌套深度,因此產生的輔助不變式也是經過連續精化的[20]。

既然k-induction和CPAAlgorithm都能生成輔助不變式,可以通過并行主KI、從KI與CPAAlgorithm,在回歸驗證中將證據自動機中的不變式信息與數據流分析生成的輔助不變式相結合。如圖5所示,既可用數據流分析生成的輔助不變式增強從KI的歸納假設,再由從KI將其提供給主KI間接增強主KI的歸納假設(用虛線表示),又可以將數據流分析與從KI生成的兩部分輔助不變式合并后直接增強主KI的歸納假設(用點劃線表示)。

圖5 結合數據流分析的回歸驗證Fig. 5 Regression verification combined with data flow analysis

CPAchecker為用輔助不變式增強的k-induction算法實現了三種不變式生成策略,其中除了不生成不變式的策略DO_NOTHING之外,INDUCTION接受從KI生成的不變式,REACHED_SET接受數據流分析生成的不變式。本文另外實現了新策略KIDF,用來同時接受從KI與數據流分析生成的不變式。

3 實驗

本章主要介紹不使用證據自動機中不變式信息的直接驗證與2.2節介紹的三種回歸驗證之間的對比實驗。為了方便表述,下面引入相應的符號記法。

3.1 回歸測例

實驗的原始測例來自于國際軟件驗證大賽的驗證任務集(https://github.com/sosy-lab/sv-benchmarks)。整個驗證任務集包含了使用C語言(遵循GNU C標準)、Java語言、霍恩(Horn)子句的待驗證程序,涵蓋了可達性、內存安全、并發安全、可終止性、溢出檢測等各個方面的驗證。驗證任務集主要為歷屆國際軟件驗證大賽提供統一的、覆蓋面盡可能廣的測例程序,同時也被許多研究項目用于評估軟件驗證算法的驗證性能。

由于測例程序被用于回歸驗證實驗,選取原始測例時需要考慮與回歸驗證方法的契合度。由于屬性違反時的證據文件不包含不變式信息,而回歸驗證的核心思想是提取并重用證據文件中的循環不變式,因此選取原始測例時要排除驗證任務集中違反驗證屬性的程序。另外,由于原始測例程序互不相關,為了由原始測例生成體現版本迭代過程的回歸測例,還需要考慮原始測例的變異效果。綜上,為了在對比實驗中更好地體現回歸驗證的作用,本文從驗證任務集C語言分支下與Linux內核相關更適合變異的ldv-linux-3.4-simple文件夾中隨機選取了56個滿足驗證屬性的程序作為版本迭代前的原始測例程序。

而為了由原始測例得到回歸測例,需要將原始測例中的每個程序看作獨立分支下的初始版本,在初始版本的基礎上依次進行程序變異得到該分支下的其他版本。進行回歸驗證時,上一個版本的證據文件作為下一個版本程序驗證的輸入。由于要驗證不變式重用的效果,與選取原始測例時類似,變異程序時同樣需要舍棄違反驗證屬性的版本。

對于每一個原始測例程序P0,用開源C程序變異工具Milu[21]對其進行變異得到P1,若P1滿足其驗證屬性(用CPAchecker和UAutomizer參與國際軟件驗證大賽的標準配置對P1的驗證結果均為true),再在P1的基礎上變異得到P2；否則重新由P0變異P1。類似可得P3、P4、P5,從P0到P5代表了一系列版本迭代的完整流程。這樣就得到了56組用于回歸驗證的測例程序,每組回歸測例包含6個版本。

本文用獨立于驗證工具的輕量級開源基準測試(benchmarking)框架BenchExec[22]對所有回歸測例進行批量驗證,統計其驗證結果、時間與內存消耗。BenchExec接受一個XML文件作為輸入,XML文件定義了待執行命令、資源使用限制與驗證任務集合。在本實驗中,BenchExec調用CPAchecker驗證所有測例程序,時間限制為200 s,內存限制為4 GB,CPU核心數限制為4。

3.2 運行環境

實驗機器的CPU為i5-4590 (3.30 GHz×4),內存為8 GB,操作系統為Ubuntu 16.04 (64位)。實驗所用的CPAchecker版本為1.6.1-svn,Frama-C版本為16.0-Sulfur-beta,Milu版本為3.0,BenchExec版本為1.14。

3.3 實驗結果與分析

表1 base.properties新增配置項Tab. 1 Additional configuration options in base.properties

表2 對比實驗結果Tab. 2 Contrast experiment results

BenchExec調用CPAchecker得到的驗證結果可能為true、 false或unknown,分別表示屬性滿足、屬性違反或無法確定(原因可能是運行錯誤、超時或內存不足等)。由于本實驗在原始測例選取和版本變異時均確保程序滿足其驗證屬性,因此驗證結果為true對應表2的正確計數,驗證結果為false對應錯誤計數,而當驗證結果為unknown時,驗證時間不足200 s(即由超時以外的原因導致驗證結果無法確定)對應錯誤計數,反之對應超時計數。由表2可知,除了因驗證時間限制引起的部分超時(國際軟件驗證大賽的超時時間一般設置為900 s,而本實驗為200 s),所有驗證方式得到的驗證結果均為true,與CPAchecker和UAutomizer標準參賽配置的驗證結果相一致,說明了實驗結果的正確性。

4 結語

在多版本程序的驗證中,為了利用鄰近版本之間的共享信息,本文提出了基于證據自動機的回歸驗證。基于CPAchecker中用輔助不變式增強的k-induction算法,本文設計并實現了三種使用不同不變式生成策略的回歸驗證方法,并與不使用不變式信息的直接驗證進行了對比實驗。實驗結果表明，當程序滿足其驗證屬性時,基于證據自動機的回歸驗證能極大地提高驗證效率,而將證據自動機與數據流分析相結合的驗證方式能得到更好的驗證效果。

由于證據文件包含的不變式可能不足以輔助程序驗證或不一定必需,基于證據自動機的回歸驗證仍然存在一定的局限性,三種回歸驗證方法之間的對比結果也反映了這一點。在已有回歸驗證實現的基礎上,未來的工作方向主要在于改進不變式生成方法,提高證據文件中的不變式質量,使得只基于證據自動機的回歸驗證就能得到足夠好的驗證效果。