程序狀態條件合并中變量隱式關聯分析方法

郭 曦 王 盼

1(華中農業大學信息學院計算機科學系 武漢 430070)2(武漢電力職業技術學院電力工程系 武漢 430079)

程序分析的一個主要目標是提高路徑的覆蓋率，從而對程序的行為、狀態和屬性等特征進行分析.然而在實際操作過程中，窮盡地覆蓋分析往往導致過大的時空開銷，并且伴隨有極大的狀態冗余以及約束條件精度丟失.現有的程序分析方法通常采用符號執行和約束求解的方法來開展各種分析，其中存在的問題主要有狀態空間爆炸和約束求解器對于路徑約束求解能力的限制等.導致狀態空間爆炸的原因，除了程序本身的規模決定了搜索空間呈指數級增長之外，程序狀態合并的效率、輸入集合的優化程度以及約束求解器對于不同類型符號表達式的求解能力等，都會導致分析的時空開銷激增，從而極大地影響分析的效率.

狀態合并作為減少狀態空間爆炸的常見方法，其思路是對不同的執行路徑進行分析，在合并點通過引入輔助變量[1]來對目標變量進行表示，從而區分輸入的符號值.但是引入的輔助變量往往會極大影響后期的約束求解器的求解效果，因為目前的約束求解器對于線性約束有較好的處理效果，但當約束條件中存在浮點類型數據、函數調用等結構時，約束求解器為了能夠持續運行，可能會刪除部分路徑條件或者停止工作從而導致分析結果不完備.同時在逆向符號執行過程中，路徑條件在改變執行路徑過程中，可能會導致部分路徑條件丟失的問題，從而遺漏部分執行分支使分析結果不夠精確.

本文針對符號執行過程中通常使用的狀態合并方法進行優化研究，使用改進符號表達式表示形式的方法，提高約束求解器的分析效果，從而減少狀態空間爆炸對于路徑分析效率的影響.在該過程中，針對路徑條件在迭代分析過程中存在條件丟失的問題，提出改進的路徑條件優化組合方法，以提高路徑分析的精度.本文主要貢獻有2個方面：

1) 通過對狀態合并的符號表示方式進行改進，將路徑約束與目標變量作為一個整體參與分析，從而精簡符號執行樹的表示形式；

2) 基于該符號執行樹，根據基本塊的之間的依賴關系對路徑條件進行優化組合，減少路徑條件的丟失，提高逆向分析的精度.

1 相關研究進展

符號執行作為主流的程序分析方法在路徑覆蓋、測試用例生成等研究方向發揮了重要的作用.符號執行的主要思路是使用符號替代具體的數值作為程序的輸入，模擬程序的執行，通過收集、求解路徑中的條件表達式來研究程序的狀態和性質.隨著程序規模的增大，其狀態搜索空間呈指數增長，同時大量冗余的執行分支以及因為約束求解器的分析性能導致的路徑遺漏等問題嚴重影響了分析的效果.為了緩解狀態空間爆炸帶來的影響，狀態合并[2]作為目前主要的分析方法得到了廣泛的應用，它通過分析不同路徑的符號表達式在合并點的狀態來研究各種合并策略[2-5].SMART[2]通過計算程序的函數摘要的方法生成測試用例集，并使用輔助變量來對不同路徑的符號狀態進行合并.MergePoint[3]采用符號執行和狀態合并的搜索方法，狀態合并的操作只能在沒有函數調用、跳轉語句的程序中才能使用.SMASH[4]使用不可達分析的方法對程序狀態進行分析，并刪除與需求不相關的執行路徑.這幾種方法都在函數調用時引入了輔助變量，它會增加符號變量分析的難度，從而進一步制約了約束求解器的求解性能[5].ROSSETTE[6]使用減少輔助變量引入的方法對狀態合并展開分析，但該方法只能適用于對等的數據結構.對于狀態空間中的冗余狀態以及不可達狀態，主要通過分析當前狀態是否出現在之前的分析結果中，以及將狀態空間分解為若干獨立的子空間的方法進行研究.JPF[7]使用狀態匹配的方法減少狀態規模，Boonstoppel等人[8]使用讀寫集的方法來簡化狀態匹配條件.文獻[9-10]使用程序切片的方法對狀態空間進行分組.函數摘要[11-12]作為一種靜態分析方法，主要對接口符號變量開展分析，該過程可以與別名分析、可達分析、指向分析等方法進行協同工作.這些方法都存在對程序行為推理不夠精確的問題.靜態單賦值(static single assignment, SSA)通過改變變量的下標，獲得不同變量的定義，使得每個變量只有惟一的定義，同時每個變量只有一條定義-使用鏈，主要應用于程序分析、編譯器優化等領域[13].文獻[14]提出將變量轉換為守衛符號表達式集合的符號執行方法，但該方法并未分析路徑條件的順序對約束求解的影響.文獻[15]基于程序輸出的符號將程序的執行路徑進行劃分，從而對回歸測試和程序版本進行測試，該方法并沒有對路徑條件的表示形式進行優化，易導致約束求解器停止工作.文獻[16]通過分析缺陷的類型以及關聯的路徑，以計算不同上下文中危險操作的覆蓋能力為目標，使用符號執行的分析方法來生成高效輸入.文獻[17]采用抽象引導的半形式化方法框架對候選狀態進行評估，生成能夠覆蓋多個目標狀態的狀態序列.文獻[18]從最短路徑、條件約束集概率和可達路徑數量的角度，通過推遲變量實例化的方法緩解路徑組合爆炸問題.

Fig. 1 Symbolic execution tree圖1 符號執行樹

針對狀態合并分析過程中由于輔助變量的引入帶來的約束求解困難問題，以及路徑約束條件在求解過程中存在條件遺漏的問題，本文以傳統的符號執行樹為起點，以基本塊為單位對符號執行樹進行優化表示，將相同的基本塊進行合并，從形式上約簡符號執行樹的規模.在狀態合并過程中，將約束條件和目標變量作為整體向目標變量提供反饋信息，從而避免輔助變量的引入.在路徑條件的約束求解階段，本文以程序輸出語句為起點，采用逆向符號執行和流敏感的數據流的分析方法，提取能夠改變輸出變量值的隱式語句集合，再通過對路徑約束條件的重新組合，使得約束條件在新的路徑分析過程中得以完整地保留，避免因約束條件丟失帶來的路徑搜索不完備的問題.與傳統基于狀態合并的符號執行方法相比，本文方法可以減少符號表達式和路徑約束條件的數量，同時在約束條件求解過程中有更高的分析精度.

2 符號執行和狀態合并

符號執行的基本思想是使用變量符號來代替具體的輸入值，模擬程序的執行.這種抽象的分析方法相對于具體的執行可以獲得更多的路徑信息，從而可以更加高效地生成測試用例，以及挖掘未執行的路徑.

定義1. 路徑條件(path condition).對于一個程序P、一個測試輸入t，設π為P在t作用下的執行路徑，其對應的路徑條件φ是由π中的分支條件等信息組成的一階邏輯公式.

路徑條件的生成是符號執行中的一個重要步驟，在程序的一次執行過程中，當遇到條件分支時，符號執行工具會收集當前的分支條件，并計算在t作用下的約束公式，該約束公式由該路徑中所有分支條件進行連接得出.任何輸入只要符合t所對應的路徑約束條件都會產生與t一致的執行路徑.

對于圖1(a)所示的程序，傳統符號執行所生成的符號執行樹如圖1(b)所示.符號執行在執行過程中需要保存當前的符號狀態：由符號表達式組成的變量，以及當前路徑條件φ.當執行過程中遇到分支條件時，符號執行工具使用可達的分支對應的當前路徑條件φ更新當前的符號狀態.

對于圖1(a)所示的程序，傳統的符號執行采用符號值x0,y0,z0分別替代輸入變量x,y,z.對于圖1(b)所示的每條執行路徑，符號執行會記錄該路徑所對應的狀態，圖1(b)所對應的狀態集合如表1所示.同時將圖1(b)轉換為圖1(c)所示的形式，即將相同的結點進行合并，可以有效減少執行路徑集合中結點存儲的次數，第3節的分析也是基于轉換后的符號執行樹.

Table 1 State Set of Symbolic Execution表1 符號執行狀態集合

Fig. 2 Potential dependent analysis圖2 隱式依賴分析

符號執行在遇到新的路徑分支時，會將該路徑條件加入到狀態集合中，并依據路徑的可達性對各符號變量的值進行更新.路徑條件φ可以表示為φ=φ1∨φ2∨φ3∨φ4∨φ5.由于符號執行對于路徑的搜索依賴于路徑條件φ，即通過反轉最近新增的路徑條件符號的值來進行，例如對于程序ifkthena=0.3 elsea=fun(b)，其符號執行狀態可以表示為(k=k0)∧((k∧a=0.3)∨(k∧a=fun(b))).圖1(a)中的程序具有嵌套分支條件，可以產生類似的執行狀態.注意到表1中φ5所在的行對應的輸入變量存在浮點數，在現實程序中除了浮點數以外，存在函數返回以及庫函數調用等方式對變量的賦值，目前的約束求解器在處理浮點數以及函數調用等類型的約束條件時，其分析性能受到很大限制.故這種符號執行狀態表示方法在實際分析過程中，存在較高的概率使得約束求解器丟棄不能求解的約束條件，從而影響分析的精度.本文使用一種新的狀態表示方法，將狀態表達式中的路徑條件φ和輸入變量符號作為2個獨立的部分進行表示，從而緩解因約束求解器性能而導致的求解不完備或中斷問題，第3節將詳細分析該方法的工作過程.

逆向符號分析由于具有明確的分析目標，故在路徑挖掘、程序調試等方向有廣泛的應用.在逆向分析過程中，目標語句一般選取最后一條表達式語句，也可以通過設置斷言的方法將某一可疑語句設為目標語句.從目標語句開始，對程序進行逆向分析直到程序的入口語句，該過程中目標語句可以表示為程序輸入的符號表達式，從而枚舉出與目標語句相關的路徑條件表達式集合.

與目標語句相關的符號分析方法可以精簡地表示程序全部執行路徑，該處用與目標語句中變量b相關的3個符號表達式就可以概括圖2(a)的全部8條執行路徑.依據程序輸出，將程序執行路徑集合進行分組，即2條執行路徑π1，π2對應的輸出符號有相同的表達式形式，則π1和π2有相同的關聯切片[19].關聯切片對數據依賴、控制依賴進行傳遞閉包運算.數據依賴和控制依賴依據執行路徑π中修改目標語句中變量值的語句集合進行分析.

定義2. 直接依賴.設b1和b2為符號執行樹中的2個結點，v為目標語句中的變量，如果：

1)b1重新定義了變量v的值；

2)b2中的語句使用了變量v的值；

3)b1和b2之間存在一條可達路徑π，同時在π中的所有語句均沒有重定義變量v的值；

則稱b2直接依賴于b1.直接依賴是符號執行樹中最常見的依賴形式，圖2(b)中實線表示2個結點存在直接依賴關系，但是在逆向符號執行分析過程中，目標語句中的變量在不同的執行路徑π中會有不同的語句對其符號值進行重定義，故存在如下定義:

定義3. 隱式依賴.對于程序P中的一條執行路徑π，目標語句為s，π中某條語句s′對應的路徑條件為φ，稱s隱式依賴于s′，當且僅當以下條件成立:

1)s具有與φ一致的路徑條件sφ；

2)s中的變量v在π中的語句集合中都沒有被重新定義，但v在s與s′之間另一條路徑π′中被重定義了；

3) 通過反轉φ中某個邏輯公式的值，可以觸發新路徑π′的執行.

定義4. 依賴條件(dependency condition).對于程序P中的一條執行路徑π，目標語句為s，π中某條語句s′對應的路徑條件為φ，若s隱式依賴于s′，同時經修改φ中若干分支謂詞表達式的真值，得到φ′，使得s與s′之間另一條路徑π′可達，則該分支謂詞φ′表達式構成路徑π的依賴條件.

以圖2(a)所示的程序為例，對比傳統符號執行、傳統逆向分析和依賴條件分析在路徑條件φ表達方面的區別.設圖2(a)所示的程序的一組輸入為{x=6,y=2,z=2}，記語句④，⑧，⑩對應的謂詞表達式分別為p1,p2,p3，它們在當前輸入下的真值分別為true,false,true，對應的執行路徑π可以標記為[p1,t,p2,f,p3,t].在當前輸入值的作用下，傳統符號執行的路徑條件為(x-y>0)∧(x+y>10)∧(z×z>3).對于傳統逆向分析，以語句為目標語句進行逆向分析，由于p2的真值為false，故語句⑨沒有對目標語句中的符號變量b進行重定義操作，此時與符號變量b相關的路徑為[,②]，p1,p2,p3均不出現在該路徑條件中，故逆向分析的路徑條件為true.依賴條件分析在收集路徑條件的過程中，加入了流敏感的數據流分析方法，故可以通過“定義-使用鏈”分析來提取對變量b有重定義操作的符號語句位置，這些對目標變量有隱式作用的語句集合S′成為隱式依賴分析的依據，在p1,p2,p3的取值過程中，通過修改部分謂詞表達式的真值能夠實現對S′可達，則這些謂詞表達式構成目標語句的依賴條件.本例中若p2的當前真值經修改為true，則語句⑨對目標語句中的符號變量b有重定義操作，從而改變程序的輸出結果，此時逆向分析的路徑為[,⑧,②]，對應的依賴條件為(x+y>10).只要輸入符合該依賴條件，則可以使目標語句中的符號變量b有相同的符號表達式.

基于路徑條件的程序分析主要用來提高語句或者分支的覆蓋率.隱式依賴分析可以將程序的輸入符號以及依賴條件與目標語句中的變量符號進行關聯，對于依賴條件φ1∧φ2∧…∧φn,每次路徑分析時通過取反最近加入的條件表達式來獲取不同的路徑，即通過約束求解器對集合{φ1∧φ2∧…∧φi|1≤i≤n}的可滿足性進行分析，若某個路徑條件可解，則將其從集合中刪除，當集合為空時分析結束.對于程序2(a)以及一組輸入{x=6,y=2,z=2}，其路徑分析過程如表2所示：

Table 2 Paths Analysis Based on Dependent Condition表2 基于依賴條件的路徑分析

3 符號簽名與依賴條件重構

經過第2節的分析可以將一段程序生成精簡的符號執行樹，并在其基礎上進行路徑條件的生成以及路徑搜索操作，從而提高語句和分支覆蓋率.但在上述分析過程中存在2個問題：

1) 現有的路徑條件中常包含較為復雜的數據結構和方法調用，這種表示形式對于主流的約束求解器難以求解，故約束求解器需要刪除某些不能求解的邏輯公式從而保持求解過程的連續性，但這種直接刪除的邏輯公式往往包含關鍵的路徑信息，從而使得求解的結果不完備.

2) 新路徑的生成需要對依賴分析后的路徑條件進行增量修改，但在增量修改過程中存在部分約束表達式丟失的現象.其原因是約束求解器在增量求解過程中，對依賴條件產生的輸入符號可能與之前增量過程所產生的輸入符號相同，導致該依賴條件在下一步的增量分析中被刪除，這種間接刪除的邏輯公式會屏蔽部分新路徑的發掘，從而對約束求解器的分析精度產生影響.

對于第1個問題，本文使用符號簽名的方法，使用新的路徑條件表示形式，將路徑條件中目標語句包含的符號表達式抽出，從而避免狀態合并中輔助變量對于約束求解器的干擾，提高約束求解器的執行效率.對于第2個問題，本文提出依賴條件的優化表示算法，減少因間接刪除邏輯公式所產生的影響.

3.1 符號簽名

符號執行的方法在一次計算過程中，對每個變量只保存一個符號表達式，故在狀態合并時，對于在多次執行過程中有多個符號表達式的變量，需要引入輔助變量來代替該變量的符號表達式.例如對于圖1(a)中語句⑥，對應的符號執行狀態如表3所示，由于變量z在3條路中有不同的符號表達式(z0,2.5)，則在狀態合并時，需要引入輔助變量z′來表示[14]，如表4所示，狀態合并后的路徑條件φ為每條路徑對應的路徑條件與當前變量z的符號值的合取操作進行析取.

若基于表4的結果進行約束求解，由于路徑條件中存在諸如z′=2.5這樣帶有浮點數運算的表達式，則約束求解器在計算過程中可能受制于求解能力而導致狀態合并失敗，故下面給出在不影響路徑條件邏輯含義的基礎上刪除輔助變量的方法.對于圖1(a)的程序，其符號執行的最終狀態如表1所示.這種表示方法難以直觀地獲得每個變量對應的符號值集合以及每個符號值對應的約束條件.

Table 3 Example of Intermediate State (Statement ⑥ in

Table 4 Example of State Merging表4 狀態合并示例

對于一個程序P，其輸入變量集合為T(t1,t2,…,tm)，P的路徑條件集合記為Φ(Φ=φ1∨φ2∨…∨φn)，設某個輸入變量t(t∈T)在狀態合并點對應的符號值集合為V(V=v1∨v2∨…∨vi)，則有如下定義.

定義5[14]. 符號簽名(symbol signature).令某個符號表達式vk對應的路徑條件Φv k為：

{φx∨φy∨…∨φz|1

例如對于圖1(a)的程序，依據表1所示的狀態表和符號簽名的定義，可以將其轉換為符號簽名視圖[14]，該視圖反映了圖1(a)中語句⑧位置經狀態合并后程序的最終狀態：

(1)

注意式(1)中沒有輔助變量，且邏輯上與含有輔助變量的狀態一致.下面分析式(1)的產生過程.首先對于圖1(a)中的狀態合并點語句⑥，語句①～⑥對應的符號執行狀態如表3所示.

對于即將執行的語句⑥，其邏輯表達式z>2需要進行運算以求出下一個合并點，即語句⑧處的符號簽名視圖.對于變量z對應的符號表達式z0和2.5，進行z>2的運算，即此時語句⑥對應的符號簽名為{(φ5,z0>2),(φ5,2.5>2)}，由于 (2.5>2)恒為真，故可以表示為{(φ5,z0>2),(φ5,true)}.此時語句⑥對應的路徑條件為φ6=(φ5∧z0>2)∨(φ5∧true).

當φ6可滿足時語句⑦可達，此時的y=z-1運算存在對變量y的重定義，變量y在目標語句⑧處對應的符號簽名為：y={(φ6,y0),(φ5∧φ6,z0-1),(φ5∧φ6,1.5)}，這和式(1)中的y的符號簽名在邏輯上是等價的.此時依據前一個狀態合并點的符號執行狀態信息和符號簽名信息，計算出程序最終狀態的符號簽名信息，這與依據程序最終狀態的符號執行狀態獲得的簽名信息在邏輯上是一致的.

這種符號簽名視圖可以直觀地獲得每個輸入變量在合并點處的符號值以及對應的路徑條件，對于表2中不同的符號值，采用灰色背景進行標記.符號簽名的特點如下.

1) 對于某個符號表達式的符號簽名vs，設(φ1,v1)和(φ2,v2)是vs中的2個不同元素，若v1=v2，則這2個元素可以合并為(φ1∨φ2,v1)，且此時的符號簽名等價于vs{(φ1,v1),(φ2,v2)}∪{φ1∨φ2,v1}；

2) 如果vs中存在形如(false,v)的元素，則可以將其從vs中刪除.

符號簽名的表示形式相對于傳統符號執行的狀態表示形式，其最大優點在于不同執行路徑的路徑條件表達式和變量的符號表達式，在符號簽名中的表達形式中可以共享，例如在圖1(a)中語句⑥處，傳統符號執行依據路徑條件有3條不同的執行路徑，但通過符號簽名分析，可以獲得在此處變量z的2個不同符號值(r0,2.5)，從而減少對約束求解器的調用次數.

本文將變量符號與符號簽名之間建立起關聯，使用符號簽名的常用符號執行語義[14]表示如圖3所示：

Binary Operation:

Condition Operation:

Fig. 3 Symbol execution semantic
圖3 符號執行語義

其中v1⊙v2表示對2個符號簽名v1和v2進行合并操作，但與普通的合并運算的區別于v1⊙v2還進行重復的路徑條件和約束表達式的共享，從而減少對求解器的調用.更新操作主要使用⊙運算符進行運算，其中當路徑條件φ可滿足時，則將符號簽名v1作用于后續路徑中的符號簽名，當φ可滿足時，將v2作用于后續路徑中的符號簽名.當存在對變量符號進行賦值操作時，常量操作和符號輸入操作對該變量符號值進行更新，該過程中⊙運算只對滿足路徑條件φ的執行路徑中的賦值操作進行運算.二元運算主要對2個符號變量(a,b)間存在二元運算符時進行操作，運算結果為變量a的符號表達式與變量b的符號表達式的笛卡兒積.在條件運算中，當條件表達式e可滿足時，則對e和后續可達語句s的各自符號簽名進行笛卡兒積運算，并將e對應的符號表達式并入到當前的路徑條件中，當e不可滿足時，則需要對x的每個符號簽名中的符號變量進行分析.

3.2 依賴條件重構

對于程序的一次執行，傳統的路徑發掘方法具有如下性質：如果φ1∧φ2∧…∧φn為該執行對應路徑條件的一個前綴，則滿足條件φ1∧φ2∧…∧φn的輸入，其對應的路徑條件均以φ1∧φ2∧…∧φn為前綴.通過第2節分析，該性質對于依賴條件不成立.由于依賴條件dc在邏輯上要弱于路徑條件pc，即φ?dc，故對于依賴條件所具有的性質：如果φ1∧φ2∧…∧φn為程序一次執行對應依賴條件的一個前綴，則滿足條件φ1∧φ2∧…∧φn的輸入，其對應的依賴條件均以φ1∧φ2∧…∧φn為前綴，由于φ?dc，此時該性質也適用于路徑條件.

導致依賴信息丟失的原因是依賴條件的表示方法，為了能夠獲得遺漏路徑的依賴條件，需要將現有的依賴條件表示方法進行修改，即采用依賴條件重構的方法對目前的依賴條件進行重新排序.依賴條件重構的算法[15]如下所示.

算法1. 依賴條件重構算法.

輸入:程序P、測試集t、目標語句C;

輸出:重構后的依賴條件DCR.

①Stack=?;

② 執行函數Execute(t,0);

③ whileStack≠?

④ 將pop(Stack)的值賦給(f,j);

⑤ iff不能被滿足

⑥a是一個可以滿足f的輸入;

⑦ 將a賦值給T;

⑧ 執行函數Execute(a,j);

⑨ end if

⑩ end while

其中函數Reorder( )用來對現有的依賴條件序列進行重構，其工作過程類似于快速排序算法.對于由多個邏輯表達式序列seq組成的待重組的依賴條件dc，該算法依據最近加入的條件表達式e將待重組的序列seq分解為2個子序列seq1和seq2，seq中與e存在隱式依賴的邏輯表達式依據seq中的相對順序存放到seq1中，對應地將seq中與e不存在隱式依賴的邏輯表達式依據seq中的相對順序存放到seq2中，并將e存入到一個棧Stack中.然后分別對seq1和seq2重復上述過程，直到棧Stack=?，最后程序輸出為重組后的路徑分支表達式.圖4表示該算法的執行過程[15].其中圖4(a)表示待重組的序列seq中邏輯表達式之間的隱式依賴關系，其中每個邏輯表達式用一個結點表示，例如e6→e1，則表示e6隱式依賴于e1.初始時，由于e6與其他結點存在隱式依賴關系，故將e6存入棧Stack中，并以e6為中心結點，將其余結點依據是否存在依賴關系依據原始相對順序移到e6兩側.由于e1和e3均與e6存在隱式依賴，故將e1和e3依據原始序列seq中的順序存放到e6左側，記為seq1，e2，e5，e6則存放到e6右側，記為seq2.然后分別對seq1和seq2重復上述過程，直到棧Stack=?，此時重構后的依賴條件序列.當每次從棧Stack中彈出一個依賴條件，函數Execute( )需要對該依賴條件的可滿足性進行分析，若該依賴條件可解，則可以計算出對應的輸入i，該輸入i可以生成新的依賴條件，并對該依賴條件進行分析.為了提高分析速度，在函數Execute( )的參數中加入了一個參數n，該參數用以指示分析從當前序列第n個結點開始，如該節開頭分析，前n個結點的作為前綴時，分析結果能夠得以傳遞到下一次迭代分析中，從而提高分析的速度.在表2的分析結果基礎上，算法1的執行步驟如表5所示，其中第3個函數中生成了表2中未能發掘的路徑[p1,f,p2,t,p3,t]，如表5中灰色背景標記所示.

Fig. 4 Example of dependent condition reconstruction圖4 依賴條件重組示例

StepInputPathDependency ConditionDependency Condition After Reconstruction1{x=6,y=2,z=2}[p1,t,p2,f,p3,t](x+y>10)(x+y>10)2{x=6,y=5,z=2}[p1,t,p2,t,p3,t](x-y>0)∧(x+y>10)(x+y>10)∧(x-y>0)3{x=5,y=6,z=2}[p1,f,p2,t,p3,t](x-y>0)∧(x+y>10)(x+y>10)∧(x-y>0)

通過符號簽名的分析方法對路徑條件的表示形式進行修改，并在此基礎上使用依賴條件重組算法對路徑中的依賴關系進行分析，可以有效減少傳統符號執行方法和狀態合并方法因直接刪除或間接刪除路徑條件所帶來的分析精度上的損失.

定理1. 對于程序P對應的2個輸入t1和t2，ti(i=1,2)對應的執行路徑為π(ti)，設s是π(t1)中的一條語句，但s不在π(t2)中.設b為π(t1)中的最后一個分支條件，且有sb，同時b也在π(t2)中，此時b在π(t1)和π(t2)中有不同的表達形式.

證明. 采用反證法.依據已有條件sb，設b′→b為π(t1)中從s到b的路徑中的最后一個連接，此時有sb′→b.此時假設b在π(t1)和π(t2)中有相同的表達形式，則b同樣也在路徑π(t2)中，故在π(t2)中b也滿足sb，即b也出現在路徑π(t2)中，這與定理中b為π(t1)中的最后一個滿足sb分支條件的條件相矛盾，故b在π(t1)和π(t2)中有不同的表達形式.

證畢.

定理2. 對于程序P對應的2個輸入t1和t2，ti(i=1,2)對應的執行路徑為π(ti)，設s是π(t1)中的一條語句，若t2=dc(s,π(t1))，則s是路徑π(t2)中一條語句.

證明. 設si和sj是2條有先后順序的語句，即si→sj，則由sj和π(t1)共同決定的路徑π(sj,π(t1))中的語句都會包含在由si和π(t1)共同決定的路徑π(sj,π(t1))中，故dc(si,π(t1))?dc(sj,π(t1)).因t2dc(si,π(t1))，故t2dc(sj,π(t1))，從而sj將包含在π(t1)和π(t2)中，即任意的si是路徑π(t2)中一條語句.

證畢.

定理1使得依賴條件可以確保在目標語句中，每個符號變量只有惟一的符號值.定理2使得對于一個可達路徑π，本文方法可以發掘一條路徑π′，使得π′和π有相同的依賴條件.

4 實驗及分析

本文在WALA平臺上構建實驗原型系統，該平臺可以讀取待分析的程序，構建程序調用圖和控制流圖，同時采用Z3作為約束求解器，對線性約束表達式和字符串進行求解操作.Java語言由于具有動態類型，使得變量在分析過程中可以方便地替換為符號表達式或者具體的數值，故本文以Java程序為測試集.實驗方案如圖5所示:

Fig. 5 Experimental setup圖5 實驗方案

依賴條件是在逆向符號執行過程中生成的.對于目標語句中的符號變量，主要分析與其有重定義操作的語句集合.實驗以狀態合并和符號執行作為分析工具，主要實驗內容包括：對比傳統狀態合并方法和本文方法在狀態合并上的數量，以及相對于傳統符號執行方法，本文方法在發掘可行的隱式路徑數量上性能的提升.同時驗證了路徑條件和符號表達式的共享在符號簽名的分析方法中的有效性.

表6中“符號簽名均值”表示程序中各符號變量在不同路徑中對應的不同符號表達式個數的平均值，符號簽名的平均值不超過6.該值越小，表明程序變量間的隱式依賴數量越少.“符號簽名共享比率”表示達到目標位置的不同路徑的數量與該目標位置的符號簽名個數的比值，表明路徑表達式和符號表達式在不同路徑中存在相同的前綴，故在新路徑發掘過程中，可以有效利用相同的前綴從而減少重復分析帶來的額外計算開銷.“傳統合并方法合并程度”表示對當前程序進行傳統合并方式與本文方法在狀態合并數量上的比值.從表6中可以看出除了3個程序，本文方法在其余程序中均可以較傳統方法有更多的狀態合并.在進行符號執行過程中，本文方法相對于傳統的符號執行方法DART，均可以減少時間開銷.其中“有效路徑對比”表示傳統符號執行方法所生成的路徑數量與本文方法所生成的路徑數量的比值，由于本文方法采用了符號簽名和依賴條件重組的分析方法，能夠有效減少因直接刪除和間接刪除依賴條件所導致的路徑分析精度上的損失.約束求解器在程序分支條件處需要對當前的分支條件表達式進行求解，由于約束求解器在計算過程中有較大的時間開銷，故在實際分析過程中需要盡可能減少約束求解器的調用次數.“求解次數比率”表示傳統符號執行方法與本文方法在調用約束求解器時數量的對比.由于采用了共享路徑條件和符號表達式的分析方法，故本文方法能夠較少地調用約束求解器.

Table 6 Comparison of State Merging and Symbolic Execution表6 狀態合并和符號執行的對比

Fig. 6 Comparison of path coverage圖6 路徑覆蓋率對比

為了對比在路徑發掘方面的效率，本文以表6中規模最大的3個程序為例，實驗結果如圖6所示:

本文方法使用了基于依賴條件重組的路徑分析方法，相對于傳統符號執行方法可以發掘更多的可達路徑.本文方法較傳統符號執行方法在路徑覆蓋率方面有較大提高，但沒有達到100%，其原因是對于程序執行語義的建模精度還有待提高，尤其是對于數組下表、內存地址訪問、循環終止條件等符號表達式的處理還有待進一步完善.另一個原因是約束求解器的性能對于依賴條件的求解有直接的影響，雖然本文采用路徑條件和變量符號分離的表示方法來提高約束求解器的求解性能，但同樣由于數組下表等復雜數據結構的影響，在一定程度上影響了路徑的覆蓋率，這是本文將來主要的研究工作.對于程序中一條具有n個分支條件的執行路徑，本文的方法需要約束求解器對該路徑對應的依賴條件進行n次分析，另外不同執行路徑的依賴條件之間有相似性，將來工作中可以采用并行符號執行的方法以提高這2個過程的分析效率.

5 結束語

符號執行是路徑分析中的傳統方法，但狀態空間爆炸和約束求解器性能嚴重制約了其性能的發揮.狀態合并作為一種有效的狀態約簡方法得到了廣泛的應用，但因路徑條件的表示形式影響了約束求解器求解的性能.本文采用一種基于改進符號執行樹的分析方法，在其基礎上通過分離路徑條件和符號表達式，從而可以提高約束求解器的求解性能而提高狀態合并的效率.在約束求解器的求解過程中，本文還提出了基于依賴條件的重構算法，從而避免因路徑條件的直接刪除和間接刪除所導致的路徑分析不夠完備的問題.如實驗部分所述，本文方法在路徑分析的性能方面較傳統方法有較大提高，但由于對程序中數組下標、地址解析等復雜結構執行語義建模還不夠精確，故影響了路徑覆蓋率的進一步提升.將來的工作中主要是復雜數據結構語義建模，例如可以加入靜態單賦值(SSA)的分析方法，減少路徑條件分析時引入臨時變量的數量及變量間命名的沖突，從而可以構建更為精確的路徑條件.