狀態操作
angr中提到的狀態（state）實際上是一個Simstate類，該類可由Project預設得到，預設完成后，還可以根據需要對某些部分進行細化操作，
一個state包含了程式運行到某個階段時，記憶體、暫存器、檔案系統、符號變數和符號約束等內容，
暫存器訪問
可以通過state.regs.暫存器名來訪問和修改暫存器
>>> print(state.regs.eax, state.regs.ebx) <BV32 0x1c> <BV32 0x0> >>> state.regs.eax +=1 >>> print(state.regs.eax, state.regs.ebx) <BV32 0x1d> <BV32 0x0>
堆疊訪問
堆疊訪問涉及兩個暫存器：ebp和esp，以及兩個指令：push和pop，對于暫存器的訪問與其他暫存器相同
push和pop指令可以通過以下方法呼叫
state.stack_push(value)
state.stack_pop()
記憶體訪問
使用以下兩個指令對記憶體讀寫：
讀記憶體-state.memory.load(addr, size,endness)
寫記憶體-state.memory.store(data,size,endness)
endness是指使用的大小端，通常應該和程式使用的大小端保持相同，而程式所使用的大小端可以用p.arch.memory_endness查詢，因此在對默認值沒有把握時，請讓endness=p.arch.memory_endness，
此外，上述兩個函式的size的單位均為位元組，示例如下：
>>> state.memory.store(0x4000,state.solver.BVV(0x0123456789,40)) >>> print(state.memory.load(0x4001,2)) <BV16 0x2345>
其中存入地址0x4000處的資料是一個位向量，之后會介紹，
檔案操作
angr提供了一個SimFile類用來模擬檔案，通過將SimFile物件插入到狀態的檔案系統中，在使用angr分析程式時就可以使用該檔案
filename = 'test.txt' simfile = angr.storage.SimFile(name=filename, content=data, size=0x40) state.fs.insert(filename, simfile)
上述指令能創建一個SimFile物件，檔案名為test.txt，內容為data，輸入的內容長度為0x40，單位為位元組
之后，使用state.fs.insert方法，將SimFile物件插入到狀態的檔案系統中，在模擬運行程式時就可以使用這個檔案了
位向量
對于記憶體、暫存器等進行操作時，不僅可以使用python的int，angr還提供了位向量（Bit Vector，BV）
位向量就是一串位元的序列，這于python中的int不同，例如python中的int提供了整數溢位上的包裝，而位向量可以理解為CPU中使用的一串位元流，需要注意的是，angr封裝的位向量有兩個屬性：值以及它的長度
我們先生成幾個位向量：
>>> one = state.solver.BVV(1,64) >>> one_hundred = state.solver.BVV(100,64) >>> short_nine = state.solver.BVV(9,27) >>> print(one,one_hundred,short_nine) <BV64 0x1> <BV64 0x64> <BV27 0x9>
BVV能夠生成一個位向量，第二個引數表示該位向量的長度，單位為bit
這些位向量相互之間能夠進行運算，但參與運算的位向量的長度必須相同
>>> print(short_nine+1) <BV27 0xa> >>> print(one+one_hundred) <BV64 0x65> >>> print(one+short_nine) Traceback (most recent call last): File "<stdin>", line 1, in <module> File "/home/kali/angr/venv/lib/python3.9/site-packages/claripy/operations.py", line 50, in _op raise ClaripyOperationError(msg) claripy.errors.ClaripyOperationError: args' length must all be equal
可以看到，當長度不一樣時，claripy會提示“length must all be equal”，同時我們也得知，位向量運算的底層模塊時claripy，之后會繼續說明claripy
如果一定要進行長度不相等位向量之間的運算，可以擴展位向量，使用zero_extend會用零擴展高位，而sign_extend會在此基礎上帶符號地進行擴展
>>> print(one+short_nine.zero_extend(64-27)) <BV64 0xa>
請注意zero_extend的引數是擴展多少位，而不是擴展到多少位
此外，位向量還可以之間與python的int進行運算：
>>> print(one+1,one*5) <BV64 0x2> <BV64 0x5>
接下來使用BVS（Bit Vectort Symbol）創建一些符號變數
>>> x = state.solver.BVS('x',64) >>> y = state.solver.BVS('y',64) >>> z = state.solver.BVS('notz',64) >>> print(x,y,z) <BV64 x_42_64> <BV64 y_43_64> <BV64 notz_44_64>
BVS的引數分別是符號變數名和長度，通過z的例子可以看到，BVS中符號變數名引數會影響位向量的名稱，但這與你在angr腳本中使用這個符號變數的變數（也就是z）無關，
此時對符號變數進行運算，做比較判斷，都不會得到一個具體的值，而是將這些操作統統保存到符號變數中：
>>> print(x+1)
<BV64 x_42_64 + 0x1>
符號約束與求解
符號約束
每個符號變數本質上可以看做是一顆抽象語法樹（AST），之前單獨生成的符號變數<BV64 x_42_64>可以看作是只有一層的AST，對它進行操作實際上是在擴展AST，這樣的AST的構造規則如下：
- 如果AST只有根節點的話，那么它必定是符號變數或位向量
- 如果AST有多層，那么葉子節點為符號變數和位向量，其他節點為運算子
其中一個節點的左右孩子可以使用args來訪問，節點本身存放的資訊則使用op來訪問，可以通過下面的例子來理解：
>>> ast = (x+5)*(y-1) >>> print(ast) <BV64 (x_45_64 + 0x5) * (y_43_64 - 0x1)> >>> print(ast.op) __mul__ >>> print(ast.args) (<BV64 x_45_64 + 0x5>, <BV64 y_43_64 - 0x1>) >>> print(ast.args[0].op) __add__
>>> print(ast.args[0].args[0]) <BV64 x_45_64>
>>> print(ast.args[0].args[1]) <BV64 0x5>
>>> print(ast.args[0].args[1].op) BVV
>>> print(ast.args[0].args[1].args) (5, 64)
>>> print(ast.args[0].args[0].args) ('x_45_64', None, None, None, False, False, None)
>>> print(ast.args[0].args[0].op)
BVS
可以發現，對單獨的節點取op的話，可以得到它的型別（示例中為BVV和BVS）
之前我們使用BVS創建了符號變數，現在如果對該符號變數進行比較判斷操作，會得到如下結果：
>>> print(x>0) <Bool x_42_64 > 0x0>
它現在不是一個位向量了，而是一個符號化的布爾型別
這些布爾型別的值可以通過is_true和is_false來判斷，但對于上述有符號變數參與的布爾型別，它永遠為false
>>> print(state.solver.is_true(x>0)) False >>> print(state.solver.is_false(x>0)) False
此外需要注意的是，直接使用比較符號比較兩個位向量，通常是默認不帶符號的，例子如下：
>>> mfive = state.solver.BVV(-5,64) >>> one = state.solver.BVV(1,64) >>> print(one>mfive) <Bool False> >>> print(mfive) <BV64 0xfffffffffffffffb> >>> print(state.solver.is_true(one>mfive)) False
-5在記憶體中以0xfffffffffffffffb存盤，作為無符號數，它比1要大
符號約束是一個和狀態相關的概念，或者說一個state除了包含記憶體、暫存器中的值這些資訊外，還包含了符號約束，也就是要到達當前狀態符號變數所必須滿足的條件，
除了運行程式，SM根據分支收集起來的符號約束之外，也可以自行手動添加約束：
>>> print(x,y) <BV64 x_45_64> <BV64 y_43_64> >>> state.solver.add(x>y) [<Bool x_45_64 > y_43_64>] >>> state.solver.add(x>5) [<Bool x_45_64 > 0x5>] >>> state.solver.add(x<8) [<Bool x_45_64 < 0x8>]
此時，x必須滿足大于5小于8，而y必須滿足小于x，
符號求解
可以使用state.solver.eval(x)來求解當前狀態（即state）中的符號約束下，x的值
>>> state.solver.eval(x)
6
求解完x之后，此時如果求解y，則會得到之前求解結果條件下的y，也就是說，y此時必定小于6
此外，很明顯能夠看到，x應該是有多個值的，可以solver中的其他方法取出來：
- solver.eval(x):給出運算式的一個可能解
- sovler.eval_one(x):給出運算式的解，如果有多個解，將拋出錯誤
- solver.eval_upto(x,n)給出運算式的至多n個解
- sovler.eval_taleast(x,n):給出運算式的n個解，如果解的數量少于n，則拋出錯誤
- solver.eval_exact(x,n):給出運算式的n個解，如果解的個數不為n，則拋出錯誤
- sovler.min(x):給出運算式的最小解
- sovler.max(x):給出運算式的最大解
這些方法還有兩個可省略的引數：
- extra_constraints：可以作為約束進行求解，但不會被添加到當前狀態
- cast_to：將傳遞結果轉換成指定資料型別，目前只能是int和bytes，例如
state.solver.eval(state.solver.BVV(0x41424344, 32), cast_to=bytes)將回傳b'ABCD'
此外，如果將兩個互相矛盾的約束加入到一個state當中，那么這個state就會被放到unsat這個stash里面，對這樣的state進行求解會導致例外，可以使用state.satisfiable()來檢查是否有解
加入到狀態中的約束在進行約束求解時的關系是“與”的關系，也就是說必須都得滿足，那么如果有其他的關系，比如或之類的關系，該如何表示呢？
事實上，根本不會存在或這樣的約束之間的關系，因為angr保存所有分支，因此到達某個狀態的條件必然是一層一層都滿足的情況下到達的，如果在條件判斷時有“或”這樣的關系存在，那么這樣的解將會出現在另一個state當中，而另一個state當中的符號約束之間也必然都是“與”的關系，
實戰：03_angr_symbolic_registers
此題用萬能腳本也可以解，但出于練習的目的，使用本節講的內容（angr_ctf作者認為angr在處理多個由scanf接收的輸入時表現不好，應該想辦法跳過scanf）
首先還是在IDA中逆向分析一下
函式get_user_input()使用scanf在一行中接收三個輸入，三個輸入之后分別被complex_function混淆后參與if陳述句的判斷
查看匯編指令，發現函式get_usr_input()接收的輸入，通過三個暫存器保存在了區域變數當中
因此為了跳過scanf（也就是get_user_input函式），可以考慮讓程式在call之后的陳述句開始模擬運行，同時在三個暫存器中存放三個符號變數，這樣程式從mov開始運行時，就會從三個暫存器中分別取出符號變數參與后續運行，也就使用這三個符號變數進行路徑選擇，保存符號約束，最后在能夠到達Good Job的state里求解這三個符號變數即可，
angr腳本如下：
import angr import claripy path_to_binary = './dist/03_angr_symbolic_registers' p = angr.Project(path_to_binary, auto_load_libs=False)
#call get_user_input后的下一條陳述句 start_addr = 0x08048980
#從目標地址開始模擬運行，而不是程式的入口點
init_state = p.factory.blank_state(addr=start_addr)
#使用claripy創建三個符號變數，之前提到過state有關位向量的底層實作是claripy passwd_size = 32 passwd0 = claripy.BVS('passwd0', passwd_size) passwd1 = claripy.BVS('passwd1', passwd_size) passwd2 = claripy.BVS('passwd2', passwd_size)
#對暫存器進行賦值 init_state.regs.eax = passwd0 init_state.regs.ebx = passwd1 init_state.regs.edx = passwd2
#將初始化后的state添加到SM中 simgr = p.factory.simgr(init_state) good = 0x080489e9 bad = 0x080489d7 simgr.explore(find=good, avoid=bad) if simgr.found:
#solution_state是能夠到達Good Job的狀態 solution_state = simgr.found[0]
在該狀態中求解三個符號變數即可 solution0 = hex(solution_state.solver.eval(passwd0)) solution1 = hex(solution_state.solver.eval(passwd1)) solution2 = hex(solution_state.solver.eval(passwd2)) print(solution0, solution1, solution2) else: raise Exception('Could not find')
實戰：04_angr_symbolic_stack
此題與03一樣，需要繞過scanf函式，然而上一題中輸入的引數被保存在暫存器當中之后再轉移到區域變數，此題則是直接保存在區域變數當中了，因此創建的符號變數需要存放在堆疊上，
那么進行動態除錯，查看執行完scanf后的堆疊結構（我輸入了1234 5678，對應16進制為4d2 162e）：
可以發現，輸入進去的數字被保存在了距離ebp 0xc的位置上，那么我們只要將兩個符號變數壓入這個位置即可，
angr腳本：
import angr import claripy path_to_binary = './dist/04_angr_symbolic_stack' p = angr.Project(path_to_binary, auto_load_libs=False)
#call scanf的下一個匯編指令 start_addr = 0x08048694 init_state = p.factory.blank_state(addr=start_addr) good = 0x080486e4 bad = 0x080486d2 v1 = claripy.BVS('v1', 32) v2 = claripy.BVS('v2', 32)
#tmp保存當前esp的內容，以便待會還原 tmp = init_state.regs.esp
#-減8而不是減12的原因在于，esp保存了當前不為空的堆疊頂，push時esp先+4再存放內容 init_state.regs.esp = init_state.regs.ebp - 0x8 init_state.stack_push(v1) init_state.stack_push(v2)
#還原esp，維持堆疊平衡 init_state.regs.esp = tmp
#之后的步驟同3 simgr = p.factory.simgr(init_state) simgr.explore(find=good, avoid=bad) if simgr.found: solution_state = simgr.found[0] s0 = solution_state.solver.eval(v1) s1 = solution_state.solver.eval(v2) print(s0, s1) else: raise Exception('Could not find')
實戰：05_angr_symbolic_memory
此題邏輯與前兩個也一樣，區別在于這次輸入的東西被保存在了.bss段作為全域變數存放了
那么只需要創建符號變數，并保存在對應的地址處就可以了，使用state.memory.store方法進行記憶體寫，
angr腳本：
import angr import time 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 time_start = time.perf_counter() p = angr.Project('./dist/05_angr_symbolic_memory') start_addr = 0x080485FE init_state = p.factory.blank_state(addr=start_addr) passwd_size_in_bits = 8 * 8 password0 = claripy.BVS('password0', passwd_size_in_bits) password1 = claripy.BVS('password1', passwd_size_in_bits) password2 = claripy.BVS('password2', passwd_size_in_bits) password3 = claripy.BVS('password3', passwd_size_in_bits) # 四個變數地址連續，向其中寫入符號變數即可 password0_address = 0x0A1BA1C0 init_state.memory.store(password0_address, password0) init_state.memory.store(password0_address + 0x08, password1) init_state.memory.store(password0_address + 0x10, password2) init_state.memory.store(password0_address + 0x18, password3) simgr = p.factory.simgr(init_state) simgr.explore(find=good, avoid=bad) if simgr.found: solution = simgr.found[0] solution0 = solution.solver.eval(password0, cast_to=bytes).decode('utf-8') solution1 = solution.solver.eval(password1, cast_to=bytes).decode('utf-8') solution2 = solution.solver.eval(password2, cast_to=bytes).decode('utf-8') solution3 = solution.solver.eval(password3, cast_to=bytes).decode('utf-8') print(solution0, solution1, solution2, solution3) else: raise Exception("Could not find solution") print('program last:', time.perf_counter() - time_start)
實戰：06_angr_symbolic_dynamic_memory
和前三題一樣，只是此題將輸入進來的資料保存到了malloc申請來的記憶體空間當中了
雙擊進入buffer0和buffer1，對應的地址分別是.bss:0x0abcc8ac和.bss:0x0abcc8ac，這兩個地址將來會存放由malloc申請來的地址，而malloc申請來的地址當中，將存放輸入的字串，也就是說，我們需要將符號變數保存在buffer中保存的指標指向的地方，而我們并不會清楚malloc具體會申請到哪個地址，因此考慮直接跳過malloc陳述句，往buffer中填入一個不影響程式運行的地址，然后在該地址中存放符號變數
這里是一個多重指標，熟悉堆管理方式的朋友應該不會陌生，它們的呼叫關系如下：
buffer -> malloc申請到的地址 -> 字串保存的地址
angr腳本如下：
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 p = angr.Project('./dist/06_angr_symbolic_dynamic_memory') # scanf后的第一潭訓編指令 start_addr = 0x08048699 init_state = p.factory.blank_state(addr=start_addr) # fake_addr為不影響程式運行的任意地址 fake_addr1 = 0x085fa000 fake_addr2 = 0x085fa010 buffer1 = 0x0abcc8a4 buffer2 = 0x0abcc8ac # 注意設定大小端 init_state.memory.store(buffer1, fake_addr1, endness=p.arch.memory_endness) init_state.memory.store(buffer2, fake_addr2, endness=p.arch.memory_endness) v1 = claripy.BVS('v1', 64) v2 = claripy.BVS('v2', 64) # 符號變數不是具體的值，不需要考慮大小端 init_state.memory.store(fake_addr1, v1) init_state.memory.store(fake_addr2, v2) simgr = p.factory.simgr(init_state) simgr.explore(find=good, avoid=bad) if simgr.found: solution_state = simgr.found[0] s1 = solution_state.solver.eval(v1, cast_to=bytes).decode() s2 = solution_state.solver.eval(v2, cast_to=bytes).decode() print(s1, s2) else: raise Exception("Could not find solution")
實戰：07_angr_symbolic_file
此題邏輯也一樣，只是這次需要從檔案中讀取輸入了
因此我們需要創建一個SimFile物件，該物件是個模擬檔案，然后將符號變數存放在模擬檔案中并將模擬檔案插入到state中，這樣在模擬運行時，程式就會從我們模擬的檔案中讀取符號變數作為輸入的引數進行后續的運行，
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() p = angr.Project('./dist/07_angr_symbolic_file', auto_load_libs=False) # memset的后一條指令 start_addr = 0x080488e7 init_state = p.factory.blank_state(addr=start_addr) v = claripy.BVS('v', 0x40*8) filename = 'OJKSQYDP.txt' # 創建SimFile物件 simfile = angr.storage.SimFile(name=filename, content=v, size=0x40) # 將SimFile插入到state的檔案系統中 init_state.fs.insert(filename, simfile) simgr = p.factory.simgr(init_state) simgr.explore(find=good, avoid=bad) if simgr.found: solution_state = simgr.found[0] s = solution_state.solver.eval(v, cast_to=bytes) print(s) else: raise Exception("Could not find solution") print('program last: ', time.perf_counter() - time_start)
需要注意的是，我們只是模擬了檔案，并沒有直接將符號變數存在buffer中，因此程式還是需要從檔案中讀取符號變數的，所以我們blank_state中的初始地址不能超過fopen函式，
此外，由于參與混淆和比較的字串被保存在了buffer當中，也可以使用之前的方式將符號變數直接保存在buffer中，然后跳過所有的檔案操作開始運行程式，
該題也可以通過萬能腳本完成，但是通過計算程式實際運行的時間，發現使用模擬檔案的方式要更快一些，前者大約是5秒半，后者大約3秒，這也是angr腳本的意義——通過更詳細的設定angr狀態和路徑搜索策略，提高angr的效率，
轉載請註明出處，本文鏈接：https://www.uj5u.com/qita/538712.html
標籤：其他