基于抽象解釋的跡劃分技術研究

張弛+丁澤文+劉林武

摘 要：確保程序中沒有運行時錯誤，對于軟件安全性的保證十分重要。基于抽象解釋的靜態分析方法對程序語義進行抽象，是驗證運行時錯誤最合適的形式化方法之一。然而抽象解釋對于程序語義的抽象可能導致過近似問題，從而引發誤報，降低了分析精度。因此提出了跡劃分的技術，根據程序的跡對程序控制流圖進行劃分，對靜態分析過程進行局部細化，減少了抽象解釋過程中過近似引發的誤報。跡劃分技術以局部分析效率降低為代價換來了分析精度的提高。

關鍵詞：抽象解釋；跡劃分；靜態分析；運行時錯誤；軟件安全性

中圖分類號：TP311 文獻標志碼：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 引 言

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

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

抽象解釋方法通過將程序的具體執行過程轉化到狀態遷移系統，在抽象環境中分析狀態的可達性，用以驗證實際執行時是否滿足某一性質。在以程序控制流圖表示程序具體的執行過程時，該過程本身可能導致過近似問題，導致在驗證某些程序性質時引發誤報。例如，我們考慮圖1中C程序片段。

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

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

本文主要工作如下：

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

2 跡劃分的理論框架

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

2.1 相關概念

定義1（程序）：我們定義一個程序P為一個遷移系統（S，→Sl），其中S是一個一個程序狀態的集合，→是描述程序可能的基本執行步驟的遷移關系，Sl表示初始狀態的集合。

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

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

2.2 跡劃分的形式化定義

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

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

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

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

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

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

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

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

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

對于條件判斷語句，可以根據條件判斷語句的分支數對程序控制流圖進行劃分，在抽象解釋的靜態分析過程中，由于部分結構的細化，導致分析效率的下降。具體的跡劃分過程如圖3所示。

（2）循環語句的跡劃分

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

（3）變量取值的跡劃分

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

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

3 跡劃分技術的應用

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

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

3.1 變量間存在線性關系的情況

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

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

3.2 變量為除數的情況

當變量作為除數時，即使變量的取值范圍的區間很小，其算術運算結果也肯能在較大范圍內變動，導致分析結果精度下降，有誤報產生的可能。當變量除數的取值區間較小時（例如小于1000），可以根據變量的所有可能取值，對控制流圖進行跡劃分，當所有計算結果全部計算完畢后，對控制流圖進行合并，可以極大增加分析的精度。考慮如下的程序。

int r=0；float x=0.0；

while（true）{

r=random（0，50）；

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

若使用區間抽象域分析變量x的取值范圍，當迭代到不動點時，有x∈[-5100，5100]，若根據變量r的取值將控制流圖劃分成r=0、r=2…r=50的51條跡，在合并后得到x∈[-100，100]，即對所有的r∈[0，50]都有x∈[-100，100]。提高了分析精度。

3.3 循環中存在算術運算的情況

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

4 結束語

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

參考文獻

[1] 黃志球，徐丙鳳，闞雙龍，等.嵌入式機載軟件安全性分析標準、方法及工具研究綜述[J].軟件學報，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] 黃傳林，黃志球，胡軍，等.基于擴展SysML 活動圖的嵌入式系統設計安全性驗證方法研究[J].小型微型計算機系統，2015，36（ 3） ： 408-417.

[4] 侯剛，周寬久，勇嘉偉，等.模型檢測中狀態爆炸問題研究綜述[J].計算機科學，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] 陸陳，黃志球，闞雙龍，等.基于八邊形抽象域的襟縫翼控制系統安全性分析[J].小型微型計算機系統，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