linux 符号执行,[原创]符号执行Symcc与模糊测试AFL结合实践
上個月末無聊的劃水時間段內，在推上看到有人發了一篇關于如何結合去年新發布的符號執行Symcc與模糊測試引擎AFL，以提升Fuzz效率的視頻貼。打開這個鏈接后才發現是個賣課的，emmm.... , 看價格￡1499果斷打擾了，果然沒錢的都不配學安全嗎23333；原技術文章看來是看不到了，只能靠公開的一段視頻還原操作。
背景介紹
雖然有很多大佬肯定已經十分熟悉模糊測試和符號執行了，還是簡單介紹一下背景知識，這樣更有連貫性。
模糊測試 AFL
模糊測試(fuzz testing, fuzzing)是一種軟件測試技術。 其核心思想是將自動或半自動生成的隨機數據輸入到一個程序中，并監視程序異常，如崩潰，斷言(assertion)失敗，以發現可能的程序錯誤，比如內存泄漏。 模糊測試常常用于檢測軟件或計算機系統的安全漏洞。
模糊測試誕生于1988年秋季的一個黑暗暴風雨之夜 [Takanen et al, 2008.]。巴頓·米勒教授坐在麥迪遜威斯康星州的公寓里，通過一條1200波特的電話線連接到他所屬大學的計算機。陣陣的雷暴在線路上造成噪音，這些噪音又導致兩端的UNIX命令獲得錯誤的輸入，并導致崩潰。頻繁的崩潰使他感到驚訝—我們編寫的程序不是應該十分強大嗎？作為一名科學家，他想探究該問題的嚴重程度及其原因。因此，他為威斯康星大學麥迪遜分校的學生編寫了一個編程練習，而該練習將使他的學生創建第一個模糊測試器。
這項作業的原文描述是這樣的：
The goal of this project is to evaluate the robustness of various UNIX utility programs, given an unpredictable input stream. [...] First, you will build a fuzz generator. This is a program that will output a random character stream. Second, you will take the fuzz generator and use it to attack as many UNIX utilities as possible, with the goal of trying to break them.
該項目的目標是在給定不可預測的輸入流的情況下評估各種UNIX實用程序的健壯性。[...]首先，您將構建一個模糊發生器。這是一個將輸出隨機字符流的程序。其次，您將使用模糊發生器，并使用它來攻擊盡可能多的UNIX實用程序，以試圖破壞它們。
這個作業在不經意間抓住了模糊測試的本質：創建隨機的輸入，并持續性觀察它是否會破壞目標應用程序，理論上只要運行足夠長的時間，我們就會看到錯誤的發生。
AFL(american fuzzy lop)最初由Micha? Zalewski開發，和libFuzzer等一樣是基于覆蓋引導(Coverage-guided)的模糊測試工具，它通過記錄輸入樣本的代碼覆蓋率，從而調整輸入樣本以提高覆蓋率，增加發現漏洞的概率。其工作流程大致如下：
從源碼編譯程序時進行插樁，以記錄代碼覆蓋率(Code Coverage)
選擇一些輸入文件，作為初始測試集加入輸入隊列(queue)
將隊列中的文件按一定的策略進行“突變”
如果經過變異文件更新了覆蓋范圍，則將其保留添加到隊列中
上述過程會一直循環進行，期間觸發了crash的文件會被記錄下來
符號執行 Symcc
符號執行簡單來說是在目標程序的執行過程中跟蹤中間值是如何計算的，每一個中間值都可以表示為程序輸入的一個公式。在任何點，系統都會使用這個公式查看這個點是否可達，這個指針是否為空等。如果答案是確定的，那么符號執行引擎將會提供測試用例，一個新的輸入例子來觸發對應的行為。所以符號執行可以被方便的用來探測程序路徑以及觸發bug。
新的符號執行Symcc發表于去年頂會USENIX’20，論文名稱為Symbolic execution with SYMCC: Don’t interpret, compile!
那么Symcc和它的前輩們又有什么不同呢？論文作者Aurélien Francillon認為傳統符號執行主要分為兩類：IR-based和IR-less。
IR-based是指無論測試對象如何，先把目標的二進制程序給轉換到IR層(中間表達形式)再進行抽象解釋，其缺點是特別容易路徑爆炸。常見用此方法的符號執行有angr、KLEE和Mayhem，主要過程如下圖所示：
IR-less是指符號執行引擎通過動態插樁技術(利用PIN插樁框架等)先對二進制程序插樁，執行部分指令后再構造符號表達式。其優點是快，缺點是插入的代碼函數可能無法生成正確的符號表達式，且較依賴于指令集。常見用此方法的符號執行有Triton、QSYM、SAGE和Driller，主要過程如下圖所示：
作者提出的SymCC不同點在于，直接在編譯期就開始在生成的IR上植入符號執行相關代碼，進一步提升性能；其流程大致如下：
開始結合
整體的結合流程沒什么新花樣，基本是按照 安裝各種包環境—> 編譯簡單的后端/功能更強的qsym后端 —> 用symcc編譯llvm的libcxx —> 開始嘗試fuzz 的過程循序漸進。
安裝各種環境
先安裝各種包和依賴：
這里的LLVM 要求是 8, 9, 10 或者11 ，C++編譯器要支持 C++17。實際安裝過程中有些unbuntu版本可能無法直接apt-get，使用llvm官方https://apt.llvm.org/ 的包支持。
隨后安裝Z3，要求版本號大于4.5
這里有點小坑，用該方式安裝的z3可能在后面編譯時llvm無法找到路徑。如果報此類似錯誤的，該步可用cmake的Ninja進行編譯，指路鏈接：https://github.com/Z3Prover/z3/blob/master/README-CMake.md
然后安裝afl，沒什么可說的先安原版
下載symcc的源碼做好之后編譯backend的準備
編譯backend
symcc帶了兩種后端，一種是功能簡單(simple)的；另一種是qsym的后端，與前者相比功能性更強，我們兩種都編譯一下。在配置構建時，選項都將通過“ -D”傳遞給CMake，常見選項如下表所示：
選項
作用
- QSYM_BACKEND=ON/OFF (default OFF)
是否編譯QSYM后端，若否即為編譯simple后端；每次執行時可以使用LD_LIBRARY_PATH在后端之間切換
- TARGET_32BIT=ON/OFF (default OFF)
啟用64位主機對32位編譯的支持
- LLVM_DIR/LLVM_32BIT_DIR (default empty)
提供編譯時llvm的位置
- Z3_DIR/Z3_32BIT_DIR (default empty)
提供編譯時Z3的位置
- Z3_TRUST_SYSTEM_VERSION (default OFF)
信任系統版本的Z3，不檢查Z3版本的兼容性；如果Z3的安裝版本太舊，則可能發生編譯錯誤。
首先編譯簡單的后端，這里的LLVM_DIR指向你所用版本llvm位置
后面在ninja check時會有8個錯誤，不影響后面的正常執行。(參考視頻的編譯過程中也有錯誤)
下面編譯qsym的后端，與前者相比區別就是把DQSYM_BACKEND改成ON
check時也會有一些錯誤，問題不大。
用symcc編譯llvm的libcxx
對于更加復雜的C++代碼，symcc提供了兩種解決方法。一種是使用系統提供的C ++標準庫。這是最簡單的不需要額外的編譯，但是它有一個重要的缺點：會影響符號執行的過程。另一種方法是自己編譯一個檢測的C ++標準庫，這樣就可以通過庫跟蹤數據，但這需要構建庫并針對它編譯所有代碼。
建立C ++標準庫是一項一次性的工作，建一次后可以在所有后續的C ++編譯中使用，每當我們使用libc++就會自動使用我們編譯的llvm標準庫實現。
編譯過程如下：
請自己手動把$BASE指向之前準備工作的文件位置
開始嘗試Fuzz！
這里我們準備一個特殊的苛刻例子
根據這段源碼，我們可以判斷出當且僅當文件輸入為0xdeadbeef 時，return (int)(20 / t1)會出現除零錯誤，而該例子單純使用afl是難以發現錯誤的。
我們分別使用qsym編譯出的后端symcc和afl對其進行編譯，并且創建一個樣例AAAAAAA
之后就開始運行吧，我們使用afl的并行模式
這里symcc_fuzzing_helper的參數中-o指向afl的out目錄，-a指向要輔助的afl進程名字，如上所示這里我就是fuzz2.
symcc_fuzzing_helper其實就是在使用afl生產的testcase進行符號執行，如果它認為樣例有趣就會生成新的，并將它傳送到正在執行的afl隊列里，afl就能夠使用該新生成樣例進行測試，這一流程輔助了afl能夠到達一些之前無法到達的路徑。
這里有個小坑，單純執行afl時afl-fuzz命令后面的--可帶也可不帶，但是symcc_fuzzing_helper是通過檢測afl-fuzz里--后面命令執行的，所以如果我們在afl-fuzz后習慣性不加--就可能導致symcc無有效的輸出結果。
一切準備就緒，開始運行吧！
我們驚喜的發現單純fuzz難以找到的漏洞，在symcc_fuzzing_helper的協助下，直接就找到了crash。
簡單分析一下，用Hexdump看到crash真的是0xdeadbeef，symcc輔助AFL找到了使目標程序崩潰的testcase。
總結
使用符號執行Symcc與模糊測試引擎Afl的簡單驗證成功了，之后可以就試一試現實中的一些項目，比如論文中提的Tcpdump之類的；還可以考慮將Symcc與其他模糊測試引擎相結合，比如Afl++，在各種算法加持下的Afl++再結合符號執行可能會有更好的效果。
最后特別感謝Symcc發明人和論文的原作者 Aurélien Francillon 與 ADALogics 的安全研究員David Korczynski，它們在推特上幫助了我很多，同時感謝Discord的Fuzzing板塊討論讓我有興趣進行各種新的嘗試，我仍有很多需要學習的地方。
參考資料
帶你搞懂符號執行的前世今生與最近技術
https://www.anquanke.com/post/id/231413
G.O.S.S.I.P 學術論文推薦
https://wemp.app/posts/40a16228-7a86-4985-b7c2-b3507e3fc161
Symcc源碼
https://github.com/eurecom-s3/symcc/
入門afl
https://i-m.dev/posts/20191001-225746.html
總結
以上是生活随笔為你收集整理的linux 符号执行,[原创]符号执行Symcc与模糊测试AFL结合实践的全部內容，希望文章能夠幫你解決所遇到的問題。
- 上一篇： C++打卡4-宝箱密码
- 下一篇： linux平台 wifi 7601 po