行的關(guān)鍵技巧)
1. 問題起源為什么單獨把“malloc地址單元符號化”拎出來講寫這一篇純屬被坑出來的。前面幾篇筆記里我一直在處理“標(biāo)準輸入符號化”“argv符號化”這類常規(guī)操作當(dāng)時覺得 angr 已經(jīng)很順手了直到遇到一個程序邏輯看起來非常簡單就是讀入一段數(shù)據(jù)經(jīng)過一個校驗函數(shù)對了就打印 flag。結(jié)果 angr 跑下來路徑倒是探索了一堆但求解器死活給不出一個合法的輸入。最后排查了半天問題就出在 malloc 分配的地址內(nèi)容沒有被符號化上。這里先解釋一下背景。符號執(zhí)行的本質(zhì)是把輸入變成符號變量讓程序帶著符號跑碰到分支就把條件收集起來最后交給約束求解器去解。但這里的“輸入”是有范圍的你符號化的是 stdin、argv 還是某個全局緩沖區(qū)angr 只會把明確標(biāo)成 BVSBitVectorSymbolic的那部分內(nèi)存當(dāng)成“可變”的其余內(nèi)存內(nèi)容 angr 會按具體值處理。malloc 出來的堆區(qū)怎么處理就很微妙了。它不像棧上聲明的數(shù)組有明確的地址和大小malloc 返回的地址在符號執(zhí)行里是動態(tài)生成的angr 默認不知道你這個地址指向的內(nèi)存區(qū)域代表什么含義更不會主動給這塊內(nèi)存灌入符號變量。結(jié)果就是程序從堆區(qū)讀數(shù)據(jù)、做比較angr 真以為堆里那些字節(jié)是“固定值”于是產(chǎn)生了大量不可能滿足的條件分支。這也就引出了本篇筆記要講的方案如何讓 malloc 分配出來的那塊地址空間其內(nèi)容也成為符號變量從而讓符號執(zhí)行真正覆蓋到程序的核心校驗邏輯。這篇筆記適合兩類人看。一類是剛接觸 angr、只跑通過幾道入門題準備挑戰(zhàn)真實程序的人malloc 符號化是繞不過去的一關(guān)。另一類是已經(jīng)會用 angr 但經(jīng)常遇到“求解無解”“分支全走死”這類問題、排查無頭緒的人。本篇會從原理講到實操最后給出排查技巧核心是一個可復(fù)現(xiàn)的 Demo萬金油思路。2. 能力鋪墊angr 符號執(zhí)行里“內(nèi)存狀態(tài)”的本質(zhì)2.1 從符號變量到約束求解angr 到底在做什么angr 跑一個程序時維護的是一個“符號狀態(tài)”。這個狀態(tài)可以理解成一張大表記錄了當(dāng)前執(zhí)行到的指令地址、寄存器的值、內(nèi)存中每個地址的內(nèi)容。這些“值”有兩種形態(tài)一種是確定的具體數(shù)值比如0x401000另一種是符號變量比如一個 32 位的BVS(input_0, 32)它不是一個固定值而是一個“待定值”。angr 在模擬執(zhí)行過程中遇到分支指令比如cmp; jz時會同時探索兩個方向每條路徑上都會記錄一個路徑條件。比如某條路徑可能記錄了input_0 0x41另一條路徑可能記錄了input_0 0x41。到最后你想讓某一條路徑走到 “success” 分支就把這條路徑上所有的路徑條件收集出來連同你自己手動添加的其他約束一起交給底層求解器z3去解。z3 會返回一個具體的數(shù)值使得這些條件全部成立。這個數(shù)值就是讓程序走進目標(biāo)分支的輸入。這個模型看似簡單但注意一個關(guān)鍵點約束求解器只能基于符號變量去求解。如果一個值不是符號變量而是一個具體常量那 angr 是不可能“反過來算”出一個輸入去改變它的。說得夸張一點如果你壓根沒把一個內(nèi)存位置標(biāo)記成符號那 angr 眼里它就永遠是某個固定值哪怕程序邏輯上它初始依賴 stdin。所以 malloc 地址單元符號化本質(zhì)上就是在回答一個問題堆上這塊內(nèi)存的“值”能不能隨輸入變化如果能angr 才有機會通過路徑條件反推出輸入如果不能那 angr 就只能看見一個死板的具體值路徑探索也戛然而止。2.2 malloc 在符號執(zhí)行里是“黑盒”問題就出在這真實程序里 malloc 可不是拿來看的。常見模式是程序從標(biāo)準輸入讀固定字節(jié)數(shù)存到 malloc 得到的緩沖區(qū)里然后對這個緩沖區(qū)做字節(jié)變換、查表、比較。比如下面這類簡化邏輯char *buf malloc(10); read(0, buf, 10); if (buf[0] f buf[1] l buf[2] a buf[3] g) { puts(correct); }如果是在真實系統(tǒng)上跑read會從 stdin 往 buf 指向的地址填充數(shù)據(jù)。但在 angr 里問題出現(xiàn)了angr 默認的read系統(tǒng)調(diào)用如果遇到未知的文件描述符通常是提前處理后返回確定值或觸發(fā)異常具體行為取決于 angr 對read的模擬方式。即使你通過SimFile或者 hook 方式把 stdin 提供了也存在一個更深層的坑angr 的read模擬是寫在系統(tǒng)調(diào)用層面的它的“目標(biāo)地址”是 malloc 返回的那個地址。而 malloc 在 angr 的 SimHeap 里大多被 hook 成返回某個地址但這個地址指向的內(nèi)存并沒有被初始化為符號。于是你在狀態(tài)里做了state.solver.BVS(stdin, 10*8)以為萬事大吉實際上 angr 執(zhí)行read時確實把符號變量“拷貝”到了 malloc 地址上但前提是你正確配置了 stdin 的文件描述符并且 angr 把這次 read 識別為讀符號數(shù)據(jù)。如果程序不是走read而是先從 stdin 讀到一個臨時棧緩沖再手動memcpy到堆區(qū)那 angr 在 memcpy 時是逐字節(jié)復(fù)制符號變量的這種情況反而沒事。真正出問題的場景是程序校驗邏輯直接作用在 malloc 內(nèi)容上但 malloc 的內(nèi)容來源不是 angr 認識的符號通道而是來自程序內(nèi)部的某種初始化邏輯。舉個典型例子程序從 stdin 讀入一串十六進制字符串strtol轉(zhuǎn)換成整數(shù)再當(dāng)作種子去初始化一個偽隨機序列最后用這個序列去校驗堆區(qū)的某個數(shù)據(jù)。strtol、srand、rand這些函數(shù)在 angr 里的模擬如果不做額外處理會產(chǎn)生具體數(shù)值所以堆區(qū)數(shù)據(jù)就不可能被符號化。這種情況下你必須跳過“生成鏈條”直接在 malloc 地址單元上做符號化——人為聲明“這塊內(nèi)存的內(nèi)容是符號變量”。2.3 為什么“符號化地址”不等于“符號化內(nèi)容”這里有必要區(qū)分兩個概念。一個是把 malloc 返回的指針值符號化一個是把 malloc 指向的內(nèi)存內(nèi)容符號化。很多入門教程講“malloc 符號化”時說的是前者讓 malloc 的返回值成為一個符號變量這樣能讓程序走不同的堆分配分支比如檢查 malloc 是否失敗。字符串比較常見的一個坑是在分析帶堆噴的程序時需要讓 malloc 返回不同的地址來探索堆布局分支。但本文討論的“malloc 地址單元符號化”指的是后者malloc 返回的地址是確定的或可計算的但該地址上的內(nèi)存單元內(nèi)容是符號化的。打個比方你和朋友約好在一家餐廳見面地址是固定的但你不知道朋友在那家餐廳坐哪一桌內(nèi)容你想通過一定規(guī)則反推出來。符號化內(nèi)容就是給“坐哪一桌”這個變量建立數(shù)學(xué)模型讓求解器去算。兩者在 angr 里的具體操作位置也不同符號化返回值需要 hook malloc 本身符號化地址內(nèi)容需要在 malloc 之后拿到地址再用 store 操作往這個地址寫入 BVS。理解了這一點后面看別人代碼就不容易暈。3. 方案選型四種“讓 malloc 區(qū)域符號化”的方式對比3.1 方式一hook malloc拿到返回值后再 store BVS最直接的做法通過project.hook_symbol(malloc, hook_func)劫持 malloc 符號在 hook 函數(shù)里先返回一塊地址通常用state.heap相關(guān)接口或直接返回一個固定地址然后立刻在這個地址上 store 一個 BVS。這樣程序后續(xù)對這塊地址的讀取就讀到了符號變量。import angr import claripy def malloc_hook(state): # 手動指定一塊地址避開已有內(nèi)存區(qū)域 addr 0x5000000 # 只是一個示例地址實際要選堆區(qū) size 0x40 # 讓 malloc 返回這個地址 state.regs.rax addr # 在這塊區(qū)域?qū)懭?64 字節(jié)的符號值 sym claripy.BVS(heap_data, 8 * size) state.memory.store(addr, sym)這種方式的好處是直觀你能控制全流程。壞處也很明顯一個程序里不止一處調(diào)用 malloc如果你全都 hook 到一個統(tǒng)一處理所有 malloc 區(qū)域內(nèi)容都一樣同一個 BVS邏輯就亂了。所以這種方式更適合目標(biāo)明確、malloc 調(diào)用點不多的情況一般實驗里也就一兩個關(guān)鍵 malloc。3.2 方式二在輸入符號化階段同步填充堆區(qū)域不少初學(xué)者看到“malloc 地址單元符號化”第一反應(yīng)是我先不碰 malloc直接把符號變量寫到那個地址不就行了比如你知道 malloc 返回地址的規(guī)律像 glibc 的 fastbin 在固定偏移就硬編碼一個地址在initial_state里storeBVS。這種方式在很多 CTF 題目里很有效因為題目程序簡單甚至不校驗 malloc 的返回值。不過這種方式有個前提你必須知道 malloc 返回地址到底是多少。angr 里 malloc 的默認 implementation 通常返回一塊固定的模擬堆地址每次運行基本一致。但不同版本的 angrSimHeap 的地址策略不一樣你硬編碼的地址可能會踩到 angr 給?；蛉謪^(qū)域預(yù)留的空間。穩(wěn)妥起見可以在 setup 階段 hook 住 malloc打印返回地址再決定往哪填充。3.3 方式三利用 angr 的 SimHeap 自定義分配器這是“正統(tǒng)”做法。angr 內(nèi)部有SimHeap類體系比如SimHeapBrk、SimHeapLibc。通過自定義一個繼承SimHeap的分配器重寫_allocate方法在分配時自動記錄所有 malloc 返回的地址并在返回前將地址寫入符號變量。這樣程序里所有 malloc 出來的區(qū)域內(nèi)容都是“全新符號”每個 malloc 對應(yīng)一個獨立 BVS互不干擾。class SymHeap(angr.state_plugins.heap.SimHeapLibc): def _allocate(self, size, **kwargs): addr super()._allocate(size, **kwargs) sym claripy.BVS(fheap_{addr:x}, 8 * size) self.state.memory.store(addr, sym) return addr # 使用時 state.heap SymHeap()這種方式約束力最強但復(fù)雜度也高。還有坑過度的自動符號化會讓路徑條件爆炸。每個 malloc 區(qū)域都有一整塊 BVS一旦程序?qū)@塊區(qū)域做逐字節(jié)比較angr 會為每個字節(jié)引入分叉狀態(tài)數(shù)呈指數(shù)級增長。所以這種方式適合研究目的不適合直接對真實大型程序用。3.4 方式四高階玩法——用 concretization 和約束定向符號化前面幾種叫“寬泛符號化”還有更精細的定向符號化不讓整個 malloc 區(qū)域一開始就是 BVS而是讓它先保持具體值等 angr 執(zhí)行到某個比較指令時發(fā)現(xiàn)該分支不可滿足再“回頭”把相關(guān)內(nèi)存地址符號化。angr 確實存在某種程度上“從失敗中學(xué)習(xí)”的機制——如果你在探索時設(shè)置了save_unconstrained常見的是保存未約束狀態(tài)而不是自動回填符號。這里說的“回頭符號化”通常要你手動根據(jù)失敗路徑的特征在特定地址上補充約束。這種方式我已經(jīng)一年沒在實戰(zhàn)中用了因為多數(shù)情況下方式一和方式二夠用。但了解這個概念有助于理解 angr 的局限符號執(zhí)行不是魔法它要在“盡可能多地探索”和“避免狀態(tài)爆炸”之間取舍。手動符號化 malloc 區(qū)域本質(zhì)上就是一種人工引導(dǎo)這種取舍的行為。3.5 選型建議按判定條件選不按喜好選說實話我在自己的實踐里沒用過一種包打天下的方案。我建議按下面這個標(biāo)準來選場景特征推薦方式理由程序 malloc 調(diào)用點少關(guān)鍵區(qū)域只有一處方式一代碼短好控制調(diào)試直觀CTF 題目、程序結(jié)構(gòu)簡單且 malloc 地址穩(wěn)定方式二寫起來最快能跑就行想系統(tǒng)分析某類程序需要讓所有堆區(qū)域都可變方式三自動化程度最高但要防狀態(tài)爆炸求解出現(xiàn) unsat 或路徑走死需要精確定位方式四實際是排查局部符號化靈活但依賴經(jīng)驗判斷本篇下面的實操用方式一做演示因為最能體現(xiàn)“malloc 地址單元符號化”的思路先拿到地址再填充符號。把這一步走通其他方式就是在它的基礎(chǔ)上做變通。4. 實操演示從零跑通“malloc 內(nèi)容符號化”完整流程4.1 準備實驗環(huán)境與模擬程序首先準備好 angr 環(huán)境。我用的版本是 angr 9.2往下的 9.0 和往上的 10.x 在 API 上有細微差別但核心思路一致。安裝就是常規(guī)的pip install angr需要注意的是 angr 依賴的 z3-solver 版本可能跟系統(tǒng)其他包沖突建議建虛擬環(huán)境避免污染系統(tǒng) Python。然后是模擬程序。本文要分析的 Demo 用 C 語言寫成為了簡化后面解釋原理我刻意寫得很“人工”#include stdio.h #include stdlib.h #include string.h int check(char *buf, int len) { if (buf[0] * buf[1] 0x861) { if (buf[2] buf[3] 0xcb) { if (buf[4] ^ buf[5] 0x5c) { return 1; } } } return 0; } int main(int argc, char **argv) { char *heap_buf (char *)malloc(0x20); // 模擬從某處填充數(shù)據(jù)關(guān)鍵是在符號執(zhí)行中這塊內(nèi)容沒有被正常符號化 memcpy(heap_buf, ABCDEF, 6); if (check(heap_buf, 6)) { puts(ok); } else { puts(bad); } return 0; }編譯gcc -o demo demo.c -no-pie -fno-stack-protector。這里關(guān)掉 PIE 不是為了別的只是后面分析時地址固定方便說明問題。真實復(fù)現(xiàn)時你可以保留 PIEangr 也支持。這個 Demo 里check函數(shù)對 heap_buf 的內(nèi)容做了幾組算術(shù)校驗。如果按常規(guī)思路直接跑會看到 angr 走到check之后兩個分支都不可滿足因為內(nèi)存里是固定的ABCDEF算不出滿足條件的解法。這正是我們要解決的。4.2 常規(guī)分析腳本與失敗現(xiàn)象記錄先寫一個最常規(guī)的 angr 腳本看看失敗長什么樣import angr def main(): proj angr.Project(./demo, auto_load_libsFalse) state proj.factory.entry_state() sm proj.factory.simulation_manager(state) sm.explore(find0x4006a4, avoid0x4006ad) # 目標(biāo)是 ok 分支 if sm.found: print(Found!) print(sm.found[0].posix.dumps(0)) else: print(No found) # 看看活躍狀態(tài)情況 print(active:, len(sm.active)) for st in sm.active[:3]: print(st.solver.constraints[-3:]) if __name__ __main__: main()跑一下結(jié)果大概率是No found。這就說明內(nèi)存內(nèi)容確確實實沒有被符號化程序執(zhí)行到比較時就沒有合法路徑了。只用看路徑活躍數(shù)會發(fā)現(xiàn)所有狀態(tài)都是 unsatisfiable在sm.active里檢查state.solver.satisfiable()會返回 False。這里要專門提醒一下在 angr 里一個狀態(tài)“活著”不代表它能繼續(xù)往后執(zhí)行。很多人在sm.explore沒找到結(jié)果時就打印sm.active里的狀態(tài)數(shù)發(fā)現(xiàn)數(shù)量不少就覺得是不是其他 bug。實際上這些 active 狀態(tài)很可能全是 unsat后續(xù)指令執(zhí)行全是死胡同。所以排查時第一件事就是檢查狀態(tài)的可滿足性。4.3 方案落地hook malloc 并符號化返回地址指向的內(nèi)容現(xiàn)在按方式一改造。先 hookmalloc符號讓 malloc 返回一個我們指定的地址并在這個地址上寫入 BVS。angr 的hook_symbol接受一個符號名和 hook 函數(shù)。hook 函數(shù)的輸入是state你可以在里面修改寄存器、內(nèi)存、求解器約束。import angr import claripy def setup_malloc_sym(state): # 選一個地址作為“堆區(qū)”注意避開已知區(qū)域 fake_heap 0x600000 size 0x20 sym_data claripy.BVS(malloc_0, 8 * size) state.memory.store(fake_heap, sym_data) # malloc 的返回結(jié)果放在 rax state.regs.rax fake_heap然后把 hook 掛到符號上。angr 里hook_symbol的第一個參數(shù)是字符串對應(yīng)程序里malloc在動態(tài)符號表中的名字。def main(): proj angr.Project(./demo, auto_load_libsFalse) proj.hook_symbol(malloc, setup_malloc_sym, length0) # length 為 0 表示完全替換寫完這個 hook 之后重新用同樣的 explore 跑就能在found里看到狀態(tài)了。這時候可以 dump 一下標(biāo)準輸入如果你程序里有讀入或者直接查看malloc_0這個符號變量的值found_state sm.found[0] solver found_state.solver solution solver.eval(claripy.BVS(malloc_0, 8 * 6), cast_tobytes) print(solution)如果不出意外你得到的 bytes 就是滿足check條件的“目標(biāo)值”比如bKI\xe5TZ之類。驗證方式很簡單用這個字節(jié)串替換 Demo 里 memcpy 的數(shù)據(jù)重新編譯跑一下發(fā)現(xiàn)打印ok。這一步的關(guān)鍵點在于順序必須先 store BVS 到地址再讓 malloc 返回地址。如果反過來先設(shè)置 rax 再 storestore 的地址還是我們自己指定的理論上沒區(qū)別但如果你 store 的地址依賴 rax 的內(nèi)容那順序就很重要。另外store 的 size 要跟后面讀取的長度匹配只 store 6 字節(jié)也行但為了穩(wěn)妥我會按整個分配大小 store 一整塊 BVS后面讀取哪一段都能命中。4.4 完整腳本與邊界參數(shù)說明下面給一個完整的腳本可以直接替換地址、符號名跑別的程序用import angr import claripy fake_heap_base 0x200000 malloc_size 0x100 def malloc_hook(state): # 可以在這里打印調(diào)用?；蛘叻峙浯笮”阌谡{(diào)試 # state.inspect 相關(guān)用法可以拿到調(diào)用參數(shù)這里略過 addr fake_heap_base sym claripy.BVS(heap_0, 8 * malloc_size) state.memory.store(addr, sym) state.regs.rax addr def main(): proj angr.Project(./demo, auto_load_libsFalse) proj.hook_symbol(malloc, malloc_hook, length0) state proj.factory.entry_state() sm proj.factory.simulation_manager(state) sm.explore(find0x4006a4, avoid0x4006ad) if sm.found: st sm.found[0] # 解析整個堆區(qū)域的具體解 heap_bytes st.solver.eval(claripy.BVS(heap_0, 8 * 6), cast_tobytes) print(Found, heap bytes:, heap_bytes) else: print(No found) for i, st in enumerate(sm.active[:5]): print(factive[{i}] satisfiable:, st.solver.satisfiable()) if __name__ __main__: main()說幾個容易踩的坑。第一fake_heap_base一定要選一個 angr 不會主動使用的地址。前面我用 0x600000對大多數(shù)小型二進制沒問題但如果你程序本身加載地址就在這個范圍就要避開?？梢杂胹tate.memory._get_region或者干脆打印state.regs.rsp、加載基地址后估算。第二malloc_size建議取你實際需要大小的兩倍以上留余量。第三hook_symbol的length參數(shù)如果不傳angr 默認會以符號對應(yīng)的函數(shù)長度做替換容易出問題hook 我們自己的純 Python 函數(shù)時length0更安全。第四如果你的二進制是靜態(tài)鏈接的可能沒有malloc動態(tài)符號hookmalloc會失敗。處理方式是 hook 地址先通過proj.loader.main_object.get_symbol(malloc)拿到地址或者直接對proj.loader的 memory 地圖找到 malloc 所在的 PLT 入口用proj.hook(addr, hook_func)。4.5 設(shè)計點詳解為什么這里要“同時符號化整個 size 塊”很多人在成功跑出一次結(jié)果后會有個疑問為什么我要符號化整個 0x100 字節(jié)而不是只在 hook 到的 malloc size這里是 0x20對應(yīng)的空間上做符號化這有兩個層面的原因。一方面符號化整個保留區(qū)域的成本并不高。angr 的 BVS 在約束求解時只對實際參與比較的字節(jié)產(chǎn)生約束那些沒有被讀取的字節(jié)不會影響求解復(fù)雜度。你把整個區(qū)域標(biāo)成符號相當(dāng)于為后續(xù)可能發(fā)生的越界讀取或者各種偏移訪問留了后路。另一方面真實程序里malloc 后面往往還跟著realloc、memcpy、strlen等各種操作你無法預(yù)測程序會讀取哪一段偏移。動態(tài)規(guī)劃一步到位后續(xù)就不用反復(fù)回頭看。如果擔(dān)心狀態(tài)爆炸可以只符號化實際參與校驗的那幾個字節(jié)。這需要你先摸清程序邏輯指向性更強。操作方式是一樣的把 BVS 長度設(shè)成目標(biāo)字節(jié)數(shù)store 到對應(yīng)偏移即可。自由度在你自己手上。5. 實操過程與核心環(huán)節(jié)實現(xiàn)從一個更真實的例子看符號化代碼設(shè)計5.1 新案例程序接收字符串后存堆、校驗且?guī)аh(huán)上面 Demo 非常簡單主要是驗證思路?，F(xiàn)在換一個稍微真實一點的例子。假設(shè)程序從 argv[1] 接收字符串長度限制 0x20把它拷貝到 malloc 分配的緩沖區(qū)里隨后在一個循環(huán)中逐字節(jié)累加異或校驗最后比較結(jié)果。直接對 argv 符號化很簡單但問題來了程序把 argv 字符串拷貝到 malloc 區(qū)域后如果 angr 正確識別了 memcpy該區(qū)域的值仍是符號變量。關(guān)鍵難點在于循環(huán)結(jié)構(gòu)的處理。循環(huán)在符號執(zhí)行里容易造成路徑爆炸但如果校驗邏輯是“無分支”的循環(huán)比如只是累加、異或而不根據(jù)內(nèi)存內(nèi)容跳轉(zhuǎn)angr 的執(zhí)行路徑不會分叉只是狀態(tài)會包含大量循環(huán)變量。不要被“循環(huán)”兩個字嚇到angr 并不是盲人騎瞎馬它會管理路徑的。對無分支循環(huán)執(zhí)行次數(shù)就算成百上千次也完全沒問題。真正麻煩的是循環(huán)內(nèi)依賴內(nèi)容的條件跳轉(zhuǎn)。這種情況下malloc 地址單元符號化能幫你把循環(huán)條件變成符號約束而不是把條件里出現(xiàn)的每個具體值都固定死。比如程序里有if (buf[i] a)這樣的判斷angr 在 i 未知時會嘗試所有可能。如果你提前把整個 malloc 區(qū)域符號化了angr 就能正確處理這種分支探索所有可能字符值。實戰(zhàn)里對這類循環(huán)條件一個非常有效的技巧是“約束內(nèi)生符號化”你在 hook 的 malloc 里不光 store BVS還可以主動 store 幾個額外的約束。比如你知道校驗一定要求某個字節(jié)是字母就可以直接加state.solver.add(buf[i] A)減少無用分支。這類約束越早加狀態(tài)精簡越明顯。5.2 結(jié)合“查找目標(biāo)地址”與“避免地址”的工程化腳本實戰(zhàn)中你一旦開始符號化 malloc就不能只關(guān)注找目標(biāo)那一支。很多程序校驗失敗的分支會調(diào)用 exit 或者 abort這些地址如果不寫進avoidangr 會為了探索它們消耗大量資源。我給一個稍微工程化的腳本框架def run_analysis(proj, start_addrNone, find_addrs[], avoid_addrs[]): if start_addr is None: state proj.factory.entry_state() else: state proj.factory.blank_state(addrstart_addr) # 初始化符號化堆 fake_heap_base 0x200000 sym_size 0x200 state.memory.store(fake_heap_base, claripy.BVS(heap_symbolic, 8 * sym_size)) # 探索 sm proj.factory.simulation_manager(state) sm.use_technique(angr.exploration_techniques.DFS()) # 深度優(yōu)先找路徑失敗后快速回溯 sm.explore(findfind_addrs, avoidavoid_addrs) if sm.found: for st in sm.found: # 按需提取 return st return None這個框架把 malloc 符號化的動作和執(zhí)行解耦了你可以在任意起點狀態(tài)調(diào)用。注意我用的是DFS而不是默認的BFS。找 target 時深度優(yōu)先往往更快但如果你希望覆蓋更全面的路徑BFS 更穩(wěn)。實際場景中我會根據(jù)程序復(fù)雜度切換小而精的程序用 DFS大而雜的程序用 BFS。另外blank_state配合start_addr是處理復(fù)雜反調(diào)試、自修改代碼的好姿勢。你可以先手動分析程序邏輯直接跳到某個關(guān)鍵函數(shù)入口把上下文寄存器、棧設(shè)置好后再符號化堆區(qū)開始探索。5.3 參數(shù)計算符號化范圍與約束條件怎么寫更經(jīng)濟這個點我覺得很有必要詳細展開因為很多腳本卡死不是符號化太少而是符號化太多、約束太寬造成的。假設(shè)程序有 10 個 malloc 調(diào)用點每個分配 0x100 字節(jié)。如果你統(tǒng)一 hook對每個 malloc 區(qū)域都寫入一整塊全新的 BVS那 angr 需要同時跟蹤的可能符號變量就是 10 × 0x100 × 8 字節(jié) 12800 個 bit。約束求解器面對這些符號光維護可達性關(guān)系就可能內(nèi)存爆炸。所以我給自己定了三條規(guī)矩只符號化必要地址。如果程序只校驗 malloc 區(qū)域的前 16 字節(jié)那 BVS 長度就設(shè)成 16 字節(jié)甚至更小別貪多。同一時間只讓少數(shù)幾個 malloc 區(qū)域“活著”。一個技巧是判斷 malloc 的調(diào)用點只有當(dāng)它是關(guān)鍵位置比如某個函數(shù)里的 malloc才寫入符號其他 malloc 返回具體地址內(nèi)容不管。盡早加約束。如果你從逆向分析或動態(tài)調(diào)試已經(jīng)知道輸入字節(jié)屬于可打印字符那就提前 add 約束不要等求解器自己去探索 256 種可能。用生活例子來說你讓一個快遞員送包裹給某個神秘收件人只給了他“地址在某某小區(qū)”這個信息他要跑遍整個小區(qū)你得讓他跑多久但如果你提前說“收件人姓王”他直接去查門牌系統(tǒng)效率完全不一樣。符號執(zhí)行里的約束約等于這個“提前信息”。判斷調(diào)用點的姿勢在 hook 函數(shù)里用state.inspect的 call 事件拿到調(diào)用返回地址。注意 hook 時length0會完全替換函數(shù)你可能拿不到原始調(diào)用參數(shù)更好的辦法是用state.inspect在函數(shù)入口處監(jiān)聽寄存器參數(shù)def malloc_hook(state): size_arg state.regs.rdi # System V 下第一個參數(shù)在 rdi # 你要分析的那個關(guān)鍵 malloc 很可能 size 是一個特定常量或范圍 if state.solver.eval(size_arg) 0x100: # 粗略篩一下 addr fake_heap_base sym claripy.BVS(key_heap, 8 * state.solver.eval(size_arg)) state.memory.store(addr, sym) state.regs.rax addr else: state.regs.rax fake_heap_base 0x1000 # 其他 malloc 返回另一個地址不過要注意state.solver.eval(size_arg)如果你不去約束它它可能返回任意值。這個例子只是演示思路真正使用時建議先約束size_arg或者直接用state.solver.min、max判斷范圍。更穩(wěn)妥的做法是不依賴 size直接在調(diào)用點返回地址上做判斷這需要你從反匯編結(jié)果里查到 malloc 的調(diào)用方地址。5.4 現(xiàn)場問題一符號化之后求解結(jié)果不對如何定位按上面的腳本執(zhí)行你可能成功 found 了但拿到的字節(jié)串塞回程序卻不對。這種問題一般有三個來源。第一個來源是約束沒加全。有些校驗邏輯不只有一層比較可能是算術(shù)運算后再比較或者有可能通過查表實現(xiàn)。如果你的約束只覆蓋了表層判斷求解器給出的解可能只滿足表層條件內(nèi)層條件被繞過了。這時候需要結(jié)合反匯編確認整個校驗鏈有多少步。第二個來源是符號化地址選錯了。你符號化的是 malloc 返回的地址但程序后面可能把數(shù)據(jù)拷貝到了另一塊地址或者 malloc 返回的地址被某個指針變量改動過。用 angr 的state.memory.load檢查那個地址的內(nèi)容就能發(fā)現(xiàn)是不是符號變量。很多次我發(fā)現(xiàn)符號變量在但程序讀取的來源卻是一個別的地方因為程序里有個中間變量保存了 malloc 結(jié)果后來又改了這個變量。第三個來源是內(nèi)存模型默認的字節(jié)序問題。x86 用的是小端序當(dāng)你把整個 8 字節(jié)的 BVS store 到地址上后續(xù)如果程序按字節(jié)讀取沒問題但如果程序把這塊區(qū)域當(dāng)成一個 uint64 來比較小端序會把 BVS 的低字節(jié)放在低地址與常規(guī)直覺相反。解決方式是統(tǒng)一用endnessstate.arch.memory_endness或者顯式使用state.memory.store(addr, sym, endnessIend_BE)具體按你程序里的讀取方式調(diào)整。5.5 現(xiàn)場問題二符號化后路徑爆炸卡在循環(huán)出不來另一個高頻問題是符號化成功后 angr 確實“活”了但它非常興奮把每條路徑都探索了個遍尤其是程序中存在循環(huán)結(jié)構(gòu)時幾秒鐘就爆出幾百萬狀態(tài)。這種情況下不要慌第一步先看是不是循環(huán)條件依賴了符號內(nèi)容。比如for (i 0; buf[i] ! 0; i)一旦 buf 被符號化這個循環(huán)條件就變成了一個探索點buf[i] 是否等于 0angr 會同時探索“等于 0”和“不等于 0”的分支然后繼續(xù)執(zhí)行更深層的邏輯。對策有三個方向。第一手動約束 buf[i] 的取值范圍比如可打印字符減少窮舉空間。第二限制路徑深度或使用veritesting技術(shù)它能把部分循環(huán)條件合并。angr 的Veritestingexploration technique 是對付這類情況的常用工具雖然原理復(fù)雜但調(diào)用很簡單sm proj.factory.simulation_manager(state) sm.use_technique(angr.exploration_techniques.Veritesting()) sm.explore(find..., avoid...)第三直接對循環(huán)結(jié)構(gòu)下手用angr的SimProcedure替換循環(huán)函數(shù)。如果你的循環(huán)可以抽象成一個簡單的數(shù)學(xué)函數(shù)直接 hook 循環(huán)入口計算完結(jié)果后放在指定內(nèi)存里能大幅加快分析。不過這需要你對目標(biāo)代碼結(jié)構(gòu)有足夠理解屬于高級玩法。我自己實戰(zhàn)中70% 的情況用約束DFS 能解決20% 情況用 veritesting 解決剩下 10% 只能換思路放棄完全符號化改用“混合符號執(zhí)行”把部分已知的具體值噴到堆區(qū)只符號化真正未知的部分。6. 常見問題排查與避坑指南6.1 現(xiàn)象對照看到這些情況優(yōu)先懷疑 malloc 符號化問題現(xiàn)象可能原因排查動作sm.active全是 unsat沒有 found符號化范圍沒覆蓋關(guān)鍵內(nèi)存或約束過強打印活躍狀態(tài)約束檢查是否包含 address 對應(yīng)的內(nèi)存內(nèi)容explore 卡死內(nèi)存暴漲符號化范圍過大循環(huán)條件生成海量狀態(tài)收縮符號化大小添加取值范圍約束found 了但塞回程序不對約束缺失或符號化地址/字節(jié)序問題反匯編比較鏈逐步驗證malloc 返回值不對hook 方式錯誤或 Return address 被覆蓋用state.inspect監(jiān)聽返回值同步檢查寄存器符號化后無法執(zhí)行到malloc后續(xù)可能 malloc 內(nèi)部還有分支或間接跳轉(zhuǎn)檢查 hook 是否完全替換了原實現(xiàn)length0確認這個表既是我自己排查的索引也是寫給后面看筆記的自己的速查卡。不少問題看起來五花八門根源指向同一個方向符號變量的位置、范圍、約束與真實程序邏輯不對齊。6.2 遇到 unsat 時如何拆解不少同學(xué)看到unsat就以為 angr 壞了。這里有個很重要的調(diào)試方法把活躍狀態(tài)的約束打印出來逐個檢查。for i, st in enumerate(sm.active[:5]): print(State, i, satisfiable:, st.solver.satisfiable()) if not st.solver.satisfiable(): for idx, c in enumerate(st.solver.constraints): print( Constraint, idx, :, c)逐個看約束列表你會發(fā)現(xiàn)很多 unsat 是因為你手動 add 了范圍約束比如buf[0] A和buf[0] Z但程序本身的比較條件要求buf[0] -這就產(chǎn)生矛盾。如果是這種情況說明你的全局約束跟程序固有邏輯沖突要放寬手動約束。另一個常見原因是符號區(qū)域里有多個不同 BVS程序把它們做了乘法或除法操作導(dǎo)致某些非線性的算術(shù)關(guān)系不可滿足。z3 對非線性算術(shù)乘法、除法的支持并不好遇到就可能直接拋出 unsat 或返回 unknown。這種情況的解法是盡量在源頭把符號變量拆分避免一次符號化一整塊后讓程序做整體乘法校驗。6.3 hook malloc 時被遞歸調(diào)用或被靜態(tài)鏈接坑hook 符號碰到“遞歸”問題的時候不多但碰到一次就很折磨。如果你的 hook 函數(shù)內(nèi)部又調(diào)用了state.memory.store而某個后續(xù)指令再次調(diào)用 malloc你沒有在 hook 里做區(qū)分處理就會導(dǎo)致內(nèi)存被反復(fù)覆蓋。比如程序在一個循環(huán)里 malloc 三次每次 malloc 都返回同一個 fake_heap_base那第二次 malloc 會把第一次符號化區(qū)域沖掉。解決方法是維護一個分配計數(shù)每次 store 一個不同地址。靜態(tài)鏈接的情況下hook_symbol(malloc)往往靜默失效。我排查這類問題時就用proj.loader.main_object.symbols看有沒有 malloc 符號。沒有就改用 hook 地址方式從 IDA 或 Ghidra 里找到 malloc 函數(shù)的起始地址通常在 .text 段里直接proj.hook(addr, my_malloc_hook)。要注意地址在 PIE 開啟時是相對偏移angr 內(nèi)部處理加載基址時會換算你只要確認地址與 IDA 里顯示的靜態(tài)地址一致就行。6.4 關(guān)于 angr 版本差異的提醒我一直強調(diào)這一點因為不同版本的 angr API 變化太大。老版本 7.x 和現(xiàn)在 9.x/10.x在sim_manager、hook_symbol、BVS的位置上都有改動。我筆記里的代碼基于 9.2如果你用的是其他版本跑不通時先看 API 變化其次才懷疑分析思路。尤其是 10.x 中SimState的插件體系和state.memory.store的默認參數(shù)有調(diào)整BVS 包導(dǎo)入也從claripy.BVS遷移到state.solver.BVS這類方式。版本變了但“malloc 地址單元符號化”的思想不變確定地址、寫入符號、約束求解。7. 一點個人經(jīng)驗收尾我在這篇筆記里寫的方法說白了就是一套“給 angr 補內(nèi)存上下文”的思路。malloc 地址單元符號化只是這套思路里最常見的一種落地形式。實際分析中很多東西都能人為符號化棧上的未初始化變量、文件讀入的緩沖區(qū)、甚至全局對象內(nèi)部的某個字段。你只要記住一個原則凡是你希望求解器能“推算”出來的值就必須讓它成為一個符號變量并且最好提前加上已知約束。這樣想后面遇到各種奇奇怪怪的程序思路就不會亂。最后給一個新手的實用建議如果你剛開始學(xué) angr不要一上來就研究各種高深技巧。先把我這篇筆記里的 Demo 完整跑通然后試著改幾個參數(shù)比如改 malloc 返回地址、改符號化大小、加一個取值范圍約束看求解結(jié)果怎么變。等你親手撞過一次 unsat、親手把約束從矛盾里解放出來你對符號執(zhí)行的直覺會上一個臺階。這個領(lǐng)域沒有捷徑但每一次“哇原來是這里”的瞬間都會讓你離真正的約定求解玩家更近一步。 malloc地址單元符號化：angr符號執(zhí)行的關(guān)鍵技巧
1. 問題起源為什么單獨把“malloc地址單元符號化”拎出來講寫這一篇純屬被坑出來的。前面幾篇筆記里我一直在處理“標(biāo)準輸入符號化”“argv符號化”這類常規(guī)操作當(dāng)時覺得 angr 已經(jīng)很順手了直到遇到一個程序邏輯看起來非常簡單就是讀入一段數(shù)據(jù)經(jīng)過一個校驗函數(shù)對了就打印 flag。結(jié)果 angr 跑下來路徑倒是探索了一堆但求解器死活給不出一個合法的輸入。最后排查了半天問題就出在 malloc 分配的地址內(nèi)容沒有被符號化上。這里先解釋一下背景。符號執(zhí)行的本質(zhì)是把輸入變成符號變量讓程序帶著符號跑碰到分支就把條件收集起來最后交給約束求解器去解。但這里的“輸入”是有范圍的你符號化的是 stdin、argv 還是某個全局緩沖區(qū)angr 只會把明確標(biāo)成 BVSBitVectorSymbolic的那部分內(nèi)存當(dāng)成“可變”的其余內(nèi)存內(nèi)容 angr 會按具體值處理。malloc 出來的堆區(qū)怎么處理就很微妙了。它不像棧上聲明的數(shù)組有明確的地址和大小malloc 返回的地址在符號執(zhí)行里是動態(tài)生成的angr 默認不知道你這個地址指向的內(nèi)存區(qū)域代表什么含義更不會主動給這塊內(nèi)存灌入符號變量。結(jié)果就是程序從堆區(qū)讀數(shù)據(jù)、做比較angr 真以為堆里那些字節(jié)是“固定值”于是產(chǎn)生了大量不可能滿足的條件分支。這也就引出了本篇筆記要講的方案如何讓 malloc 分配出來的那塊地址空間其內(nèi)容也成為符號變量從而讓符號執(zhí)行真正覆蓋到程序的核心校驗邏輯。這篇筆記適合兩類人看。一類是剛接觸 angr、只跑通過幾道入門題準備挑戰(zhàn)真實程序的人malloc 符號化是繞不過去的一關(guān)。另一類是已經(jīng)會用 angr 但經(jīng)常遇到“求解無解”“分支全走死”這類問題、排查無頭緒的人。本篇會從原理講到實操最后給出排查技巧核心是一個可復(fù)現(xiàn)的 Demo萬金油思路。2. 能力鋪墊angr 符號執(zhí)行里“內(nèi)存狀態(tài)”的本質(zhì)2.1 從符號變量到約束求解angr 到底在做什么angr 跑一個程序時維護的是一個“符號狀態(tài)”。這個狀態(tài)可以理解成一張大表記錄了當(dāng)前執(zhí)行到的指令地址、寄存器的值、內(nèi)存中每個地址的內(nèi)容。這些“值”有兩種形態(tài)一種是確定的具體數(shù)值比如0x401000另一種是符號變量比如一個 32 位的BVS(input_0, 32)它不是一個固定值而是一個“待定值”。angr 在模擬執(zhí)行過程中遇到分支指令比如cmp; jz時會同時探索兩個方向每條路徑上都會記錄一個路徑條件。比如某條路徑可能記錄了input_0 0x41另一條路徑可能記錄了input_0 0x41。到最后你想讓某一條路徑走到 “success” 分支就把這條路徑上所有的路徑條件收集出來連同你自己手動添加的其他約束一起交給底層求解器z3去解。z3 會返回一個具體的數(shù)值使得這些條件全部成立。這個數(shù)值就是讓程序走進目標(biāo)分支的輸入。這個模型看似簡單但注意一個關(guān)鍵點約束求解器只能基于符號變量去求解。如果一個值不是符號變量而是一個具體常量那 angr 是不可能“反過來算”出一個輸入去改變它的。說得夸張一點如果你壓根沒把一個內(nèi)存位置標(biāo)記成符號那 angr 眼里它就永遠是某個固定值哪怕程序邏輯上它初始依賴 stdin。所以 malloc 地址單元符號化本質(zhì)上就是在回答一個問題堆上這塊內(nèi)存的“值”能不能隨輸入變化如果能angr 才有機會通過路徑條件反推出輸入如果不能那 angr 就只能看見一個死板的具體值路徑探索也戛然而止。2.2 malloc 在符號執(zhí)行里是“黑盒”問題就出在這真實程序里 malloc 可不是拿來看的。常見模式是程序從標(biāo)準輸入讀固定字節(jié)數(shù)存到 malloc 得到的緩沖區(qū)里然后對這個緩沖區(qū)做字節(jié)變換、查表、比較。比如下面這類簡化邏輯char *buf malloc(10); read(0, buf, 10); if (buf[0] f buf[1] l buf[2] a buf[3] g) { puts(correct); }如果是在真實系統(tǒng)上跑read會從 stdin 往 buf 指向的地址填充數(shù)據(jù)。但在 angr 里問題出現(xiàn)了angr 默認的read系統(tǒng)調(diào)用如果遇到未知的文件描述符通常是提前處理后返回確定值或觸發(fā)異常具體行為取決于 angr 對read的模擬方式。即使你通過SimFile或者 hook 方式把 stdin 提供了也存在一個更深層的坑angr 的read模擬是寫在系統(tǒng)調(diào)用層面的它的“目標(biāo)地址”是 malloc 返回的那個地址。而 malloc 在 angr 的 SimHeap 里大多被 hook 成返回某個地址但這個地址指向的內(nèi)存并沒有被初始化為符號。于是你在狀態(tài)里做了state.solver.BVS(stdin, 10*8)以為萬事大吉實際上 angr 執(zhí)行read時確實把符號變量“拷貝”到了 malloc 地址上但前提是你正確配置了 stdin 的文件描述符并且 angr 把這次 read 識別為讀符號數(shù)據(jù)。如果程序不是走read而是先從 stdin 讀到一個臨時棧緩沖再手動memcpy到堆區(qū)那 angr 在 memcpy 時是逐字節(jié)復(fù)制符號變量的這種情況反而沒事。真正出問題的場景是程序校驗邏輯直接作用在 malloc 內(nèi)容上但 malloc 的內(nèi)容來源不是 angr 認識的符號通道而是來自程序內(nèi)部的某種初始化邏輯。舉個典型例子程序從 stdin 讀入一串十六進制字符串strtol轉(zhuǎn)換成整數(shù)再當(dāng)作種子去初始化一個偽隨機序列最后用這個序列去校驗堆區(qū)的某個數(shù)據(jù)。strtol、srand、rand這些函數(shù)在 angr 里的模擬如果不做額外處理會產(chǎn)生具體數(shù)值所以堆區(qū)數(shù)據(jù)就不可能被符號化。這種情況下你必須跳過“生成鏈條”直接在 malloc 地址單元上做符號化——人為聲明“這塊內(nèi)存的內(nèi)容是符號變量”。2.3 為什么“符號化地址”不等于“符號化內(nèi)容”這里有必要區(qū)分兩個概念。一個是把 malloc 返回的指針值符號化一個是把 malloc 指向的內(nèi)存內(nèi)容符號化。很多入門教程講“malloc 符號化”時說的是前者讓 malloc 的返回值成為一個符號變量這樣能讓程序走不同的堆分配分支比如檢查 malloc 是否失敗。字符串比較常見的一個坑是在分析帶堆噴的程序時需要讓 malloc 返回不同的地址來探索堆布局分支。但本文討論的“malloc 地址單元符號化”指的是后者malloc 返回的地址是確定的或可計算的但該地址上的內(nèi)存單元內(nèi)容是符號化的。打個比方你和朋友約好在一家餐廳見面地址是固定的但你不知道朋友在那家餐廳坐哪一桌內(nèi)容你想通過一定規(guī)則反推出來。符號化內(nèi)容就是給“坐哪一桌”這個變量建立數(shù)學(xué)模型讓求解器去算。兩者在 angr 里的具體操作位置也不同符號化返回值需要 hook malloc 本身符號化地址內(nèi)容需要在 malloc 之后拿到地址再用 store 操作往這個地址寫入 BVS。理解了這一點后面看別人代碼就不容易暈。3. 方案選型四種“讓 malloc 區(qū)域符號化”的方式對比3.1 方式一hook malloc拿到返回值后再 store BVS最直接的做法通過project.hook_symbol(malloc, hook_func)劫持 malloc 符號在 hook 函數(shù)里先返回一塊地址通常用state.heap相關(guān)接口或直接返回一個固定地址然后立刻在這個地址上 store 一個 BVS。這樣程序后續(xù)對這塊地址的讀取就讀到了符號變量。import angr import claripy def malloc_hook(state): # 手動指定一塊地址避開已有內(nèi)存區(qū)域 addr 0x5000000 # 只是一個示例地址實際要選堆區(qū) size 0x40 # 讓 malloc 返回這個地址 state.regs.rax addr # 在這塊區(qū)域?qū)懭?64 字節(jié)的符號值 sym claripy.BVS(heap_data, 8 * size) state.memory.store(addr, sym)這種方式的好處是直觀你能控制全流程。壞處也很明顯一個程序里不止一處調(diào)用 malloc如果你全都 hook 到一個統(tǒng)一處理所有 malloc 區(qū)域內(nèi)容都一樣同一個 BVS邏輯就亂了。所以這種方式更適合目標(biāo)明確、malloc 調(diào)用點不多的情況一般實驗里也就一兩個關(guān)鍵 malloc。3.2 方式二在輸入符號化階段同步填充堆區(qū)域不少初學(xué)者看到“malloc 地址單元符號化”第一反應(yīng)是我先不碰 malloc直接把符號變量寫到那個地址不就行了比如你知道 malloc 返回地址的規(guī)律像 glibc 的 fastbin 在固定偏移就硬編碼一個地址在initial_state里storeBVS。這種方式在很多 CTF 題目里很有效因為題目程序簡單甚至不校驗 malloc 的返回值。不過這種方式有個前提你必須知道 malloc 返回地址到底是多少。angr 里 malloc 的默認 implementation 通常返回一塊固定的模擬堆地址每次運行基本一致。但不同版本的 angrSimHeap 的地址策略不一樣你硬編碼的地址可能會踩到 angr 給?；蛉謪^(qū)域預(yù)留的空間。穩(wěn)妥起見可以在 setup 階段 hook 住 malloc打印返回地址再決定往哪填充。3.3 方式三利用 angr 的 SimHeap 自定義分配器這是“正統(tǒng)”做法。angr 內(nèi)部有SimHeap類體系比如SimHeapBrk、SimHeapLibc。通過自定義一個繼承SimHeap的分配器重寫_allocate方法在分配時自動記錄所有 malloc 返回的地址并在返回前將地址寫入符號變量。這樣程序里所有 malloc 出來的區(qū)域內(nèi)容都是“全新符號”每個 malloc 對應(yīng)一個獨立 BVS互不干擾。class SymHeap(angr.state_plugins.heap.SimHeapLibc): def _allocate(self, size, **kwargs): addr super()._allocate(size, **kwargs) sym claripy.BVS(fheap_{addr:x}, 8 * size) self.state.memory.store(addr, sym) return addr # 使用時 state.heap SymHeap()這種方式約束力最強但復(fù)雜度也高。還有坑過度的自動符號化會讓路徑條件爆炸。每個 malloc 區(qū)域都有一整塊 BVS一旦程序?qū)@塊區(qū)域做逐字節(jié)比較angr 會為每個字節(jié)引入分叉狀態(tài)數(shù)呈指數(shù)級增長。所以這種方式適合研究目的不適合直接對真實大型程序用。3.4 方式四高階玩法——用 concretization 和約束定向符號化前面幾種叫“寬泛符號化”還有更精細的定向符號化不讓整個 malloc 區(qū)域一開始就是 BVS而是讓它先保持具體值等 angr 執(zhí)行到某個比較指令時發(fā)現(xiàn)該分支不可滿足再“回頭”把相關(guān)內(nèi)存地址符號化。angr 確實存在某種程度上“從失敗中學(xué)習(xí)”的機制——如果你在探索時設(shè)置了save_unconstrained常見的是保存未約束狀態(tài)而不是自動回填符號。這里說的“回頭符號化”通常要你手動根據(jù)失敗路徑的特征在特定地址上補充約束。這種方式我已經(jīng)一年沒在實戰(zhàn)中用了因為多數(shù)情況下方式一和方式二夠用。但了解這個概念有助于理解 angr 的局限符號執(zhí)行不是魔法它要在“盡可能多地探索”和“避免狀態(tài)爆炸”之間取舍。手動符號化 malloc 區(qū)域本質(zhì)上就是一種人工引導(dǎo)這種取舍的行為。3.5 選型建議按判定條件選不按喜好選說實話我在自己的實踐里沒用過一種包打天下的方案。我建議按下面這個標(biāo)準來選場景特征推薦方式理由程序 malloc 調(diào)用點少關(guān)鍵區(qū)域只有一處方式一代碼短好控制調(diào)試直觀CTF 題目、程序結(jié)構(gòu)簡單且 malloc 地址穩(wěn)定方式二寫起來最快能跑就行想系統(tǒng)分析某類程序需要讓所有堆區(qū)域都可變方式三自動化程度最高但要防狀態(tài)爆炸求解出現(xiàn) unsat 或路徑走死需要精確定位方式四實際是排查局部符號化靈活但依賴經(jīng)驗判斷本篇下面的實操用方式一做演示因為最能體現(xiàn)“malloc 地址單元符號化”的思路先拿到地址再填充符號。把這一步走通其他方式就是在它的基礎(chǔ)上做變通。4. 實操演示從零跑通“malloc 內(nèi)容符號化”完整流程4.1 準備實驗環(huán)境與模擬程序首先準備好 angr 環(huán)境。我用的版本是 angr 9.2往下的 9.0 和往上的 10.x 在 API 上有細微差別但核心思路一致。安裝就是常規(guī)的pip install angr需要注意的是 angr 依賴的 z3-solver 版本可能跟系統(tǒng)其他包沖突建議建虛擬環(huán)境避免污染系統(tǒng) Python。然后是模擬程序。本文要分析的 Demo 用 C 語言寫成為了簡化后面解釋原理我刻意寫得很“人工”#include stdio.h #include stdlib.h #include string.h int check(char *buf, int len) { if (buf[0] * buf[1] 0x861) { if (buf[2] buf[3] 0xcb) { if (buf[4] ^ buf[5] 0x5c) { return 1; } } } return 0; } int main(int argc, char **argv) { char *heap_buf (char *)malloc(0x20); // 模擬從某處填充數(shù)據(jù)關(guān)鍵是在符號執(zhí)行中這塊內(nèi)容沒有被正常符號化 memcpy(heap_buf, ABCDEF, 6); if (check(heap_buf, 6)) { puts(ok); } else { puts(bad); } return 0; }編譯gcc -o demo demo.c -no-pie -fno-stack-protector。這里關(guān)掉 PIE 不是為了別的只是后面分析時地址固定方便說明問題。真實復(fù)現(xiàn)時你可以保留 PIEangr 也支持。這個 Demo 里check函數(shù)對 heap_buf 的內(nèi)容做了幾組算術(shù)校驗。如果按常規(guī)思路直接跑會看到 angr 走到check之后兩個分支都不可滿足因為內(nèi)存里是固定的ABCDEF算不出滿足條件的解法。這正是我們要解決的。4.2 常規(guī)分析腳本與失敗現(xiàn)象記錄先寫一個最常規(guī)的 angr 腳本看看失敗長什么樣import angr def main(): proj angr.Project(./demo, auto_load_libsFalse) state proj.factory.entry_state() sm proj.factory.simulation_manager(state) sm.explore(find0x4006a4, avoid0x4006ad) # 目標(biāo)是 ok 分支 if sm.found: print(Found!) print(sm.found[0].posix.dumps(0)) else: print(No found) # 看看活躍狀態(tài)情況 print(active:, len(sm.active)) for st in sm.active[:3]: print(st.solver.constraints[-3:]) if __name__ __main__: main()跑一下結(jié)果大概率是No found。這就說明內(nèi)存內(nèi)容確確實實沒有被符號化程序執(zhí)行到比較時就沒有合法路徑了。只用看路徑活躍數(shù)會發(fā)現(xiàn)所有狀態(tài)都是 unsatisfiable在sm.active里檢查state.solver.satisfiable()會返回 False。這里要專門提醒一下在 angr 里一個狀態(tài)“活著”不代表它能繼續(xù)往后執(zhí)行。很多人在sm.explore沒找到結(jié)果時就打印sm.active里的狀態(tài)數(shù)發(fā)現(xiàn)數(shù)量不少就覺得是不是其他 bug。實際上這些 active 狀態(tài)很可能全是 unsat后續(xù)指令執(zhí)行全是死胡同。所以排查時第一件事就是檢查狀態(tài)的可滿足性。4.3 方案落地hook malloc 并符號化返回地址指向的內(nèi)容現(xiàn)在按方式一改造。先 hookmalloc符號讓 malloc 返回一個我們指定的地址并在這個地址上寫入 BVS。angr 的hook_symbol接受一個符號名和 hook 函數(shù)。hook 函數(shù)的輸入是state你可以在里面修改寄存器、內(nèi)存、求解器約束。import angr import claripy def setup_malloc_sym(state): # 選一個地址作為“堆區(qū)”注意避開已知區(qū)域 fake_heap 0x600000 size 0x20 sym_data claripy.BVS(malloc_0, 8 * size) state.memory.store(fake_heap, sym_data) # malloc 的返回結(jié)果放在 rax state.regs.rax fake_heap然后把 hook 掛到符號上。angr 里hook_symbol的第一個參數(shù)是字符串對應(yīng)程序里malloc在動態(tài)符號表中的名字。def main(): proj angr.Project(./demo, auto_load_libsFalse) proj.hook_symbol(malloc, setup_malloc_sym, length0) # length 為 0 表示完全替換寫完這個 hook 之后重新用同樣的 explore 跑就能在found里看到狀態(tài)了。這時候可以 dump 一下標(biāo)準輸入如果你程序里有讀入或者直接查看malloc_0這個符號變量的值found_state sm.found[0] solver found_state.solver solution solver.eval(claripy.BVS(malloc_0, 8 * 6), cast_tobytes) print(solution)如果不出意外你得到的 bytes 就是滿足check條件的“目標(biāo)值”比如bKI\xe5TZ之類。驗證方式很簡單用這個字節(jié)串替換 Demo 里 memcpy 的數(shù)據(jù)重新編譯跑一下發(fā)現(xiàn)打印ok。這一步的關(guān)鍵點在于順序必須先 store BVS 到地址再讓 malloc 返回地址。如果反過來先設(shè)置 rax 再 storestore 的地址還是我們自己指定的理論上沒區(qū)別但如果你 store 的地址依賴 rax 的內(nèi)容那順序就很重要。另外store 的 size 要跟后面讀取的長度匹配只 store 6 字節(jié)也行但為了穩(wěn)妥我會按整個分配大小 store 一整塊 BVS后面讀取哪一段都能命中。4.4 完整腳本與邊界參數(shù)說明下面給一個完整的腳本可以直接替換地址、符號名跑別的程序用import angr import claripy fake_heap_base 0x200000 malloc_size 0x100 def malloc_hook(state): # 可以在這里打印調(diào)用?；蛘叻峙浯笮”阌谡{(diào)試 # state.inspect 相關(guān)用法可以拿到調(diào)用參數(shù)這里略過 addr fake_heap_base sym claripy.BVS(heap_0, 8 * malloc_size) state.memory.store(addr, sym) state.regs.rax addr def main(): proj angr.Project(./demo, auto_load_libsFalse) proj.hook_symbol(malloc, malloc_hook, length0) state proj.factory.entry_state() sm proj.factory.simulation_manager(state) sm.explore(find0x4006a4, avoid0x4006ad) if sm.found: st sm.found[0] # 解析整個堆區(qū)域的具體解 heap_bytes st.solver.eval(claripy.BVS(heap_0, 8 * 6), cast_tobytes) print(Found, heap bytes:, heap_bytes) else: print(No found) for i, st in enumerate(sm.active[:5]): print(factive[{i}] satisfiable:, st.solver.satisfiable()) if __name__ __main__: main()說幾個容易踩的坑。第一fake_heap_base一定要選一個 angr 不會主動使用的地址。前面我用 0x600000對大多數(shù)小型二進制沒問題但如果你程序本身加載地址就在這個范圍就要避開?？梢杂胹tate.memory._get_region或者干脆打印state.regs.rsp、加載基地址后估算。第二malloc_size建議取你實際需要大小的兩倍以上留余量。第三hook_symbol的length參數(shù)如果不傳angr 默認會以符號對應(yīng)的函數(shù)長度做替換容易出問題hook 我們自己的純 Python 函數(shù)時length0更安全。第四如果你的二進制是靜態(tài)鏈接的可能沒有malloc動態(tài)符號hookmalloc會失敗。處理方式是 hook 地址先通過proj.loader.main_object.get_symbol(malloc)拿到地址或者直接對proj.loader的 memory 地圖找到 malloc 所在的 PLT 入口用proj.hook(addr, hook_func)。4.5 設(shè)計點詳解為什么這里要“同時符號化整個 size 塊”很多人在成功跑出一次結(jié)果后會有個疑問為什么我要符號化整個 0x100 字節(jié)而不是只在 hook 到的 malloc size這里是 0x20對應(yīng)的空間上做符號化這有兩個層面的原因。一方面符號化整個保留區(qū)域的成本并不高。angr 的 BVS 在約束求解時只對實際參與比較的字節(jié)產(chǎn)生約束那些沒有被讀取的字節(jié)不會影響求解復(fù)雜度。你把整個區(qū)域標(biāo)成符號相當(dāng)于為后續(xù)可能發(fā)生的越界讀取或者各種偏移訪問留了后路。另一方面真實程序里malloc 后面往往還跟著realloc、memcpy、strlen等各種操作你無法預(yù)測程序會讀取哪一段偏移。動態(tài)規(guī)劃一步到位后續(xù)就不用反復(fù)回頭看。如果擔(dān)心狀態(tài)爆炸可以只符號化實際參與校驗的那幾個字節(jié)。這需要你先摸清程序邏輯指向性更強。操作方式是一樣的把 BVS 長度設(shè)成目標(biāo)字節(jié)數(shù)store 到對應(yīng)偏移即可。自由度在你自己手上。5. 實操過程與核心環(huán)節(jié)實現(xiàn)從一個更真實的例子看符號化代碼設(shè)計5.1 新案例程序接收字符串后存堆、校驗且?guī)аh(huán)上面 Demo 非常簡單主要是驗證思路?，F(xiàn)在換一個稍微真實一點的例子。假設(shè)程序從 argv[1] 接收字符串長度限制 0x20把它拷貝到 malloc 分配的緩沖區(qū)里隨后在一個循環(huán)中逐字節(jié)累加異或校驗最后比較結(jié)果。直接對 argv 符號化很簡單但問題來了程序把 argv 字符串拷貝到 malloc 區(qū)域后如果 angr 正確識別了 memcpy該區(qū)域的值仍是符號變量。關(guān)鍵難點在于循環(huán)結(jié)構(gòu)的處理。循環(huán)在符號執(zhí)行里容易造成路徑爆炸但如果校驗邏輯是“無分支”的循環(huán)比如只是累加、異或而不根據(jù)內(nèi)存內(nèi)容跳轉(zhuǎn)angr 的執(zhí)行路徑不會分叉只是狀態(tài)會包含大量循環(huán)變量。不要被“循環(huán)”兩個字嚇到angr 并不是盲人騎瞎馬它會管理路徑的。對無分支循環(huán)執(zhí)行次數(shù)就算成百上千次也完全沒問題。真正麻煩的是循環(huán)內(nèi)依賴內(nèi)容的條件跳轉(zhuǎn)。這種情況下malloc 地址單元符號化能幫你把循環(huán)條件變成符號約束而不是把條件里出現(xiàn)的每個具體值都固定死。比如程序里有if (buf[i] a)這樣的判斷angr 在 i 未知時會嘗試所有可能。如果你提前把整個 malloc 區(qū)域符號化了angr 就能正確處理這種分支探索所有可能字符值。實戰(zhàn)里對這類循環(huán)條件一個非常有效的技巧是“約束內(nèi)生符號化”你在 hook 的 malloc 里不光 store BVS還可以主動 store 幾個額外的約束。比如你知道校驗一定要求某個字節(jié)是字母就可以直接加state.solver.add(buf[i] A)減少無用分支。這類約束越早加狀態(tài)精簡越明顯。5.2 結(jié)合“查找目標(biāo)地址”與“避免地址”的工程化腳本實戰(zhàn)中你一旦開始符號化 malloc就不能只關(guān)注找目標(biāo)那一支。很多程序校驗失敗的分支會調(diào)用 exit 或者 abort這些地址如果不寫進avoidangr 會為了探索它們消耗大量資源。我給一個稍微工程化的腳本框架def run_analysis(proj, start_addrNone, find_addrs[], avoid_addrs[]): if start_addr is None: state proj.factory.entry_state() else: state proj.factory.blank_state(addrstart_addr) # 初始化符號化堆 fake_heap_base 0x200000 sym_size 0x200 state.memory.store(fake_heap_base, claripy.BVS(heap_symbolic, 8 * sym_size)) # 探索 sm proj.factory.simulation_manager(state) sm.use_technique(angr.exploration_techniques.DFS()) # 深度優(yōu)先找路徑失敗后快速回溯 sm.explore(findfind_addrs, avoidavoid_addrs) if sm.found: for st in sm.found: # 按需提取 return st return None這個框架把 malloc 符號化的動作和執(zhí)行解耦了你可以在任意起點狀態(tài)調(diào)用。注意我用的是DFS而不是默認的BFS。找 target 時深度優(yōu)先往往更快但如果你希望覆蓋更全面的路徑BFS 更穩(wěn)。實際場景中我會根據(jù)程序復(fù)雜度切換小而精的程序用 DFS大而雜的程序用 BFS。另外blank_state配合start_addr是處理復(fù)雜反調(diào)試、自修改代碼的好姿勢。你可以先手動分析程序邏輯直接跳到某個關(guān)鍵函數(shù)入口把上下文寄存器、棧設(shè)置好后再符號化堆區(qū)開始探索。5.3 參數(shù)計算符號化范圍與約束條件怎么寫更經(jīng)濟這個點我覺得很有必要詳細展開因為很多腳本卡死不是符號化太少而是符號化太多、約束太寬造成的。假設(shè)程序有 10 個 malloc 調(diào)用點每個分配 0x100 字節(jié)。如果你統(tǒng)一 hook對每個 malloc 區(qū)域都寫入一整塊全新的 BVS那 angr 需要同時跟蹤的可能符號變量就是 10 × 0x100 × 8 字節(jié) 12800 個 bit。約束求解器面對這些符號光維護可達性關(guān)系就可能內(nèi)存爆炸。所以我給自己定了三條規(guī)矩只符號化必要地址。如果程序只校驗 malloc 區(qū)域的前 16 字節(jié)那 BVS 長度就設(shè)成 16 字節(jié)甚至更小別貪多。同一時間只讓少數(shù)幾個 malloc 區(qū)域“活著”。一個技巧是判斷 malloc 的調(diào)用點只有當(dāng)它是關(guān)鍵位置比如某個函數(shù)里的 malloc才寫入符號其他 malloc 返回具體地址內(nèi)容不管。盡早加約束。如果你從逆向分析或動態(tài)調(diào)試已經(jīng)知道輸入字節(jié)屬于可打印字符那就提前 add 約束不要等求解器自己去探索 256 種可能。用生活例子來說你讓一個快遞員送包裹給某個神秘收件人只給了他“地址在某某小區(qū)”這個信息他要跑遍整個小區(qū)你得讓他跑多久但如果你提前說“收件人姓王”他直接去查門牌系統(tǒng)效率完全不一樣。符號執(zhí)行里的約束約等于這個“提前信息”。判斷調(diào)用點的姿勢在 hook 函數(shù)里用state.inspect的 call 事件拿到調(diào)用返回地址。注意 hook 時length0會完全替換函數(shù)你可能拿不到原始調(diào)用參數(shù)更好的辦法是用state.inspect在函數(shù)入口處監(jiān)聽寄存器參數(shù)def malloc_hook(state): size_arg state.regs.rdi # System V 下第一個參數(shù)在 rdi # 你要分析的那個關(guān)鍵 malloc 很可能 size 是一個特定常量或范圍 if state.solver.eval(size_arg) 0x100: # 粗略篩一下 addr fake_heap_base sym claripy.BVS(key_heap, 8 * state.solver.eval(size_arg)) state.memory.store(addr, sym) state.regs.rax addr else: state.regs.rax fake_heap_base 0x1000 # 其他 malloc 返回另一個地址不過要注意state.solver.eval(size_arg)如果你不去約束它它可能返回任意值。這個例子只是演示思路真正使用時建議先約束size_arg或者直接用state.solver.min、max判斷范圍。更穩(wěn)妥的做法是不依賴 size直接在調(diào)用點返回地址上做判斷這需要你從反匯編結(jié)果里查到 malloc 的調(diào)用方地址。5.4 現(xiàn)場問題一符號化之后求解結(jié)果不對如何定位按上面的腳本執(zhí)行你可能成功 found 了但拿到的字節(jié)串塞回程序卻不對。這種問題一般有三個來源。第一個來源是約束沒加全。有些校驗邏輯不只有一層比較可能是算術(shù)運算后再比較或者有可能通過查表實現(xiàn)。如果你的約束只覆蓋了表層判斷求解器給出的解可能只滿足表層條件內(nèi)層條件被繞過了。這時候需要結(jié)合反匯編確認整個校驗鏈有多少步。第二個來源是符號化地址選錯了。你符號化的是 malloc 返回的地址但程序后面可能把數(shù)據(jù)拷貝到了另一塊地址或者 malloc 返回的地址被某個指針變量改動過。用 angr 的state.memory.load檢查那個地址的內(nèi)容就能發(fā)現(xiàn)是不是符號變量。很多次我發(fā)現(xiàn)符號變量在但程序讀取的來源卻是一個別的地方因為程序里有個中間變量保存了 malloc 結(jié)果后來又改了這個變量。第三個來源是內(nèi)存模型默認的字節(jié)序問題。x86 用的是小端序當(dāng)你把整個 8 字節(jié)的 BVS store 到地址上后續(xù)如果程序按字節(jié)讀取沒問題但如果程序把這塊區(qū)域當(dāng)成一個 uint64 來比較小端序會把 BVS 的低字節(jié)放在低地址與常規(guī)直覺相反。解決方式是統(tǒng)一用endnessstate.arch.memory_endness或者顯式使用state.memory.store(addr, sym, endnessIend_BE)具體按你程序里的讀取方式調(diào)整。5.5 現(xiàn)場問題二符號化后路徑爆炸卡在循環(huán)出不來另一個高頻問題是符號化成功后 angr 確實“活”了但它非常興奮把每條路徑都探索了個遍尤其是程序中存在循環(huán)結(jié)構(gòu)時幾秒鐘就爆出幾百萬狀態(tài)。這種情況下不要慌第一步先看是不是循環(huán)條件依賴了符號內(nèi)容。比如for (i 0; buf[i] ! 0; i)一旦 buf 被符號化這個循環(huán)條件就變成了一個探索點buf[i] 是否等于 0angr 會同時探索“等于 0”和“不等于 0”的分支然后繼續(xù)執(zhí)行更深層的邏輯。對策有三個方向。第一手動約束 buf[i] 的取值范圍比如可打印字符減少窮舉空間。第二限制路徑深度或使用veritesting技術(shù)它能把部分循環(huán)條件合并。angr 的Veritestingexploration technique 是對付這類情況的常用工具雖然原理復(fù)雜但調(diào)用很簡單sm proj.factory.simulation_manager(state) sm.use_technique(angr.exploration_techniques.Veritesting()) sm.explore(find..., avoid...)第三直接對循環(huán)結(jié)構(gòu)下手用angr的SimProcedure替換循環(huán)函數(shù)。如果你的循環(huán)可以抽象成一個簡單的數(shù)學(xué)函數(shù)直接 hook 循環(huán)入口計算完結(jié)果后放在指定內(nèi)存里能大幅加快分析。不過這需要你對目標(biāo)代碼結(jié)構(gòu)有足夠理解屬于高級玩法。我自己實戰(zhàn)中70% 的情況用約束DFS 能解決20% 情況用 veritesting 解決剩下 10% 只能換思路放棄完全符號化改用“混合符號執(zhí)行”把部分已知的具體值噴到堆區(qū)只符號化真正未知的部分。6. 常見問題排查與避坑指南6.1 現(xiàn)象對照看到這些情況優(yōu)先懷疑 malloc 符號化問題現(xiàn)象可能原因排查動作sm.active全是 unsat沒有 found符號化范圍沒覆蓋關(guān)鍵內(nèi)存或約束過強打印活躍狀態(tài)約束檢查是否包含 address 對應(yīng)的內(nèi)存內(nèi)容explore 卡死內(nèi)存暴漲符號化范圍過大循環(huán)條件生成海量狀態(tài)收縮符號化大小添加取值范圍約束found 了但塞回程序不對約束缺失或符號化地址/字節(jié)序問題反匯編比較鏈逐步驗證malloc 返回值不對hook 方式錯誤或 Return address 被覆蓋用state.inspect監(jiān)聽返回值同步檢查寄存器符號化后無法執(zhí)行到malloc后續(xù)可能 malloc 內(nèi)部還有分支或間接跳轉(zhuǎn)檢查 hook 是否完全替換了原實現(xiàn)length0確認這個表既是我自己排查的索引也是寫給后面看筆記的自己的速查卡。不少問題看起來五花八門根源指向同一個方向符號變量的位置、范圍、約束與真實程序邏輯不對齊。6.2 遇到 unsat 時如何拆解不少同學(xué)看到unsat就以為 angr 壞了。這里有個很重要的調(diào)試方法把活躍狀態(tài)的約束打印出來逐個檢查。for i, st in enumerate(sm.active[:5]): print(State, i, satisfiable:, st.solver.satisfiable()) if not st.solver.satisfiable(): for idx, c in enumerate(st.solver.constraints): print( Constraint, idx, :, c)逐個看約束列表你會發(fā)現(xiàn)很多 unsat 是因為你手動 add 了范圍約束比如buf[0] A和buf[0] Z但程序本身的比較條件要求buf[0] -這就產(chǎn)生矛盾。如果是這種情況說明你的全局約束跟程序固有邏輯沖突要放寬手動約束。另一個常見原因是符號區(qū)域里有多個不同 BVS程序把它們做了乘法或除法操作導(dǎo)致某些非線性的算術(shù)關(guān)系不可滿足。z3 對非線性算術(shù)乘法、除法的支持并不好遇到就可能直接拋出 unsat 或返回 unknown。這種情況的解法是盡量在源頭把符號變量拆分避免一次符號化一整塊后讓程序做整體乘法校驗。6.3 hook malloc 時被遞歸調(diào)用或被靜態(tài)鏈接坑hook 符號碰到“遞歸”問題的時候不多但碰到一次就很折磨。如果你的 hook 函數(shù)內(nèi)部又調(diào)用了state.memory.store而某個后續(xù)指令再次調(diào)用 malloc你沒有在 hook 里做區(qū)分處理就會導(dǎo)致內(nèi)存被反復(fù)覆蓋。比如程序在一個循環(huán)里 malloc 三次每次 malloc 都返回同一個 fake_heap_base那第二次 malloc 會把第一次符號化區(qū)域沖掉。解決方法是維護一個分配計數(shù)每次 store 一個不同地址。靜態(tài)鏈接的情況下hook_symbol(malloc)往往靜默失效。我排查這類問題時就用proj.loader.main_object.symbols看有沒有 malloc 符號。沒有就改用 hook 地址方式從 IDA 或 Ghidra 里找到 malloc 函數(shù)的起始地址通常在 .text 段里直接proj.hook(addr, my_malloc_hook)。要注意地址在 PIE 開啟時是相對偏移angr 內(nèi)部處理加載基址時會換算你只要確認地址與 IDA 里顯示的靜態(tài)地址一致就行。6.4 關(guān)于 angr 版本差異的提醒我一直強調(diào)這一點因為不同版本的 angr API 變化太大。老版本 7.x 和現(xiàn)在 9.x/10.x在sim_manager、hook_symbol、BVS的位置上都有改動。我筆記里的代碼基于 9.2如果你用的是其他版本跑不通時先看 API 變化其次才懷疑分析思路。尤其是 10.x 中SimState的插件體系和state.memory.store的默認參數(shù)有調(diào)整BVS 包導(dǎo)入也從claripy.BVS遷移到state.solver.BVS這類方式。版本變了但“malloc 地址單元符號化”的思想不變確定地址、寫入符號、約束求解。7. 一點個人經(jīng)驗收尾我在這篇筆記里寫的方法說白了就是一套“給 angr 補內(nèi)存上下文”的思路。malloc 地址單元符號化只是這套思路里最常見的一種落地形式。實際分析中很多東西都能人為符號化棧上的未初始化變量、文件讀入的緩沖區(qū)、甚至全局對象內(nèi)部的某個字段。你只要記住一個原則凡是你希望求解器能“推算”出來的值就必須讓它成為一個符號變量并且最好提前加上已知約束。這樣想后面遇到各種奇奇怪怪的程序思路就不會亂。最后給一個新手的實用建議如果你剛開始學(xué) angr不要一上來就研究各種高深技巧。先把我這篇筆記里的 Demo 完整跑通然后試著改幾個參數(shù)比如改 malloc 返回地址、改符號化大小、加一個取值范圍約束看求解結(jié)果怎么變。等你親手撞過一次 unsat、親手把約束從矛盾里解放出來你對符號執(zhí)行的直覺會上一個臺階。這個領(lǐng)域沒有捷徑但每一次“哇原來是這里”的瞬間都會讓你離真正的約定求解玩家更近一步。