符號執(zhí)行中的約束求解問題研究進展

鄒權(quán)臣， 吳潤浦， 馬金鑫， 王欣， 辛偉， 侯長玉， 李美聰

(1.中國信息安全測評中心，北京 100085； 2. 360安全研究院，北京 100016；3. 北京中測安華科技有限公司，北京 100085)

在符號執(zhí)行中，對路徑約束條件的可達性判定以及生成實際的測試輸入都嚴重依賴于可滿足模理論(SMT)求解器. 雖然當前的SMT求解器已經(jīng)能夠處理較大型的約束，但對復(fù)雜約束的處理能力不足，而且隨著約束體積的增大，求解的效率會越顯低下；這使得約束求解問題成為了符號執(zhí)行中的主要瓶頸問題之一.

約束求解問題的研究關(guān)系著符號執(zhí)行的效率和性能，影響著符號執(zhí)行應(yīng)用到大型應(yīng)用程序中. 同時，這方面的研究對漏洞挖掘、自動化網(wǎng)絡(luò)攻防等領(lǐng)域也具有非常重要的意義.

本文介紹了符號執(zhí)行和約束求解的基本概念，并分析了符號執(zhí)行中約束求解問題的由來，對近年來的約束求解問題研究進展進行了歸類，展望和總結(jié).

1 符號執(zhí)行與約束求解

1.1 SMT理論

可滿足模理論(satisfiability modulo theories， SMT)主要用于自動化演繹的研究方法，是為了檢驗基于邏輯理論的一階謂詞公式的可滿足性而提出[1]，已經(jīng)被廣泛應(yīng)用于模型檢測、自動化測試生成等計算機科學(xué)領(lǐng)域. 典型的應(yīng)用理論主要包括了各種形式的算術(shù)運算、數(shù)組、有限集、比特向量、代數(shù)數(shù)據(jù)類型(algebraic datatypes)、字符串、浮點數(shù)以及各種理論的結(jié)合等.

相對于SAT(boolean satisfiability problem)求解器，SMT求解器不僅僅支持布爾運算符，而且在使用SMT求解器解決問題的時候不需要把問題轉(zhuǎn)化成復(fù)雜的CNF(conjunctive normal form)范式，能大幅度簡化求解問題.

當前性能比較好的SMT求解器有CVC[2]、Z3[3]、STP[4]、YICES[5]、MathSat[6]等，其性能對比如表1所示. 其中Z3求解器在每年的SMT求解器競賽[7]中各方面的性能都名列前茅，通過內(nèi)置理論對一階邏輯多種排列進行可滿足性校驗，Z3當前支持如位向量、實數(shù)和整形運算(有限支持非線性運算)、陣列、函數(shù)和謂詞符號、元組、枚舉類型和代數(shù)(遞歸)數(shù)據(jù)類型等理論.

表1 常用SMT求解器對比

SMT理論和技術(shù)的發(fā)展是驅(qū)動符號執(zhí)行應(yīng)用于大型程序最主要的動力之一，同時當前SMT求解器能力和性能的不足也制約著符號執(zhí)行應(yīng)用的發(fā)展.

1.2 符號執(zhí)行中的約束求解問題

符號執(zhí)行在20世紀70年代被提出[8-12]，是一種能夠系統(tǒng)性探索程序執(zhí)行路徑的程序分析技術(shù)，通過對程序執(zhí)行過程中的被污染的分支條件及相關(guān)變量的收集、翻譯、取反，生成新的路徑約束條件，然后使用SMT求解器進行求解,判斷路徑的可達性以及生成相應(yīng)的測試輸入. 通過這種方式產(chǎn)生的路徑與測試輸入之間的關(guān)系是一一對應(yīng)的，能夠避免冗余測試輸入的產(chǎn)生，并有效解決模糊測試中冗余測試用例過多導(dǎo)致的代碼覆蓋率低的問題.

自符號執(zhí)行特別是動態(tài)符號執(zhí)行[13-14]技術(shù)提出以來，目前已經(jīng)廣泛應(yīng)用于程序分析的各個領(lǐng)域，如自動化測試輸入生成、漏洞挖掘、漏洞利用自動生成、簽名生成、協(xié)議逆向工程等. 很多相關(guān)的項目和工具也已經(jīng)被應(yīng)用到實際的漏洞挖掘當中，如angr[15-17]、KLEE[18]、Bitblaze[19]、Mayhem[20]、SAGE[21-23]、S2E[24]等. 其中微軟開發(fā)的符號執(zhí)行工具SAGE已經(jīng)被應(yīng)用到了微軟內(nèi)部的日常開發(fā)安全測試中，每天有上百臺機器同時在運行此工具，并已聲稱發(fā)現(xiàn)了Windows 7系統(tǒng)中1/3的漏洞[23]. MergePoint已經(jīng)在Debian系統(tǒng)下發(fā)現(xiàn)上千個bug，其中有上百個被證實是安全漏洞[25]. 另外，在2016年8月份由美國國防部高級研究計劃局(DARPA)舉辦的全自動化的網(wǎng)絡(luò)安全挑戰(zhàn)賽(cyber grand challenge)[26]決賽中，大部分團隊都采用了符號執(zhí)行技術(shù)對測試集進行漏洞挖掘. 符號執(zhí)行技術(shù)將成為未來網(wǎng)絡(luò)攻防自動化和智能化的重要技術(shù)基礎(chǔ).

雖然符號執(zhí)行相比其他程序測試和分析技術(shù)有諸多的優(yōu)勢，在科研和工業(yè)領(lǐng)域也取得了長足的進展，但就當前的形勢而言，要大規(guī)模應(yīng)用到工業(yè)領(lǐng)域，仍然還有很多問題需要解決. 如路徑爆炸、約束求解、浮點計算、內(nèi)存建模、環(huán)境交互以及并行計算等問題是符號執(zhí)行急需解決的問題，這些問題影響著符號執(zhí)行應(yīng)用到大型應(yīng)用程序當中.

約束求解問題是符號執(zhí)行遇到的主要瓶頸問題之一[27]. 在符號執(zhí)行中，因為對路徑約束條件可達性的判定以及相應(yīng)路徑的測試輸入的計算都需要頻繁地調(diào)用SMT求解器進行求解，而路徑的數(shù)量關(guān)系著對SMT求解的頻率，每條路徑約束的體積和復(fù)雜度影響著單次求解的效率和能力. 目前SMT求解器在能力上對浮點運算和非線性運算的支持并不好，而在求解效率上，雖然每年的SMT求解競賽一直在促進這方面的研究，但約束求解本身是一個NP完全(NP-complete)問題,在最差的情況下求解NP完全問題的復(fù)雜度為指數(shù)級，求解器的性能和能力仍然受限于可滿足模理論(SMT)的研究進展. 頻繁調(diào)用加上高的求解難度直接導(dǎo)致約束求解占用了符號執(zhí)行系統(tǒng)中的大部分資源消耗.

另一方面，近年來也有研究人員采用符號執(zhí)行輔助模糊測試繞過校驗和檢驗機制[28]或者引導(dǎo)路徑探測[29-32]. 如Stephens等[31]采用模糊測試和符號執(zhí)行交替探索程序執(zhí)行路徑，解決模糊測試陷入代碼覆蓋率增長慢的情況，這樣能引導(dǎo)模糊測試探索到程序更深層次的節(jié)點，也能直接避免符號執(zhí)行可能帶來的路徑爆炸問題. 但Dolangavitt等[33]文獻的實驗結(jié)果表明，使用符號執(zhí)行對模糊測試中部分路徑約束求解時，仍然有很大一部分路徑出現(xiàn)求解失敗的情況(Driller實驗中有41個測試程序陷入了較淺路徑，使用符號執(zhí)行對其求解時只有13個程序能夠生成新的測試輸入). 所以基于符號執(zhí)行增強的模糊測試技術(shù)仍然會受限于符號執(zhí)行中的約束求解問題，符號執(zhí)行的引入可能會弱化模糊測試本身的可擴展性.

2 研究進展

當前，約束求解遇到的兩大問題可歸結(jié)為求解器求解能力與求解效率問題. 求解能力問題是指求解器對復(fù)雜約束條件(如浮點數(shù)以及非線性約束)處理能力的不足. 而求解效率問題是指對于含有大量的約束條件的路徑約束，求解器的性能會隨著約束條件數(shù)量的增長而逐漸下降.

針對以上問題，研究人員提出了很多約束求解性能優(yōu)化措施，主要可分為內(nèi)部優(yōu)化和外部優(yōu)化. 求解器內(nèi)部優(yōu)化是指通過優(yōu)化求解器本身對約束條件處理能力和效率來提高符號執(zhí)行的性能，雖然近年來這方面的研究已經(jīng)取得了比較大的突破[34-39]，但仍然嚴重依賴于可滿足模理論以及NP完全問題的研究進展；求解器外部優(yōu)化主要是指在調(diào)用約束求解器對路徑約束求解之前的優(yōu)化，是通過減少甚至避免符號查詢的工作來增加符號執(zhí)行性能的措施. 當前大部分技術(shù)都對路徑約束進行了啟發(fā)式處理，如精簡約束式盡量減少求解器的求解負擔；對求解結(jié)果進行緩存和重用，減少調(diào)用求解器的次數(shù)等. 本文主要關(guān)注求解器外部優(yōu)化處理問題.

對于求解器外部性能優(yōu)化問題，早期很多的符號執(zhí)行工具提出了各種切實可行的解決方案. 如CUTE[40-41]、EXE[42]和KLEE[18]提出的一系列如表達式重寫、符號值的實際替換、不相關(guān)約束的刪除以及約束緩存等的措施對路徑約束進行精簡和結(jié)果重用. 近年來，在這方面的研究又有了不小的突破，其中有Memoise[43-44]、Green[45]、GeenTrie[46]以及Recal[47]等，這些工具的提出主要側(cè)重于優(yōu)化符號執(zhí)行結(jié)果切片、標準化命名、求解結(jié)果的緩存、搜索和重用的效率等問題. 這些文獻的實驗結(jié)果表明，符號執(zhí)行結(jié)果的緩存和重復(fù)使用能在同一程序的不同路徑以及不同程序的不同路徑間的約束求解問題上大幅度減少對求解器的調(diào)用.

本文對約束求解研究的相關(guān)工作進行了梳理歸類(如圖1所示)，按照約束求解優(yōu)化措施的實施的階段(相對于對求解器調(diào)用的時機而言)不同，把近年來的相關(guān)研究工作大致分為求解前優(yōu)化、求解時優(yōu)化以及求解后優(yōu)化. 下面將對這些約束求解方面的優(yōu)化技術(shù)進行詳細介紹.

圖1 約束求解研究進展Fig.1 Research progress on constraint solving

2.1 求解前優(yōu)化

求解前優(yōu)化主要是在調(diào)用SMT求解器對路徑約束進行求解之前做的一些預(yù)處理工作，包括非相關(guān)約束分支切片、約束簡化以及冗余約束精簡等. 這些工作既能減小路徑約束的體積和邏輯復(fù)雜度，也能減輕后續(xù)求解負擔、提高約束求解的效率，還能為約束求解結(jié)果的緩存和重用操作節(jié)省空間和時間.

2.1.1非相關(guān)約束分支切片

非相關(guān)約束分支切片又稱為切片(slicing)或約束獨立(constraints independent)，是通過把路徑約束條件切分成一個或多個不相交的約束子集再求解的技術(shù). 同一程序或不同程序中，很少情況下會存在兩條相同的路徑，如果對整條路徑約束及結(jié)果進行緩存，則其重用性會非常低. 另一方面，程序中因為分支條件而使得路徑數(shù)量的逐漸增多，會存在大量的相似路徑. 例如，對路徑約束中某一條件約束取反從而生成另一條路徑約束，除了取反的這一約束條件以外，其余約束都是相同的. 切片算法的提出能使得大部分相似路徑約束求解結(jié)果的重用變得可能而且實用.

一條路徑約束可以映射到無向加權(quán)圖中，稱這一類圖為約束圖(constraints graph). 在約束圖G=(V,E)中，節(jié)點V表示約束式，而節(jié)點之間的邊E則表示兩條約束之間的共享變量. 例如，在圖2中路徑約束為

圖2 非相關(guān)約束分支切片示例Fig.2 Explanatory chart of non-correlation restriction sliding

{3x+y≤3,x+2y≤2,v+w≤5,

v-w≤2,x+y≤3}，

因為約束式C1、C2、C5和C3、C4沒有共享變量，所以路徑約束Φ可被切分成兩個約束子集

Φ1={C1,C2,C5}=

{3x+y≤3,x+2y≤2,x+y≤3}，

Φ2={C3,C4}={v+w≤5,v-w≤2}.

約束子集對應(yīng)的兩個約束子圖如圖2所示.

切片對約束求解的好處有兩方面，一是能夠簡化路徑約束，將路徑約束碎片化能減小求解約束集的體積，加快求解速度. 事實上，在求解器內(nèi)部也會對約束集做切片工作，但會消耗比較大的計算量. 外部切片再求解能減小求解器求解負擔，提高求解效率. 二是有助于求解結(jié)果的重用. 符號執(zhí)行中存在大量的相似路徑，對路徑約束進行切片，能增加相似路徑求解結(jié)果重用的概率.

切片策略由Cristian Cadar等提出[18,42]，并在其開發(fā)的EXE和KLEE工具中配合約束結(jié)果緩存策略同時使用. 后來Mayhem[20]、Green[45]、GeenTrie[46]、Memoise[43-44]以及Recal[47]等工具中都有采用此方法進行約束求解優(yōu)化. 切片策略能獨立應(yīng)用于約束求解的優(yōu)化，同時又是其他策略如存儲、搜索等步驟的基礎(chǔ)，配合約束結(jié)果緩存能取得更好的性能優(yōu)化效果.

2.1.2約束簡化

約束簡化在英文文獻中又稱為“Simplifying”或“On-the-fly Expression Simplification”. 現(xiàn)有的符號執(zhí)行工具提出了很多針對單條約束條件的簡化技術(shù)，能夠精簡約束式，減輕求解負擔.

① 表達式重寫(expression rewriting). 表達式重寫包括一系列對單條約束式的簡化技術(shù)，這些簡化技術(shù)類似于編譯器中對編譯程序中表達式的簡化措施，具體如表2所示.

表2 表達式重寫措施及示例Tab.2 Illustrative measures of expression rewriting

② 約束集簡化(constraint set simplification). 在符號執(zhí)行中，隨著路徑約束中約束式的增加，對其中符號變量的約束限定范圍也可能會更加嚴格. 這已特性使得對其進行先行化簡變得可行和必要. 例如，當前路徑約束為x>5，隨著符號執(zhí)行的進行，有新的約束為x=6加入到此路徑約束中時，因為x=6對x的取值范圍限定更加嚴格，所以之前的約束x>5將被直接簡化為true，即直接將其從路徑約束中刪除. 約束集簡化在KLEE中提出，并取得了良好的優(yōu)化效果. 同時CUTE中也提出了稱為common sub-constraints elimination的簡化措施，方法是類似的，其實驗結(jié)果證明此方法能減少64%～90%的約束式的體積[41].

③ 隱含值的實際化(implied value concretization). 隱含值實際化主要是把路徑約束中隱含實際值的符號變量全部以實際值替換，以此達到簡化路徑約束的目的. 例如路徑約束中有約束式x+5=6，則經(jīng)過計算可以得到x是一個隱含值，可以對其進行簡化處理，得到x=1. 而后續(xù)出現(xiàn)x變量的約束式中，對x的值都可以用實際值替換，如x+y<8∧x+z>12，最終將被化簡為y<7∧z>11. 隱含值實際化技術(shù)在KLEE中被提出.

④ 最大公約數(shù)化簡. Recal[47]中也采用了一些技術(shù)對約束式進行簡化，如除以所有變量系數(shù)和常量的最大公約數(shù)等(例如2x+2<4可被簡化為x+1<2).

⑤ 數(shù)組約束編碼簡化. 數(shù)組在符號路徑約束中普遍存在，約束數(shù)組求解問題是符號執(zhí)行中求解開銷最大的問題之一. 許多程序的輸入都包含各種形式的數(shù)組(如字符串通常是以字符數(shù)組的形式被編碼)，開發(fā)人員也普遍采用數(shù)組完成各種數(shù)據(jù)結(jié)構(gòu)(如哈希表和向量等). 另外，底層代碼的指針操作常常使用數(shù)組模型[48]. 雖然使用實際索引的數(shù)組能被相似的方式處理，但因為指向位置的不確定性使得符號索引更難管理.

Perry等[49]提出了一系列不丟失語義的數(shù)組操作編碼轉(zhuǎn)換方法，通過對符號執(zhí)行期間的上下文信息的分析，把數(shù)組操作轉(zhuǎn)換成語義上等價的且滿足判定條件數(shù)組約束的形式. 此種轉(zhuǎn)換方法能使用更簡單的編碼方式表示數(shù)組的操作，并能夠大規(guī)模改進帶有數(shù)組操作的符號執(zhí)行的性能.

2.1.3冗余約束精簡

在符號執(zhí)行中，路徑約束可以看成是由m條約束條件，n個變量組成的約束集

Ax≤b.

(1)

如果刪除某些約束式后，約束集的可行域及求解結(jié)果不變，則被刪除的一條或多條約束式是冗余的.

圖3形象地說明了路徑約束中的冗余約束問題. 假設(shè)灰色區(qū)域S={x∈Zm|Aix≤bi}是路徑約束的可行域(feasible region)，而Sk={x∈Zm|Aix≤bi,i≠k}是刪除第k條約束之后的可行域，當且僅當S=Sk時，稱第k條約束條件是冗余的.

冗余約束精簡(redundant constraints elimination)是指在調(diào)用SMT求解器進行求解之前對邏輯上冗余的約束式進行刪除的操作. 冗余精簡能夠加快約束求解的速度，同時也能節(jié)省內(nèi)存空間，也為后續(xù)的匹配查找、求解結(jié)果重用節(jié)省時間.

Green[45]中的切片和約束式標準轉(zhuǎn)化工作使得變量順序相同，但變量命名和邏輯表達形式不一樣的約束式轉(zhuǎn)化為唯一的標準表達形式，這也能一定程度上精簡約束式.

Recal[47]中提出Normalization中的算術(shù)轉(zhuǎn)化措施通過對相同變量合并、邏輯轉(zhuǎn)化以及除以變量和常數(shù)的最大公約數(shù)的方式能夠進一步精簡約束式. 此外，其中的“redundant clauses elimination”作為其Normalization部分工作組的最后一步，能通過簡單的算術(shù)對比將系數(shù)相同但常數(shù)不一樣的約束式進行精簡. 如x+y<3和x+y<2，這兩個約束式中x+y<3會被判定為冗余約束.

2.2 求解時優(yōu)化

求解時優(yōu)化主要是在調(diào)用約束求解器求解的過程中涉及到的一些優(yōu)化措施. 具體包括域約簡優(yōu)化、快速不滿足性檢查、消除不相關(guān)約束、使用斷言棧優(yōu)化求解、多求解器支持等.

2.2.1域約簡優(yōu)化

域約簡優(yōu)化(domain reduce optimization)是由Erete 和Orso等提出[50]，主要是在符號執(zhí)行中使用域與上下文信息對約束求解的性能進行優(yōu)化. 實驗結(jié)果表明，限定路徑約束的輸入域可能幫助求解器更快地找到解. 具體思路是在求解時把路徑約束的全部符號值用實際值替換，只留一個符號變量讓求解器求解，如果無解，則把另一個符號變量符號化再求解，依次類推不斷增加符號變量，直到有解為止. 在上述過程中，每次增加符號變量的過程就是不斷擴大變量作用域(輸入域)的過程. 在路徑約束有解的情況下，輸入的大小關(guān)系著求解器對路徑約束的求解難度和求解開銷，輸入域越小，求解速度越快，開銷越小，但如果解不存在，則需要再次增大輸入域；反之，輸入域越大，求解速度越慢，開銷越大，但同時求出可行解的概率越大. 所以域約簡優(yōu)化技術(shù)主要是對輸入域和求解難度、求解速度之間取最佳權(quán)衡和折衷.

2.2.2快速不滿足性檢查

快速不滿足性檢查(fast unsatisifiability check)技術(shù)同樣在CUTE[41]提中出. 此技術(shù)主要對由取反而生成的新路徑約束進行快速的邏輯語法上的判斷，如果路徑約束中存在邏輯上相互沖突的約束式，則馬上返回為unsat，不需要再交給約束求解器對其進行求解. 例如有路徑約束為(x>5)∧(y<10)∧(x≥6)，對其最后一條約束取反之后生成的新的路徑約束為(x>5)∧(y<10)∧(x<5). 在對其做快速不滿足性檢查發(fā)現(xiàn)約束式(x>5)和約束式(x<5)在邏輯語法上有沖突，則無需在調(diào)用約束求解器對其做可達性求解，直接返回unsat的結(jié)果. CUTE論文中的實驗證明，快速不滿足性檢查能夠減少對求解器60%～90%的調(diào)用檢查，對約束求解性能起到了很大的優(yōu)化作用.

2.2.3不相關(guān)約束刪除

不相關(guān)約束刪除(irrelevant constraint elimination)首先在KLEE中提出，在符號執(zhí)行中，不斷地對路徑約束條件取反會生成大量的相似路徑約束，為了判定這些路徑的可行性及生成測試用例，需要頻繁調(diào)用求解器進行求解. 而與取反前的路徑相比，新路徑可達性只與被取反的分支條件的符號變量相關(guān)，所以一種有效的優(yōu)化約束求解的方法是刪除與當前分支條件變量無關(guān)的約束后再進行求解.

Domestic cosmetic brands concern about korean brands 12 1

不相關(guān)約束刪除是切片策略的特殊應(yīng)用，根據(jù)被取反分支條件的相關(guān)性，通過把新的路徑約束切分成相互獨立的兩個約束子集. 然后只對與取反分支條件變量相關(guān)的約束子集求解，其余的約束子集則重用之前的求解結(jié)果. 通過這種方式能減小約束體積，減輕邏輯復(fù)雜度.

例如，假設(shè)當前執(zhí)行的路徑條件為(x+y>10)∧(z>0)∧(y<12)∧(z-x=0)，如果需要對條件(y<12)取反，即對(x+y>10)∧(z>0)∧┐(y<12)約束求解產(chǎn)生新的路徑，因為變量y只與x有關(guān)，所以可以直接把與Z相關(guān)的約束刪除，直接求與x和y相關(guān)的約束. 在求解完成生成新的x和y的值之后，在加上取反之前的z值，則為新的走不同路徑的輸入. 此思路還需要解決指針解引用、數(shù)組索引等問題，在相關(guān)文獻[41-42,51]中有詳細闡述.

2.2.4使用斷言棧優(yōu)化求解

求解器內(nèi)部斷言棧(assertion stack)是由求解器本身維護，通過求解器提供的命令(如push和pop命令)合理使用斷言棧能夠共享不同約束集之間相同變量的定義、聲明以及約束條件等，這樣不但能減少求解器內(nèi)部重復(fù)的計算開銷，還能同時減小存儲空間重復(fù)申請和釋放帶來的開銷，提高求解器求解效率. 使用棧的優(yōu)勢是對于一些相似問題，不用每次重復(fù)定義變量求解，而且對于相似約束，可以共用變量. 這樣能節(jié)省空間和時間. Liu等[52]首次驗證了基于斷言棧比緩存技術(shù)更能提升求解器的求解效率.

2.2.5多求解器支持

在表1中可以看到，大部分符號執(zhí)行工具只使用了單個求解器求解，如Bitblaze使用了STP，而SAGE使用了Z3求解器. 這導(dǎo)致在實驗中對單一符號執(zhí)行工具和約束求解器的實驗得出的結(jié)論并不具有通用性. 其次，不同求解器的求解性能、擅長求解的理論并不一樣，增加對多求解器的支持(multi-solver)，根據(jù)路徑約束的類型和特征選擇不同的SMT求解器，能夠增強約束求解的性能，這一結(jié)論已經(jīng)在Palikareva H等的論文[53]中得到證實.

2.3 求解后優(yōu)化

求解后優(yōu)化指在調(diào)用約束求解器求解之后對約束求解結(jié)果緩存和重用. 本文大致將這些工作分為增量求解以及其他的緩存和重用策略.

2.3.1增量求解

在符號執(zhí)行中，相鄰路徑約束有很多公共的約束條件，可以利用以前相似路徑約束的求解結(jié)果，然后對已求解約束的子集和超集進行預(yù)判或者驗證，這樣能減少對求解器調(diào)用的次數(shù)，或者減小求解的開銷. 這一策略被稱為增量求解(incremental solving)，已經(jīng)在KLEE和CUTE等一些工具中被使用.

在KLEE中這一策略又稱為反例緩存(counter-example caching)調(diào)度算法，KLEE把所有約束及其對應(yīng)的求解結(jié)果做緩存處理以便重復(fù)使用. 例如緩存中存有如下的約束集及其求解結(jié)果(x>6)∧(x+y<12):{x=7,y=4}，當有相似的約束集需要求解的時候，KLEE會首先在緩存中查找有無可以重用的結(jié)果：如果是某個約束集的子集(如(x+y<12))，則直接返回緩存中的結(jié)果，因為超集對變量求解的域的結(jié)果比子集有更強的約束，所以其結(jié)果同樣適用于子集；如果是某個緩存中約束集的超集，如(x>6)∧(x+y<12)∧(y>=2)，則先試探緩存中子集的求解結(jié)果是否能滿足超集中的約束條件，如果不滿足則再調(diào)用求解器求解. 事實上在符號執(zhí)行過程中，新增加的約束往往不會使得之前的約束求解結(jié)果無效. 而檢查某些值在約束集中是否適用相對于對整個約束集求解而言只會耗費非常小的計算量. 這也是這一策略能實際應(yīng)用到符號執(zhí)行中并能改善其性能的原因.

2.3.2緩存和重用

除了上面提到的增量求解外，研究人員還提出一些適用范圍更廣的緩存和重用策略，增量求解只適用于已知求解的約束的子集和超集，而后續(xù)提出的這些緩存策略則包含了更多利用緩存區(qū)優(yōu)化約束求解的方法.

Yang等[43-44]提出使用Trie樹來存儲程序的執(zhí)行狀態(tài)和結(jié)果. 使用Trie樹的好處在于對于相同前綴的約束條件選擇不需要重復(fù)存儲，這樣能節(jié)省存儲內(nèi)存空間又能加快檢索匹配速度. 在Memoise中，Trie樹中每個節(jié)點并沒有存儲路徑約束條件，而是只記錄三樣數(shù)據(jù)約束節(jié)點的選擇(choices)，所在的方法(method)及其在方法中的指令偏移(instruction offset).

Green[45]中，路徑約束經(jīng)過切片、規(guī)范化(canonization)等步驟之后與求解結(jié)果一起存入了鍵值對存儲的數(shù)據(jù)庫Redis中，使用Redis的好處是能根據(jù)配置的閾值將結(jié)果存在內(nèi)存中，這加快了存儲和查詢的速度. Green提出的對約束式規(guī)范化轉(zhuǎn)換的思想使得不同變量名但順序和邏輯都相同的約束式具有了唯一的表達式，這讓Green對約束求解結(jié)果的重用范圍不能僅僅局限于程序內(nèi)部，還擴展到了不同程序中.

GreenTrie[46]從邏輯上擴展了KLEE和Green對求解結(jié)果的重用匹配策略，對求解結(jié)果的邏輯子集和超集進行判斷和匹配. 此外GreenTrie還把Green中的存儲載體從Redis換成了Trie樹.

Recal[47]使用了一種新的方式來標準化處理切片后的約束式，使得變量順序不同但邏輯上相同的約束式具有唯一的表達形式，這增加了求解結(jié)果重用的概率.

約束求解結(jié)果緩存和重用能獨立應(yīng)用于約束求解性能優(yōu)化，又能與其他優(yōu)化策略配合使用取得更好的效果. 在KLEE中，切片和緩存策略獨立應(yīng)用于約束求解性能優(yōu)化時，各自對性能的提升比較有限；但當兩者同時應(yīng)用到KLEE中的時候，KLEE對約束求解的性能有了數(shù)量級上的提升，特別是當程序比較大的時候，這兩者相結(jié)合所顯現(xiàn)出的優(yōu)勢就更加明顯.

3 未來研究展望

雖然本文提到的研究工作都在約束求解方面取得了較大的研究進展，但當前各項研究都還存有一定的局限性，而符號執(zhí)行應(yīng)用于大型程序的研究過程是一個多種性能優(yōu)化措施并行且不斷地對性能調(diào)優(yōu)的過程，約束求解問題的研究仍然還有待繼續(xù). 未來的研究工作可以在以下幾個方面進行.

① 提高路徑約束邏輯精簡率. 在符號執(zhí)行中，對路徑約束中的冗余約束進行精簡既能減小路徑約束的體積和邏輯復(fù)雜度，又能減輕求解器負擔、提高約束求解的效率，還能為后續(xù)的約束求解結(jié)果的緩存和重用操作節(jié)省空間和時間. 當前KLEE、Green、GreenTrie和Recal等符號執(zhí)行工具都有提出對約束簡化和簡單的約束式刪減工作，但這些工具要么是對單條約束式獨立的算術(shù)式化簡，要么是對相似約束式的對比進行可行域的縮減，都不能真正從邏輯上根據(jù)路徑約束的可行域進行冗余約束判定和精簡.

② 提高約束求解結(jié)果存儲和重用的效率. 現(xiàn)有的研究工作在約束求解結(jié)果和重用方面取得了比較大的進展，并證明歷史查詢求解的結(jié)果能夠被同一程序甚至是不同程序重復(fù)使用，很大程度上減小了對SMT求解器的調(diào)用. 但這些工作得益于以空間換時間的代價，設(shè)計更加高效的存儲、查詢匹配策略將對約束求解的性能帶來更大的提升.

③ 約束求解并行化. 當對大量程序進行符號執(zhí)行測試的時候，基于單臺服務(wù)器的測試將需要非常長的CUP處理時間. 約束求解并行化處理能夠加快對測試用例的生成，提高符號執(zhí)行的效率. 在Bucur S等的工作[54]以及Vertitesting[25]中已經(jīng)使用了分布式架構(gòu)用于約束求解的并行化處理，并取得了顯著的性能提升.

④ 約束求解配置預(yù)測. 路徑約束條件的編碼形式嚴重影響著求解器的求解性能. 對于不同的SMT求解器，因為對其支持的理論的不同配置，總的求解時間變化范圍可達兩個數(shù)量級[55]. 某種求解配置只對某些約束子集具有最佳的表現(xiàn)，而對于其他約束子集則未必，所以如果能夠在求解之前對待求解的約束集進行預(yù)判，然后根據(jù)判定結(jié)果選擇合適的配置，可以使得對此次的求解具有最佳的性能開銷. 而求解的配置可能是多種求解策略配置并行組合的配置，這些配置還容易加大對CPU計算資源的消耗. 所以一種可行的方法是，使用機器學(xué)習(xí)的算法根據(jù)待查詢語句的特點預(yù)測出最佳的求解器配置. 這些配置特征可以是查詢的AST大小、嵌套的數(shù)組操作數(shù)量、ITE節(jié)點的數(shù)量等. 或者借助深度學(xué)習(xí)算法應(yīng)用到配置策略選擇上，借助其自動特征提取和分類的能力，使得配置決策更加智能化.

4 結(jié)束語

作為符號執(zhí)行的瓶頸問題之一，約束求解問題的研究對改善符號執(zhí)行的可擴展性起到了至關(guān)重要的推動作用. 本文對近年來的約束求解問題的研究按照調(diào)用SMT求解器的不同階段進行了梳理分類，并對每個階段的相關(guān)工作進行了詳細的介紹. 隨著約束求解問題以及可滿足模理論本身研究進展的增多，符號執(zhí)行中的約束求解問題將會得到更大的緩解.