問題

alpacahack.com

バイナリを実行するとflag?と聞かれ、適当に入力するとWrong...と言われます。

解法

このプログラムでは、forkで生成した子プロセスの動作をptraceで制御しています*1。

子プロセスの処理

入力を受け取り、rdiにセット
call raxでスタック上のint3命令で埋め尽くした領域に飛ぶ

親プロセスの処理無限ループの中で、

子プロセスがint3を踏むのをwaitpidで待ち構える
子プロセスが正常終了していたらCorrect! と出力して終了
子プロセスがrip & 0xff == 0x1fを満たせば、

3.1. raxが期待通りの値になっているか判定

3.2. 判定に失敗したらWrong...と出力して終了
子プロセスのripが指す命令を動的に生成した命令で書き換え、子プロセスの実行を再開させる

親プロセスが生成する命令をデバッガで抽出して逆アセンブルすると以下のようになります。最後の0x7f156432d11fが3. のチェックポイントで、プログラムはここで落ちてしまいます。

0x7f156432d100 lea rsi, [rdi + 0x28]
0x7f156432d104 mov rdx, rdi

0x7f156432d107 mov rcx, rdx
0x7f156432d10a add rdx, 1
0x7f156432d10e mov al, byte [rdx]
0x7f156432d110 imul eax, eax, 0x47
0x7f156432d113 xor byte [rcx], al
0x7f156432d115 add byte [rcx], 0x35
0x7f156432d118 cmp rdx, rsi
0x7f156432d11b jne [rip-0x14]

0x7f156432d107 mov rcx, rdx
0x7f156432d10a add rdx, 1
0x7f156432d10e mov al, byte [rdx]
0x7f156432d110 imul eax, eax, 0x4a
0x7f156432d113 xor byte [rcx], al
0x7f156432d115 add byte [rcx], 0x35
0x7f156432d118 cmp rdx, rsi
0x7f156432d11b jne [rip-0x14]

(中略)

0x7f156432d107 mov rcx, rdx
0x7f156432d10a add rdx, 1
0x7f156432d10e mov al, byte [rdx]
0x7f156432d110 imul eax, eax, 0xffffffbc
0x7f156432d113 xor byte [rcx], al
0x7f156432d115 add byte [rcx], 0x35
0x7f156432d118 cmp rdx, rsi
0x7f156432d11b jne [rip-0x14]

0x7f156432d11d mov eax, dword [rdi]
0x7f156432d11f imul eax, eax, 0xdeadbeef

疑似コードにするとこんな感じです。

for (int i = 0; i < 0x28; i++) {
    int m = (int)((signed byte)(0x47 + 3*i));
    byte v = input[i+1] * m;
    input[i] = (input[i] xor v) + 0x35;
}
// このraxを親が覗き見て判定
int rax = (inputの最初の4byte) * 0xdeadbeef;

親による判定はcmp命令でなされるので、ブレークポイントを貼れば目標とするraxの値は分かります。さらにz3などで逆算*2するとinputの最初の5byteが分かり*3、これをflagとしてもう一度実行すればコードの続きを見ることができます。

0x7f156432d11f imul eax, eax, 0xdeadbeef
0x7f156432d125 add rdi, 4
0x7f156432d129 cmp rdi, rsi
0x7f156432d12c jne [rip-0xe]
0x7f156432d11d mov eax, dword [rdi]
0x7f156432d11f imul eax, eax, 0xdf6ebedd

今度はinputの次の4byteを使って同様の判定をしているようなので、先程と同様にしてinputの最初の9byteが計算できます。これを繰り返せばflagが分かります。*4

最初の9byteを割り出すコード

radare2を使っています。 radare2 python scripting - r2wiki

solve.py

import r2pipe
import z3

def run():
    r = r2pipe.open(filename="silver")
    r.cmd('e dbg.profile=script.rr2')

    r.cmd("aaa")
    r.cmd("ood")
    r.cmd("dko 17 cont") 
    r.cmd('e log.level=1')
    r.cmd("dcu main+35") # after fork
    cmds = []
    while True:
        r.cmd("dcu main+921") # got rip
        rip = int(r.cmd("dr rax").strip(), base=16) - 1
        print(hex(rip))
        if rip == 0xffffffffffffffd9:
            break
        r.cmd("dcu main+1077") # calculated next op
        op = int(r.cmd("dr rax").strip(), base=16).to_bytes(8, "little").hex()
        cmd = r.cmd(f"!rasm2 -d {op}").splitlines()[0]
        print(f"cmd: {cmd}")
        cmds.append((rip, cmd))

        if rip & 0xff == 0x1f:
            r.cmd("dcu main+820") # cmp rdx, rax
            rdx = r.cmd("dr rdx").split()
            rax = r.cmd("dr rax").split()
            print(f"checking if target:{rdx} == rax:{rax}")

    for r, c in cmds:
        print(hex(r), c)

def solve():
    targets = [0x66993576, 0x3bd23991]
    xs = [z3.BitVec(f"n{i}", 32) for i in range(len(targets))]
    
    solver = z3.Solver()
    solver.add((xs[0] * 0xdeadbeef) == targets[0])
    solver.add((xs[1] * 0xdf6ebedd) == targets[1])

    solver.check()
    s = [(solver.model()[xs[i]].as_long()) for i in range(len(targets))]

    target = bytes()
    for t in s:
        target += t.to_bytes(4, "little")
    print(target.hex())

    muls = (list(range(0x47,0x7d+1,3)) + list(range(0xffffff80, 0xffffffbc+1, 3)))
    xs = [z3.BitVec(f"n{i}", 8) for i in range(len(target)+1)]
    solver = z3.Solver()
    for i in range(len(target)):
        v = ((xs[i] ^ ((xs[i+1] * muls[i]) )) + 0x35)
        print(v)
        solver.add(v == target[i])
    solver.check()
    m = solver.model()
    ans = bytes([(m[xs[i]].as_long()) for i in range(len(target)+1)])
    with open("stdin", "wb") as f:
        f.write(ans + b"a" * 0x32)
    print(solver.model())

solve()
run()

script.rr2

#!/usr/bin/rarun2
program=./silver
stdin=./stdin

*1:子プロセスのint3によるSIGTRAPを親プロセスが捕捉する仕組みについてはman ptrace(2)のSignal-delivery-stopの箇所などが詳しいです。

*2:自分で計算するなら、拡張GCDでx * 0xdeadbeef ≡ rax (mod 2³²) を満たすxを求めて、適当にinput[4]を決め打ちした上で input[0..=3] = x となるinput[0..=3]を求めることになります（多分）。

*3:条件を満たす5byteは複数あるので、ここで逆算した結果がflagの最初の5byteに一致するとは限りません。

*4:flagが2000byteとかあったらこの作業を500回繰り返す必要があって腕が破綻するので、もうちょっと賢いやり方があるかもしれない

めもなみ

Everything Silver writeup [AlpacaHack Round 4(Rev)]

問題

解法

最初の9byteを割り出すコード