靜態(tài)程序分析過程中形式化驗證工具Frama-C的應(yīng)用

崔少軒 喻壵慎

摘要：軟件的靜態(tài)程序分析是確保軟件安全可靠的一種有效手段。常見的形式化的靜態(tài)分析工具一般是基于模型檢測，定理證明或抽象解釋理論來對軟件進行分析驗證。然而，基于單一理論的驗證工具具有一定的局限性。介紹了一個開源的靜態(tài)分析平臺Frama-C，根據(jù)該工具的特點，分別使用不同的插件對一小段代碼進行靜態(tài)分析，有助于將不同的程序分析方法相結(jié)合。最后對如何使用Frama-C工具解決航空控制軟件等安全關(guān)鍵軟件的執(zhí)行時間分析問題的過程進行了演示。

關(guān)鍵詞：靜態(tài)程序分析;形式化驗證;Frama-C

中圖分類號：TP391

文獻標(biāo)識碼：A

隨著計算機技術(shù)在安全關(guān)鍵領(lǐng)域的廣泛應(yīng)用，計算結(jié)果的準(zhǔn)確性和產(chǎn)生計算結(jié)果的時間屬性稱為人們關(guān)注的焦點。一般采用軟件測試的方法來保證程序的正確性。但是在測試過程中又不可能將程序所有的輸入情況和執(zhí)行條件覆蓋在內(nèi)。為了對軟件的質(zhì)量進行更加完備的評估，現(xiàn)在學(xué)術(shù)界正在廣泛地研究使用形式化的靜態(tài)分析方法來對軟件的性質(zhì)進行分析驗證。但是形式化驗證方法在實際應(yīng)用中使用程度不高。一方面是一些形式化的驗證工具的自動化程度不高，需要用戶有較高的理論基礎(chǔ)才能使用，因而難以被推廣。另一方面，許多形式化驗證工具的只是基于一種形式化驗證方法，難以兼顧不同形式化驗證方法的優(yōu)點。

第1節(jié)簡單描述了模型檢測，定理證明和抽象解釋理論的基本原理，并且對這3中形式化的分析方法進行比較。第2節(jié)介紹了一種自動化程度較高的開源的軟件靜態(tài)分析平臺Frama-C以及基于該平臺的常用插件。第3節(jié)結(jié)合Frama-C平臺上插件之間的特點，分別使用程序切片，程序標(biāo)注和基于Widening算子的值分析插件對一段循環(huán)程序中的變量的運行結(jié)果進行計算。第4節(jié)就航空發(fā)動機等一系列控制軟件所要面臨的程序執(zhí)行時間分析過程中對循環(huán)結(jié)構(gòu)的迭代次數(shù)的估算問題，使用Frama-C工具的應(yīng)用過程進行了簡單的演示。最后在第5節(jié)中對本文的工作以及研究現(xiàn)狀進行了總結(jié)。

1 相關(guān)工作

靜態(tài)程序分析是指在不實際執(zhí)行程序的情況下對計算機軟件進行分析[1]。它常常作為動態(tài)測試的補充來保證程序的正確性。目前主要的靜態(tài)分析方法主要有模型檢測，定理證明和抽象解釋。

1.1 模型檢測

模型檢測是一種探測系統(tǒng)所有可能的狀態(tài)的驗證技術(shù)[2]。模型檢測通過遍歷遷移系統(tǒng)所有狀態(tài)空間，對遍歷到的系統(tǒng)進行自動驗證，并且對不滿足驗證性質(zhì)的情況自動構(gòu)造反例。模型檢測的本質(zhì)是驗證一個給定的系統(tǒng)的形式化模型滿足規(guī)約條件。其基本思想是使用遷移系統(tǒng)（S）表示系統(tǒng)的行為，用模態(tài)邏輯或時序邏輯公式（F）描述系統(tǒng)的性質(zhì)。將“系統(tǒng)是否具有所期望的性質(zhì)”的問題轉(zhuǎn)化為“狀態(tài)遷移系統(tǒng)S是否是滿足公式F的一個模型”的問題[3]。早期的模型檢測技術(shù)被廣泛應(yīng)用于抽象系統(tǒng)模型以及硬件系統(tǒng)的模型，但最近模型檢測技術(shù)已經(jīng)被廣泛應(yīng)用與諸如C程序或Java程序的軟件系統(tǒng)中[4][5]。

1.2 定理證明

定理證明是一種證明邏輯公式有效性的演繹證明方法。定理證明方法通過使用推導(dǎo)規(guī)則對邏輯公式進行證明[6]。通過定理證明工具編程者可以交互式地或自動地驗證公式的正確性。定理證明的基本思想是將軟件系統(tǒng)和性質(zhì)都用邏輯方法來規(guī)約，通過基于公理和推理規(guī)則組成的形式系統(tǒng)，以如同數(shù)學(xué)中定理證明的方法來證明軟件系統(tǒng)是否具備所期望的關(guān)鍵性質(zhì)[7]。

1.3 抽象解釋

抽象解釋理論[8]是一套抽象和構(gòu)建逼近的理論，它提供了一個通用框架來設(shè)計和構(gòu)建靜態(tài)分析以自動化地推導(dǎo)程序的靜態(tài)性質(zhì)[9]。抽象解釋理論的作用對象是對復(fù)雜或無窮系統(tǒng)以及進行形式化表述的數(shù)學(xué)結(jié)構(gòu)以及推導(dǎo)或驗證這些系統(tǒng)的組合或不可判定的性質(zhì)[10]。抽象解釋理論的提出就是為了在對程序進行靜態(tài)分析時構(gòu)造和逼近程序的不動點語義。抽象解釋嚴(yán)格定義了具體程序語義與抽象形式語義之間的關(guān)系、正確性與精確性等不依賴于特定應(yīng)用的抽象數(shù)學(xué)概念。它的本質(zhì)是在計算效率和計算精度之間取得均衡，以損失計算精度求得計算可行性，再通過迭代計算計算增強計算精度的一種抽象逼近方法[11]。

與模型檢測技術(shù)相比，采用抽象解釋的基本理論為分析框架，在模型檢測方法中去掉一些無關(guān)信息，通過狀態(tài)集合之間的映射關(guān)系構(gòu)造抽象模型，可以有效解決模型檢測方法中狀態(tài)空間爆炸的問題。與定理證明相比，一階邏輯是半可判定的，定理證明不能保證停機問題，而抽象解釋是解決不可判定問題的一種有效的方法。由此可見將不同的形式化驗證方法進行有效的結(jié)合的新的形式化驗證工具是十分必要的。

2 Frama-C工具簡介

Frama-C就是一個基于不同理論對程序進行分析驗證的平臺。它的分析對象是C程序源代碼。如圖1給出了Frama-C的基本框架。這個平臺基于同一個核（ kemel），并且使用同一種形式化的規(guī)約語言ACSL即標(biāo)準(zhǔn)C規(guī)約語言（ANSI C Specifi-cation Language）用于對C程序做標(biāo)注（annota-tion），因此基于Frama-C平臺開發(fā)的一系列插件可以合作用于對軟件進行靜態(tài)分析，推導(dǎo)證明以及測試[12]。同時，F(xiàn)rama-C也提供了一些可擴展的API方便用戶開發(fā)插件。其中，F(xiàn)rama-C平臺上基于抽象解釋，演繹驗證和具體的符號執(zhí)行測試開發(fā)三個基本的插件，并在此基礎(chǔ)上衍生了一些列其他的插件。一些常見的Frama-C插件如表1所示。

Frama-C的插件之間可以組合使用得益于構(gòu)建在該平臺上的各插件之間共享使用Frama-C提供的一種形式化的行為規(guī)約語言ACSL，用戶對程序的功能特性進行描述。針對Frama-C上的幾個常用插件的簡單介紹如下：

（1）基于抽象解釋的值分析插件

Frama-C的值分析插件基于抽象解釋原理，能夠自動地計算程序變量在不同的程序點中可能的取值，并且對潛在的運行時錯誤發(fā)出警報。類似的商業(yè)化的軟件例如Polyspace和Astree也有這些的功能。但是Frama-C的值分析插件除了具有開源的優(yōu)勢外，更顯著的不同的是，F(xiàn)rama-C的值分析插件可以應(yīng)用于滿足ISO C99標(biāo)準(zhǔn)的所有源代碼，而并不針對某一特定的應(yīng)用領(lǐng)域。除此之外Value插件的獨特之處在于它根植于Frama-C的系統(tǒng)框架中，其結(jié)果能夠別Frama-C的其它插件重用。

（2）基于推導(dǎo)驗證的Jessie和WP插件

這兩個插件基于最弱前置條件技術(shù)，用于證明C代碼滿足使用ACSL描述的程序規(guī)約。推導(dǎo)驗證的方法是基于模型的。對一個C程序，使用抽象表達的算法模型來對整數(shù)或浮點數(shù)進行描述，使用內(nèi)存模型對程序的存儲進行抽象。而使用WP插件能夠減緩驗證條件，獨立于特定的模型.對于算法模型，用戶可以使用選擇整數(shù)、浮點數(shù)機器整數(shù)、實數(shù)或浮點數(shù)。而WP插件的內(nèi)存模型直接收到最弱前置條件算子的啟發(fā)，假定程序中是不包含指針的。

（3）基于程序流分析的切片插件

Frama-C的切片插件（slicing）將原有的代碼的一個子集作為輸出。產(chǎn)生切片程序的依據(jù)是用戶提供的切片準(zhǔn)則。并且作為輸出的切片程序仍然是與原程序具有相同行為的可編譯的C代碼。

3 應(yīng)用示例

與一些基于模型檢測或定理證明或抽象解釋理論等單一理論的形式化驗證工具相比，F(xiàn)rama-C基于不同理論的插件之間能夠互相協(xié)作有利于兼顧不同理論的優(yōu)點。產(chǎn)生了基于Frama-C平臺的組合驗證策略。通過使用一個插件的輸出作為另一個插件的輸入，可以將不同的分析驗證理論相結(jié)合。例如，首先可以在如下代碼段中使用Frama-C的Slicing插件對程序中與循環(huán)相關(guān)的變量進行切片，得到與循環(huán)相關(guān)的切片程序如圖2所示：

由切片程序可以得到與循環(huán)相關(guān)的程序變量i，j，n，顯然，n的大小在整個循環(huán)過程中不變。由此我們在程序中對相關(guān)的循環(huán)變量添加形如/*@looppragma WIDEN_HINTS vl，，vn，el，…，em;術(shù)/的標(biāo)注來指定循環(huán)迭代的次數(shù)，如圖3所示：

最后，使用Value Analysis插件對循環(huán)進行分析得到變量i，j的在程序運行后可能運行結(jié)果：

[value]======VALUES COMPUTED======

[value] Values at end of function main：

i∈{13;14;15）

j∈[0_55]

n∈{13）

此外，針對循環(huán)，值分析插件分別提供了不同的循環(huán)選項，分別是在缺省狀態(tài)下計算循環(huán)中變量的取值范圍（ default），強制指定循環(huán)邊界（stipulat-ing），以及對循環(huán)的句法展開（syntactic unrolling）和語義展開（ semantic unrolling），如表2給出了針對不同的循環(huán)處理，得到最終變量的取值范圍。

4 應(yīng)用領(lǐng)域

在一些安全關(guān)鍵領(lǐng)域的程序分析驗證過程中，形式化的分析驗證方法對軟件的安全性質(zhì)驗證具有重要的作用。例如在一些實時的安全關(guān)鍵系統(tǒng)中，比如航空發(fā)動機系統(tǒng)，飛機的襟縫翼控制系統(tǒng)，對程序能夠在規(guī)定的時間范圍內(nèi)完成指定的任務(wù)有較高的要求。在對程序的執(zhí)行時間進行分析時，需要對程序的軟件執(zhí)行過程和程序所運行的硬件環(huán)境進行分析。其中軟件的執(zhí)行過程的分析過程中著重考慮的是程序的執(zhí)行路徑。例如程序在執(zhí)行過程中循環(huán)結(jié)構(gòu)的迭代次數(shù)等問題。為此需要采用Frama-C的切片插件將程序執(zhí)行過程中與循環(huán)相關(guān)的程序語句作為切片的結(jié)果。例如在某程序的切片處理后得到如圖所示的切片結(jié)果。切片程序中僅僅保留了與循環(huán)迭代相關(guān)的程序語句?，F(xiàn)在對該程序的循環(huán)迭代次數(shù)進行估計。

input（i）;//循環(huán)變量i=[1..4]

while（i<10）f

input（j）;//循環(huán)變量j=[1..4]

while（j<10）f

j=j+2;

}

i++：

）

通過使用Frama-C的值分析插件對程序中的循環(huán)變量進行分析之后得到i和j取值分別為：l=[1;。10]，j=[1。。10]。在較為粗糙的循環(huán)邊界計算過程中，可以簡單的認(rèn)定程序的循環(huán)邊界為10*10=100次，實際的程序循環(huán)迭代次數(shù)顯然是小于這個值的。將變量i和j的初始值i=[1。。4]，j=[1。。4]帶人切片程序中，循環(huán)的迭代過程中計算結(jié)果如表3所示：

不難估算程序的循環(huán)邊界為10：1：5=45次。為了對驗證估值45是否可以作為更加精確的程序循環(huán)邊界，首先使用Frama-C值分析插件中對循環(huán)進行展開的模塊在設(shè)置循環(huán)展開100次是得到如圖4所示結(jié)果：

顯見，在循環(huán)展開100次之前循環(huán)變量i和j的取值已經(jīng)滿足了循環(huán)的退出條件，循環(huán)的實際迭代次數(shù)小于100。為了對45進行驗證，設(shè)定循環(huán)的展開次數(shù)為45次，仍然得到如上圖所示的結(jié)果。從而證明45次可以做為相對100次更加精確的循環(huán)迭代次數(shù)。在對程序的循環(huán)邊界進行分析過程中，獲取較為精確的循環(huán)邊界對程序的執(zhí)行時間分析具有中要的意義，尤其是程序的循環(huán)上界對航空發(fā)動機系統(tǒng)的最壞執(zhí)行時間（ Worst Case ExecutionTime，WCET）的分析過程中意義重大。

5 結(jié)論

第3節(jié)的示例是簡單展示了Frama-C平臺上Slicing插件和Value Analysis插件的使用，使得不同原理的靜態(tài)分析技術(shù)可以組合使用完成程序的靜態(tài)分析過程。在第4小節(jié)中針對一些航空控制軟件普遍面臨的執(zhí)行時間分析的問題中如何使用Frama-C進行程序的循環(huán)邊界的分析驗證過程進行了簡單的演示。而在[13]的案例程序分析過程中，使用通過迭代使用Value Analysis插件和WP插件不斷對程序添加標(biāo)注以及分析來對程序進行驗證。類似的分析驗證策略還出現(xiàn)在軟件最壞執(zhí)行時間分析軟件SWEET[14]中，首先對程序進行切片，計算循環(huán)邊界最后依據(jù)程序標(biāo)注中的不變式對產(chǎn)生的循環(huán)邊界進行精化，能夠得到較為精確的循環(huán)邊界。這些案例表明支持使用不同靜態(tài)分析技術(shù)的形式化分析驗證平臺對軟件的形式化分析驗證意義重大。

參考文獻

[1]

WICHMANN B A，CANNING A A.Industrial perspective on staticanalysis[J].Software Engineering Journal. 1995，10（2）：69-75.

[2] BAIER C.KATOEN J P.Principles of model checking [M]. TheMIT Press Camhridge， Massachusetts， 2008.

[3] LIN H M.ZHANG W|L Model checking：theories，techniquesand applications[J]. ACTS ELECTRONICA SINICA.2002.30（12）：1907-1910.

[4]

VISSER W，HAVELUND K.BRAT G， et al.Model checking pro-grams[J]. Automated Software Engineering;， 2003， 10（2）：203- 232.

[5]

BEYER D.KEREMOGLU M E.A tool for configurahle softwareverification[J].Computer Aided Verification（ CAV' 11）， 2011，184-190.

[6]

SCHUMANN J M.Automated theorem proving in software engi-neering[M].Springer， Berlin， 2001.

[7]

CHEN H W.WANG J. DONG W. High confidence software engi-neering technologies [J]. ACTA ELECTRONICA SINICA . 2003 .31（12） ：1933-1938.

[8] COUSOT P. COUSOT R. Abstract interpretation ： a unified latticemodel for static analysis of programs by construction or approxi- mation of fixpoints [C]. Proc. of the 4th POPL. Los Angeles ： ACMPress . 1977 ： 23 8-252.

[9] CHEN L Q， WANG J.HOU S N. An abstract domain of one-vari-ahle interval linear inequalities

[J]. Chinese Jouranl of Comput-ers . 2010 . 33 （3） ： 238-252.

[10]

COUSOT P . COUSOT R. Ahstract interpretation ： past ， present andfuture [C]. CSL-LICS '14 Proceedings of the Joint Meeting of theTwenty-Third EACSL Annual Conference on Computer ScienceLogic

（CSL） and the Twenty-Ninth Annual ACM/IEEE Sympo-sium on Logic in Computer Science （ LICS ） .2014.

[11] LI M J， Li Z J .CHEN H W. Program verification techniques basedon the abstract interpretation theory [J]. Journal of Software.2008 .19（ 1） ： 17-26.

[12] KIRCHNER F.KOSMATOV N.PREVOSTO et al. Frama -C ： asoftware analysis perspective

[J] . Formal Aspects of Computing ，2015 .27（ 3 ） ： 573-609.

[13] BOULANCER J L. Static analysis of software [M].ISTE Ltd andJohn Wiley & Sons， 2012.

[14] ERMEDAHL A.SANDBERG C.GUSTAFSSON J，et al. Loophound analysis hased on a comhination of program slicing，ah-stract interpretation ， and invariant analysis

[C] . 7th InternationalWorkshop on Worst-Case Execution Time Analysis （ WCET'07 ） . 2007.