基于符號表達式的程序語義缺陷警報關聯識別方法

王淑棟，劉 浩，董玉坤，陳紅旗，張 莉，尹文靜

(中國石油大學(華東)計算機科學與技術學院，青島 266580)

靜態分析技術是一種檢測程序語義缺陷的有效技術，通過靜態分析程序的語法與語義，并根據程序安全規則判斷被測程序是否違反了程序安全屬性[1-3]。目前，在靜態測試領域，已經出現了一些相對成熟的工具，外國具有代表性的有Klocwork、PMD、Findbugs、Coverity等，中國有DTS(defect test system)[4-5]等靜態缺陷檢測工具。據統計，利用這些靜態檢測工具對程序編譯與測試后，語義缺陷密度[6]大致是1個/KLOC[7]，這些存在的缺陷嚴重影響著軟件質量，將直接導致程序運行時出現系統崩潰、運算結果異常、安全漏洞等情況。

由于靜態分析技術對程序的非平凡屬性分析不夠精確，目前的靜態分析工具與方法不可避免的會存在缺陷的漏報[8]與誤報[9]。現有的靜態分析工具漏報率為9%～32%，誤報率為35%～91%[10]，這些檢測出的真實缺陷和誤報被稱為警報。在圖1中，函數f1第5行在沒有進行判斷指針p是否是空指針的情況下就直接進行了引用，會引起空指針解引用(null pointer dereference，NPD)警報；函數f1第6行在沒有判斷分母是否為0就進行了算術運算，引起非法計算操作(illegal arithmetic operand，IAO)警報。

隨著軟件的規模與復雜度遞增式增長，靜態檢測工具報告的警報數量也急劇增加，這些檢測出的警報需要警報判定人員逐一進行人工判定，大大降低了缺陷檢測效率，也造成缺陷檢測的成本大幅度增加，甚至已經導致軟件開發和管理人員在軟件開發過程中拒絕使用靜態缺陷檢測工具。

靜態缺陷檢測結果分析顯示，大多數的警報與其他警報之間存在著關聯關系。如圖1所示，函數f1和函數f2分別報告了一個NPD警報，兩處警報的觸發原因都是因為在沒有進行任何空指針判斷的情況下就進行了變量引用，兩處警報分別與變量p和變量q有關，兩個變量引用了同一塊內存地址，具有相同的符號表達式，表明這兩個警報存在恒等關聯關系。如果能夠找到這些警報間的關聯關系并對警報進行分組，在人工判定警報的時候，只需要對一組中的一個或幾個警報進行判定，就可以大大縮短判定的時間。

圖1 程序代碼片段Fig.1 Program code fragment

關于警報關聯[11]的相關技術已有大量報道。Lee等[12]提出一種基于靜態分析的警報聚類的可靠方法，該方法首先判定一個警報的錯誤狀態，然后通過觀察這個錯誤狀態的傳播對其他警報的影響來判斷警報間的關系。Zhang等[13]提出一種錯誤狀態切片的警報關聯方法，該方法首先在缺陷檢測過程中去除警報的錯誤狀態切片，同時生成一個新的狀態切片作為外部約束，從而得到警報觸發點的抽象求精語義，之后根據程序是否會觸發警報進行關聯計算。Heckman等[10]基于機器學習技術提出一種警報關聯特征模型，利用該模型可以實現警報間的關聯。該方法首先基于該模型構建評估框架，選取了警報的類型和代碼位置等特征信息，并利用了15個機器學習算法建立警報關聯模型。最后根據此模型對檢測結果進行匹配，將具有相同特征的警報進行關聯。以上大部分方法只對警報進行了簡單的關聯分析，并沒有對警報關聯的范圍及準確性進行更深層次的深究。

鑒于上述現象，提出一種基于符號表達式的程序語義缺陷警報關聯識別方法，使用該方法可以得到更高精度、可信度的警報關聯關系，進而更多的減輕人工判定警報的工作量。研究的貢獻可以概括如下。

(1)提出了一種警報關聯識別方法，在缺陷檢測階段將檢測出的每個警報由基于區域的符號化三值邏輯(region-based symbolic three valued logic，RSTVL)[14]的符號表達式表示，根據該警報的符號表達式與其他警報間的符號表達式的邏輯關系，總結得出恒等、非、或、與四種關聯類型。

(2)不僅實現過程內警報關聯，還通過符號化函數摘要實現過程間警報關聯，進一步提高了識別警報關聯的精度。

(3)實驗驗證了所提方法的有效性，減輕了人工判定警報的工作量，提高了人工判定警報工作的效率。

1 相關定義

一個程序P可以被表示為一個六元組P=。其中V表示程序的變量集合，L表示程序點集合，S表示程序語句集合，τ?LSL表示一個遷移關系，init∈L表示程序的入口，end∈L表示程序的出口。

程序中警報的觸發跟其變量的來源有著直接的關系，當該警報跟多個變量都有關系的時候，每一個變量的來源都可能對警報產生影響。

2 基于符號表達式的警報關聯

2.1 符號表達式

采用基于區域的符號化三值邏輯(region-based symbolic three valued logic，RSTVL)來表示程序變量的抽象存儲狀態。

基于區域的符號化三值邏輯(RSTVL)定義為四元組，RSTVL=，其中，Var表示內存對象，Region表示區域，SExp表示符號表達式，Domain表示取值區間。

定義8(符號表達式)符號表達式SExp由符號通過數學運算與關系操作構成，遞歸定義如式(1)所示：

(1)

式(1)中：符號表達式SExp由邏輯表達式RelExp通過關系操作構成；RelExp由數學表達式Exp通過邏輯操作構成；Exp由項Term通過加減運算組成；Term由多個因子Power通過乘除運算組成；每個Power由一個或多個原子Factor通過冪運算組成；原子Factor是符號表達式的最基本元素，它可以是一個數值常量Constant、符號變量Symbol或者符號表達式SExp。

董玉坤等[15]提出了符號化函數摘要，符號化函數摘要應用RSTVL描述符號化的函數摘要，將函數的行為通過符號化表示，在函數調用點基于過程內數據流分析的結果對函數摘要進行實例化，實現對調用點處抽象存儲狀態的更新，可實現過程間可靠的數據流分析，通過符號化函數摘要可以建立過程間警報關聯。

每個警報可能存在n個相關變量，每個相關變量的符號表達式在程序生存周期內是唯一的，當其中任意兩個相關變量的符號表達式不一致時，可以認定這是不同的相關變量。

例如在圖1中，函數f1第5行在沒有進行任何空指針判斷的情況下進行了引用，在第7行調用函數f2將指針p的值傳遞過去，函數f2同樣在沒有進行任何空指針判斷的情況下進行了引用。在第5行和第10行各報告了一個NPD警報，兩個警報都對應著同一個取值區域，具有相同的符號表達式。

在程序點l上，?Va,Vb,Vc∈Vl，Ω假定表示區間全集，假定VaExp、VbExp和VcExp分別表示變量Va、變量Vb和變量Vc對應的符號表達式，D[VaExp]、D[VbExp]、D[VcExp]分別表示變量Va、變量Vb和變量Vc對應的取值區間。

定義9(符號表達式的級數)符號表達式的級數(rank)表示符號表達式的復雜程度，根據符號表達式的個數將符號表達式分為n個級別，用符號ρ表示符號表達式的級數。假定單個符號表達式VaExp為1級，每增加一個邏輯運算符號或者符號表達式，相應的級數也增加1，例如符號表達式VaExp為2級，VaExp&&VbExp為3級，依次類推。

當變量間對應的符號表達式存在非、或、與三種關系時，其對應的取值區間運算存在以下規則。

非關系符號表達式的區間運算，如式(2)所示。

(2)

或關系符號表達式的區間運算，如式(3)所示：

(3)

與關系符號表達式的區間運算，如式(4)所示：

(4)

2.2 程序語義缺陷警報

將一類缺陷產生時程序所呈現的共同的語法或語義特征稱為缺陷模式。常見的語義類缺陷模式包括空指針解引用(null pointer dereference，NPD)、數組越界(out of bound，OOB)、非法計算操作(illegal arithmetic operand，IAO)等類型。

程序中警報間具有相同的缺陷模式是警報關聯的基礎，兩個警報只有屬于同一個缺陷模式才可以進行關聯；相反，如果兩個警報來自不同的缺陷模式，即使警報的相關變量為同一個，也無法進行關聯。

為了能夠準確、全面地表示警報的數據信息，通過構建警報特征信息來進行描述。將警報特征信息定義為一個由結構信息、變量信息組成的二元組SV=。

Struinfo表示警報的結構信息，由七元組Struinfo=組成。其中，Num表示在警報文檔中該警報的編號，Category表示缺陷類型，File表示被測工程，StartLine表示警報觸發位置所在工程代碼起始行號，IPLine表示警報觸發位置所在行號；DeType表示警報被判定為真實缺陷或誤報；Flag表示警報是否已經被判定的標記，當Flag=0時，代表警報沒有被判定，當Flag=1時，代表警報被判定。

Varinfo表示警報的變量信息，由三元組Varinfo =組成。其中，Var表示警報的相關變量名稱，SExp表示警報相關變量對應的符號表達式，Domain表示警報相關變量對應的取值區間。

2.3 程序語義缺陷的警報關聯推導規則

對于任意的兩個警報am和an，假定?Exp(am)表示警報am的相關變量對應的符號表達式，?Exp(an)表示警報an的相關變量對應的符號表達式。如果警報間對應的符號表達式符合以下規則，則判定警報am和警報an存在關聯關系。

警報與警報之間具有恒等、非、或、與等關聯，這些關聯信息是人工判定過程中警報確認的前提。

2.3.1 恒等關聯

如果?Exp(am)==?Exp(an)，若警報am和an同為誤報或真實缺陷，則警報am和an警報存在恒等關系。

2.3.2 非關聯

如果?Exp(am)==?Exp(an)，若其中一個為誤報，則另一個為真實缺陷，則警報am和警報an存在非關聯關系。

2.3.3 或關聯

如果?Exp(am)==?Exp(an)‖?Exp(a)，其中?Exp(a)表示任意警報對應的一個符號表達式，稱警報am與警報an存在或關聯關系。

2.3.4 與關聯

如果?Exp(am)==?Exp(an)&&?Exp(a)，其中?Exp(a)表示任意警報對應的一個符號表達式，稱警報am與警報an存在與關聯關系。

假定存在警報a，與警報a存在關聯的警報集合可以由四元組Corinfo=表示。其中，Con表示與警報a存在恒等關聯的警報集合；Not表示與警報a存在非關聯的警報集合；Or表示與警報a存在或關聯的警報集合；And表示與警報a存在與關聯的警報集合。

3 程序語義缺陷的警報關聯算法與實現

3.1 程序語義缺陷的警報關聯算法

根據之前的警報關聯推導規則，給出一個具體算法來計算警報關聯，其警報關聯算法如下。

算法1中輸入為檢測的全部警報；輸出為警報與警報之間的關聯關系。其中，Sw表示警報集合，Sr表示警報的級數集合，N表示警報的全部數量。

(1)首先判斷所有警報對應的符號表達式的級數，然后按照警報的符號表達式級數從小到大進行排序，得出警報序列，接著人工判定符號表達式級數最小的警報。

(2)判定兩個警報是否為同一類缺陷模式，若兩個警報不屬于同一類缺陷模式，則不存在任何關聯，若兩個警報屬于同一類缺陷模式，再接著下一步。

(3)對警報集合中的警報進行兩兩比較，并將存在關聯關系的警報加入到相應的關聯集合中。若兩個警報對應的符號表達式滿足?Exp(am)=?Exp(an)，則兩個警報存在恒等關聯關系；若2個警報對應的符號表達式滿足?Exp(am)=?Exp(an)，則兩個警報存在非關聯關系；若兩個警報對應的符號表達式滿足?Exp(am)=?Exp(an)‖?Exp(a)，則兩個警報存在或關聯關系；若兩個警報對應的符號表達式滿足?Exp(am)=?Exp(an)&&?Exp(a)，則兩個警報存在與關聯關系。如果這四種關聯都不存在，則警報間不存在關聯關系。

算法1程序語義缺陷的警報關聯算法。

輸入:檢測的全部警報

輸出:警報與警報間的關聯關系

function WarningCorrelation(Sw)

for eacha∈Swdo

Sr←ρ(a);

Warning sort from small rank to large rank.

Manual determine each warninga∈Srthat Minimum rank of warning.

for(i=1;i≤N;i++)

for(j=i+1;j≤N;j++)

if(ai.Category!=aj.Category)

continue;

else

if(?Exp(ai)==?Exp(aj))then

ai.Con←aj;

aj.Con←ai;

else if(?Exp(ai)==?Exp(aj))then

ai.Not←aj;

aj.Not←ai;

else if(?Exp(ai)==?Exp(aj)‖?Exp(a))then

ai.Or←aj;

aj.Or←ai;

else if(?Exp(ai)==?Exp(aj)&&?Exp(a))then

ai.And←aj;

aj.And←ai;

else

No correlation;

通過警報關聯算法后，如果警報間具有關聯關系，則將這些警報的關聯信息分別存儲在警報關聯文件Corinfo相應的Con、Not、Or、And集合中，方便以后人工判定警報的工作。

3.2 基于警報關聯的人工警報判定

通過之前的警報關聯算法已經得到了警報間的關聯關系，這些警報可能是真實缺陷也可能是誤報，還需要進一步人工判定警報的真實性。當人工判定一個警報后，警報判定系統會把跟這個警報相關的進行自動判定。

算法2的輸入為警報及警報關聯關系，輸出為警報判定結果。其中，Sm表示人工重新判定集合。

首先人工判定警報集合中某警報是真實缺陷還是誤報，然后依次判定警報a判定是否存在恒等、非、或、與關聯關系。

若警報集合a.Con非空，表示警報a存在恒等關聯的警報，判斷存在關聯的警報的判定標記Flag，如果Flag為0，則與警報a的判定結果相同，如果Flag為1，則判斷已判定的類型是否與警報a的判定結果相同，如果不相同，則加入Sm集合；若警報集合a.Not非空，表示警報a存在非關聯的警報，判斷過程同上，只是判定結果與警報a相反；若警報集合a.Or非空，表示警報a存在或關聯的警報，如果警報a的判定結果是真實缺陷，判定過程同恒等關聯判定過程，如果警報a的判定結果是誤報，則將與之關聯的警報加入Sm集合；若警報集合a.And非空，表示警報a存在與關聯的警報，如果警報a的判定結果是誤報，判定過程同恒等關聯判定過程，如果警報a的判定結果是真實缺陷，則將與之關聯的警報加入Sm集合。最后，若集合Sm非空，則人工親自判定集合Sm中的警報，人工判定完成警報后，算法結束。

算法2警報判定算法。

輸入:警報及警報關聯關系

輸出:警報判定結果

function WarningDetermine(Sw，Corinfo)

for eacha∈Swdo

Manual determinea’s DeType;

if(a.Con!=?)then

for eachw∈a.Con do

call function Redet(w);

else if(a.Not!=?)then

for eachw∈a.Not do

if(w.Flag==0)then

else

if(w.DeType==a.DeType)then

Sm←w;

else if(a.Or!=?)then

for eachw∈a.Or do

if(a.DeType==defect)then

call function Redet(w);

else

Sm←w;

else if(a.And!=?)then

for eachw∈a.And do

if(a.DeType==false positive)then

call function Redet(w);

else

Sm←w;

if(Sm!=?)then

for eachw∈Smdo

Manual determinew;

function Redet(w)

if(w.Flag==0)then

w.DeType←a.DeType.

else

if(w.DeType!=a.DeType)then

Sm←w;

4 實驗驗證

在第4節中，已經介紹了警報關聯算法和警報判定算法，為了證明上述方法能夠實現警報關聯及警報判定，將上述算法嵌入靜態缺陷測試工具DTSC_RSTVL中進行實驗。

4.1 實驗平臺

實驗平臺是在原型工具DTSC_RSTVL[14]的基礎上進行改進，并得到了工具DTSC_Corr，通過該工具可以實現對典型語義缺陷的充分檢測，并在缺陷檢測階段對警報進行關聯與排序。圖2所示為DTSC_Corr處理流程的基本框架，包括5個處理部分，分別為：輸入部分、基本處理部分、數據流分析部分、自動檢測部分、結果分析部分。

圖2 DTSC_Corr工具處理流程圖Fig.2 DTSC_Corr processing flow chart

4.2 實驗結果及分析

選擇3種常見的缺陷模式空指針解引用(NPD)、數組越界(OOB)、非法計算操作(IAO)作為DTSC_Corr的檢測故障對象，并選擇5個開源C工程Barcode、Sphinxbase、Uucp、Git、Httpd作為被測對象，5個工程共計1 232個文件447 250行代碼，其中工程代碼量最小的為3 409行，最大為204 229行。選擇的這5個工程對于所用方法都具有一定的代表性，其包含大量復雜的指針操作和函數調用操作。

表1所示為在DTS平臺測試5個C工程的警報詳細信息。統計結果表明：5個工程共檢測出914個警報，其中真實缺陷378個，誤報536個。存在關聯關系的警報總數占全部警報總數的61.71%，對警報的恒等、非、或、與關聯統計，恒等關聯占四種關聯中的占比最多，為84.65%；其次是或關聯占比13.30%，與關聯占比2.05%，非關聯沒有匹配到，占比0，這是因為雖然非關聯邏輯上是存在的，但是在真實的編程中卻是很少使用，所以并沒有檢測到。在運行時間方面來看，采用警報關聯后的DTS運行時間普遍略高于沒有采用警報關聯算法的時間。Barcode、Sphinxbase、Uucp、Git、Httpd 5個工程的處理時間分別增加9.38%、10.53%、6.86%、7.66%、12.40%，平均增加9.44%的程序處理時間。

利用警報關聯方法可以減少345次警報判定工作，占警報總數的37.75%。其中，警報關聯程度最高的工程是Git-1.8.2，通過警報關聯算法可以減少46.26%的警報判定工作；警報關聯程度最低的工程是Uucp-1.07，通過警報關聯算法可以減少21.78%的警報判定工作。當工程規模更大時，警報數也將隨之增加，通過警報關聯算法可以減少的警報判定次數也會更多，人工判定減輕更大的負擔。

圖3為工程Barcode-0.98pcl.c中檢測出的警報關聯的實例，第65、第66、第67、第68行在沒有進行任何空指針判斷的情況下進行了引用，會引起NPD警報，該警報對應的相關變量為指針*ptr，4個NPD警報對應著相同的符號表達式，屬于恒等關聯關系。

圖3 警報恒等關聯示例Fig.3 Alarm identity association example

圖4為Uucp-1.07/prot.c中檢測出的另一個警報關聯實例。第244行、第248行、第251行各報告了一個OOB警報，244行和248行因為潛在的存在分母為0的取值可能，第251行中drawWidth取值存在小于0的可能，違反了sqrt中參數必須大于等于0的規則，drawWidth的取值來源也是多個，這3個警報存在或關聯。通過分析5個開源C工程的實驗數據，發現所用警報關聯方法在平均程序處理時間增加9.44%的情況下，可以減少21.78%～46.26%的警報判定工作。對于大型工程而言，這將在很大程度上減輕警報判定人員的工作量，從而可以提高整體的缺陷檢測效率。

圖4 警報或關聯示例Fig.4 Alert or association example

表1 警報關聯數據Table 1 Alert associated data

4.3 相關方法對比

基于警報關聯的抽象解釋優化試圖通過警報間的關聯性對靜態分析報告的警報分類，對于存在關聯關系的警報，只要確定其中一個警報即可完成與之相關聯警報的判定。

本文方法與文獻[12]、文獻[13]的方法都是在抽象解釋技術框架下，對檢測到的警報進行警報關聯。不同之處是，文獻[12]借鑒反例求精思想方法，首先需要對被測程序生成一個超級控制流圖進而進行完整的程序分析，這種分析無疑將需要大量的時間和空間開銷，在大型程序的分析過程中無法實現；文獻[13]采用程序切片技術的方法，首先給出了警報關聯的定義，然后正式提出了警報錯誤狀態切片，將警報的錯誤狀態切片作為一種程序的外部輸入約束，進而得到基于外部約束的程序求精語義。采用符號表達式的方法，基于警報對應符號表達式的邏輯關系推導出警報間的關聯。本文方法與文獻[12]、文獻[13]方法主要有以下幾方面區別。

4.3.1 警報關聯精度

文獻[12]方法主要是實現過程內警報間關聯，無法實現過程間警報關聯。文獻[13]方法主要局限于警報錯誤狀態切片過程中，對每一種警報類型生成對應的警報錯誤切片，由于符號化區間抽象域的表示及計算能力不足，并不能精確地利用現有靜態分析工具所提供的抽象域切除其錯誤狀態。對于警報間復雜的關聯關系及語法類警報，不能準確地得到警報的關聯關系。而本文方法利用符號表達式，通過警報對應的符號表達式間的邏輯關系，不僅可以實現過程內警報關聯，同時可以實現過程間警報關聯，且得出警報關聯精度較高。

4.3.2 警報關聯可信度

靜態分析工具DTS在前期已經得到了大量求精與優化，肖慶等[5]通過使用變量取值信息來表達程序的路徑狀態，實現了DTS的路徑敏感的分析；董玉坤等[15]在原有表達式區間抽象域的基礎上引入了符號化三值邏輯區間抽象域，不但可以表示變量間的線性關聯關系，還可以表達變量間的邏輯關聯關系。在靜態分析求精工作基礎上進行研究，所得出的警報關聯具有較高的可信度。

4.3.3 實驗效果對比

表2為本文方法與文獻[12]、文獻[13]方法同時測試Barcode、Sphinxbase、Uucp、Git、Httpd 5個工程所得數據。從實驗效果來看，主要可以分為減少警報確認數量和關聯增加時間兩大方面。由表2可知，從實驗結果中減少警報確認數量來看，文獻[12]方法的減少警報確認數量為23.42%，文獻[13]方法的減少警報確認數量為28%，本文方法的平均關聯比例為37.75%，本文方法在減少警報確認數量上均優于文獻[12]、文獻[13]的方法。當檢測工程量很大時，對減輕人工判定工作具有更好效果。從表2的增加時間來看，本文方法的增加時間為9.44%，略低于文獻[12]方法的增加時間15.06%，但高于文獻[13]方法的增加時間8.81%。但目前的計算機處理性能都相對比較高效，時間上的增加也不是很多，屬于在可以接受的范圍內。

綜合來看，本文方法可以在更高精度、可信度下識別出警報間的關聯，從而可以更好地減輕人工判定工作的工作量。

表2 相關工作對比Table 2 Related work comparison

5 結論

提出了一種基于符號表達式的程序語義缺陷警報關聯識別方法。首先提出警報關聯的定義，然后通過警報相關變量對應的符號表達式之間的邏輯關系，總結出恒等、非、或、與四種類型的關聯關系，其中通過符號化函數摘要實現了過程間警報關聯，最后通過警報關聯算法實現了過程內警報關聯和過程間警報關聯。通過實驗驗證得出，本文方法可以有效地實現警報間的關聯，在程序處理時間略有升高的情況下，平均可以減少37.75%的人工判定警報工作量。

所做工作的局限性在于，研究主要集中在如何構建警報間的關聯關系，因此在警報關聯的結果中可能會存在誤關聯現象。如何改進警報間存在的誤關聯，進一步提高對實際工程的應用，仍然是下一步需要改進的方向。