000.md

debugalyzer

フラグを2文字取ってきて計算する処理があるので、gdbで動かして取ってきて脳死z3で解ける。

import gdb

e = lambda c: gdb.execute(c, to_string=True)
p = lambda x: gdb.parse_and_eval(x)

e('set pagination off')
e('set confirm off')

e('file ./dwarf')
e('b *0x555555555505')
e('b *0x55555555552F')
e('b *0x55555555553B')
e('b *0x555555555576')
e('commands\nsilent\nend')
e('r main')

script = []
script.append('''
from z3 import *

s = Solver()

flag = [BitVec(f'flag_{i}', 8) for i in range(40)]
''')

while True:
    try:
        idx1 = p('$rax')
        e('c')

        idx2 = p('$rax')
        e('c')

        op = p('$edi')
        e('c')

        cl = p('{unsigned char}($rcx+1)')
        cl = int(cl)

        match op:
            case 0:
                script.append(f's.add(flag[{idx1}] + flag[{idx2}] == {cl})')
            case 1:
                script.append(f's.add(flag[{idx1}] - flag[{idx2}] == {cl})')
            case 2:
                script.append(f's.add(flag[{idx1}] * flag[{idx2}] == {cl})')
            case 3:
                script.append(f's.add(flag[{idx1}] ^ flag[{idx2}] == {cl})')
            case _:
                assert 0

        e('c')
    except Exception as e:
        print(e)
        break

script.append('''
assert s.check() == sat
m = s.model()
print(''.join([chr(m[flag[i]].as_long()) for i in range(40)]))
''')

with open('test2.py', 'w') as f:
    f.write('\n'.join(script))

oño

memfd_createしてELFファイルを中で作ってfexecveするというのを中で繰り返している。最初はフラグの先頭8バイトとxorするだけなのでELFヘッダと一致するように考えるとdice{n0wが求められる。

適当にmemfd_createで作成したfdに対してwriteする部分にbreakpointを置いてダンプして次のELFを解析していく。またフラグの8バイトを渡している形なので、単にそのままz3に移植するとdice{n0w_w3r3_cまで求められる。 (envに入っている値は計算しなくてもstraceすると見えるのでそのまま取ってこれる)

from z3 import *

s = Solver()

flag = [BitVec(f'flag_{i}', 8) for i in range(8)]

flag1 = BitVec('flag1', 64)

env = bytearray(b'8940005473485202353')

N = len(env)
r = [BitVec(f'r_{i}', 64) for i in range(N + 1)]
s.add(r[0] == flag1)
for i, c in enumerate(env):
    y = 1337 * r[i]
    if c & 1 != 0:
        y = RotateLeft(r[i], 19)
    s.add(r[i + 1] == y)

s.add(r[-1] == 0xF5B5E8549FA67DB9)
print(s)

assert s.check() == sat
m = s.model()
v = m[flag1].as_long()
print(v.to_bytes(8, 'little'))
print(v)

また次のELFを解析していくと、次のフラグの8バイトが求められる。

from z3 import *

s = Solver()

flag2 = BitVec('flag2', 64)

env = 5508492437801227502

s.add(flag2 % 0x539 != 800)
s.add(0x7E34413175C77CE8 + 0x0D4308F96CA525D5A * flag2 == env)

assert s.check() == sat
m = s.model()
v = m[flag2].as_long()
print(v.to_bytes(8, 'little'))
print(v)

ここまででdice{n0w_w3r3_c0oK1nG_w1まで求められたが、次のELFの解析が少し面倒。残りの文字数からnow were cooking with gas!のleet変換であることが推測できるので、候補はかなり少ない。手で試していたらdice{n0w_w3r3_c0oK1nG_w1tH_g4s!}で通った。

nonograms

手で操作していくとどういう値でxorしているかがwasmを読まなくてもわかる。あとはz3で制約を書いていくだけ。そのままだと候補がいくつも出てくるが、QRコードのパターンを制約として追加してあげると一意に定まる。

import re
from z3 import *
from PIL import Image

init = 0xffff
values = [
    0xc4cf,
    0x899f,
    0x133f,
    0x1b1a,
    0x0b50,
    0x2bc4,
    0x6aec,
    0xe8bc,
    0x1a55,
    0x09ce,
    0x2ef8,
    0x6094,
    0xfc4c,
    0xf899,
    0xf133,
    0xe267,
    0x0b27,
    0x2b2a,
    0x6b30,
    0xeb04,
    0xd609,
    0xac13,
    0x5827,
    0x8d2a,
    0xc29a,
]
values = [v ^ init for v in values]

rows = '''
6d5c(ffff)
e1f4(ffff)
0e05(ffff)
4c83(ffff)
801c(ffff)
9d09(ffff)
d041(ffff)
7680(ffff)
a050(ffff)
2024(ffff)
7a61(ffff)
9c87(ffff)
f321(ffff)
98e0(ffff)
3698(ffff)
ef35(ffff)
5c48(ffff)
86aa(ffff)
80c7(ffff)
05be(ffff)
c22d(ffff)
b6a4(ffff)
f609(ffff)
f01a(ffff)
501a(ffff) 
'''.strip()
check_rows = [
    int(re.match(r'([0-9a-f]+)\(ffff\)', row).group(1), 16)
    for row in rows.split('\n')
]

cols = '''
464f(ffff) c1a4(ffff) c29a(ffff) 210c(ffff) eaf5(ffff) 494e(ffff) d041(ffff) ad51(ffff) 58f2(ffff) 55f0(ffff) 1bbd(ffff) fb91(ffff) d098(ffff) 9af1(ffff) 8384(ffff) af30(ffff) 4a10(ffff) 5eaa(ffff) 9553(ffff) 92ab(ffff) d4b7(ffff) 3249(ffff) d3be(ffff) ffc6(ffff) a050(ffff) 
'''.strip()
check_cols = [
    int(re.match(r'([0-9a-f]+)\(ffff\)', col).group(1), 16)
    for col in cols.split(' ')
]

s = Solver()

answer_rows = [[BitVec(f'answer_rows_{y}_{x}', 16) for x in range(25)] for y in range(25)]
answer_cols = [[BitVec(f'answer_cols_{y}_{x}', 16) for x in range(25)] for y in range(25)]

for y in range(25):
    for x in range(25):
        s.add(Or(answer_rows[y][x] == values[x], answer_rows[y][x] == 0))
        s.add(Or(answer_cols[y][x] == values[y], answer_cols[y][x] == 0))

for y in range(25):
    for x in range(25):
        s.add(Or(
            And(answer_rows[y][x] == 0, answer_cols[y][x] == 0),
            And(answer_rows[y][x] != 0, answer_cols[y][x] != 0)
        ))

for y in range(25):
    calc_x = init
    for x in range(25):
        calc_x ^= answer_rows[y][x]
    s.add(calc_x == check_rows[y])

for x in range(25):
    calc_y = init
    for y in range(25):
        calc_y ^= answer_cols[y][x]
    s.add(calc_y == check_cols[x])

qr_code = '''
xxxxxxx ????????? xxxxxxx
x     x ????????? x     x
x xxx x ????????? x xxx x
x xxx x ????????? x xxx x
x xxx x ????????? x xxx x
x     x ????????? x     x
xxxxxxx ????????? xxxxxxx
        ?????????        
?????????????????????????
?????????????????????????
?????????????????????????
?????????????????????????
?????????????????????????
?????????????????????????
?????????????????????????
?????????????????????????
????????????????xxxxx????
        ????????x   x????
xxxxxxx ????????x x x????
x     x ????????x   x????
x xxx x ????????xxxxx????
x xxx x ?????????????????
x xxx x ?????????????????
x     x ?????????????????
xxxxxxx ?????????????????
'''.strip()
qr_code = [[c for c in row] for row in qr_code.split('\n')]

for y in range(25):
    for x in range(25):
        match qr_code[y][x]:
            case 'x':
                s.add(answer_rows[y][x] != 0)
                s.add(answer_cols[y][x] != 0)
            case ' ':
                s.add(answer_rows[y][x] == 0)
                s.add(answer_cols[y][x] == 0)
            case '?':
                pass
            case _:
                assert 0


assert s.check() == sat
m = s.model()

img = Image.new("L", (25, 25))
pixels = img.load()
for y in range(25):
    for x in range(25):
        try:
            v = m[answer_cols[y][x]].as_long()
            pixels[x, y] = 0 if v != 0 else 255
        except Exception as e:
            print(e)
            pass

img.save("out.png")

dicetok

Rustのバイナリ。strace -fiv -e'!futex,openat,ioctl,fcntl,close,epoll_wait,write' -s 1000000などで観察するとhttp://api.thecatapi.com/v1/images/searchのAPIを叩いているような処理が見える。

コード量が多いが、あやしい部分を探すと、__int64 __fastcall dicetok__load_image____closure__(__int64, _DWORD *, __int64);に以下の比較があることが見える。

この文字列自体は"gangFailAvifk"という見た目になっているが、単にnull終端な文字列ではないので4文字であることを最初にみている。よってここで参照されるのは"gang"。

その文字列があった周辺に"dice"という文字列もあるので、呼び出し元を探すと unsigned __int64 *__fastcall __mut_serde_json__de__Deserializer_R__as_serde__de__Deserializer___deserialize_struct(unsigned __int64 *, unsigned __int64);で比較している処理がある。

JSONのデシリアライザの処理ということはAPIを叩いているところでJSONのkeyを見ていると推測して、以下のような"dice":"gang"を含むレスポンスを返すサーバを立てておいて、/etc/hostsでapi.thecatapi.comの向き先変えてあげるとフラグが表示された。

from flask import Flask, jsonify

app = Flask(__name__)

@app.route('/v1/images/search', methods=['GET'])
def get_images():
    return jsonify([{"id": "106hayhS4", "url": "http://localhost/", "width": 1600, "height": 1303, "dice":"gang"}])

if __name__ == '__main__':
    app.run(debug=True, port=80)

akiym/000.md

debugalyzer

oño

nonograms

dicetok