符號執行框架綜述：代碼轉換為符號執行所需符號的工具與技術
引言
符號執行是一種程序分析技術，它通過使用抽象的符號值代替具體輸入值來分析程序執行情況。這種技術能夠有效探索程序路徑，并生成對應路徑的輸入條件，因此被廣泛應用于軟件測試、漏洞檢測和逆向工程等領域。本報告將深入探討目前主流的符號執行框架，分析它們的功能特點、應用場景以及技術實現，為讀者提供全面的符號執行工具參考。
符號執行技術概述
符號執行的基本概念
符號執行是一種靜態分析技術，旨在理解程序在輸入條件的不同組合下的行為。與傳統的具體執行不同，符號執行使用符號變量代替具體值作為程序輸入，并用符號表達式表示與符號值相關的程序變量的值[0]。在遇到程序分支指令時，程序的執行也會相應地分支，形成不同的符號約束條件。 符號執行技術是一種白盒的靜態分析技術，它通過采用抽象的符號代替精確值作為程序輸入變量，得出每個路徑抽象的輸出結果[31]。這種技術的核心思想是通過使用符號值來代替具體值作為程序輸入，并用符號表達式來表示與符號值相關的程序變量的值[4]。
符號執行的應用領域
符號執行技術在多個領域有著廣泛的應用：
- 軟件測試：通過生成滿足特定路徑條件的輸入，實現對程序路徑的全面覆蓋
- 漏洞檢測：發現程序中可能存在的安全漏洞和錯誤
- 惡意軟件分析：分析惡意軟件的行為模式和攻擊方式
- 代碼逆向工程：理解編譯后的二進制代碼的功能和邏輯
- 固件安全分析：分析嵌入式設備固件的安全性[30]
主流符號執行框架
Angr框架
Angr是一個基于Python的二進制分析框架，它支持靜態分析和符號執行，尤其在惡意軟件分析、漏洞挖掘和逆向工程等安全領域中扮演著重要角色[9]。Angr的主要特點：
- 開源性：Angr是一個開源的Python框架，可以直接通過pip安裝
- 功能強大：提供了多種工具，用于靜態和動態分析二進制文件，包括反匯編、控制流圖分析、模擬執行、符號執行等功能[10]
- 多架構支持：是一個多架構開源二進制分析工具包
- 動態符號執行：能夠對二進制文件執行動態符號執行，如Mayhem、KLEE等[29] Angr的架構包括CLE（用于處理二進制文件和庫）、VEX（中間表示）、SimProcedures（模擬系統調用）等多個組件。CLE對不同的二進制格式進行抽象，以處理加載給定的二進制文件和它所依賴的任何庫、解析動態符號、執行重定位以及正確初始化程序狀態[24]。 Angr被廣泛應用于CTF競賽中的逆向分析，研究人員可以利用這個工具嘗試對一些CTF題目進行符號執行來找到正確的解答，即flag[21][22]。 此外，Angr還被用于惡意軟件分析工具SEMA的開發，SEMA基于angr，而angr則用于提取API調用[27]。
KLEE框架
KLEE是一個封裝比較好的符號執行工具，可以直接輸入程序進行分析，不像angr那樣更像是一個框架[15]。KLEE主要用于C語言代碼的符號執行分析。KLEE的特點：
- 封裝性：相比于angr，KLEE是一個可以直接使用的工具
- 針對C語言：主要面向C代碼的符號執行
- 高效性：在處理非聚合類型的輸入時，Klee表現卓越（達82.80%）[25] KLEE在軟件測試和漏洞挖掘領域有著廣泛的應用，它可以有效地探索程序的執行路徑，并生成滿足特定路徑條件的輸入。
S2E框架
S2E是一個選擇性的符號執行平臺，構建于QEMU之上。在Avatar框架中，S2E提供了一個功能強大的插件接口，插件可以通過這些接口攔截仿真事件（比如，基本塊）[33]。S2E的主要特點：
- 基于QEMU：構建于QEMU虛擬機監控器之上
- 選擇性符號執行：可以選擇性地對程序的某些部分進行符號執行
- 插件系統：提供強大的插件接口，方便擴展功能 S2E是針對KLEE無法對二進制生成LLVM IR的缺點而開發的，它在QEMU虛擬機上實現了將二進制程序翻譯成中間表示的功能[16]。
Z3約束求解器
Z3是由微軟開發的一個SMT（滿意賦值理論）求解器，雖然它本身不是一個完整的符號執行框架，但在符號執行過程中扮演著重要角色。Z3用于解決符號執行過程中生成的約束條件，幫助確定是否存在滿足特定路徑條件的輸入。Z3的特點：
- 高效約束求解：能夠高效地求解符號執行過程中生成的約束條件
- 多語言支持：提供多種編程語言的接口，包括Python、C++等
- 廣泛應用于符號執行工具：許多符號執行工具，如angr，都使用Z3作為約束求解器 Z3在符號執行過程中與符號執行引擎（如angr）配合使用，在整個過程中，會使用Z3來求解路徑約束，以生成滿足特定路徑條件的測試用例[18]。
Boomerang框架
Boomerang是一個反編譯工具，它可以將二進制代碼轉換為高級語言表示，為符號執行提供更高級的抽象。雖然它本身不是一個完整的符號執行框架，但可以與符號執行工具結合使用。
Triton框架
Triton是一個用于分析二進制程序的符號執行框架，它可以幫助定位與用戶輸入有交互的代碼塊，并對這些代碼塊進行符號執行，從用戶輸入點作為符號變量開始，直到達到所需的約束條件[23]。
μEmu和Jetset
2021年的μEmu和Jetset將符號執行框架（如S2E或Angr）與固件重新托管技術結合，以提高固件仿真的效率[30]。這些工具在嵌入式設備固件安全分析領域有著重要應用。
Driller
Driller是AFL（American Fuzzy Lop）和angr結合的產物，它通過結合模糊測試和符號執行，提高漏洞發現的效率。Driller的使用需要通過import來導入angr和driller接口，在包含afl和angr的虛擬環境中部署好之后，可以通過腳本來調用[32]。
DICE
DICE是在P2IM的基礎上增加DMA仿真功能的符號執行框架，它擴展了符號執行的應用范圍，使其能夠處理更復雜的系統[30]。
符號執行框架的比較
S2E、Angr、KLEE和QSYM的比較
根據搜索結果，S2E、Angr、KLEE和QSYM是四個主要的符號執行引擎[16]。它們的主要區別在于：
- S2E：構建于QEMU之上，是一個選擇性的符號執行平臺，提供強大的插件接口
- Angr：基于Python的二進制分析框架，支持動態符號執行和靜態分析
- KLEE：封裝比較好的符號執行工具，主要用于C語言代碼的分析
- QSYM：可能是一個針對特定場景優化的符號執行引擎
動態符號執行和LLM的比較
在生成測試用例方面，動態符號執行工具如Klee在特定場景下表現良好。對于非聚合類型的輸入，Klee表現卓越（達82.80%），展示了符號執行技術在理想條件下的高效性。但在實際復雜場景中，其局限性也較為明顯[25]。
靜態二進制分析的局限性
靜態二進制分析盡管使得系統能檢測到所有可能的程序路徑，卻犧牲了可擴展性和表現。靜態二進制分析通常很慢，在處理間接跳轉語句時也受限。在構造CFG（控制流圖）時處理非直接跳轉語句也面臨挑戰[34]。
符號執行工具的最新發展
多線程并行符號執行引擎
隨著計算能力的提升，多線程并行的符號執行引擎成為研究熱點。基于多線程并行的符號執行引擎設計與實現的研究表明，這種技術可以顯著提高符號執行的效率和性能[26]。
結合機器學習的符號執行
將機器學習技術與符號執行相結合，可以提高符號執行的效率和準確性。例如，利用LLM（大語言模型）與動態符號執行相結合，可以生成更有效的測試用例[25]。
嵌入式設備固件安全分析
隨著物聯網設備的普及，嵌入式設備固件的安全分析成為研究熱點。2021年的μEmu和Jetset將符號執行框架（如S2E或Angr）與固件重新托管技術結合，以提高固件仿真的效率。2021年的DICE在P2IM的基礎上增加DMA仿真功能，進一步擴展了符號執行的應用范圍[30]。
符號執行工具的使用場景
漏洞挖掘
符號執行工具在漏洞挖掘領域有著廣泛應用。通過符號執行，可以系統地探索程序的執行路徑，發現可能導致安全漏洞的輸入條件。例如，Angr、KLEE等工具都被廣泛應用于漏洞挖掘研究中。
代碼混淆研究
符號執行工具如KLEE和Angr也被用于代碼混淆研究。通過對混淆代碼進行符號執行，可以分析代碼的行為，理解混淆技術的實現原理，從而開發更有效的反混淆方法[19]。
惡意軟件分析
符號執行技術在惡意軟件分析領域也有重要應用。例如，SEMA是一款基于符號執行的惡意軟件分析工具，可以幫助研究人員輕松執行惡意軟件分析任務。SEMA基于angr，而angr則用于提取API調用[27]。
CTF逆向分析
在CTF競賽中，符號執行工具如Angr被廣泛用于逆向分析。研究人員可以利用這些工具嘗試對CTF題目進行符號執行，找到正確的解答，即flag[21][22]。
符號執行工具的局限性
性能問題
符號執行工具通常面臨性能問題，特別是在處理大型程序時。符號執行需要維護大量的符號狀態，這可能導致計算資源消耗過大，執行時間過長。
狀態爆炸問題
隨著程序路徑的增加，符號執行需要維護的狀態數量可能會呈指數級增長，導致狀態爆炸問題。這限制了符號執行在復雜程序上的應用。
間接跳轉處理困難
靜態二進制分析在處理間接跳轉語句時面臨挑戰。間接跳轉可能導致無法準確構建控制流圖，影響符號執行的準確性[34]。
結論
符號執行是一種強大的程序分析技術，它通過使用符號變量代替具體值，探索程序的所有可能執行路徑。目前，已經開發了多種符號執行框架和工具，如Angr、KLEE、S2E等，它們在軟件測試、漏洞檢測、惡意軟件分析等領域有著廣泛的應用。 隨著技術的發展，符號執行工具也在不斷演進，出現了多線程并行符號執行引擎、結合機器學習的符號執行等新技術。這些技術的發展使得符號執行工具能夠處理更復雜的程序，提高分析效率和準確性。 然而，符號執行工具仍然面臨性能問題、狀態爆炸問題和間接跳轉處理困難等挑戰。未來的研究方向可能包括優化符號執行算法，減少狀態空間，提高處理間接跳轉的能力，以及結合其他技術（如機器學習）來提高符號執行的效率和準確性。
參考文獻
[0] test Symbolic Execution-01-符號執行（Symbolic Execution）簡介原創. https://blog.csdn.net/ryo1060732496/article/details/135543800.
[4] 符號執行(Symbolic Execution) 與約束求解(Constraint Solving) - 騰訊云. https://cloud.tencent.com/developer/article/2377216.
[9] 符號執行之angr初探原創 - CSDN博客. https://blog.csdn.net/hanxuer_/article/details/106065133.
[10] 符號執行angr安裝與使用原創 - CSDN博客. https://blog.csdn.net/xshower/article/details/113869873.
[15] KLEE 源碼閱讀筆記-安全KER. https://www.anquanke.com/post/id/240038.
[16] 符號化執行引擎對比原創 - CSDN博客. https://blog.csdn.net/m0_37907383/article/details/105674577.
[18] 符號執行，從漏洞掃描到自動化生成測試用例. http://www.ekrvqnd.cn/article/663849.html.
[19] 2021看雪SDC議題回顧| 代碼混淆研究的新方向. https://zhuanlan.zhihu.com/p/426876577.
[21] 符號執行-Angr實踐原創 - CSDN博客. https://blog.csdn.net/yalecaltech/article/details/88753923.
[22] 利用Angr進行簡單CTF逆向分析-符號執行工具. http://www.ekrvqnd.cn/article/554933.html.
[23] [翻譯]使用Triton框架分析混淆代碼(How Triton may help to ... - 看雪. https://bbs.kanxue.com/thread-277009.htm.
[24] angr原理與實踐（一）——原理- WelkinChan - 博客園. https://www.cnblogs.com/welkinchan/p/16483119.html.
[25] LLM與動態符號執行生成測試用例的比較原創 - CSDN博客. https://blog.csdn.net/qq_44370676/article/details/144159798.
[26] 基于多線程并行的符號執行引擎設計與實現 - 計算機研究與發展. https://crad.ict.ac.cn/cn/article/doi/10.7544/issn1000-1239.202220920?viewType=HTML.
[27] SEMA：一款基于符號執行的惡意軟件分析工具 - FreeBuf. https://www.freebuf.com/sectool/412060.html.
[29] ANGR初識原創 - CSDN博客. https://blog.csdn.net/leiwuhen92/article/details/134171222.
[30] [PDF] 嵌入式設備固件仿真器綜述 - 計算機研究與發展. https://crad.ict.ac.cn/cn/article/pdf/preview/10.7544/issn1000-1239.202330476.pdf.
[31] 符號執行 - 極客方舟. https://deelmind.com.cn/reverse/symbolic/.
[32] 符號執行結合fuzz總結原創 - CSDN博客. https://blog.csdn.net/sjlving123/article/details/114636197.
[33] [PDF] 嵌入式設備固件安全分析技術研究綜述 - 計算機學報. http://cjc.ict.ac.cn/online/bfpub/yyc-2020818141436.pdf.
[34] 關于CRS中的自動化漏洞檢測和攻擊代碼生成研究綜述. https://rowl1ng.com/MyWiki/machine_learning/application/automated_vulnerability_detection.html.
