路徑爆炸
之前說過，angr在處理分支時，采取統統收集的策略，因此每當遇見一個分支，angr的路徑數量就會乘2，這是一種指數增長，也就是所說的路徑爆炸，
以下是路徑爆炸的一個例子：
char buffer[17];
for(int i=0;i<16;i++){ if(buffer[i]!='B'){ return 0; } } return 1;
buffer的字符長度為16，當它等于16個連續的'B'時，程式回傳1，然而angr在探索這樣的路徑時，會遇上16次if陳述句，也就相應地產生2的16次方個路徑，但正確的答案只有一條路徑能夠達到（if全為false的那一條），這一條路徑就被淹沒在大量錯誤路徑中，產生了路徑爆炸，
因此當遇見大量分支（尤其是回圈中嵌套的if陳述句）時，必須想辦法緩解這種路徑爆炸，
angr常用的緩解路徑爆炸的方式有四種：
- 重寫可能導致路徑爆炸的函式或代碼片段，可以采用angr提供的hook
- veritesting：結合動態符號執行和靜態符號執行
- Lazy Solve：跳過不必要的函式
- Symbion：結合具體執行和符號執行
在angr_ctf中只涉及到了前兩種方式，因此本篇著重說說第一種方式，以及簡略介紹下第二種方式，angr緩解路徑爆炸的策略，后續新開一篇詳細談談，
重寫代碼片段
仍然以上一節路徑爆炸中用的代碼片段為例，字串buffer要按位比較16次從而產生2的16次方條路徑，它的路徑大致如下圖：
angr必須選擇16次F才能達到目標狀態，
然而根據逆向分析得出的結果來看，只要讓buffer='B'*16就可以通過這段代碼了，因此如果我們之間跳過這段代碼，然后在跳過了這段代碼的state中添加一個約束：buffer='B'*16，這樣就不會產生路徑了，
你可能會問，既然我們都通過逆向的手段看出來buffer等于16個B了，那為什么還要使用angr呢，
然而如果真正的目標狀態在該代碼片段的后面，這段會產生路徑爆炸的代碼如果不繞開的話，你很可能無法達到真正的目標狀態，
Hook
Hook可以譯為掛鉤或者鉤子，是逆向工程中改變程式運行流程的技術，可以讓自己的代碼運行在其他程式當中，通常說Hook函式，則是接收被Hook函式的引數，然后使用這些引數執行自己的代碼，并將回傳值回傳（也可以沒有回傳值），至于被Hook的函式，可以選擇讓它繼續執行，或者不執行，
聽上去Hook技術很麻煩，讓其他程式運行自己寫的代碼似乎挺不可思議的，Hook技術值得深入研究，但angr提供了簡便的Hook介面，能夠用于Hook被angr模擬執行的程式，它通常有兩種方式：
- 裝飾器@project.hook
- 函式project.hook_symbol
裝飾器@project.hook
@project.hook(hook_addr, length=ins_length) def hook_ins(state): #your code
請注意，這里的project.hook來自于你使用angr.Project方法創建的頂層模塊（即project=angr.Project('filename')），
該方法相當于在hook_addr處刪去長度為length的指令，然后用hook_ins中的指令替代，
該裝飾器需要傳入待hook的地址，以及要跳過的指令的長度，然后在hook_ins中實作你的代碼即可，
使用裝飾器的方法，如果是對函式進行hook而不是對某一代碼片段進行hook的話，無法接收函式的引數，需要根據情況來使用，
hook_symbol
假設程式中有一個這樣的原始函式：
int my_add(int a, int b){ return a+b; }
那么這樣的函式可以被下面的方式hook掉：
class Replace_my_add(angr.SimProcedure): def run(self, a, b): return a - b hooked_func_name = 'my_add' project.hook_symbol(hooked_func_name, Replace_my_add())
該方法相當于替換了原函式，為此你需要創建一個類，繼承自angr.SimProcedure，類名隨意，
然后在類中重寫run方法，run的self后的引數與待hook的函式相同，
最后在主函式中，呼叫project.hook_symbol，并傳入待hook的函式名以及新建的繼承自SimProcedure的類的物件即可，
設立回傳值
- 對于裝飾器
該方法相當于代碼片段的替換，因此如果你選擇跳過了某條函式呼叫陳述句（例如 call my_add這潭訓編指令），那么就需要去查看該函式的回傳值，或者說代碼片段的最終計算結果，被保存在了什么地方，找到這個地方，然后使用記憶體或者暫存器操作，將回傳值填入即可，
一般來說，32位程式函式的回傳值會放在eax暫存器中
- 對于hook_symbol
該方式相當于替換了函式的內容，因此直接在重寫的run方法中使用return回傳即可
回傳值的時候，如果需要根據某個符號變數來決定回傳的內容（例如判斷一個符號變數等于某個字串時回傳1，否則回傳0），此時不能用python的if陳述句來判斷，然后分別回傳1和0，這有兩個問題：
- 符號變數與其他內容進行比較（無論是符號變數、位向量、常數、變數），它的真值永遠是false
- 如果回傳值后續參與了其他的路徑選擇，此時若只回傳了值而不是帶約束的符號變數，可能會造成約束丟失
這種情況下，需要使用claripy.If來回傳值：
state.regs.eax = claripy.If(buffer == target, claripy.BVV(1, 32),claripy.BVV(0, 32))
上面代碼的意思是，當buffer==target時，將位向量<BVV32 1>傳遞給eax，否則將位向量<BVV32 0>傳遞給eax
而如果不這么做，你可能會寫出這樣的代碼：
if buffer==target: state.regs.eax = claripy.BVV(1,32) else: state.regs.eax = claripy.BVV(0,32)
這兩種做法的區別在于，如果buffer或target中至少存在一個符號變數，下面的方式將永遠判斷為false，
此外，兩種方式傳遞給eax的內容也不同，下面一種方式傳遞的是一個位向量，而上面的方式傳遞的是帶約束的符號變數（之后實戰中你會看到更多），
Veritesting
veritesting意為路徑歸并，它在動態符號執行（DSE）和靜態符號執行（SSE）之間切換，結合兩種方式減少了路徑爆炸的影響，
- DSE：為路徑生成公式，生成公式時負載很高，但公式易解
- SSE：為陳述句生成公式，公式生成容易，也能覆寫更多路徑，但更難解
詳細可參見這篇論文：Enhancing symbolic execution with veritesting (acm.org)
在angr中，要啟動veritesting，有以下兩種方式：
p = angr.Project('/bin/true') state = p.factory.entry_state() #初始化SM時啟動 simgr = p.factory.simgr(state, veritesting=True) #或者在SM初始化后啟動 simgr = p.factory.simgr(state) simgr.use_technique(angr.exploration_techniques.Veritesting())
state插件
之前提到的angr的求解器solver，以及操作記憶體、暫存器、檔案系統的方法：memory、regs、fs等，實際上都是state的插件，下面說明兩個其他常用的插件，
全域插件global
state.global實作了標準python dict介面，使用它你能夠在模擬執行的state中存盤任意資料，并且很方便的就能訪問到，可以使用如下的陳述句訪問全域變數：
state.globals['x'] = a_symbol
全域變數名x不需要提前宣告，但當你需要使用這個全域變數之前，需要對它賦值，
history插件
history記錄了一個狀態的執行路徑，它是一個鏈表，每個節點代表一次執行的狀態，你可以不斷使用.parent來回溯這個鏈表，history的使用方式如下：
- state.history.bbl_addrs：回傳當前state執行的基本塊的地址串列
- state.history.parent.bbl_addrs：回傳上一個state執行的基本塊的地址串列
- state.history.descriptions：描述state上每輪執行的狀態的字串串列
- state.histroy.guards：到達當前state所走路徑需要滿足的條件的串列（也就是每次分支判斷時為True還是False）
- state.history.events：執行程序中發生的事件串列，比如符號跳轉條件、彈出訊息框等
此外，在每種方法前加上recent_，就可以獲取串列中最近的那個地址，例如state.history.recent_bbl_addrs會回傳當前state最近執行的基本塊的地址，
實戰：08_angr_constraints
先逆向查看邏輯
和之前一樣，先對輸入進行混淆，然后再判斷，
但這里的問題在于，首先字串的長度為16，此外，在check_equals函式中，采用的是按位比較的方式：
而字串長度為16，那么就會進行16次比較，從而產生2的16次方條路徑，這樣angr就會陷入路徑爆炸，
但能夠注意到，check函式中實際上是在讓buffer與password進行比較（0x0804a040就是password的地址），而password在main的開頭被初始化為一串已知的字串，
因此可以考慮讓模擬運行在呼叫check函式之前停下來，然后添加一個符號約束（buffer==已知的字串），之后再用求解器求解buffer即可，
angr腳本如下：
import angr import claripy import time def good(state): tag = b'Good' in state.posix.dumps(1) return True if tag else False def bad(state): tag = b'Try' in state.posix.dumps(1) return True if tag else False time_start = time.perf_counter() path_to_binary = './dist/08_angr_constraints' p = angr.Project(path_to_binary, auto_load_libs=False) start_addr = 0x08048625 init_state = p.factory.blank_state(addr=start_addr) buffer = claripy.BVS('buffer', 16*8) # buffer的地址 buffer_addr = 0x0804a050 init_state.memory.store(buffer_addr, buffer) simgr = p.factory.simgr(init_state) # call check指令的地址 check_addr = 0x08048565 # 讓程式模擬運行到call check時就標記為目標狀態 simgr.explore(find=check_addr) if simgr.found: solution_state = simgr.found[0] # 由于buffer經過混淆函式混淆發生了變化 # 因此需要從buffer的記憶體地址中取出buffer目前的值 buffer_current = solution_state.memory.load(buffer_addr, 16) key = 'AUPDNNPROEZRJWKB' # 為當前狀態添加約束 solution_state.solver.add(buffer_current == key) # 求解buffer solution = solution_state.solver.eval(buffer, cast_to=bytes) print('[+]Success:', solution.decode()) else: raise Exception("Could not find solution") print('program last: ', time.perf_counter() - time_start)
你大概有兩個問題：
- 為何要重新從buffer_addr中取出符號變數，不能直接使用buffer嗎？
- 在實戰05中輸入字串的長度為32，然后使用了strncmp進行比較，strncmp的底層實作也是按位比較的，為何之前不用考慮路徑爆炸的問題呢？
首先第一個問題，我們可以先將buffer列印出來，應該能得到一個位向量<BV128 buffer_0_128>，該位向量之后被我們保存在了buffer的地址當中，
然后列印一下buffer_current：
_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:0]))[63:32] >> 0x3[7:0] + 26 * 0xffffffbf + (buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:7] .. buffer_0_128[7:0]) >> 0x1f[7:0]>
會得到一個極為龐大的符號變數，或者說一個運算式，這是位向量<BV128 buffer_0_128>經過混淆函式混淆后的結果，因此要求解的應該是這個運算式，
我們創建的符號buffer被保存在了buffer的地址當中，然后模擬程式運行時，從地址中取出符號進行混淆，混淆的程序也被保存在buffer的地址中，因此在最后需要從這個地址里面取出混淆后的符號進行求解，
第二個問題，先說結論：angr在路徑選擇時只進入庫函式一次，而不關心庫函式內部的實作采用了多少次if，
撰寫以下兩個c程式并編譯（我這里使用gcc編譯成64位了，與題目的32位不符，但原理相同）：
#include<stdio.h> char buffer[9]; char passwd[9] = "abcdefgh"; int main(){ scanf("%8s", buffer); if (strncmp(buffer, passwd ,8)==0){ printf("good"); } else{ printf("bad"); } }
#include<stdio.h> char buffer[9]; char passwd[9] = "abcdefgh"; int check(int size){ int i = 0; for(i;i<size;i++){ if(buffer[i]!=passwd[i]){ return 0; } } return 1; } int main(){ scanf("%8s", buffer); printf("%s\n",buffer); if (check(8)){ printf("good"); } else{ printf("bad"); } }
兩個程式都接收8個字符，然后與abcdefgh進行比較，區別在于第一個程式使用庫函式strncmp進行比較，而后一個程式則自己定義了一個check進行比較，兩者比較的內部原理都是按位回圈比較（strncmp還進行了一些額外處理，但基本原理仍然是按位回圈比較，具體可參見strncmp原始碼）
然后，我們使用符號變數填充到buffer對應的地址中，讓模擬執行從scanf后的陳述句開始執行，并以列印good為目標狀態，
獲取目標狀態后，使用history插件列印出當前state執行的基本塊，這些步驟的angr代碼如下：
import angr import claripy import time def good(state): tag = b'good' in state.posix.dumps(1) return True if tag else False def bad(state): tag = b'bad' in state.posix.dumps(1) return True if tag else False start_time = time.perf_counter() p = angr.Project('./a', auto_load_libs=False) init_state = p.factory.blank_state(addr=0x40118b) buffer_addr = 0x404060 x = claripy.BVS('x', 8 * 9) init_state.memory.store(buffer_addr, x) simgr = p.factory.simgr(init_state) simgr.explore(find=good, avoid=bad) if simgr.found: solution_state = simgr.found[0] x_current = solution_state.memory.load(buffer_addr, 8)
# 列印路徑 for address in solution_state.history.bbl_addrs: print(hex(address)) result = solution_state.solver.eval(x_current, cast_to=bytes) print(result) else: raise Exception("Could not find solution") print(time.perf_counter() - start_time)
兩個程式的angr腳本相同，修改一下地址和檔案名即可，此外還需要注意，如果編譯時沒加任何引數，裝載的地址可能會跟你在IDA中看到的不一樣，例如我使用angr時提示如下：
WARNING | 2022-11-29 02:41:46,685 | cle.loader | The main binary is a position-independent executable. It is being loaded with a base address of 0x400000.
它提示我們，程式被裝載到基地址0x400000中了，而我們在IDA中看到的程式的地址main函式以0x1169開頭，這是一個相對地址，因此在撰寫angr腳本時，要將這些相對地址加上0x400000.
此時列印出來兩種判斷方式的路徑如下：
#程式1 0x40118b 0x401040 0x500010 0x40119a 0x401030 0x500008 0x4011b8 0x401050 0x500018 0x4011ce 0x401030 0x500008 0x4011ec 0x4011f0 0x401050 0x500018 #程式2 0x4011c9 0x401030 0x500008 0x4011d8 0x401159 0x401198 0x401169 0x401194 0x401169 0x401194 0x401169 0x401194 0x401169 0x401194 0x401169 0x401194 0x401169 0x401194 0x401169 0x401194 0x401169 0x401194 0x4011a0 0x4011e2 0x4011e6 0x401040 0x500010
程式1中0x40119a所在的基本塊就是呼叫strncmp的基本塊，它只被執行了一次，因此在if陳述句中只會產生2個路徑，
而程式2中check函式內部的回圈陳述句所在的基本塊0x401169和0x401194被執行了8次，從而產生了2的8次方個路徑，
因此可以得到開頭的結論，庫函式內部如何實作，與angr無關，并不會產生額外的路徑，
實戰：09_angr_hooks
仍然先逆向查看邏輯
程式先接收一個輸入，輸入被混淆后與password進行比較，password被初始化為一個已知的字串，
然后程式混淆password，再接收一個輸入，將輸入與混淆后的password進行比較，（兩個for回圈中的地址分別是buffer和password的地址）
第一次比較在check函式中按位比較，后一次比較則是使用了strncmp函式，因此路徑爆炸發生在check函式中，對于strncmp則無須處理，
這次使用裝飾器的方法來解決這個問題：
- 使用裝飾器跳過呼叫check函式的指令，也就是call cehck_equals
- 在裝飾器內部實作符號==AUPDNNPROEZRJWKB的約束
- 將符號約束作為回傳值回傳，查看匯編代碼可以知道，check函式的回傳值保存在了eax暫存器中
angr腳本如下：
import angr import time import claripy time_strat = time.perf_counter() def good(state): tag = b'Good' in state.posix.dumps(1) return True if tag else False def bad(state): tag = b'Try' in state.posix.dumps(1) return True if tag else False path_to_binary = './dist/09_angr_hooks' p = angr.Project(path_to_binary, auto_load_libs=False) init_state = p.factory.entry_state() # call check_equal的地址 check_addr = 0x080486b3 # call check_equal的指令長度 ins_size = 5 @p.hook(check_addr, length=ins_size) def skip_check(state): buffer_addr = 0x0804a054 buffer = state.memory.load(buffer_addr, 16) target = 'XYMKBKUHNIQYNQXE' # 使用claripy.If回傳一個符號約束 tmp = claripy.If(buffer == target, claripy.BVV(1, 32), claripy.BVV(0, 32)) print(type(tmp)) print(tmp) state.regs.eax = tmp simgr = p.factory.simgr(init_state) simgr.explore(find=good, avoid=bad) if simgr.found: solution_state = simgr.found[0] flag = solution_state.posix.dumps(0) print(flag) else: raise Exception("Could not find solution")
列印出tmp的內容，其中最后的片段如下：
packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:7] .. packet_0_stdin_4_128[7:0]) >> 0x1f[7:0]) == 0x58594d4b424b55484e4951594e515845 then 0x1 else 0x0>
tmp前面的內容即buffer的內容，是經過混淆計算后的符號，而在最后可以看到，claripy.If創建了一個判斷，因此實際上回傳了一個約束，這就是為什么不適用python中的if然后傳遞一個<BVV32 1>的原因，
實戰：10_angr_simprocedures
第十題的路徑爆炸仍然發生在check_equals函式當中，與上一題的區別在于，此時輸入的字串被保存在區域變數當中，我們無法提前得知它的地址，因此如果要hook掉check函式，則必須獲取check函式的引數，
因此需要使用hook_symbol的方式來hook掉check函式
使用方式之前說明了，只需要注意使用hook_symbol的方法本質上是創建了新的函式取代了原有函式，因此在回傳值的時候使用return回傳，而不用將值保存在eax當中（事實上重寫的run方法中沒有當前的state，你也保存不到eax里面）
angr腳本如下：
import angr import time import claripy time_strat = time.perf_counter() def good(state): tag = b'Good' in state.posix.dumps(1) return True if tag else False def bad(state): tag = b'Try' in state.posix.dumps(1) return True if tag else False path_to_binary = './dist/10_angr_simprocedures' p = angr.Project(path_to_binary, auto_load_libs=False) init_state = p.factory.entry_state() class Hook(angr.SimProcedure): def run(self, addr, size): # 后兩個引數即為check_equals函式的引數 input_buffer = addr input_size = size # 從記憶體中讀取輸入 input_str = self.state.memory.load(input_buffer, input_size) right_str = 'ORSDDWXHZURJRBDH' # 比較回傳符號約束 result = claripy.If(input_str == right_str, claripy.BVV(1, 32), claripy.BVV(0, 32)) return result # funcname一定要相同，可在IDA中查看 hooked_funcname = 'check_equals_ORSDDWXHZURJRBDH' p.hook_symbol(hooked_funcname, Hook()) simgr = p.factory.simgr(init_state) simgr.explore(find=good, avoid=bad) if simgr.found: solution_state = simgr.found[0] flag = solution_state.posix.dumps(0) print(flag)
實戰：11_angr_sim_scanf
此題與實戰2-7中的題類似，實際上使用萬能腳本就可以成功，出于練習的目的，跟著angr_ctf作者的思路，我們使用hook_symbol方法來hook掉scanf函式，
angr腳本如下，使用到了state的全域變數插件，用法很簡單，用于進行約束求解，如果不使用全域變數的話，從buffer的地址中取出符號進行求解也是一樣的（就像在實戰8中做的那樣）
import angr import claripy def good(state): tag = b'Good' in state.posix.dumps(1) return True if tag else False def bad(state): tag = b'Try' in state.posix.dumps(1) return True if tag else False path_to_binary = './dist/11_angr_sim_scanf' project = angr.Project(path_to_binary, auto_load_libs=False) initial_state = project.factory.entry_state() class ReplacementScanf(angr.SimProcedure): # 第一個引數是scanf的格式化字串，接著是兩個buffer地址 def run(self, format_string, scanf0_address, scanf1_address): # 在run中完成scanf的功能，即向目標地址寫入符號 # 定義兩個符號變數，用于寫入buffer scanf0 = claripy.BVS('scanf0', 32) scanf1 = claripy.BVS('scanf1', 32) # 寫入記憶體，最后一個引數指定位元組序 self.state.memory.store(scanf0_address, scanf0, endness=project.arch.memory_endness) self.state.memory.store(scanf1_address, scanf1, endness=project.arch.memory_endness) # 保存變數到全域，方便后續約束求解 self.state.globals['solution0'] = scanf0 self.state.globals['solution1'] = scanf1 # scanf的函式名稱，可在ida中查看 scanf_symbol = '__isoc99_scanf' project.hook_symbol(scanf_symbol, ReplacementScanf()) simulation = project.factory.simgr(initial_state) simulation.explore(find=good, avoid=bad) if simulation.found: solution_state = simulation.found[0] # 對符號變數進行約束求解 stored_solutions0 = solution_state.globals['solution0'] stored_solutions1 = solution_state.globals['solution1'] scanf0_solution = solution_state.solver.eval(stored_solutions0) scanf1_solution = solution_state.solver.eval(stored_solutions1) print(scanf0_solution, scanf1_solution) else: raise Exception('Could not find the solution')
實戰：12_angr_veritesting
先逆向分析
可以看到，此題與之前的題目不同的地方在于，它不僅是按位進行比較的，而且是按位進行混淆后馬上比較，之前的題目都是整體混淆后比較，因此路徑爆炸同時出現在混淆和比較兩個地方，
之前的做法是跳過回圈比較，直接讓混淆后的字串與正確的字串比較，但這里不能這樣做，跳過回圈比較就意味著跳過了混淆，
因此考慮使用路徑歸并的搜索策略veritesting，此題就是用來體驗一把veritesting的強大功能的，
angr腳本如下，直接使用萬能腳本，并且開啟veritesting：
import angr import claripy import time start_time = time.perf_counter() p = angr.Project('./dist/12_angr_veritesting', auto_load_libs=False) init_state = p.factory.entry_state() def good(state): tag = b'Good' in state.posix.dumps(1) return True if tag else False def bad(state): tag = b'Try' in state.posix.dumps(1) return True if tag else False simgr = p.factory.simgr(init_state, veritesting=True) simgr.explore(find=good, avoid=bad) if simgr.found: solution_state = simgr.found[0] print(solution_state.posix.dumps(0).decode()) print(time.perf_counter() - start_time)
（不加veritesting直接能跑死機，大佬的智慧真是看不懂，但是真好用）
轉載請註明出處，本文鏈接：https://www.uj5u.com/qita/538713.html
標籤：其他