當前位置：首頁 > 编程资源 > 编程问答 >内容正文

编程问答

符号执行技术总结（A Brief Summary of Symbol Execution）- wcventure

發布時間：2023/12/14 编程问答 49 豆豆

生活随笔收集整理的這篇文章主要介紹了符号执行技术总结（A Brief Summary of Symbol Execution）- wcventure 小編覺得挺不錯的,現在分享給大家,幫大家做個參考.

符號執行技術總結（A Brief Summary of Symbol Execution）

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

Prologue

近期查閱了符號執行的經典文章(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年中，人們對軟件測試的符號執行產生了極大的興趣，因為它能夠生成高覆蓋率的測試套件并在復雜的軟件應用程序中發現深層次的錯誤。符號執行已經在數十種開發工具中孵化，從而在許多突出的軟件可靠性應用中取得重大的實際突破。

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

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

簡介

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

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

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

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

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

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

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

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

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

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

函數foobar的符號執行，可以有效地表示為樹，如下圖所示。

經典符號執行技術

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

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

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

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

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

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

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

當代碼中包含循環和遞歸時，如果終止條件是符號的話，那么符號執行會產生無限數量的執行路徑。例如下圖所示，

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

在實踐中，需要對搜索施加限制，例如超時，或對路徑數量，循環迭代或探索深度的限制。

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

現代符號執行技術

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

混合執行測試（Concolic testing）

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

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

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

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

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

Concoic測試和EGT是現代符號執行技術的兩個實例，其主要優勢在于它們混合具體和符號執行的能力。為簡單起見，在本文的其余部分，我們將這些技術統稱為“動態符號執行”。

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

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

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

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

主要挑戰和解決方案

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

路徑爆炸(Path Explosion)

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

解決方案:

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

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

約束求解(Constraint Solving)

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

解決方案:

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

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

內存建模(Memory Modeling)

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

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

并發控制(Handling Concurrency)

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

符號執行工具

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

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.

博客：更好地理解符號執行

符號執行基礎
http://pwn4.fun/2017/03/20/符號執行基礎/

符號執行：基礎概念
https://blog.csdn.net/wannafly1995/article/details/80842459

符號執行入門
https://zhuanlan.zhihu.com/p/26927127

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

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

結束語

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

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

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

總結

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

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。

上一篇：解决WebStorm中文显示不正常的问题
下一篇：数学符号大全