張弛+丁澤文+劉林武

摘 要：確保程序中沒有運(yùn)行時錯誤，對于軟件安全性的保證十分重要?；诔橄蠼忉尩撵o態(tài)分析方法對程序語義進(jìn)行抽象，是驗(yàn)證運(yùn)行時錯誤最合適的形式化方法之一。然而抽象解釋對于程序語義的抽象可能導(dǎo)致過近似問題，從而引發(fā)誤報(bào)，降低了分析精度。因此提出了跡劃分的技術(shù)，根據(jù)程序的跡對程序控制流圖進(jìn)行劃分，對靜態(tài)分析過程進(jìn)行局部細(xì)化，減少了抽象解釋過程中過近似引發(fā)的誤報(bào)。跡劃分技術(shù)以局部分析效率降低為代價換來了分析精度的提高。

關(guān)鍵詞：抽象解釋；跡劃分；靜態(tài)分析；運(yùn)行時錯誤；軟件安全性

中圖分類號：TP311 文獻(xiàn)標(biāo)志碼：A

Research on Trace Partitioning Based on Abstract Interpretation

ZHANG Chi，DING Ze-wen，LIU Lin-wu

（College of Computer Science and Technology，Nanjing University of Aeronautics and Astronautics，Nanjing，Jiangsu 211106，China）

Abstract：Ensuring the absence of run-time errors in the program is important for the software safety.The program semantics was abstracted by the static analysis method based on abstract interpretation.It is the most appropriate formal method for validating run-time errors.However，the over-approximation of program semantics by the abstract interpretation may lead to false alarms，which reduce the accuracy of analysis.So the technology of trace partitioning was proposed.The control-flow-graph was partitioned according to the trace，and then the process of static analysis can be local refinement.The method reduced the false alarms caused by over-approximation.Trace partitioning obtains higher analytical accuracy at the cost of reduction of local analysis efficiency.

Key words：abstract interpretation；trace partitioning；static analysis；run-time error；software safety

1 引 言

近幾年來，安全關(guān)鍵領(lǐng)域中，如何保證軟件安全性已經(jīng)成為了一個廣受關(guān)注的重要課題，如何提高軟件質(zhì)量，保證系統(tǒng)安全性，防止災(zāi)害事故的發(fā)生，已經(jīng)成為當(dāng)前工業(yè)界和學(xué)術(shù)界的重要研究課題[1]。程序的運(yùn)行時錯誤是一類特定的軟件錯誤，是指程序在運(yùn)行時或運(yùn)行后發(fā)生的錯誤，并不是軟件需求和設(shè)計(jì)階段引入的問題，而是由于違反程序語言的安全性規(guī)范而引入的問題[2]，例如某條程序執(zhí)行路徑可能存在除數(shù)為零或者數(shù)據(jù)越界的情況。

對于運(yùn)行時錯誤，工業(yè)界常用的仿真、模擬、測試等手段可以發(fā)現(xiàn)大部分錯誤，但卻無法保證軟件中沒有運(yùn)行時錯誤。形式化分析與驗(yàn)證方法是保障軟件安全性和可靠性的一種重要方法[3]。目前常用的形式化靜態(tài)分析方法有模型檢測[4]、定理證明[5]和抽象解釋[6]。模型檢測需要窮舉所有狀態(tài)空間，存在狀態(tài)空間爆炸的問題；定理證明需要大量人工參與，難以自動化。抽象解釋對程序語義進(jìn)行抽象，將程序的具體語義轉(zhuǎn)化到抽象域中對程序的性質(zhì)進(jìn)行分析。其根據(jù)需求對程序語義進(jìn)行近似，調(diào)節(jié)靜態(tài)分析的精度和效率，是目前對運(yùn)行時錯誤進(jìn)行分析和驗(yàn)證十分有效的方法。

抽象解釋方法通過將程序的具體執(zhí)行過程轉(zhuǎn)化到狀態(tài)遷移系統(tǒng)，在抽象環(huán)境中分析狀態(tài)的可達(dá)性，用以驗(yàn)證實(shí)際執(zhí)行時是否滿足某一性質(zhì)。在以程序控制流圖表示程序具體的執(zhí)行過程時，該過程本身可能導(dǎo)致過近似問題，導(dǎo)致在驗(yàn)證某些程序性質(zhì)時引發(fā)誤報(bào)。例如，我們考慮圖1中C程序片段。

可以看出來，在執(zhí)行y=1/y這行代碼之前，變量y的取值只可能是1或者-1，語句y=1/y這行語句不可能發(fā)生除零錯誤。然而在使用基于區(qū)間抽象域的抽象解釋方法對于示例程序進(jìn)行分析時，將變量的單個取值抽象成區(qū)間表示，分析結(jié)果為變量的取值范圍。在執(zhí)行第一行語句前，變量y的取值是[- SymboleB@ ，+ SymboleB@ ]，在執(zhí)行左側(cè)分支y=-1后再S4處y的取值是[-1，-1]，在執(zhí)行右側(cè)分支y=1后，根據(jù)區(qū)間抽象域的定義，在S4處y的取值是區(qū)間[-1，-1]和1，1的最小上界，即[-1，1]，即此時執(zhí)行語句y=1/y可能發(fā)生除零錯誤，而這個錯誤在實(shí)際執(zhí)行時是不可能發(fā)生的，屬于誤報(bào)。對于此類問題，即使使用更加復(fù)雜的抽象域，例如八邊形抽象[7]和多面體抽象[8]，也無法解決這類問題。事實(shí)上，在S4處變量y的取值只可能是-1或者1，分別通過兩條執(zhí)行路徑得到，，即S1-S2-S4-S5和S1-S3-S4-S5，都不會出現(xiàn)除零錯誤。如果按照如圖2所示的細(xì)化后的控制流圖進(jìn)行分析，就不會發(fā)生除零錯誤。endprint

跡劃分的方法最早被提出用于數(shù)據(jù)流分析（data-flow analysis）[9]，這里使用跡劃分方法改進(jìn)抽象解釋的靜態(tài)分析方法，根據(jù)反映程序具體執(zhí)行過程的跡，對程序控制流圖進(jìn)行局部細(xì)化，以分析效率為代價，提高分析的精度，減少誤報(bào)。

本文主要工作如下：

首先介紹了跡劃分技術(shù)的理論框架，說明如何使用跡劃分對程序控制流圖進(jìn)行劃分；之后說明在具體的基于抽象解釋的靜態(tài)分析過程中，如何使用跡劃分來提高分析進(jìn)度，降低誤報(bào)率。

2 跡劃分的理論框架

本章主要介紹跡劃分的理論框架，其用于對抽象解釋的分析過程進(jìn)行改進(jìn)以調(diào)高分析精度。抽象解釋是一種可以驗(yàn)證程序變量性質(zhì)的形式化靜態(tài)分析方法，有許多國內(nèi)外相關(guān)文章[10-11]對抽象解釋的基本概念進(jìn)行介紹，本文不再贅述，下面主要介紹跡劃分技術(shù)的相關(guān)概念[12]。

2.1 相關(guān)概念

定義1（程序）：我們定義一個程序P為一個遷移系統(tǒng)（S，→Sl），其中S是一個一個程序狀態(tài)的集合，→是描述程序可能的基本執(zhí)行步驟的遷移關(guān)系，Sl表示初始狀態(tài)的集合。

定義2（跡trace）：跡是一個用于描述程序所有運(yùn)行狀態(tài)的非空的有限狀態(tài)序列的集合S*。其中σ是其中一個有限狀態(tài)序列，我們稱σi是該序列的第i+1個狀態(tài)，σ0和σ-1分別為該序列的第一個狀態(tài)和最后一個狀態(tài)。

因此基于跡的程序的形式化定義為[P]Δ{σεS*|σ0∈Sl∧i，σi→σi+1}，即程序可以定義為許多條跡的集合，每條跡反映程序的一條實(shí)際執(zhí)行路徑。

2.2 跡劃分的形式化定義

在進(jìn)行靜態(tài)程序分析過程中，抽象解釋方法通過將程序從具體域轉(zhuǎn)化到抽象域中，極大的加快了分析過程的效率，與模型檢測相比，大大縮減了狀態(tài)空間的數(shù)目，避免了狀態(tài)空間爆炸的問題。然而其對于具體執(zhí)行環(huán)境的抽象可能導(dǎo)致過近似的問題，引發(fā)實(shí)際運(yùn)行中不會出現(xiàn)的虛假反例。抽象解釋中具體域與抽象域之間的轉(zhuǎn)化通過一個Galois連接[13]來表示：

α（P，≤）（P*，≤*）γ

其中（P，≤）稱為具體域，（P*，≤*）稱為抽象域，α和γ分別稱為抽象函數(shù)和具體化函數(shù)。

跡劃分是一種將分析過程細(xì)化的方法，根據(jù)不同的跡將控制流圖劃分成更多狀態(tài)，犧牲分析效率以換得分析精度的調(diào)高。跡劃分的本質(zhì)上是一種具體化的過程，可以通過一個具體化函數(shù)δ來實(shí)現(xiàn)，我們有如下形式化定義。

定義3（跡劃分trace partition）：一個具體化函數(shù)δ：E→P（F）稱為遷移系統(tǒng)F的劃分，當(dāng)且僅當(dāng)∪x∈E（δ（x））=F并且x，y∈E，x≠yδx∩δy=。

也就是說，跡劃分過程將一個遷移系統(tǒng)分成若干個子分區(qū)，各個分區(qū)的合集與原遷移系統(tǒng)等價，并且分區(qū)之間互不相交。跡劃分可以保證抽象解釋分析過程的可靠性（soundness），不會為分析過程帶來額外的誤報(bào)或者漏報(bào)。

2.3 程序控制流圖的跡劃分方法

程序控制流圖（control-flow graph）[14]是程序的一種重要的表示形式，其反應(yīng)了程序中語句之間的執(zhí)行先后順序和程序運(yùn)行過程中的所有可能執(zhí)行流向。抽象解釋方法一般以控制流圖為分析對象，在抽象環(huán)境中迭代計(jì)算不動點(diǎn)，以驗(yàn)證變量的數(shù)值性質(zhì)。具體的，對于程序控制流圖的跡劃分主要有條件判斷語句的跡劃分、循環(huán)語句的跡劃分、變量取值的跡劃分三種情況，下面具體進(jìn)行說明。

（1）條件判斷語句的跡劃分

對于條件判斷語句，可以根據(jù)條件判斷語句的分支數(shù)對程序控制流圖進(jìn)行劃分，在抽象解釋的靜態(tài)分析過程中，由于部分結(jié)構(gòu)的細(xì)化，導(dǎo)致分析效率的下降。具體的跡劃分過程如圖3所示。

（2）循環(huán)語句的跡劃分

對于循環(huán)語句，可以根據(jù)循環(huán)體的執(zhí)行次數(shù)對程序控制流圖進(jìn)行劃分，每條跡分別代表程序循環(huán)體執(zhí)行1次、2次…的執(zhí)行路徑。為了保證分析過程的可終止性，劃分過程不能無限進(jìn)行，根據(jù)實(shí)際情況設(shè)置循環(huán)劃分上限n，將循環(huán)語句劃分成n部分。具體的跡劃分過程如圖4所示。

（3）變量取值的跡劃分

在抽象解釋過程中，有些變量的取值是離散的幾個點(diǎn)，例如變量x的值可能為-100和100，此時對其取值范圍進(jìn)行抽象表示的精度很差，此時x的區(qū)間抽象域表示為[-100，100]，有極大的可能導(dǎo)致虛假反例的產(chǎn)生。根據(jù)變量取值遍歷跡，對程序控制流圖進(jìn)行劃分。具體的跡劃分過程如圖5所示。

為了保證跡劃分方法所帶來的時間和空間開銷是局部的，需要在變量性質(zhì)得到驗(yàn)證之后，對跡劃分后的程序控制流圖進(jìn)行合并（merge）。否則，程序控制流圖的跡劃分會導(dǎo)致分析過程的復(fù)雜度據(jù)劃分點(diǎn)的數(shù)目成幾何倍數(shù)上升，此時付出的分析效率代價對于驗(yàn)證變量性質(zhì)沒有價值。對于控制流圖的合并過程如圖6所示，圖6以條件判斷語句為例，說明了如何對于劃分的控制流圖進(jìn)行合并，其他類型跡劃分就不在贅述。

3 跡劃分技術(shù)的應(yīng)用

上文提到了跡劃分技術(shù)的理論框架，指出了跡劃分可以對哪幾類程序控制流圖進(jìn)行劃分，從而將分析過程細(xì)化，以期可以減少抽象解釋分析過程由于過近似產(chǎn)生的誤報(bào)。當(dāng)然的，我們可以在實(shí)際分析過程中遇到誤報(bào)時，根據(jù)遇到的具體問題，手動對控制流圖進(jìn)行跡劃分，在程序性質(zhì)得到驗(yàn)證后，即找到真實(shí)錯誤或者排除了虛假反例，則可以對跡劃分后的控制流圖進(jìn)行合并，繼續(xù)進(jìn)行靜態(tài)分析，直至所有程序分析完畢。

然而對于靜態(tài)分析而言，自動化分析能力的強(qiáng)弱十分重要，還是需要一些自動的策略來自動地進(jìn)行控制流圖的劃分和合并，經(jīng)過大量的實(shí)驗(yàn)，對以下三類程序片段進(jìn)行跡劃分時效果十分顯著，可以加入自動的策略中，提高分析精度。

3.1 變量間存在線性關(guān)系的情況

很多情況下待變量的之間是存在線性關(guān)系的，而傳統(tǒng)的非關(guān)系型抽象域卻無法表達(dá)變量之間的關(guān)系，導(dǎo)致分析精度大大下降。若為了解決部分程序分析過程的誤報(bào)而引入關(guān)系型抽象域，如八邊形抽象域，全局的時間復(fù)雜度會由O（n）提高到O（n3），極大地降低了分析效率。此時可以使用跡劃分技術(shù)對程序控制流圖進(jìn)行劃分，只會在局部提高分析復(fù)雜度。endprint

如果發(fā)生存在線性關(guān)系變量發(fā)生算術(shù)運(yùn)算，例如：如果整數(shù)x∈[-1，1]，那么根據(jù)區(qū)間抽象域的計(jì)算結(jié)果，則有x-x∈[-2，2]，可能發(fā)生誤報(bào)，此時采用變量取值的跡劃分，根據(jù)x=1和x=-1兩條跡對程序控制流圖進(jìn)行劃分，都有x-x=0的結(jié)果，之后再對控制流圖進(jìn)行合并，可以得到x-x∈[0，0]。

3.2 變量為除數(shù)的情況

當(dāng)變量作為除數(shù)時，即使變量的取值范圍的區(qū)間很小，其算術(shù)運(yùn)算結(jié)果也肯能在較大范圍內(nèi)變動，導(dǎo)致分析結(jié)果精度下降，有誤報(bào)產(chǎn)生的可能。當(dāng)變量除數(shù)的取值區(qū)間較小時（例如小于1000），可以根據(jù)變量的所有可能取值，對控制流圖進(jìn)行跡劃分，當(dāng)所有計(jì)算結(jié)果全部計(jì)算完畢后，對控制流圖進(jìn)行合并，可以極大增加分析的精度?？紤]如下的程序。

int r=0；float x=0.0；

while（true）{

r=random（0，50）；

x=（x*r+random（-100，100））/（r+1）；}

若使用區(qū)間抽象域分析變量x的取值范圍，當(dāng)?shù)讲粍狱c(diǎn)時，有x∈[-5100，5100]，若根據(jù)變量r的取值將控制流圖劃分成r=0、r=2…r=50的51條跡，在合并后得到x∈[-100，100]，即對所有的r∈[0，50]都有x∈[-100，100]。提高了分析精度。

3.3 循環(huán)中存在算術(shù)運(yùn)算的情況

當(dāng)循環(huán)中存在算術(shù)運(yùn)算時，特別存在數(shù)組運(yùn)算時，大部分抽象域的近似過程都會導(dǎo)致循環(huán)變量無法參與循環(huán)體內(nèi)的算術(shù)運(yùn)算，例如對于i∈[0，3]，xi=-10，0，3，7，yi={-1，2，3，4}，如果循環(huán)體內(nèi)存在算術(shù)運(yùn)算xi×yi，根據(jù)區(qū)間抽象域的定義，其結(jié)果取值范圍是所有可能結(jié)果的最小上界，即xi×yi∈[-40，28]。實(shí)際上，若根據(jù)循環(huán)語句將控制流圖劃分成四個部分，其結(jié)果只可能是10、0、9和28，因此有xi×yi∈[0，28]，同樣提高了分析過程的精度。由于編程習(xí)慣，許多循環(huán)體中都會在第一次循環(huán)時對變量進(jìn)行初始化，因此可以將循環(huán)語句的控制流圖劃分成第一次循環(huán)和剩余循環(huán)兩條跡來進(jìn)行分析，也可以提高分析精度。

4 結(jié)束語

基于抽象解釋的跡劃分技術(shù)是一種提高分析精度的方法，其根據(jù)程序運(yùn)行的跡對程序控制流圖進(jìn)行了劃分，以局部分析復(fù)雜度上升為代價，提高了全局分析精度，可以減少許多誤報(bào)，增加了基于抽象解釋的靜態(tài)分析方法在實(shí)際應(yīng)用過程中的適用性。介紹了基于抽象解釋的跡劃分技術(shù)的理論框架，說明了其如何對程序控制流圖進(jìn)行劃分；之后解釋了在實(shí)際分析過程中，在哪些情況下使用跡劃分技術(shù)可以顯著提高分析精度，降低分析過程中由于抽象解釋的過近似而產(chǎn)生的誤報(bào)。在之后的工作中，可以對跡劃分可以應(yīng)用的場景進(jìn)行擴(kuò)展，以期其可以具備更高的適用性。

參考文獻(xiàn)

[1] 黃志球，徐丙鳳，闞雙龍，等.嵌入式機(jī)載軟件安全性分析標(biāo)準(zhǔn)、方法及工具研究綜述[J].軟件學(xué)報(bào)，2014，25（2）：200-218.

[2] DELMAS D，SOUYRIS J.Astrée： from research to industry[C]//International Static Analysis Symposium.Springer Berlin Heidelberg，2007： 437-451.

[3] 黃傳林，黃志球，胡軍，等.基于擴(kuò)展SysML 活動圖的嵌入式系統(tǒng)設(shè)計(jì)安全性驗(yàn)證方法研究[J].小型微型計(jì)算機(jī)系統(tǒng)，2015，36（ 3） ： 408-417.

[4] 侯剛，周寬久，勇嘉偉，等.模型檢測中狀態(tài)爆炸問題研究綜述[J].計(jì)算機(jī)科學(xué)，2013，40（S1）：77-86.

[5] JHALA R，MAJUMDAR R.Software model checking[J].ACM Computing Surveys （CSUR），2009，41（4）： 21.

[6] COUSOT P，COUSOT R，MAUBORGNE L.Theories，solvers and static analysis by abstract interpretation[J].Journal ofthe ACM （JACM），2012，59（6）： 31.

[7] MINE A.The octagon abstract domain[J].Higher-Order and Symbolic Computation，2006，19（1）：31-100.

[8] COUSOT P，HALBWACHS N.Automatic Discovery of Linear Restraints Among Variables of a Program[C]// 2001：84-97.

[9] NIELSON F，NIELSON H R，HANKIN C.Principles of program analysis[M].Springer，2015.

[10] COUSOT P，COUSOT R.Abstract interpretation： past，present and future[C]//Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic （CSL） and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science （LICS）.ACM，2014：2.

[11] 陸陳，黃志球，闞雙龍，等.基于八邊形抽象域的襟縫翼控制系統(tǒng)安全性分析[J].小型微型計(jì)算機(jī)系統(tǒng)，2016，37（5）：902-907.

[12] HOLLEY L H，ROSEN B K.Qualified Data Flow Problems[J].IEEE Transactions on Software Engineering，1981，SE-7（1）：60-78.

[13] COUSOT P，COUSOT R.Comparing the Galois connection and widening/narrowing approaches to abstract interpretation[C]// Programming Language Implementation and Logic Programming，International Symposium，Plilp92，Leuven，Belgium，August 26-28，1992，Proceedings.1992：269-295.

[14] HARROLD M J，MALLOY B，ROTHERMEL G.Efficient Construction of Program Dependence Graphs[J].AcmSigsoft Software Engineering Notes，2000，18（3）：160-170.endprint