:從符號執(zhí)行到逆向約束求解)
前幾篇筆記把 angr 的環(huán)境搭建、Project 加載、符號執(zhí)行的基本流程都過了一遍今天這篇單獨寫一個特別容易踩坑、但又特別出效果的點寄存器符號化。很多剛接觸符號執(zhí)行的朋友會有一個困惑我用 angr 跑一個二進制明明已經(jīng)拿到了控制流為什么條件分支里的變量還是“看不懂”或者我想分析某個函數(shù)的輸入輸出關系但程序是從文件、網(wǎng)絡、硬件里讀數(shù)據(jù)參數(shù)根本不在內(nèi)存里我怎么讓 angr 知道“這里有一個未知值”答案就是寄存器符號化。把 CPU 寄存器從“具體的 0 或 1”變成“一個待求解的符號表達式”讓 angr 在模擬執(zhí)行時把這個符號一路攜帶、一路參與運算、一路約束下來最后用求解器反推出滿足條件的取值。這篇筆記就圍繞這個主題展開適合已經(jīng)跑通 angr 基礎 demo、但想深入做函數(shù)級分析的人。1. 寄存器符號化到底在解決什么問題1.1 具體執(zhí)行和符號執(zhí)行的差別先從一個最樸素的視角看起。普通調(diào)試器執(zhí)行程序時寄存器里裝的一定是具體數(shù)字比如eax 0x7fffffffe2a0、rcx 3。每一步運算都會產(chǎn)生一個確定的新值我們順著執(zhí)行流走一遍能看到的只是“某一條路徑”上的結果??扇绻绦蛴?100 個條件分支每次輸入不同走的路徑就不同用具體執(zhí)行去試那真是大海撈針。符號執(zhí)行的思路完全不同它允許寄存器里裝的是一個“未知數(shù)”。比如我新建一個狀態(tài)把rdi設成符號變量x之后 CPU 執(zhí)行add rdi, 5時angr 不會去算出一個具體數(shù)字而是記下“此時 rdi 的表達式是 x 5”。等執(zhí)行到某個判斷指令cmp rdi, 100時angr 會分別往兩個分支走一個分支里額外記錄約束x 5 100另一個分支里記錄約束x 5 ! 100。這個過程很像我們在高中數(shù)學里“帶著未知數(shù)做題”只不過符號執(zhí)行把每一步的表達式、每個分支的約束都自動化地累加了下來最后交給 SMT 求解器angr 默認用 Z3去解。寄存器符號化就是整個鏈條的起點告訴模擬器“這個寄存器里是一個我還沒定下來的值”。1.2 寄存器符號化的典型應用場景寄存器符號化最常用的場景我總結成三類。第一類是逆向分析中的函數(shù)級分析。你拿到一個二進制在 IDA 或 Ghidra 里看到一個關鍵函數(shù)sub_401120它的參數(shù)來源是程序前面復雜的計算或者干脆是外部設備的輸入。你不想把整個程序都跑一遍只想單獨分析這個函數(shù)的行為那就在函數(shù)入口處新建一個狀態(tài)把參數(shù)寄存器符號化然后只分析這個函數(shù)的邏輯。第二類是路徑條件還原。程序里有一段加密、校驗或者關鍵判斷邏輯你希望知道“滿足什么條件才能走到某個分支”。這種情況下符號化的參數(shù)會被帶到分支判斷中angr 自動收集路徑約束你最后用 solver 求出滿足條件的值這就是約束還原。第三類是物聯(lián)網(wǎng)固件、驅(qū)動、Shellcode 這類“無操作系統(tǒng)上下文”的分析。這類樣本經(jīng)常直接從寄存器里拿數(shù)據(jù)比如從硬件寄存器讀取狀態(tài)、從某個約定的寄存器接收參數(shù)內(nèi)存里的狀態(tài)幾乎不可依賴。這時候寄存器符號化幾乎是唯一干凈地建立抽象輸入的方法。1.3 為什么偏偏是“寄存器”不是普通變量你可能會問符號執(zhí)行不是也能符號化內(nèi)存變量嗎為什么單獨把寄存器拎出來講因為寄存器是 CPU 與程序邏輯交互的最短路徑。函數(shù)調(diào)用約定規(guī)定參數(shù)先放寄存器系統(tǒng)調(diào)用通過寄存器傳遞調(diào)用號和參數(shù)硬件狀態(tài)通過寄存器暴露給軟件。你想給一個函數(shù)“喂輸入”本質(zhì)就是在給它“喂寄存器”。而內(nèi)存符號化通常要處理地址空間、大小端、棧布局稍不留神就和真實執(zhí)行對不上寄存器符號化則簡單得多一個state.regs.rax BVS就能解決。另一個實踐層面的原因是angr 對寄存器符號化的支持非常完善state.regs這個屬性可以按架構自動映射所有通用寄存器的名字和位寬還會處理別名關系比如rax和eax。這比手動去構造內(nèi)存地址、手動讀寫棧要可靠得多。后面我會具體展開這塊。2. 動手之前angr符號化必備基礎2.1 claripy與BVS/BVVangr 的符號表達式底層由名為 claripy 的庫實現(xiàn)。你不需要把 claripy 的所有 API 都背下來但兩個最基礎的概念必須清楚。第一個是BVS全稱 BitVectorSymbol用來創(chuàng)建一個符號位向量。它有兩個核心參數(shù)名稱和位寬。名稱只是給這個符號起的字符串名字通常是給人看的比如flag、arg0不一定需要唯一但實踐中建議起成有含義的名字因為后續(xù)調(diào)試 AST 時你會靠名字辨認變量。位寬必須是整數(shù)常見的有 8、16、32、64。創(chuàng)建一個 32 位符號變量寫法是import claripy x claripy.BVS(x, 32)第二個是BVV全稱 BitVectorValue用來創(chuàng)建一個具體值的位向量。比如claripy.BVV(10, 32)表示一個 32 位的具體數(shù)值 10。你可能覺得這不是多余嗎直接用 Python 的int不就行了不行。因為在 claripy 的表達式體系里符號變量是 AST 節(jié)點具體值也要以 AST 節(jié)點形式參與運算才能統(tǒng)一進行位寬檢查和表達式化簡。如果你把一個 Python int 直接塞給 angr 的某個寄存器可能會得到類型錯誤或者在運算時出現(xiàn)隱式位寬不匹配。類型名稱用途示例BVSBitVectorSymbol符號變量代表未知值claripy.BVS(x, 32)BVVBitVectorValue具體值節(jié)點claripy.BVV(0x10, 32)這兩個概念是所有符號化操作的基石。在 angr 的SimState里你通??梢灾苯佑胹tate.solver.BVS來創(chuàng)建符號變量它其實就是 claripy.BVS 的一層封裝效果完全一樣。2.2 SimState與state.regsangr 模擬執(zhí)行的核心對象是SimState中文常翻譯成“狀態(tài)”。一個狀態(tài)里包含了 CPU 寄存器、內(nèi)存、文件描述符、求解器、路徑約束等一大堆東西。你可以把狀態(tài)理解成“某一條執(zhí)行路徑在當前時刻的完整快照”。操作寄存器的入口是state.regs。這是一個類似字典的屬性對象按寄存器名訪問或賦值。例如在 x86-64 架構下state.regs.rax claripy.BVS(input, 64)這一行執(zhí)行后rax就變成了一個 64 位的符號變量。接下來任何指令只要讀取rax拿到的都是這個符號表達式的后續(xù)演化結果。讀取時也可以直接取state.regs.rax返回的是一個 AST 對象它的類型是claripy.ast.BV。state.regs真正強大的地方在于它自動處理了架構差異。同樣是“棧指針”x86 里叫espARM 里叫spangr 都會映射到對應架構的寄存器集合里。你不需要記“這個架構到底用哪個寄存器存返回值”只要用state.regs.eax或者state.regs.raxangr 會按照架構的寄存器名約定進行訪問。如果你的目標架構比較偏門還可以用state.arch.registers查看到底有哪些寄存器名可用。2.3 最小符號化骨架代碼一個最基礎的寄存器符號化流程可以壓縮成四步加載程序、創(chuàng)建狀態(tài)、符號化寄存器、求解。下面的代碼是一個可以照著改的最小骨架import angr import claripy proj angr.Project(./target_binary, auto_load_libsFalse) state proj.factory.blank_state(addr0x401120) state.regs.rcx claripy.BVS(arg0, 64) simgr proj.factory.simulation_manager(state) simgr.explore(find0x401156, avoid0x40116a) if simgr.found: found simgr.found[0] solution found.solver.eval(found.regs.rcx) print(hex(solution))這段代碼里有一個很多人一開始不理解的細節(jié)為什么用blank_state(addr...)而不是entry_state()因為entry_state是從程序入口開始執(zhí)行你很少能直接控制入口處的寄存器值而blank_state允許你指定“從哪個地址開始模擬”并自由設置初始寄存器內(nèi)容。做函數(shù)級分析時blank_state配合一個函數(shù)入口地址是最干凈的組合。不過這個骨架非常粗糙真實場景里你會發(fā)現(xiàn)很多坑比如find地址找不準、符號變量在某個指令里被偷偷截斷了、求解器給出的解和預期不符等等。下面我用一個完整可復現(xiàn)的例子帶你一步步搞清楚寄存器符號化到底應該怎么寫。3. 寄存器符號化的完整實操流程3.1 準備一個可復現(xiàn)的目標程序紙上談兵沒意思我寫一個足夠小、但包含真實邏輯的程序來演示。假設我們有這樣一個 C 文件// mystery.c #include stdio.h int mystery(int a, int b) { if (a * b 30 a b 11) { return 1; } return 0; } int main(int argc, char **argv) { int a 3, b 7; printf(%d\n, mystery(a, b)); return 0; }這個mystery函數(shù)就是我們的分析目標參數(shù)a、b通過寄存器傳入函數(shù)內(nèi)部有一個復合條件。我們希望做的是不修改程序、不手動試值讓 angr 自己把滿足條件的a和b求出來。編譯時建議關掉優(yōu)化和 PIE方便找地址gcc -O0 -fno-pie -no-pie -o mystery mystery.c編譯后用nm mystery找到mystery函數(shù)的地址。在我本機上是0x401126你環(huán)境里的地址可能不同以后面nm輸出為準。再反匯編看一眼結構確認兩個分支分別落在哪里。為了敘述方便我假設反匯編后的布局是這樣的0x401126mystery函數(shù)入口0x401156條件滿足時設置eax 1并返回的基本塊0x40116a條件不滿足時設置eax 0并返回的基本塊實際分析時請用objdump -d mystery確認不要照抄我的地址。3.2 把未知參數(shù)寫進寄存器在 angr 里給函數(shù)傳參除了最直接的state.regs.rdi a還有更規(guī)范的做法call_state。這個接口能按照目標架構的函數(shù)調(diào)用約定自動把參數(shù)放到對應的寄存器里并且自動初始化返回地址和棧幀。對 x86-64 來說mystery的兩個整數(shù)參數(shù)會分別放到rdi和rsi。import angr import claripy proj angr.Project(./mystery, auto_load_libsFalse) a claripy.BVS(a, 64) b claripy.BVS(b, 64) state proj.factory.call_state(0x401126, a, b)為什么符號變量用 64 位而不是 32 位因為在 x86-64 調(diào)用約定里即使 C 語言函數(shù)參數(shù)是int參數(shù)寄存器也使用完整的 64 位寄存器rdi和rsi只是讀取時只使用低 32 位。如果你用 32 位符號變量賦給state.regs.rdiangr 會做隱式零擴展后面求解時會出現(xiàn)一些不好理解的約束。先統(tǒng)一用 64 位符號變量配合int語義是相對省心的選擇。這里插一句我自己的經(jīng)驗如果你不想關心調(diào)用約定也可以直接用blank_state加手動賦值state proj.factory.blank_state(addr0x401126) state.regs.rdi a state.regs.rsi b兩種方式最終的效果差不多但call_state會自動把返回地址等信息準備好后續(xù)如果你想分析函數(shù)返回后的行為會方便很多。本篇以call_state為主線。3.3 設置探索目標和規(guī)避地址符號化好參數(shù)寄存器之后我們讓 angr 從mystery函數(shù)入口開始跑。但這里有個關鍵點我們關心的不是“程序最終走到哪”而是“走到某個目標地址時參數(shù)應該滿足什么條件”。用符號執(zhí)行引擎自帶的路徑探索功能我們可以讓 angr 同時探索所有可能路徑并篩選出我們關心的那兩條路徑。find參數(shù)指定目標地址avoid參數(shù)指定要避開的地址simgr proj.factory.simulation_manager(state) simgr.explore(find0x401156, avoid0x40116a) if simgr.found: found_state simgr.found[0] print(found state at, hex(found_state.addr))find和avoid都可以是地址列表也可以是帶addr屬性的函數(shù)。用函數(shù)會更靈活比如“當eax 1時停下”但在我們的簡單例子里直接按地址找最直觀。走到這一步angr 內(nèi)部已經(jīng)發(fā)生了很多事情它沿著二進制指令一條條模擬執(zhí)行每次遇到條件跳轉(zhuǎn)就分叉出一個新狀態(tài)每個狀態(tài)各自保存自己的路徑約束。mystery函數(shù)里那個復合條件會被 angr 拆成多個分支約束。我們找到的那個found_state里面的求解器已經(jīng)攜帶了“走到地址 0x401156 必須滿足的所有條件”。3.4 把符號解回具體值現(xiàn)在到了最關鍵也最讓人興奮的一步用求解器把符號變量解成具體數(shù)字。sol_a found_state.solver.eval(a) sol_b found_state.solver.eval(b) print(a , sol_a, b , sol_b)solver.eval的作用是在滿足當前狀態(tài)所有約束的前提下給符號變量求出一個可行的具體解。在我的環(huán)境里輸出的結果是a 5、b 6正好滿足5 * 6 30且5 6 11。不過要注意eval只返回一個解而滿足條件的解可能不止一個。比如把函數(shù)條件改成a b 5那么解就有無數(shù)多個eval會隨便挑一個。如果你想拿到所有有代表性的值可以用eval(expr, n)一次求多個解或者用min、max求極值min_a found_state.solver.min(a) max_a found_state.solver.max(a)每個符號執(zhí)行狀態(tài)里默認帶有一個solver它內(nèi)部維護著該狀態(tài)的全部路徑約束。你也可以用found_state.solver.add_constraint(...)手動追加約束比如你額外知道“a 必須大于 0”就追加一條再重新求解。追加約束不會抹掉之前的路徑條件只是讓可行域縮小。到這里一個最完整的寄存器符號化流程就跑通了。你可能會覺得這個例子這么簡單手動心算也能出結果。沒錯但同樣的流程放到幾 MB 的二進制、幾十個嵌套分支里手動算是不可能的而寄存器符號化依然能穩(wěn)定地把約束收集起來這就是它的價值所在。4. 進階玩法從單寄存器到整機狀態(tài)4.1 寄存器別名與高低位處理真正寫代碼時會遇到一個繞不開的細節(jié)x86-64 的寄存器別名。rax、eax、ax、al都指向同一塊物理寄存器只是位寬不同。angr 在state.regs里也模擬了這個行為但有一些細節(jié)必須注意。如果你先執(zhí)行state.regs.rax claripy.BVS(x, 64)然后讀取state.regs.eaxangr 會返回x的低 32 位表達式記作Extract(31, 0, x)。這沒問題。但反過來就有講究了如果你先執(zhí)行state.regs.eax claripy.BVS(y, 32) state.regs.rax ...x86-64 的硬件語義是寫 32 位寄存器會清零高 32 位angr 在大多數(shù)架構下也模擬了這一點。這意味著你寫eax后再讀rax得到的并不是“一個符號變量 y 另一個保留的 rax 高位”而是“y 的零擴展”。如果沒意識到這一點后面求解出來的值可能和你預期的完全不一樣。實操建議是在一個分析中對同一個物理寄存器始終使用同一種位寬訪問。如果你主要關注函數(shù)參數(shù)就都用 64 位符號變量如果你主要關注返回值的低 32 位就始終用 32 位讀取?;煊脛e名是很多“莫名其妙”問題的根源。4.2 多寄存器協(xié)同約束單個寄存器符號化只是第一步。真實程序里一個函數(shù)的多個參數(shù)往往不是獨立的它們會共同參與同一個判斷條件。我們的mystery例子就是這樣——a和b必須同時滿足兩個等式。當多個參數(shù)都是符號變量時angr 的路徑約束會自動把它們的關聯(lián)關系帶上。你不需要手動寫a b 11這樣的額外約束因為模擬執(zhí)行到cmp指令時angr 已經(jīng)自動把a b 11這條約束加進當前路徑的求解器了。你要做的只是確保每個參數(shù)的符號變量在創(chuàng)建后沒有重復使用。這里有一個很容易踩的坑符號變量的“名字復用”。很多人會這樣寫param1 claripy.BVS(p, 64) param2 claripy.BVS(p, 64) state.regs.rdi param1 state.regs.rsi param2兩個符號變量名字都叫p但它們是兩個完全不同的 AST 對象。angr 不會因為它們名字相同就認為它們相等。如果你誤以為同名的符號變量一定相等最終求解結果會讓你困惑很久。正確的做法是給每個參數(shù)不同的名字并且全程復用同一個對象。4.3 與內(nèi)存符號化配合使用說完了寄存器再說說寄存器和內(nèi)存的連接。函數(shù)經(jīng)常先把參數(shù)寄存器存到棧上之后再從棧里取出來判斷代碼經(jīng)過編譯優(yōu)化后尤其常見。angr 在執(zhí)行mov [rbp-0x4], rdi時會自動把符號表達式寫入對應的內(nèi)存位置之后從該地址讀出的仍然是同一個符號表達式。這是符號執(zhí)行非常優(yōu)雅的一點符號值在寄存器和內(nèi)存之間搬運時不會丟失其“身份”。更進一步你完全可以混合使用寄存器符號化和內(nèi)存符號化。比如你想模擬一個結構體第一個字段由寄存器傳入的某個值經(jīng)過計算得到第二個字段是固定的內(nèi)存值你就可以stack_var state.stack_load(8, claripy.BVS(stack_data, 64))這里stack_load會從當前棧指針偏移 8 的位置讀入符號值并把這個地址標記為已初始化。這樣內(nèi)存和寄存器同時帶著符號執(zhí)行起來就和真實程序一樣自然。4.4 還原入口參數(shù)約束的完整思路有了前面的基礎我分享一個真正在做逆向分析時非常有用的思路還原某個關鍵函數(shù)的入口參數(shù)約束。假設你有一個加密函數(shù)輸入是rdi指向的緩沖區(qū)、rsi是長度、rdx是密鑰你手里只有密文和程序想知道密鑰是什么。你可以這樣做找到加密函數(shù)入口地址用call_state創(chuàng)建狀態(tài)把rdi設成一個指向符號緩沖區(qū)的指針rsi設成具體的密文長度rdx設成符號密鑰再準備一塊符號化的緩沖區(qū)往里面填入密文字節(jié)作為約束讓 angr 從函數(shù)入口執(zhí)行到函數(shù)返回在返回后的狀態(tài)里檢查緩沖區(qū)內(nèi)容是否等于明文把這個等號作為額外約束加入求解器用solver.eval(rdx)求出密鑰。這套方法聽起來很神奇但本質(zhì)上就是“寄存器符號化 內(nèi)存符號化 路徑約束 求解”的組合拳。你在自己的分析任務里也可以把“哪些輸入是已知的”設成具體值把“哪些輸入是未知的”設成符號變量剩下的事情交給 angr 自動完成。5. 常見問題與避坑速查5.1 為什么符號化寄存器后程序直接崩了/狀態(tài)不可行符號化寄存器之后最常見的報錯是unsat也就是狀態(tài)不可行。原因不外乎三類。第一類是初始約束就矛盾。比如你從一個blank_state開始前面已經(jīng)手動加了state.regs.rax 10后面又符號化覆蓋了rax之前的約束還掛在求解器里新的符號對象和舊約束之間就會出現(xiàn)矛盾。遇到這種情況清理掉不需要的約束或者干脆新建狀態(tài)。第二類是參數(shù)位寬不匹配。你給一個 64 位寄存器賦了 32 位符號變量angr 自動擴展成零擴展而程序指令卻按符號擴展或者按有符號比較來用導致求解得到的值完全對不上。解決辦法是統(tǒng)一位寬。第三類是call_state調(diào)用方式不對。call_state(addr, arg1, arg2)這種寫法必須讓 arg 數(shù)量、類型和函數(shù)真實簽名匹配。如果函數(shù)實際有三個參數(shù)你只給了兩個angr 會拿未初始化的寄存器去湊這時候求解結果就會神游四方。用objdump看一眼函數(shù)開頭的幾條指令數(shù)一下到底用了哪些參數(shù)寄存器再回頭檢查調(diào)用。5.2 求解結果千奇百怪甚至符號消失了有時候你明明符號化了某個寄存器最后求出來的值卻像是一個固定常量或者多跑幾步就不見了。這通常不是 angr 的鍋而是某條指令把符號值“具體化”了。最常見的元兇是系統(tǒng)調(diào)用和庫函數(shù)調(diào)用。如果你分析的程序調(diào)用了外部函數(shù)而 angr 沒有對應實現(xiàn)它可能返回一個未約束的具體值符號變量就斷了。所以我在例子里一直強調(diào)auto_load_libsFalse把外部庫加載關掉讓不認識的調(diào)用直接返回未約束值而不是嘗試去執(zhí)行庫代碼。另一種情況是state.regs.rax state.solver.BVS(...)之后又被某條mov指令覆蓋了。比如程序開頭就有一條xor eax, eax你的符號變量在第一條指令就被清零了。排查這類問題時最有效的工具是打印 ASTprint(state.regs.rax) print(state.regs.rax.args)看輸出結果里你的符號變量名字是否還保留著。如果 AST 里已經(jīng)是一個常量說明在某一步符號被覆蓋了如果 AST 里出現(xiàn)了Extract、ZeroExt等節(jié)點說明有隱式位擴展。很多時候問題一眼就能看出來。5.3 求解器跑得很慢怎么優(yōu)化符號求解的耗時是另一個大問題。我的經(jīng)驗是約束越多、符號變量越多、位寬越大求解就越慢。尤其當程序里循環(huán)次數(shù)多路徑約束會指數(shù)級累積一個很小的函數(shù)也可能讓 Z3 卡上幾十分鐘。幾個實用優(yōu)化手段盡量減少符號變量的數(shù)量。能具體化的輸入就具體化別偷懶全設成符號縮小寄存器位寬。比如int類型的參數(shù)用 32 位符號變量就行非要塞 64 位約束空間大一圈求解成本也上去用explore的avoid參數(shù)砍掉不關心的分支路徑越少狀態(tài)越少整體求解資源消耗就越低對單個狀態(tài)的求解操作可以加超時控制。angr 的 solver 支持timeout參數(shù)比如eval(expr, timeout10000)超時返回一個已知解或拋異常至少不會讓腳本無限卡死。5.4 我的寄存器值為什么對不上最后一種常見困惑是“我用 angr 解出來的值放到真實程序里跑結果不對”。我把它列成速查表現(xiàn)象可能原因排查方向求解出的值和預期差很大有符號/無符號不匹配檢查代碼里的條件跳轉(zhuǎn)是jg還是ja目標分支找到了但參數(shù)解少得離譜函數(shù)入口地址找錯了用nm或反匯編確認入口是函數(shù)頭不是中間指令多個解互相沖突符號變量名或?qū)ο笾貜蜋z查是否復用了同一個 BVS 對象解在多次運行中不穩(wěn)定求解器選了不同可行解不用糾結用min/max或追加約束縮小范圍寄存器值總是在中途歸零某條指令覆蓋了寄存器打印相關地址的反匯編逐條檢查這套表是我在實際分析中一點點攢下來的基本上覆蓋了大部分新手會踩的坑。真正遇到詭異問題時先別懷疑 angr先懷疑自己的地址和約束。最后再分享一個小技巧我個人在實際操作中的一個體會是做寄存器符號化分析建議先別急著直接上完整的大二進制而是自己動手寫一個帶三四個嵌套分支的小程序編譯后用這個流程反復練。小程序的每個地址、每個分支都是你自己設計的遇到問題你能立刻判斷是 angr 的鍋還是自己思路的鍋。等小例子跑順了再拿 CTF 題或者真實逆向樣本去試會順手非常多。另外調(diào)試時一定要多習慣看 AST。很多人把state.regs.rax當成普通 Python 值打印一下就是一個對象地址于是放棄。實際上print(state.regs.rax)會輸出一棵清晰可讀的表達式樹比如(x 5)、(Extract(31, 0, x))。學會讀這棵樹比看任何日志都管用。寄存器符號化這個主題入門看教程深入靠調(diào) AST動手實操幾次就能找到感覺。