基于輸入約束的符號執行優化

汪孫律，林渝淇，楊秋松，李明樹

?

基于輸入約束的符號執行優化

汪孫律，林渝淇，楊秋松，李明樹

（中國科學院軟件研究所基礎軟件國家工程研究中心，北京 100190）

為了解決符號執行中路徑爆炸、新路徑發現率低等問題，提出了基于輸入約束的符號執行（ICBSE）優化框架。該方法通過分析程序代碼自動提取3類輸入約束，隨后使用這些約束引導符號執行更關注于核心功能代碼。在KLEE中實現了上述優化框架，并對coreutils、binutils、grep、patch、diff這5個程序套件中的7個常用程序做了檢測。ICBSE發現了7個之前未知的缺陷（KLEE只檢測其中3個）。同時，ICBSE將指令行覆蓋率、分支覆蓋率分別提升了約20%，時間開銷降低了約15%。

符號執行；輸入約束；路徑爆炸；缺陷查找

1 引言

符號執行是一種經典程序分析技術，它將程序中的變量抽象為符號，通過符號的形式模擬程序運行，收集程序路徑上的約束條件[1-2]。使用該技術可以遍歷程序路徑空間，檢查程序是否滿足某些安全特性。符號執行當前多用于輔助軟件測試[3]、程序缺陷挖掘[4]和測試用例生成[5]。

符號執行技術面臨的主要問題是分析的對象包含大量的路徑分支，求解工具不能在有限的時間內完成窮舉過程，即存在路徑爆炸問題。如何有效地緩解路徑爆炸問題是當前符號執行領域的熱點之一，主要包括搜索約束和搜索策略這2個方面的研究：1) 搜索約束即對程序的輸入進行建模[5-6]，或以目標位置為導向排除無關路徑[4]，這類方法是通過約束對搜索路徑進行裁剪，從而達到降低復雜度的目的；2) 搜索策略除了傳統的深度優先或廣度優先之外，還包括隨機路徑搜索和覆蓋率優化等新的搜索方式，比如符號執行工具KLEE[7]所用的算法就可以選擇4種策略或這4種策略混合使用。本文方法是對符號執行工具進行改進，屬于搜索約束方向。

搜索約束面向特定類型的程序或者目標時，能夠大幅地裁剪路徑，例如基于文檔輔助對輸入建模[6]，該方法從幫助文檔、代碼注釋及文件格式中提取更多的搜索約束，幫助手冊格式（manual）的參數約束以及特殊的文件格式，如可執行和可鏈接格式（ELF, executable and linking format）。然而該方法也很有局限性，比如需要程序帶有幫助手冊，同時符合解析的規范。如果一個程序缺少必要信息，比如缺少幫助文檔，則無法使用該方法。所以該方法很難適用于所有的開源程序，尤其是一些缺乏維護的開源程序。

針對這個問題，本文提出了一種新的基于輸入約束的符號執行（ICBSE, input constraint based symbolic execution）優化框架，通過提取代碼中有效的命令行約束參數（比如rm命令中的-r選項），從而實現對搜索路徑的裁剪。本文貢獻如下。

1) 面向開源代碼，使用靜態分析等方法獲取輸入命令行種類和長度以及命令行參數長度等必要約束信息，提升符號執行效率。

2)使用源代碼生成的中間語言低級虛擬機（LLVM, low level virtual machine）[8]作為提取對象，可以做到針對LLVM支持的平臺和語言。

3) 基于開源工具KLEE實現ICBSE的支持，在增強了搜索約束的同時，還復用了KLEE已有的各類搜索策略。

本文使用Linux平臺的常用工具coreutils、grep、binutils、patch、diff作為測試對象，實驗結果表明，相比于KLEE原有的方案，ICBSE方案在覆蓋率上有約20%的提升，在搜索時間上有約15%的提升，同時該工具還發現了4個原工具未發現的缺陷。

2 相關工作

輸入約束作為符號執行優化的方向之一，近年來有許多相關的研究工作。構建輸入約束的方法包括手動構建、基于摘要產生約束、基于規范、基于運行時信息、基于文檔等方法。

手動構建方面，文獻[9]提出了稱之為切片符號執行的方法。利用這種方法，用戶可以通過指定某些范圍的代碼，將這段代碼在分析的過程排除，從而將搜索過程集中在更重要的部分。該文獻的重點在于解決切片過程中的副作用，如果能夠結合自動分析程序熱點，則會更加適用于實際程序的分析。

基于摘要產生約束方面，比如通過避免執行程序中的特定代碼塊來緩解路徑爆炸問題。具體實現方法之一就是將需要重復執行的代碼塊，如函數在第一次運行時生成摘要，在下次執行該代碼塊時直接使用該摘要而不用重復執行該代碼塊，該方法有效地緩解了代碼塊因調用次數增多和調用深度增加引起的路徑爆炸問題。摘要一般由代碼塊的前置條件和后置條件的析取構成。文獻[5]利用過程內分析方法對函數生成摘要來輔助符號執行的過程間分析，有效緩解了因調用函數次數過多帶來的路徑爆炸問題。

基于規范方面，比如文獻[10]為字符串指定規范，文獻[11]為程序中的正則表達式指定規范。

基于運行時信息方面，Ramos等[12]提出了對符號“惰性初始化”的方法，也就是前文提到的長度約束。文獻[12]所提方法的思想是當為每個數據結構（特別是復雜數據結構）建模，在聲明或者定義時只為其構建類型信息，直到被使用的時候，才根據使用的需要來初始化該變量的對象信息。這種方法實際上是先運行程序，再根據運行過程中對符號值做的運算決定符號值的長度約束，例如對數組進行操作。但這種方法一般只對程序當前執行路徑上的變量長度約束提取有效果，而對于以命令行選項/參數為輸入類型的測試效果并不明顯，遠遠達不到約束收集的要求，除非將可能的選項都運行一遍。另外，這種方法對內容約束沒有任何效果。

基于文檔方面，Wong等[6]提出了基于文檔輔助的建模方法，即前文提到的內容約束。該方法本質上也是基于規范，但是約束性和導向性更強。所謂文檔輔助即基于幫助文檔、代碼注釋以及文檔布局提取更多的輸入約束，比如幫助手冊格式的參數約束以及特殊的文檔格式（比如ELF）。這類約束與程序本身密切相關，能夠大幅裁剪執行路徑，但面臨的問題也是顯而易見的，比如需要程序帶有幫助手冊，同時符合解析的規范，并且程序處理的目標必須是工具支持的特定類型，否則該方法的作用不大。本文的工作是對基于文檔方法的進一步改進，只需要源碼就可以做到輸入約束的收集。

3 背景介紹及示例

3.1 符號執行簡介

符號執行指的是使用符號化的變量代替實際的輸入，并將程序中代碼行為轉換為相應的程序狀態表達式的操作。程序狀態包括變量的取值、路徑條件（PC, path condition）和程序計數器。當遇到分支指令時，程序會分別搜索每個分支，并且將分支需要滿足的條件加入路徑條件中。程序的可達性通過約束求解器（constraint solver）對路徑條件的可滿足性進行求解來判斷，從而生成路徑對應的測試用例。

圖1是一個簡單的示例程序。其中，函數foo()包含了2個整型變量參數和。該程序的符號執行過程如圖2所示，執行樹的初始狀態是S0，其中，和分別表示和的符號值，該節點的路徑條件為true，類似的狀態S1和S2的路徑條件也為true。當執行到4(>0)時，路徑會分叉為2條路徑，分別為狀態S3(>0)和S4(≤0)。同時，到達2個狀態的分支條件也會加入路徑條件中，以判定路徑的可行性。根據求解器的結果，表示存在相應的路徑條件為true的和的取值，隨后生成可以到達狀態S3和S4的測試用例。

圖1 示例程序1

圖2 程序1的執行樹

如上所述，目標程序將被分解為執行樹，每個葉節點都對應了程序的一條執行路徑，而每個分支節點則對應了程序的分支條件。隨著程序分支變多，執行樹的規模呈指數級增長，因而遍歷整個執行樹會引發狀態爆炸問題。下面以一個更加復雜的例子說明本文提出基于輸入約束的原因。

3.2 基于輸入約束的優化示例

圖3是一個簡單的帶參數的C語言程序。假設這個程序帶有一個參數為“AAAAAAAAAA”，在滿足輸入時會進入相應的處理程序。

圖3 示例程序2

以上描述說明能夠快速發現缺陷的2個先決條件是：1) 符號化值的長度必須大于或等于10；2)符號化值的內容限制為某些值，比如示例中的10個“A”。條件1)是必要條件，否則求解器是不可能解出長度超過10的結果；條件2)是為了提高求解速度，對搜索空間進行了限制裁剪。下文將條件1)稱為“長度約束”，條件2)稱為“內容約束”。對于學術界流行的符號執行工具KLEE來說，是無法滿足以上2個條件的，原因如下：1)KLEE的符號長度是手動設置的，只能憑“經驗”進行針對性的設置，而實際操作中，如果設置過短則無法觸發該缺陷，如果設置過長則會造成搜索空間過大，搜索效率很低；2) KLEE雖然提供內容約束的接口，但是不支持自動提取內容約束，使用者需要按照幫助文檔將所有的內容約束加入約束集中，在實際操作中非常煩瑣并且效率很低。

如何改進KLEE并將該方法推廣到實際應用程序中是本文的主要研究點。在實際程序中，命令行參數是一種特殊的輸入，用于觸發某些功能，比如rm命令如果加上“-r”參數則表示以遞歸的方式刪除文件/文件夾。在程序的代碼實現中，通過if-else或switch-case語句檢查合法參數，并進入該參數對應的處理流程。如果能夠利用靜態分析等方法定位到命令行處理流程的入口，并掃描各處理分支提取的選項內容以及參數長度，即可自動完成所有的提取工作。

基于以上基本思路，為了克服KLEE的缺陷，本文提出了ICBSE框架。使用該框架替換KLEE的前端，即自動從程序的源代碼中提取所有的預設選項并作為輸入約束驅動KLEE的符號執行引擎完成求解過程。比如rm命令有15個有效選項，ICBSE會創建15個分支執行樹。通過這種方式使所有的有效選項出現相同深度的執行樹（假設有效選項為-a、-b、-c、…、-o）。同時輸入參數的長度也會作為ICBSE的提取目標之一加入約束集中。

圖4 使用ICBSE前后執行樹的變化情況

4 基于輸入約束的符號執行優化

4.1 ICBSE整體架構

ICBSE整體架構如圖5所示。本文選用LLVM的bitcode作為中間語言，利用提供的接口靜態分析提取信息，方便和KLEE整合。隨后對提取的信息進行篩選和轉換，生成對應的約束格式。通過修改KLEE的符號生成器部分可以方便地讀取已經生成約束格式繼而生成對應的符號值，隨后利用KLEE的符號執行引擎生成缺陷報告。

圖5 ICBSE整體架構

4.2 命令行選項和參數

幾乎所有的Linux程序都遵循一些命令行選項定義的約定。程序希望出現的參數可以分成2種，選項（option）和其他類型的參數。選項修飾了程序運行的方式，其他類型的參數則提供了輸入（如輸入文件的名稱）。下面以使用Linux的readelf為例，說明提取的輸入約束的內容，包括選項和參數2類，如圖6所示。

圖6 readelf命令示例

圖6中，“-h”和“-S”單橫杠開始的為短命令行選項，這種選項后面不會跟任何參數，而“--debug-dump”這類雙橫杠開始的為長命令行參數，后面可能會跟不等長的命令行參數，比如本例中的“info”字段。最后還有可能跟一個文件名參數指示目標或源文件位置。

因為本文的工作是基于開源軟件KLEE實現對ICBSE的支持，以上約束都需要轉化為KLEE可接受的輸入。KLEE支持的選項包括：1)--sym-args，后面跟min、max、len這3個參數，表示的含義為min-max數量的符號參數，符號化長度為len；2)--sym-file，后面跟num、len這2個參數，表示的含義為符號化文件的數量為mum，長度為len。圖6中readelf命令行示例中的選項從左到右，有以下對應關系，如表1所示。

表1 命令行選項和KLEE參數的對應關系

從表1可以看出，KLEE存在2個不足：1)KLEE并不支持內容約束，比如長/短命令行選項，只能限制長度；2)KLEE的長度約束都是基于經驗手動設置的，比如表1中的命令行參數除info之外，還包括了其他如“abbrev”“pubnames”“ranges”之類的參數，其中最長為13。

4.3 基本定義

本文選用了LLVM的bitcode作為中間語言，其中間語言自頂向下由模塊（module）、函數（function）、代碼塊（block）、指令（instruction）這4個層次組成。其中，模塊包含了函數，函數又包含了代碼塊，代碼塊又由指令組成。

指令再細分又包含了操作數（operand），操作數可以是值（val），比如算術運算，也可以是函數（func），比如函數調用。

本文在bitcode結構基礎上定義了以下基本操作。

操作1(targetfunc){block?BC$Ins?block, Ins.operand=targetfunc}其中，BC表示目標程序即bitcode的縮寫，block表示基本塊，Ins表示指令。操作1表示返回所有調用了目標函數targetfunc的基本塊，且為了簡化表示，所以沒有按層次遍歷。

操作2(type,block) = {Ins.val | Ins?block, Ins.itemtype=type}其中，block表示基本塊，type表示指令的類型，比如switch、branch等。操作2返回基本塊中指令類型等于type的操作數（不包括函數）。

另外，在建立起長短選項的映射關系后，還會有以下操作和數據結構。

1) shortopset：短選項約束集。

2) longopset：長選項約束集。

3) arglenset：參數長度約束集。

4) hasargs(val)：返回某個選項是否帶有參數。

5) arglen(val)：返回某個選項帶有參數長度。

各選項集的建立過程請參見3.4節中的說明。

4.4 選項提取規則

本節將結合實際代碼實現說明ICBSE的選項自動提取規則。在Linux程序實現中，按照標準都是通過調用getopt_獲取輸入的參數。

規則1 （內容約束1）

$block (block?(getopt)) => add2shortopset ((switch, block))

規則1表示任何代碼塊中只要在入口點調用了getopt函數，即作為起始點在代碼基本塊中收集約束。因為比對輸入都是通過switch-case語句實現的，所以將基本塊中所有switch類型的指令的值加到短約束集中。

以上過程以readelf的源碼進行簡單的說明，代碼示例如圖7所示。

圖7 readelf代碼示例

通過掃描目標代碼塊發現，第2行調用了getopt_long函數（包括getopt）的輸入參數，即表示從該位置開始搜集選項。遍歷該代碼塊中的每條比較語句，即代碼中的case語句，表示對選項進行處理，比如第10行的case 'H'表示該行操作數“H”可以生成短選項，生成如“-H”類型的選項。依次掃描case語句的操作數，可生成如“-e”“-r”“-s”等短選項約束。

規則2 （內容約束2）

$val (val?longopset) and (val?shortopset) =>add2longopset(val)

規則2的作用是如果長選項沒有對應的短選項，則將該長選項加入約束集中。使用規則2可以適當地過濾功能相同的輸入選項，減少搜索的路徑。因為程序通常會提供包括長選項和短選項這2種選項形式的參數，通過規則1已經生成了短選項約束集shortopset，而長選項約束集longopset以及長/短選項之間的映射關系可以由掃描option結構體獲取，表2列出了部分的映射關系。

表2 長短選項映射關系

比如，“-a”和“---all”指向的是同一類功能的選項，那么規則中需要將短選項“-a”加入輸入約束即可。而第5行的“--debug-dump”沒有對應的短選項，則需要單獨加入輸入約束。值得注意的是，第3列表示該選項是否需要參數，比如required_argument表示必須參數，而optional_argument表示可選參數。

規則2是對內容約束的一次過濾，同時也會記錄下哪些選項需要緊跟參數，用于規則3的生成。

規則3 （長度約束1）

$val (val?shortopset and hasargs(val)) or (val?longopset and hasargs(val)) => add2arglenset (arglen(val))

規則3的作用在于收集長/短選項自帶的參數長度，并將該約束加入約束集中。規則3的前提是已經通過規則1、規則2以及代碼中的關鍵數據結構生成了短選項約束集和長選項約束集，并完成了參數長度的收集工作。在此基礎上收集某個選項詳細處理過程，比如前面提到的長項選項“--debug- dump”，通過靜態分析代碼可知，該選項可以帶“line”“info”“abbrev”“pubnames”“ranges”“macro”“frames”“frames-interp”“str”“loc”等附加參數。該條規則會選擇最長的參數“frames-interp”并將其長度13加入約束集中。但規則3并不將以上參數作為內容約束加入約束集中，原因是有些長選項可以跟不定內容的參數，比如“--hex-dump”后面跟的是目標文件名，所以該條規則被稱為長度約束規則。

綜合以上3條提取規則，整個選項提取過程算法如算法1所示。如前所述，目標代碼為bitcode格式，所以簡稱為BC。同時為了簡化，算法的循環中省略了模塊和基本塊的遍歷，只描述函數和指令的遍歷。

算法1 約束提取算法

輸入 bitcode格式的目標代碼

輸出 約束集

1) constraints set C = ?;//約束提取算法

2) input set in;

3) for each funcF ?BC do

4) forInst I Fdo

5) ifIcall getopt_long

6) shortvars= shortvars∪getshortoptions (I);

7) shortvarNeedArg=shortvarNeedArg∪getshortoptionsArgInfo(I);

8) longvars=longvars∪getlongoptions (I);

9) longvarNeedArg=longvarNeedArg∪getlongoptionsArgInfo(I);

10) end if

11) ifIhave case with option

12) get the option indexin shortvars or longvars

13) in.op = in.op∪option;

14) if(shortvarNeedArg[]=true or longvarNeedArg[]=true)

15) get the length of the argument;

16) in.arglen=;

17) end if

18) end if

19) end for

20) end for

21) //base on the rule1~3 to add constraints to C;

22) return C

算法1沿用了LLVM提供的中間代碼處理接口，比如和分別表示函數體和函數體內的指令。算法中第6)~9)行搜集所有的長/短選項，并確定該選項是否帶有參數信息，其中第6)行應用的是規則1，而第8)行應用的是規則2。而第12)~17)行表示如果選項帶有參數，則監控對該選項讀取的參數處理的語句，并搜集所有的長度，也就是規則3的實現。算法1按照規則1~規則3將以上搜集的信息轉換為ICBSE可接受的格式加入約束集中，這里使用了KLEE提供的assume函數作為約束輸入接口，在此不再展開描述。

5 實驗與分析

本文基于符號執行工具KLEE實現了ICBSE優化框架的支持。為了方便對比，本文的搜索策略都選擇隨機搜索，并在此基礎上展開了一系列的實驗，主要從3個方面對比KLEE的檢測結果：1) 缺陷檢測能力，包括發現的缺陷數量和缺陷類型；2) 代碼覆蓋率，包括指令覆蓋率和分支覆蓋率；3) 執行時間。

本文選用了Linux常用工具作為檢測目標，這些工具在之前的研究中也曾做過相關的測試[12-16]。工具的名稱、版本以及代碼行數如表3所示。

表3 測試對象

所有實驗都是在處理器為Intel Xeon X5675 CPU（24 core，3.07 GHz）、內存為94 GB的服務器上進行的，操作系統是64位的Ubuntu 14.04 LTS。KLEE的主要參數設置如下：--max-time=3 600（最大執行時間為3 600 s，即60 min），--max- solver-time=80（最大求解時間為80 s），--search=random（設置搜索策略為隨機）。

5.1 缺陷檢測能力

通過一系列實驗，KLEE發現了3個未知的錯誤，而使用ICBSE優化后發現了7個未知的錯誤（其中4個KLEE并沒有檢測到）。表4展示了檢測的結果。

以patch發現的缺陷為例說明ICBSE的檢測能力。首先，“-d”作為短選項已經加入約束集中，所以很快就能觸發對應的路徑搜索，如圖8的代碼所示。其中，第7~8行表示命令行選項為“-d”同時后面跟蹤命令參數arg時，patch會將工作目錄切換到arg指示的文件夾位置。第9行以及第14~15行表示如果arg指向的位置無效會產生錯誤退出，退出之前會清空一些臨時數據。第20行表示隨后清空流程會進入輸出文件夾清空輸出文件，但此時由于切換目錄失敗，因此file_to_output參數為空指針，從而產生了空指針錯誤。在patch2.7版本中使用“patch -d -”命令即可重現該錯誤。而KLEE在達到最大的運行時間后并未檢測出該缺陷。從結果可以看出，因為ICBSE能夠更有效率的構造合法的輸入，所以能夠搜索更多功能實現相關的代碼，進而更有效地發現核心功能的缺陷。其他的缺陷也已經反饋給開發者做了確認和相應的修改。

表4 測試結果

e>

圖8 patch中的錯誤代碼

5.2 代碼覆蓋率

在代碼覆蓋率測試中，本文關注了指令覆蓋率和分支覆蓋率這2個指標。指令覆蓋率就是度量被分析代碼中每個可執行語句是否被執行到了，分支覆蓋率也是類似。本文使用gcov作為統計語句覆蓋率的工具。值得注意的是，統計覆蓋率的對象是程序本身的可執行代碼，而不考慮各程序鏈接進來的程序庫的代碼。本文對比了ICBSE和KLEE的執行結果，如表5所示，其中，IC表示指令覆蓋率，BC表示分支覆蓋率。

表5 代碼覆蓋率

在代碼覆蓋率的對比測試中，ICBSE和KLEE均采用同樣長度的輸入參數。從結果來看，除readelf外，其他程序的指令覆蓋率和分支覆蓋率都有明顯的提升。以diff程序為例，diff程序有55個輸入選項，通過手動檢測，KLEE只搜索了55個選項路徑中的27個，而使用ICBSE后提升到了53個（全部55個），所以指令覆蓋率和分支覆蓋率分別提升了28%和26%。值得注意的是，ICBSE并未搜索全部的選項，因為在實際操作中，設置了長命令行選項的閾值為20，所以有2個超長（長度≥20）的命令行選項，如果選擇覆蓋的話，對比測試中會導致工具迅速耗盡內存。

另外，readelf對比基本持平，無明顯提升。其主要原因在于readelf除了命令行選項的約束外，還受特定的文件格式約束，可以看出，在面向特定格式的程序中，輸入的文件內容對符號執行的覆蓋率影響更大，這也是在后續的優化中需要繼續關注的。

5.3 執行時間

執行時間的對比測試與覆蓋率對比測試環境一致，最大執行時間限制在3 600 s，即60 min，如果超過60 min則自動結束。執行結果如圖9所示，其中，深色為ICBSE的運行時間，淺色為KLEE運行時間，其中有一半的程序在限定時間內完成了測試。從結果來看，需要注意3點：1) sort、diff、patch、readelf執行時間統一為3 600 s，即達到了最大的執行時間，但是如果考慮到限定之間內達到的代碼覆蓋率，ICBSE的執行效率好于KLEE；2)完成測試的grep、sed、bool，ICBSE所用的運行時間明顯短于KLEE；3) ls的KLEE測試部分因為內存耗盡而終止了運行，所以沒有結果。根據以上結果，結合相同執行時間內代碼覆蓋率的提升效果，可以得出ICBSE在執行時間上優于KLEE的結論。

注：*表示ICBSE和KLEE在限定時間內都沒有結束； **表示KLEE因為內存耗盡而沒有顯示執行時間。

6 結束語

本文提出并實現了一種基于輸入約束的符號執行優化。實驗表明，相比于原有的方案，使用ICBSE優化框架后在缺陷查找能力上有明顯提升，并發現了4個KLEE方案不能發現的缺陷，同時在覆蓋率上有約20%的提升，在搜索時間上有約15%的提升。

后續的研究工作主要從2個方面開展。

1) 在前面已經提到，類似于readelf除了命令行選項的約束外還受特定的文件格式約束，在面向特定格式的程序中，輸入的文件內容對符號執行的結果影響更大。后續將嘗試使用惰性初始化的方法改進這方面的不足，如果輸入文件采用標準結構的文件（如某個可執行文件），則將文件分為布局控制結構（如ELF的文件頭）和內容數據這2個部分。

2) 當前的輸入約束收集都是基于程序對輸入選項和參數的處理過程進行收集的，而并未考慮程序中對于輸入的使用和判定。后續可以使用過程間靜態分析，結合數據流分析、別名分析等方法提取相關的輸入變量在程序中的使用信息，從而搜集到更準確的約束，進而對執行路徑進行進一步的裁剪。

[1] 張健. 精確的程序靜態分析[J]. 計算機學報, 2008, 31(9): 1549- 1553.ZHANG J. Sharp static analysis of programs[J]. Chinese Journal of Computers, 2008, 31(9): 1549-1553.

[2] KING J C. Symbolic execution and program testing[J]. Communications of the ACM, 1976, 19(7): 385-394.

[3] CADAR C, GODEFROID P, KHURSHID S, et al. Symbolic execution for software testing in practice: preliminary assessment[C]// International Conference on Software Engineering. 2011: 1066- 1071.

[4] ANAND S, GODEFROID P, TILLMANN N. Demand-driven compositional symbolic execution[C]//Theory and Practice of Software, International Conference on TOOLS and Algorithms for the Construction and Analysis of Systems. 2008: 367-381.

[5] GODEFROID P. Compositional dynamic test generation[C]//ACM Sigplan-Sigact Symposium on Principles of Programming Languages. 2007: 47-54.

[6] WONG E, ZHANG L, WANG S, et al. DASE: document-assisted symbolic execution for improving automated software testing[C]// IEEE International Conference on Software Engineering. 2015: 620-631.

[7] CADAR C, DUNBAR D, ENGLER D. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs[C]//USENIX Conference on Operating Systems Design and Implementation. 2009: 209-224.

[8] LATTNER C, ADVE V. LLVM: a compilation framework for lifelong program analysis & transformation[C]//International Symposium on Code Generation and Optimization. 2004: 75-86.

[9] DAVID T, ANDREA M, NOAM R, et al. Chopped symbolic execution[C]//The 40th International Conference on Software Engineering. 2018: 350-360.

[10] BJ?RNER N, TILLMANN N, VORONKOV A. Path feasibility analysis for string-manipulating programs[C]//TOOLS and Algorithms for the Construction and Analysis of Systems, International Conference. 2009: 307-321.

[11] VEANES M, HALLEUX P D, TILLMANN N. Rex: symbolic regular expression explorer[C]//Third International Conference on Software Testing, Verification and Validation. 2010: 498-507.

[12] RAMOS D A, ENGLER D. Under-constrained symbolic execution: correctness checking for real code[C]//Usenix Conference on Security Symposium. 2015: 49-64.

[13] AVGERINOS T, REBERT A, SANG K C, et al. Enhancing symbolic execution with veritesting[C]//International Conference on Software Engineering. 2014: 1083-1094.

[14] MARINESCU P D, CADAR C. Make test-zesti: a symbolic execution solution for improving regression testing[C]//International Conference on Software Engineering. 2012: 716-726.

[15] CADAR C, GODEFROID P, KHURSHID S, et al. Symbolic execution for software testing in practice: preliminary assessment[C]// International Conference on Software Engineering. 2011: 1066-1071.

[16] MARINESCU P D, CADAR C. KATCH: high-coverage testing of software patches[C]//Joint Meeting on Foundations of Software Engineering. 2013: 235-245.

Symbolic execution optimization method based on input constraint

WANG Sunlyu, LIN Yuqi, YANG Qiusong, LI Mingshu

National Engineering Research Center of Fundamental Software, Institute of Software Chinese Academy of Sciences, Beijing 100190, China

To solve path explosion, low rate of new path’s finding in the software testing, a new vulnerability discovering architecture based on input constraint symbolic execution (ICBSE) was proposed. ICBSE analyzed program source code to extract three types of constraints automatically. ICBSE then used these input constraints to guide symbolic execution to focus on core functions. Through implemented this architecture in KLEE, and evaluated it on seven programs from five GNU software suites, such as coreutils, binutils, grep, patch and diff. ICBSE detected seven previously unknown bugs (KLEE found three of the seven). In addition, ICBSE increases instruction line coverage/branch coverage by about 20%, and decreases time for finding bugs by about 15%.

symbolic execution, input constraint, path explosion, bug finding

TP311

A

10.11959/j.issn.1000?436x.2019062

2018?04?23；

2018?08?31

中國科學院戰略性先導科技專項基金資助項目（No.XDA-Y01-01）

Strategic Priority Research Program of Chinese Academy of Sciences (No.XDA-Y01-01)

汪孫律（1986? ），男，安徽安慶人，中國科學院軟件研究所博士生，主要研究方向為軟件安全。

林渝淇（1988?），男，山東濰坊人，博士，中國科學院軟件研究所助理研究員，主要研究方向為系統安全與可信計算。

楊秋松（1977? ），男，河北泊頭人，博士，中國科學院軟件研究所研究員、博士生導師，主要研究方向為軟件工程、形式化方法、模型檢測、安全操作系統。

李明樹（1966?），男，吉林德惠人，博士，中國科學院軟件研究所研究員、博士生導師，主要研究方向為操作系統與基礎軟件、軟硬件協同設計以及軟件工程方法和軟件過程技術等。