白 楊，賈 悠

（1.中國電子科技集團(tuán)公司第三十研究所，四川 成都 610041；2.電子科技大學(xué) 計算機(jī)科學(xué)與工程學(xué)院（網(wǎng)絡(luò)空間安全學(xué)院），四川 成都 611731）

0 引言

可滿足性模理論（Satisfiability Modulo Theories，SMT）是用來檢查邏輯公式在一種或者多種理論下的可滿足性。已知一個邏輯公式φ，一個SMT 求解器將返回SAT、UNSAT 或UNKNOWN，并且在需要的時候嘗試構(gòu)建一個φ的模型m。一個SMT 全解求解器在給出的公式可滿足時，嘗試找出所有模型。本文假設(shè)已知公式有有限個模型，否則不可能找到所有模型。

一個SMT 全解求解器具有許多（潛在）應(yīng)用。例如，估計被分析軟件擁有某一屬性的可能性[1]；計算信息泄漏的不確定性和數(shù)量計算[2]；還有邊界模型檢查、自動測試生成、可靠性分析以及安全性量化[3]。但是，現(xiàn)有的SMT 全解求解器在速度、內(nèi)存消耗以及支持理論類型方面都存在局限性[3-5]。

本文提出了4 個新的潛在應(yīng)用，并設(shè)計了一種快速、低內(nèi)存消耗的SMT 全解求解器，采用二分查找（Binary Search，BS）把搜索空間根據(jù)先前的模型動態(tài)劃分為多個較小子空間，并嘗試在一個子空間中找到一個模型。當(dāng)所有模型都產(chǎn)生后，程序終止。BS 方法帶來兩個優(yōu)點：一是在原始公式后附加描述子空間邊界的子句，附加子句的數(shù)量受變量數(shù)量限制而傳統(tǒng)的BCM 方法在該方面有明顯的缺陷，子句會隨著生成模型的增加而增加；二分查找支持具有“來自不同模型的相同變量的分配可以互相比較”屬性的理論。由于許多理論如布爾、位向量、整數(shù)、實數(shù)、浮點數(shù)以及字符串等都符合此要求，所以提出的方法可以對這些理論的問題進(jìn)行求解。

此外，本文的方法應(yīng)用上下文感知（Context Aware，CA）機(jī)制加快求解速度，同時，通過應(yīng)用暫停恢復(fù)機(jī)制（Suspend Resume，SR）機(jī)制來降低內(nèi)存消耗。結(jié)果表明，BS、BS+CA、BS+SR 和本文提出的方法分別將BCM 方法的求解速度分別加速了4.6 倍、13.4 倍、7.3 倍以及32.4 倍。此外，與BCM 方法相比，本文提出的方法的內(nèi)存消耗只有其35.3%，并且還能通過并行化處理進(jìn)一步提升速度。

綜上所述，本文有3 個主要貢獻(xiàn)：

（1）介紹了SMT 全解求解器的4 種潛在應(yīng)用，這4 種應(yīng)用在現(xiàn)有的研究中未被提到；

（2）設(shè)計了基于BS 的SMT 全解求解器，該方法支持多種理論，并集成了CA 和SR。

（3）實驗結(jié)果表明，本文的提出的方案有速度快、內(nèi)存消耗低、能夠通過并行方式加速等優(yōu)點。

1 新應(yīng)用研究

介紹提出的SMT 全解求解器的4 個潛在的新應(yīng)用，這些應(yīng)用在現(xiàn)有的研究中沒有被討論過，且現(xiàn)有的SMT 全解求解器[3-5]不支持這些應(yīng)用?，F(xiàn)有的SMT 全解求解器只能夠找到并返回邏輯公式φ關(guān)于布爾值的所有模型。3 個應(yīng)用與外部代碼有關(guān)，這些外部代碼只能作為黑盒進(jìn)行分析，如其他模塊、進(jìn)程、內(nèi)核甚至遠(yuǎn)程服務(wù)中的代碼。

1.1 上下文感知外部代碼探索器

為動態(tài)程序分析提供有效的測試輸入極具挑戰(zhàn)，尤其是在被分析的軟件調(diào)用外部代碼時。如果分析人員能找到外部代碼路徑并收集路徑條件，則外部代碼的所有行為可以通過本文提出的方法產(chǎn)生的模型運(yùn)行外部代碼來探索。此外，使用本文方法，分析者可以對外部代碼在不同情況下的行為進(jìn)行比較。

1.2 增強(qiáng)型靜態(tài)程序分析

由于實際程序中通常會大量使用外部代碼，因此會阻止進(jìn)行徹底的靜態(tài)程序分析。傳統(tǒng)的方法如手工編寫外部代碼模型既麻煩又容易出錯。通過本文提出的方法可以使用生成的測試輸出來探索外部代碼，因此執(zhí)行外部代碼的有效性可以被包含在靜態(tài)分析中。為了找到外部代碼所有可能行為，需到達(dá)外部代碼的所有可行路徑（即所有有效上下文）。

1.3 外部感知混合執(zhí)行

混合執(zhí)行是一種多路徑程序分析技術(shù)。但是，在分析實際程序時，如何處理外部代碼是一項有難度的工作。通過本文提出的方法，分析人員可理解外部代碼在特定上下文中的行為。因此，本文的方法通過引入描述執(zhí)行外部代碼產(chǎn)生影響的新約束來執(zhí)行外部代碼（如代表外部函數(shù)的所有可能返回值的約束）。

1.4 診斷路徑分歧

路徑分歧表示預(yù)期程序路徑和實際執(zhí)行的程序路徑不匹配。路徑分歧的根本原因很難定位和診斷，因為它可能會在很寬的范圍內(nèi)在入口和分支之間發(fā)生分歧。本文提出的方法有助于通過產(chǎn)生多個測試輸入來縮小檢查范圍。由于分歧可能會發(fā)生在當(dāng)前分歧分支前，因此引入本文方法做路徑分歧診斷能夠輔助分析員節(jié)省分析開銷。

2 動機(jī)闡述

下面闡述使用本文提出的方法采用二分搜索來求解公式。

式（1）共 有100 萬（100×100×100）個 模型。其中第一個模型m0通過求解φ得到{x=50,y=50,z=50}。

傳統(tǒng)BCM 方法獲取下一個模型m1，新公式φ1是φ和子句(x≠50)∨(y≠50)∨(z≠50)的析取，可表示為：

隨后通過求解φ1得到m1。一直迭代上述流程，直到找不到模型為止。BCM 會導(dǎo)致子句隨著模型的增加而增加。極致情況下，找到最后一個模型m1000000，對應(yīng)的公式φ1000000包含了1 000 000 個子句。大量子句會花費(fèi)過多內(nèi)存，并在很大程度上減慢了求解過程。

提出的BS 方法和上述方法一樣，通過求解φ產(chǎn)生與上述方法相同的第一個模型m0。隨后產(chǎn)生6個公式φ1～φ6對應(yīng)6 個任務(wù)動態(tài)劃分搜素空間，如圖1 所示，如φ6=φ∧((x==50)∧(y==50)∧(z＞50))。

圖1 一個例子闡述二分查找

增量子句來描述子空間邊界，如x＜50 表示子空間：

-INF和+INF表示可以由變量獲取的最小值和最大值。如果在原始子空間找到模型，則這個子空間可以被分為更小的子空間。例如，可以通過求解φ6找到一個模型{x=50,y=50,z=80}，隨之產(chǎn)生兩個新公式：

反復(fù)執(zhí)行該操作，直到所有生成的公式都完成求解。與BCM 相比，所有的BS 生成的公式添加一個或多個子句來描述子空間的邊界。增加的子句數(shù)量由變量個數(shù)決定，而不是由模型數(shù)量來決定的。因此，這個例子中，由BS 產(chǎn)生的公式包含不超過4 個子句，而同樣的問題傳統(tǒng)BCM 方法的φ1000000包含1 000 000 個子句。

3 一種快速低內(nèi)存消耗的SMT 全解求解器

本文設(shè)計了一款快速低內(nèi)存消耗的SMT 全解求解器，基于Z3[6]求解器實現(xiàn)。下面將介紹這種方法用到的多種優(yōu)化方法的設(shè)計，包括CA、SR 以及并行優(yōu)化。

3.1 基于上下文感知（CA）機(jī)制的優(yōu)化

CA 適用于連續(xù)求解過程，因為SMT 求解器在求解當(dāng)前方程的過程中需要學(xué)習(xí)大量知識。為了構(gòu)造上下文感知機(jī)制，利用現(xiàn)代SMT 求解器（如Z3）支持的push/pop 命令來實現(xiàn)。提出的方法能夠通過push 命令在求解原始公式后迅速記住上下文信息。求解任務(wù)基于已經(jīng)記住的上下文內(nèi)容，通過添加子句來描述變量子空間。求解完畢后，上下文內(nèi)容通過pop 命令進(jìn)行恢復(fù)。

3.2 并行化優(yōu)化

由于求解器具有多任務(wù)模式且易于并行化處理，為了更好地利用硬件資源，本文提出的求解器創(chuàng)建了多個并行運(yùn)行工作程序。每個工作程序首先從任務(wù)隊列中獲取任務(wù)（即該位置記錄未執(zhí)行的任務(wù)），然后運(yùn)行任務(wù)生成新任務(wù)，最后將生成的任務(wù)附加到任務(wù)隊列。該過程反復(fù)進(jìn)行，直到任務(wù)隊列為空。

將上述兩種方法結(jié)合存在挑戰(zhàn)。具體描述為要了解上下文情況，每個工作程序應(yīng)該獲取一個上下文對象。為此，本文創(chuàng)建了多個上下文對象，并使用每個上下文對象求解原始公式，然后將所有上下文對象存儲在池中。上下文對象的數(shù)量和工作程序數(shù)量相等。因此，任務(wù)的解決過程變?yōu)椋海╝）至少有一個閑置工作程序；（b）工作程序從池中獲取上下文對象；（c）工作程序從任務(wù)任務(wù)隊列中選取一個任務(wù)；（d）工作程序執(zhí)行任務(wù)；（e）工作程序恢復(fù)上下文并將其釋放回池中；（f）工作程序閑置。

3.3 基于暫停-恢復(fù)（SR）機(jī)制的優(yōu)化

SR 可以暫停求解過程，然后從斷點準(zhǔn)確恢復(fù)它。在掛起過程中，所有未執(zhí)行的任務(wù)內(nèi)存將轉(zhuǎn)存儲到磁盤。本文設(shè)計了磁盤任務(wù)隊列，并通過求解原始方程來恢復(fù)上下文內(nèi)容。本文引入緩存隊列來更好地實施本優(yōu)化設(shè)計方案，即本方法使用任務(wù)緩存隊列和磁盤中的緩存文件一起維持任務(wù)，新生成的任務(wù)將被添加到緩存隊列中，所有的工作程序從任務(wù)隊列中選取任務(wù)。如果任務(wù)隊列為空，工作程序通過從緩存文件中加載任務(wù)來填充任務(wù)隊列；如果緩存文件為空，求解器用緩存隊列里的任務(wù)填充任務(wù)隊列，并清空緩存隊列。

求解器可以基于SR 通過監(jiān)視內(nèi)存狀態(tài)來控制內(nèi)存消耗。當(dāng)內(nèi)存消耗超過閾值時掛起，隨后恢復(fù)求解過程。求解器經(jīng)過優(yōu)化I/O 消耗將變小。首先，求解器將寫操作延遲到求解過程被暫停時來完成，而不是通用的寫操作在產(chǎn)生的時候就執(zhí)行；其次，求解器將數(shù)百個任務(wù)添加到內(nèi)存中，而不是直接運(yùn)行任務(wù)；再次，所有未執(zhí)行的任務(wù)被存放到一個文件，而不是每個任務(wù)一個文件，因為訪問大量小文件可能會凍結(jié)文件系統(tǒng)；最后，為了減少磁盤開銷，僅記錄必要信息，如任務(wù)ID 和邊界。

SR 機(jī)制可以設(shè)置求解器在指定條件下運(yùn)行，如可以要求求解器在工作日晚上9 點到早上7 點運(yùn)行，或者可以暫停求解過程，并在另一臺計算機(jī)上繼續(xù)執(zhí)行。

4 方法評估

實驗執(zhí)行環(huán)境說明：4 核Intel i7 CPU，8 GB 主內(nèi)存和250 GB 固態(tài)硬盤電腦。使用本文提出的求解器解決SMT 庫[7]的工業(yè)類別中的8 個基準(zhǔn)，表明所有公式都是由實際應(yīng)用生成的。表1 列出了每個測試公式的名稱、文件大小和變量數(shù)量。將求解每個公式的時間預(yù)算設(shè)置為3 h，因此測試時間為168 h（即120=5×8×3 h），以獲得如表1 所示的結(jié)果。

表1 實際公式為基礎(chǔ)的實驗結(jié)果

實驗結(jié)果表明，與BCM 相比，本文提出的方法能夠加速求解并降低內(nèi)存消耗。在求解figld.phx時，本文提出的求解器在3 h 內(nèi)產(chǎn)生的模型數(shù)是BCM 求解器的4.7 倍，使用的內(nèi)存開銷為BCM 求解器的41.8%。

表1 中展示了每個算法的模型數(shù)量和內(nèi)存消耗、BS+SR 和本文求解器的暫停恢復(fù)次數(shù)。由表1 數(shù)據(jù)可知：本文的方法是最快的方法（比BCM快32.4 倍），且消耗最少內(nèi)存（僅為BCM 方法的35.3%）；BS 的性能比BCM 在求解速度上快，是其4.6 倍；CA 能夠明顯提升BS 優(yōu)化效果，達(dá)到13.4 倍。采用SR 后，比僅有BS 機(jī)制下的求解器消耗更少的內(nèi)存。究其原因，可以理解為降低內(nèi)存消耗的同時提升求解速度，是以SR 開銷為代價的（如將未執(zhí)行的任務(wù)轉(zhuǎn)存儲到磁盤中，還原上下文）。

圖3 表明，本文提出的求解器和BS+SR 機(jī)制的求解器保持恒定的求解速度，其他3 個則從長遠(yuǎn)來看會變慢，表明SR 對于解決無法在短期內(nèi)完成的復(fù)雜公式是必須的。這一結(jié)論是合理的，因為SR 會定期重新啟動約束求解。

圖3 表明基于BS 和BD+CA 求解器隨著時間增加持續(xù)增加內(nèi)存開銷，BCM 沒有明顯增加內(nèi)存開銷，這是由于BCM 求解器會變得很慢導(dǎo)致的，如圖2所示。

圖2 式（3）的模型數(shù)量

表1 和圖3 表明，基于BS+CA 的求解器比基于BS 的求解器需要消耗更多的內(nèi)存（BS+CA 的為4.4 倍，BS 的為2.2 倍）。本文提出的求解器比基于BS+SR 的求解器在給定相同內(nèi)存閾值的情況下暫?；謴?fù)需要更多時間，前者41.4，后者8.5。導(dǎo)致這一結(jié)果是因為基于CA 的求解器需要記住上下文信息。利用SR 機(jī)制的優(yōu)點，可以降低CA 機(jī)制導(dǎo)致的高內(nèi)存開銷。

圖4 表明本文提出的求解器能夠通過并行處理進(jìn)行加速。兩個工作程序能夠?qū)⑵骄俣忍岣叩?.62 倍，4 個工作程序能夠?qū)⑵骄俣忍岣叩?.4 倍。下一步可以考慮解決以下實現(xiàn)限制提升并發(fā)性。所有的工作程序從一個共享的任務(wù)隊列中獲取任務(wù)；所有的工作程序添加他們產(chǎn)生的任務(wù)到一個共享隊列；如果當(dāng)任務(wù)隊列為空時，工作程序嘗試從磁盤獲取任務(wù)，此時其他工作程序需要等待。

5 相關(guān)工作

MathSat[4]和Z3[3,5]方法嘗試找到關(guān)于布爾變量的所有模型。Lahiri 提出一個SMT 全解求解器基于DPLL（T）框架[8]來找到SAT 問題下的所有模型。盡管如此，構(gòu)建一個SMT 全解求解器也不容易，因為SAT 內(nèi)核返回一個單SAT 模型可能表明了多個SMT 模型。因此，理論上構(gòu)建一個SAT 全解核需要增強(qiáng)從一個SAT 模型的多個SMT 模型派生能力。

LattE[9]計算了整數(shù)和實數(shù)上的線性模型，并被廣泛應(yīng)用于文獻(xiàn)[10-12]中。Sankaranarayanan 等[13]提到找通過區(qū)間約束傳播來找到區(qū)間邊界，其中區(qū)間約束傳播比精確模型技術(shù)快，僅限于整數(shù)和實數(shù)上的線性約束。qCORAL[1]使用區(qū)間約束傳播[14]來將解空間分解成為更小的區(qū)域，然后將采樣應(yīng)用到概率估計中，但qCORAL 僅支持邊界浮點數(shù)。本文提出的求解器和現(xiàn)有方法不同之處在于于支持多種理論類型，且公式的形式?jīng)]有限制。

6 結(jié)語

全解求解器可以為多種研究領(lǐng)域提供輔助計算，如軟件測試中的符號執(zhí)行等。現(xiàn)有的全解求解器在速度、內(nèi)存消耗或者支持求解的理論類型存在局限性，因此設(shè)計了一種結(jié)合二分查找（BS）、上下文感知（CA）以及暫停恢復(fù)（SR）等機(jī)制的SMT 全解求解器。實驗結(jié)果證明，該方法比傳統(tǒng)的BCM 求解速度更快，內(nèi)存消耗更小。此外，通過嘗試并行處理方法來優(yōu)化本文的求解器可以發(fā)現(xiàn)并行條件下求解速度能得到進(jìn)一步提升。同時，本文探討了求解器的4 種潛在應(yīng)用——外部代碼探索、靜態(tài)程序分析、外部感知混合執(zhí)行、診斷發(fā)散?？梢?，本文提出的快速低內(nèi)存開銷的SMT 全解求解器在軟件工程領(lǐng)域有重要的實踐意義。