基于抽象解釋的跡劃分技術(shù)研究

張弛+丁澤文+劉林武

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

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

中圖分類號(hào)：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 引 言

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

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

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

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

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

本文主要工作如下：

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

2 跡劃分的理論框架

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

2.1 相關(guān)概念

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

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

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

2.2 跡劃分的形式化定義

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

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

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

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

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

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

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

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

（1）條件判斷語(yǔ)句的跡劃分

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

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

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

（3）變量取值的跡劃分

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

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

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

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

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

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

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

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

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

當(dāng)變量作為除數(shù)時(shí)，即使變量的取值范圍的區(qū)間很小，其算術(shù)運(yùn)算結(jié)果也肯能在較大范圍內(nèi)變動(dòng)，導(dǎo)致分析結(jié)果精度下降，有誤報(bào)產(chǎn)生的可能。當(dāng)變量除數(shù)的取值區(qū)間較小時(shí)（例如小于1000），可以根據(jù)變量的所有可能取值，對(duì)控制流圖進(jìn)行跡劃分，當(dāng)所有計(jì)算結(jié)果全部計(jì)算完畢后，對(duì)控制流圖進(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ù)讲粍?dòng)點(diǎn)時(shí)，有x∈[-5100，5100]，若根據(jù)變量r的取值將控制流圖劃分成r=0、r=2…r=50的51條跡，在合并后得到x∈[-100，100]，即對(duì)所有的r∈[0，50]都有x∈[-100，100]。提高了分析精度。

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

當(dāng)循環(huán)中存在算術(shù)運(yùn)算時(shí)，特別存在數(shù)組運(yùn)算時(shí)，大部分抽象域的近似過(guò)程都會(huì)導(dǎo)致循環(huán)變量無(wú)法參與循環(huán)體內(nèi)的算術(shù)運(yùn)算，例如對(duì)于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)語(yǔ)句將控制流圖劃分成四個(gè)部分，其結(jié)果只可能是10、0、9和28，因此有xi×yi∈[0，28]，同樣提高了分析過(guò)程的精度。由于編程習(xí)慣，許多循環(huán)體中都會(huì)在第一次循環(huán)時(shí)對(duì)變量進(jìn)行初始化，因此可以將循環(huán)語(yǔ)句的控制流圖劃分成第一次循環(huán)和剩余循環(huán)兩條跡來(lái)進(jìn)行分析，也可以提高分析精度。

4 結(jié)束語(yǔ)

基于抽象解釋的跡劃分技術(shù)是一種提高分析精度的方法，其根據(jù)程序運(yùn)行的跡對(duì)程序控制流圖進(jìn)行了劃分，以局部分析復(fù)雜度上升為代價(jià)，提高了全局分析精度，可以減少許多誤報(bào)，增加了基于抽象解釋的靜態(tài)分析方法在實(shí)際應(yīng)用過(guò)程中的適用性。介紹了基于抽象解釋的跡劃分技術(shù)的理論框架，說(shuō)明了其如何對(duì)程序控制流圖進(jìn)行劃分；之后解釋了在實(shí)際分析過(guò)程中，在哪些情況下使用跡劃分技術(shù)可以顯著提高分析精度，降低分析過(guò)程中由于抽象解釋的過(guò)近似而產(chǎn)生的誤報(bào)。在之后的工作中，可以對(duì)跡劃分可以應(yīng)用的場(chǎ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 活動(dòng)圖的嵌入式系統(tǒng)設(shè)計(jì)安全性驗(yàn)證方法研究[J].小型微型計(jì)算機(jī)系統(tǒng)，2015，36（ 3） ： 408-417.

[4] 侯剛，周寬久，勇嘉偉，等.模型檢測(cè)中狀態(tài)爆炸問(wèn)題研究綜述[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