DEFCON Qualifier Reverse amadhj by angr

題目

比賽時用 python 重寫各個 function，然後嘗試用 z3 解，但不知為何，每個 char 加上限制後 check 都 unsat 。

賽後 lays 大大研究了 KLEE 的解法 link

因為最近在看 angr ，就用 angr 試著解解看此題

這題看起來就是標準 symbolic solve 題

有個主要的 check function 參數是一 32 bytes buffer

在 check function 裡 read(0, buf, 32)

input 32 bytes, 分成 4 * qword 丟到 4 個function 算一算後 xor 再一起，與 const 比對，檢查結果


解題

angr 底層也有用 z3 當 solve engine ， 所以最重要的是讓 angr 把 constrain 建立起來

透過兩個 angr example 可以發現有沒有指定 symbolic symbol 的大小，速度差很多

baby-re solve1

baby-re solve2

試著用 hook read 方式指定 sybolic symbol

def patch_read(s):
    global concated_str
    print 'patch'
    t = []
    for i in range(4):
        inp = s.se.BVS('usr_input', 8*8) # QWORD
        s.memory.store(s.regs.rsi+8*i, inp)
        t.append(inp)

gsss.append(claripy.Concat(*t))
return

state 從 check function 開始跑

指定好 find(compare success), avoid(compare fail) 後，剩下的就交給 explorer 去跑

def exp():
    global concated_str
    path = b.factory.path(state=s)
    ex = b.surveyors.Explorer(start=path, find=(0x040287F,), avoid=(0x0402886,), enable_veritesting=True)
    ex.run()
    if ex.found:
            print "found"
            for ss in concated_str:
                print ex.found[0].state.se.any_str(ss)

-重要的是 check function 的參數要固定, hook 的 symbolic symbol 才會放在對的地方

b = angr.Project('./amadhj')
b.hook(0x4026FD, patch_read, length=5)
s = b.factory.blank_state(addr=test_func)
s.regs.rdi = 0x1000 # make sure symbolic symbol at same location

或者是可以直接在 state 裡面放 symbolic symbol 然後讓 check function 的參數指過去，這樣的話 hook function 直接 return 即可

python script

跑約十幾分鐘會有結果

DEBUG   | 2016-06-12 13:11:09,750 | angr.surveyors.explorer | Avoiding path <Path with 738 runs (at 0x402886)>.
DEBUG   | 2016-06-12 13:11:09,752 | angr.surveyors.explorer | Done because we have no active paths left!
found

A PrFURjDMboQJ ScKvoH cDl  BQDqp

angr docs