符號執(zhí)行技術(shù)總結(jié)（A Brief Summary of Symbol Execution）

• Prologue
• 摘要
• 簡介
• 經(jīng)典符號執(zhí)行技術(shù)
• 現(xiàn)代符號執(zhí)行技術(shù)
• • 混合執(zhí)行測試（Concolic testing）
  • 執(zhí)行生成測試（Execution-Generated Testing (EGT)）
  • 動態(tài)符號執(zhí)行中的不精確性(imprecision) vs.完整性(completeness)
• 主要挑戰(zhàn)和解決方案
• • 路徑爆炸(Path Explosion)
  • 約束求解(Constraint Solving)
  • 內(nèi)存建模(Memory Modeling)
  • 并發(fā)控制(Handling Concurrency)
• 符號執(zhí)行工具
• • • Java
    • LLVM
    • .NET
    • C
    • JavaScript
    • Python
    • Ruby
    • Android
    • Binaries
    • Misc
• 博客：更好地理解符號執(zhí)行
• 結(jié)束語

Prologue

近期查閱了符號執(zhí)行的經(jīng)典文章(Symbolic Execution for Software Testing: Three Decades Later)，整理部分資料如下。（之前還讀過ICSE2018的Towards Optimal Concolic Testing）

Recommended reading
[1] King J C. Symbolic execution and program testing[J]. Communications of the ACM, 1976, 19(7): 385-394.
https://yurichev.com/mirrors/king76symbolicexecution.pdf
[2] Cadar C, Sen K. Symbolic execution for software testing: three decades later[J]. Communications of the ACM, 2013, 56(2): 82-90.
https://people.eecs.berkeley.edu/~ksen/papers/cacm13.pdf
[3] Baldoni R, Coppa E, D’elia D C, et al. A survey of symbolic execution techniques[J]. ACM Computing Surveys (CSUR), 2018, 51(3): 50.
https://dl.acm.org/citation.cfm?id=3182657

Lecture
1.Symbolic Execution Lecture at Harvard.
https://www.seas.harvard.edu/courses/cs252/2011sp/slides/Lec13-SymExec.pdf
2.Symbolic Execution Lecture at Iowa State University.
http://web.cs.iastate.edu/~weile/cs641/9.SymbolicExecution.pdf
3.Symbolic Execution Lecture at University of Maryland.
https://www.cs.umd.edu/class/spring2013/cmsc631/lectures/symbolic-exec.pdf

Video
Symbolic Execution Lecture at MIT.
https://www.youtube.com/watch?v=mffhPgsl8Ws
Symbolic Execution Lecture (part of Software Security course on Coursera).
https://www.coursera.org/learn/software-security/lecture/agCNF/introducing-symbolic-execution

摘要

在過去的40年中，人們對軟件測試的符號執(zhí)行產(chǎn)生了極大的興趣，因為它能夠生成高覆蓋率的測試套件并在復雜的軟件應用程序中發(fā)現(xiàn)深層次的錯誤。符號執(zhí)行已經(jīng)在數(shù)十種開發(fā)工具中孵化，從而在許多突出的軟件可靠性應用中取得重大的實際突破。

許多安全和軟件測試應用程序需要檢查程序的某些屬性是否適用于任何可能的使用場景。例如，識別軟件漏洞的工具可能需要排除任何后門的存在，以繞過程序的身份驗證。一種方法是使用不同的，可能是隨機的輸入來測試程序。由于后門可能只針對非常具體的程序工作負載，因此自動探索可能的輸入空間至關(guān)重要。符號執(zhí)行通過同時系統(tǒng)地探索許多可能的執(zhí)行路徑，在不需要具體輸入的情況下，為問題提供了一個優(yōu)雅的解決方案。該技術(shù)不是采用完全指定的輸入值，而是抽象地將它們表示為符號，使用約束解算器來構(gòu)造可能導致屬性沖突的實際實例。

本文概述了現(xiàn)代符號執(zhí)行技術(shù)，討論了它們在路徑探索、約束解決和內(nèi)存建模方面面臨的主要挑戰(zhàn)，并討論了主要從作者自己的工作中得出的幾種解決方案。

簡介

符號執(zhí)行作為一種生成高覆蓋測試套件和在復雜軟件應用中發(fā)現(xiàn)深層錯誤的有效技術(shù)，引起了人們的廣泛關(guān)注。符號執(zhí)行是一種流行的程序分析技術(shù)，在70年代中期引入，用于測試某個軟件是否可以違反某些屬性。本文概述了現(xiàn)代符號執(zhí)行技術(shù)，并從路徑探索、約束解決和內(nèi)存建模方面討論了它們的挑戰(zhàn)。請注意，本文并不打算在這里提供對該領(lǐng)域現(xiàn)有工作的全面調(diào)查，而是選擇使用簡明的示例來說明一些關(guān)鍵挑戰(zhàn)和建議的解決方案。有關(guān)符號執(zhí)行技術(shù)的詳細概述，我們將讀者引見之前在該領(lǐng)域發(fā)布的調(diào)查（A survey of symbolic execution techniques）[3].

定義
符號執(zhí)行 （Symbolic Execution）是一種程序分析技術(shù)，它可以通過分析程序來得到讓特定代碼區(qū)域執(zhí)行的輸入。顧名思義，使用符號執(zhí)行分析一個程序時，該程序會使用符號值作為輸入，而非一般執(zhí)行程序時使用的具體值。在達到目標代碼時，分析器可以得到相應的路徑約束，然后通過約束求解器來得到可以觸發(fā)目標代碼的具體值。

目標
軟件測試中的符號執(zhí)行主要目標是: 在給定的探索盡可能多的、不同的程序路徑(program path)。對于每一條程序路徑，(1) 生成一個具體輸入的集合(主要能力)；(2) 檢查是否存在各種錯誤，包括斷言違規(guī)、未捕獲異常、安全漏洞和內(nèi)存損壞。

生成具體測試輸入的能力是符號執(zhí)行的主要優(yōu)勢之一：從測試生成的角度來看，它允許創(chuàng)建高覆蓋率的測試套件，而從bug查找的角度來看，它為開發(fā)人員提供了觸發(fā)bug的具體輸入，該輸入可用于確認和調(diào)試打開的錯誤。生成它的符號執(zhí)行工具的數(shù)據(jù)。

此外，請注意，在查找給定程序路徑上的錯誤時，符號執(zhí)行比傳統(tǒng)的動態(tài)執(zhí)行技術(shù)（如由Valgrind或Purify等流行工具實現(xiàn)的技術(shù)）更強大，這取決于觸發(fā)錯誤的具體輸入的可用性。最后，與某些其他程序分析技術(shù)不同，符號執(zhí)行不僅限于查找諸如緩沖區(qū)溢出之類的一般性錯誤，而且可以導致更高級別的程序?qū)傩?#xff0c;例如復雜的程序斷言。

我們從一個簡單的例子開始，它強調(diào)了本文其余部分所討論的許多基本問題。

考慮上圖的C語言代碼，并假設(shè)我們的目標是確定哪些輸入使函數(shù)foobar的第8行的斷言失敗。 由于每個4字節(jié)輸入?yún)?shù)可以采用多達2 ^ 32個不同的整數(shù)值，因此在隨機生成的輸入上具體運行foobar的方法不太可能準確地獲取斷言失敗的輸入。 通過使用符號作為其輸入而不是具體值來評估代碼，符號執(zhí)行克服了這種限制，并且可以推斷輸入類而不是單個輸入值。更詳細地，通過代碼的靜態(tài)分析不能確定的每個值，例如函數(shù)的實際參數(shù)或從流中讀取數(shù)據(jù)的系統(tǒng)調(diào)用的結(jié)果，由符號αi表示。 在任何時候，符號執(zhí)行引擎都維持一個狀態(tài)（stmt，σ，π）。

stmt是下一個要評估的語句。 目前，我們假設(shè)stmt可以是賦值，條件分支或跳轉(zhuǎn)。

σ是一個符號存儲，它將程序變量與具體值或符號值αi上的表達式相關(guān)聯(lián)。

π表示路徑約束，即，是表示由于在執(zhí)行中為了達到stmt而采取的分支而對符號αi的一組假設(shè)的公式。 在分析開始時，π=真。

函數(shù)foobar的符號執(zhí)行，可以有效地表示為樹，如下圖所示。

經(jīng)典符號執(zhí)行技術(shù)

符號執(zhí)行的主要思想就是將輸入(input)用符號來表征而不是具體值，同時將程序變量表征成符號表達式。因此，程序的輸出就會被表征成一個程序輸入的函數(shù)，即fun(input)。在軟件測試中，符號執(zhí)行被用于生成執(zhí)行路徑(execution path)的輸入。在具體的執(zhí)行過程中，程序在特定的輸入上運行，并對單個控制流路徑進行了探索。因此，在大多數(shù)情況下，具體的執(zhí)行只能在對相關(guān)財產(chǎn)進行近似分析的情況下進行。相反，符號執(zhí)行可以同時探索程序在不同輸入下可能采用的多種路徑。這為可靠的分析鋪平了道路，可以對檢查的屬性產(chǎn)生強有力的保證。關(guān)鍵思想是允許程序采用符號而不是具體的輸入值。

執(zhí)行路徑(execution path)：一個true和false的序列seq={p0,p1,…,pn}。其中，如果是一個條件語句，那么pi=ture則表示這條條件語句取true，否則取false。
執(zhí)行樹(execution tree)：一個程序的所有執(zhí)行路徑則可表征成一棵執(zhí)行樹。

例如，圖1中的函數(shù)testme（）有三個執(zhí)行路徑，形成了圖2所示的執(zhí)行樹。

3條不同的執(zhí)行路徑構(gòu)成了一棵執(zhí)行樹。三組輸入{x=0,y=1},{x=2,y=1},{x=30,y=15}覆蓋了所有的執(zhí)行路徑。

符號狀態(tài)(symbolic state)：符號執(zhí)行維護一個符號狀態(tài)e，它將變量映射到符號表達式。
符號路徑約束(symbolic path constraint)：符號路徑約束PC，它是符號表達式上無量詞的一階公式。

符號執(zhí)行后的結(jié)果如下圖所示：e和PC都在符號執(zhí)行過程中更新。 在沿著程序的執(zhí)行路徑的符號執(zhí)行結(jié)束時，使用約束求解器來求解PC以生成具體的輸入值。如果程序在這些具體的輸入值上執(zhí)行，它將采用與符號執(zhí)行完全相同的路徑并以相同的方式終止。例如，圖1中代碼的符號執(zhí)行以空符號狀態(tài)開始，符號路徑約束為true。執(zhí)行過程中的狀態(tài)如圖中紅色部分所示。

如果符號執(zhí)行實例命中退出語句或錯誤（例如，程序崩潰或違反斷言），則終止符號執(zhí)行的當前實例并且生成對當前符號路徑約束的令人滿意的分配，使用現(xiàn)成的約束求解器。 令人滿意的賦值形成了測試輸入：如果程序是在這些具體的輸入值上執(zhí)行的，它將采用與符號執(zhí)行完全相同的路徑并以相同的方式終止。

當代碼中包含循環(huán)和遞歸時，如果終止條件是符號的話，那么符號執(zhí)行會產(chǎn)生無限數(shù)量的執(zhí)行路徑。例如下圖所示，

如果循環(huán)或遞歸的終止條件是符號的，則包含循環(huán)或遞歸的代碼的符號執(zhí)行可能導致無限數(shù)量的路徑。 例如，圖3中的代碼具有無限數(shù)量的執(zhí)行路徑，這個時候，符號路徑要么就是一串有限長度的ture后面跟著一個false（跳出循環(huán)），要么就是無限長的true。如圖所示，

在實踐中，需要對搜索施加限制，例如超時，或?qū)β窂綌?shù)量，循環(huán)迭代或探索深度的限制。

符號執(zhí)行的主要缺點：如果符號路徑約束不可解（不能被solver解決）或者是不能被高效（時間效率）的解，則不能生成input?；氐街暗睦?#xff0c;如果把函數(shù)twice改成(v*v)%50（非線性）：假設(shè)采用的sovler不可解非線性約束，那么，符號執(zhí)行將失敗，即無法生成input。假設(shè)twice函數(shù)是第三方庫函數(shù)，沒有解釋，那么約束求解器也無法對其進行求解。由于約束求解器無法解決這些約束中的任何一個，符號執(zhí)行將無法為修改后的程序生成任何輸入。接下來，我們將描述兩種現(xiàn)代符號執(zhí)行技術(shù)，它們可以緩解這個問題，并為修改后的程序生成至少一些輸入。

現(xiàn)代符號執(zhí)行技術(shù)

現(xiàn)代符號執(zhí)行技術(shù)的關(guān)鍵要素之一是它們混合具體(Concrete)執(zhí)行和符號(Symbolic)執(zhí)行的能力。 我們在下面介紹兩個這樣的擴展，然后討論它們提供的關(guān)鍵優(yōu)勢。

混合執(zhí)行測試（Concolic testing）

當給定若干個具體的輸入時，Concolic testing動態(tài)地執(zhí)行符號執(zhí)行。Concolic testing會同時維護兩個狀態(tài)：

精確狀態(tài)(concrete state): maps all variables to their concrete values.
符號狀態(tài)(symbolic state): only maps variables that have non-concrete values.

不同于傳統(tǒng)的符號執(zhí)行技術(shù)，由于Concolic testing需要維護程序執(zhí)行時的整個精確狀態(tài)，因此它需要一個精確的初始值。舉例說明，還是之前這個例子：對于圖1中的示例，concolic執(zhí)行將生成一些隨機輸入，比如{ x = 22; y = 7} 并具體和象征性地執(zhí)行程序。具體執(zhí)行將在第7行采用“else”分支，符號執(zhí)行將沿具體執(zhí)行路徑生成路徑約束 x0 != 2y0。Concolic測試否定路徑約束中的合取并解決x0 = 2y0以獲得測試輸入{x = 2; y = 1}; 執(zhí)行采用與前一個不同的路徑 - 第7行的“then”分支，現(xiàn)在在此執(zhí)行中獲取第8行的“else”分支。與前面的執(zhí)行一樣，concolic測試也沿著這個具體的執(zhí)行執(zhí)行符號執(zhí)行，并生成路徑約束。Concolic測試將生成一個新的測試輸入，強制程序以及之前未執(zhí)行的執(zhí)行路徑。在第三次執(zhí)行程序之后，concoic測試報告已經(jīng)探索了程序的所有執(zhí)行路徑并終止了測試輸入生成。

執(zhí)行生成測試（Execution-Generated Testing (EGT)）

由EXE和KLEE工具實施和擴展的EGT方法的工作原理是區(qū)分程序的具體和符號狀態(tài)。EGT在執(zhí)行每個操作之前，檢查每個相關(guān)的值是精確的還是已經(jīng)符號化了的，然后動態(tài)地混合精確執(zhí)行和符號執(zhí)行。如果所有的相關(guān)值都是一個實際的值（即精確的，concrete），那么，直接執(zhí)行原始程序（即，操作，operation）。否則（至少一個值是符號化的），這個操作將會被符號執(zhí)行。舉例說明，假設(shè)之前那個例子，第17行改成y=10。那么，在調(diào)用twice時，傳入的參數(shù)是concrete的，返回的也是一個concrete value，因此z也是一個concrete value。第7、8行中的z和y+10也會被轉(zhuǎn)換成concrete vaule。然后再進行符號執(zhí)行。

Concoic測試和EGT是現(xiàn)代符號執(zhí)行技術(shù)的兩個實例，其主要優(yōu)勢在于它們混合具體和符號執(zhí)行的能力。 為簡單起見，在本文的其余部分，我們將這些技術(shù)統(tǒng)稱為“動態(tài)符號執(zhí)行”。

動態(tài)符號執(zhí)行中的不精確性(imprecision) vs.完整性(completeness)

不精確性: 代碼調(diào)用了第三方代碼庫（由于種種原因無法進行代碼插裝），假設(shè)傳入的參數(shù)都是concrete value，那么就像EGT中的一樣，可以全部當作concrete execution。即使傳入的參數(shù)中包含符號，動態(tài)符號執(zhí)行還是可以對符號設(shè)一個具體的值。Concolic和EGT有不同的解決方法，后面再介紹。除了調(diào)用外部代碼，對于難以處理的操作數(shù)（如浮點型）或是一些復雜的函數(shù)（solver無法解決或需要耗費大量時間），使用concrete value可以幫助符號執(zhí)行環(huán)節(jié)這種impression。

完備性: 動態(tài)符號執(zhí)行通過concrete value可以簡化約束，從而防止符號執(zhí)行g(shù)et stuck。但是這也會帶來一個新問題，就是由于這種簡化，它可能會導致一些不完整性，即有時候無法對所有的execution path都能生成input。但是，當遇到不支持的操作或外部調(diào)用時，這顯然優(yōu)于簡單地中止執(zhí)行。

動態(tài)符號執(zhí)行使用具體值簡化約束的能力有助于為符號執(zhí)行卡住的執(zhí)行路徑生成測試輸入，但這需要注意：由于簡化，它可能會失去完整性，即它們可能無法生成測試 某些執(zhí)行路徑的輸入。 例如，在我們的示例中，動態(tài)符號執(zhí)行將無法為路徑true，false生成輸入。 但是，當遇到不支持的操作或外部調(diào)用時，這顯然優(yōu)于簡單地中止執(zhí)行。

主要挑戰(zhàn)和解決方案

接下來我們將討論符號執(zhí)行中的關(guān)鍵挑戰(zhàn)，以及為響應它們而開發(fā)的一些有趣的解決方案。

路徑爆炸(Path Explosion)

描述:
首先，要知道，符號執(zhí)行implicitly過濾兩種路徑：
不依賴于符號輸入的路徑；
對于當前的路徑約束，不可解的路徑。
但是，盡管符號執(zhí)行已經(jīng)做了這些過濾，路徑爆炸依舊是符號執(zhí)行的最大挑戰(zhàn)。

解決方案:

利用啟發(fā)式搜索搜索最佳路徑
目前，主要的啟發(fā)式搜索主要focus在對語句和分支達到高覆蓋率，同時他們也可被用于優(yōu)化理想的準則。
方法1：利用控制流圖來guideexporation。
方法2：interleave 符號執(zhí)行和隨機測試。
方法3（more recently）：符號執(zhí)行結(jié)合演化搜索(evolutionary search)。其中，fitness function用于drive the exploration of the input space。

利用可靠的(sound)程序分析技術(shù)來減小路徑爆炸的復雜度
方法1：靜態(tài)地合并路徑，然后再feed solver。盡管這個方法在很多場合都有效，但是他把復雜度轉(zhuǎn)移給了solver，從而導致了下一個challenge，即約束求解的復雜度。
方法2： 在后續(xù)的計算中，記錄并重用low-level function的分析結(jié)果。
方法3 ： 自動化剪枝

約束求解(Constraint Solving)

描述:
約束求解是符號執(zhí)行的技術(shù)瓶頸。因此，對于solver的優(yōu)化（提高solver的求解能力）成了解決這個技術(shù)瓶頸的手段。

解決方案:

去除不相關(guān)的約束
一般來說，程序分支主要依賴于一小部分的程序變量。也就是說，程序分支依賴于一小部分來自于路徑條件(path condition)的約束。因此，一種有效的方法就是去掉那些與當前分支的輸出不相關(guān)的路徑條件。例如，現(xiàn)有路徑條件：(x+y>10)^(z>0)(y<12)^{(z-x=0)。假設(shè)我們現(xiàn)在想生成滿足(x+y>10)}(z>0)^?(y<12)，其中我們想建立對?(y<12)（與y有關(guān)）的feasibility。那么，(z>0)和(z-x=0)這兩個約束都可以去掉，因為與y不相關(guān)。

遞增求解
核心思想就是緩存已經(jīng)求解過的約束，例如(x+y<10)^(x>5)=>{x=6,y=3}。對于新的約束，首先判斷這個新約束的搜索空間是緩存里約束的超集還是子集。如果是新的約束的搜索空間是緩存的約束的子集，那么，就把緩存中的約束去掉多余的條件后繼續(xù)求解。如果是超集，那么直接把解代入去驗證。

內(nèi)存建模(Memory Modeling)

描述:
程序語句轉(zhuǎn)化成符號約束的精度對符號執(zhí)行的覆蓋率有很大的影響。例如，內(nèi)存建模是用一個具體的數(shù)值去近似一個固定位數(shù)的整數(shù)變量可能會很有效，但是另一方面，它也會導致imprecision，比如丟失一些符號執(zhí)行的路徑，或探索一些無用的解。另一個例子就是指針，一些工具如DART[3]只能處理精確的指針。

解決方案:
precision和scalability是一個trade-off。需要考慮的因素有：
a) 代碼是high level的application code還是low-level的system code。
b) 不同的約束求解器的實際效果。

并發(fā)控制(Handling Concurrency)

描述:
大型真實世界的節(jié)目通常是并發(fā)的。 由于這些程序固有的非確定性(non-deteminism)，測試是非常困難的。 盡管存在這些挑戰(zhàn)，但動態(tài)符號執(zhí)行已經(jīng)有效地用于測試并發(fā)程序，包括具有復雜數(shù)據(jù)輸入，分布式系統(tǒng)和GPGPU程序的應用程序。

符號執(zhí)行工具

動態(tài)符號執(zhí)行已經(jīng)由學術(shù)界和研究實驗室的幾個工具實現(xiàn)。 這些工具支持多種語言，包括C / C ++，Java和x86指令集，實現(xiàn)幾種不同的內(nèi)存模型，針對不同類型的應用程序，并使用幾種不同的約束求解器和理論。

Java

• JPF-Symbc - Symbolic execution tool built on Java PathFinder. Supports multiple constraint solvers, lazy initialization, etc.
• JDart - Dynamic symbolic execution tool built on Java PathFinder. Supports multiple constraint solvers using JConstraints.
• CATG - Concolic execution tool that uses ASM for instrumentation. Uses CVC4.
• LimeTB - Concolic execution tool that uses Soot for instrumentation. Supports Yices and Boolector. Concolic execution can be distributed.
• Acteve - Concolic execution tool that uses Soot for instrumentation. Originally for Android analysis. Supports Z3.
• jCUTE - Concolic execution tool that uses Soot for instrumentation. Supports lp_solve.
• JFuzz - Concolic execution tool built on Java PathFinder.
• JBSE - Symbolic execution tool that uses a custom JVM. Supports CVC3, CVC4, Sicstus, and Z3.
• Key - Theorem Prover that uses specifications written in Java Modeling Language (JML).

LLVM

• KLEE - Symbolic execution engine built on LLVM.
• Cloud9 - Parallel symbolic execution engine built on KLEE.
• Kite - Based on KLEE and LLVM.

.NET

• PEX - Dynamic symbolic execution tool for .NET.

C

• CREST.
• Otter.
• CIVL - A framework that includes the CIVL-C programming language, a model checker and a symbolic execution tool.

JavaScript

• Jalangi2.
• SymJS.

Python

• PyExZ3 - Symbolic execution of Python functions. A rewrite of the NICE project’s symbolic execution tool.

Ruby

• Rubyx - Symbolic execution tool for Ruby on Rails web apps.

Android

• SymDroid.

Binaries

• Mayhem.
• SAGE - Whitebox file fuzzing tool for X86 Windows applications.
• DART.
• BitBlaze.
• PathGrind - Path-based dynamic analysis for 32-bit programs.
• FuzzBALL - Symbolic execution tool built on the BitBlaze Vine component.
• S2E - Symbolic execution platform supporting x86, x86-64, or ARM software stacks.
• miasm - Reverse engineering framework. Includes symbolic execution.
• pysymemu - Supports x86/x64 binaries.
• BAP - Binary Analysis Platform provides a framework for writing program analysis tools.
• angr - Python framework for analyzing binaries. Includes a symbolic execution tool.
• Triton - Dynamic binary analysis platform that includes a dynamic symbolic execution tool.
• manticore - Symbolic execution tool for binaries (x86, x86_64 and ARMV7) and Ethereum smart contract bytecode.

Misc

• Symbooglix - Symbolic execution tool for Boogie programs.

博客：更好地理解符號執(zhí)行

符號執(zhí)行基礎(chǔ)
http://pwn4.fun/2017/03/20/符號執(zhí)行基礎(chǔ)/

符號執(zhí)行：基礎(chǔ)概念
https://blog.csdn.net/wannafly1995/article/details/80842459

符號執(zhí)行入門
https://zhuanlan.zhihu.com/p/26927127

軟件測試中的符號執(zhí)行
https://www.cnblogs.com/XBWer/p/9510884.html

符號執(zhí)行——從入門到上高速
https://www.colabug.com/4288118.html

結(jié)束語

2016年美國高等研究計劃署(DAPRA)主辦了自動網(wǎng)絡(luò)攻防賽(CyberGrandChallenge)，旨在建立實時自動化的網(wǎng)絡(luò)防御系統(tǒng)，并且能夠快速地應對大量新的攻擊手法，以應對頻發(fā)的網(wǎng)絡(luò)攻擊。符號執(zhí)行在參賽隊的自動攻防系統(tǒng)中起到了舉足輕重的作用，被廣泛應用在程序脆弱性的分析上，并涌現(xiàn)出了新的二進制符號執(zhí)行分析框架，如圣塔芭芭拉大學Shellphish團隊的angr和卡內(nèi)基梅隆大學ForAllSecure團隊的Mayhem。自動網(wǎng)絡(luò)攻防賽的舉辦掀起了二進制符號執(zhí)行的又一波熱潮。

雖然近年來各種符號執(zhí)行優(yōu)化技術(shù)不斷被提出，符號執(zhí)行的可用性和實用性也極大地提高了，但在現(xiàn)實軟件分析應用中還面臨著嚴峻的挑戰(zhàn)，除了路徑空間啟發(fā)式搜索和約束求解之外，并行處理問題、內(nèi)存建模和執(zhí)行環(huán)境仿真等問題都有待進一步研究與改進。

符號執(zhí)行的另一發(fā)展方向是與Fuzzing技術(shù)相結(jié)合，以提高程序脆弱性檢測的能力。微軟研究機構(gòu)在SAGE中就已經(jīng)進行了這一嘗試和探索，并成功將其應用在對Office和Windows等產(chǎn)品的錯誤檢測上，也取得了顯著的成果。2016年，Shellphish團隊基于angr分析框架和AFL模糊測試器開發(fā)了Driller，用符號執(zhí)行來增強模糊測試，為后續(xù)的研究提供了新思路。

總結(jié)

以上是生活随笔為你收集整理的符号执行技术总结（A Brief Summary of Symbol Execution）- wcventure的全部內(nèi)容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯，歡迎將生活随笔推薦給好友。