AlpacaHack Round 8 (Rev) writeup

000.md

masking tape

デコンパイル結果を持ってきてブルートフォース。

enc1 = [0x08, 0x23, 0x03, 0x03, 0x13, 0x03, 0x13, 0x03, 0x01, 0x23, 0x31, 0x13, 0x11, 0xC8, 0x03, 0xC8, 0x03, 0x13, 0x01, 0xC8, 0x13, 0x13, 0x03, 0x13, 0x13, 0x11, 0x13, 0x23, 0x00, 0x00, 0x00, 0x00]
enc2 = [0x02, 0x40, 0x80, 0x08, 0x08, 0x08, 0xC8, 0xC8, 0x80, 0x88, 0x08, 0x80, 0x88, 0x32, 0x08, 0x32, 0x80, 0x80, 0x80, 0x32, 0x08, 0x80, 0x08, 0x08, 0x48, 0x88, 0x80, 0xC8, 0x00]

flag = ''
for i in range(100):
    for C in range(0x20, 0x7f):
        c = ((C >> 5) | (8 * C))
        if (c & 1) != 0:
            v1 = c & 0x33
            v2 = c & 0xCC
        else:
            v1 = c & 0xCC
            v2 = c & 0x33
        if enc1[i] == v1 and enc2[i] == v2:
            print(C)
            flag += chr(C)
            print(flag)
            break
    else:
        assert 0
print(flag)

hidden

0x1272のデコンパイル結果をみるとおかしいことに気づく。0で初期化されている変数は関数内では値が変わらないので、定数との比較となってデッドコードと判定されデコンパイル結果から消されているが、実は0x124F, 0x122C, 0x1209ではスタックを超えて書き込むというちょっとした解析妨害がされている。

__int64 __fastcall sub_1272(int c, _DWORD *key)
{
  var_c_sub_124F(__ROL4__(*key, 5) + __ROR4__(key[1], 3));
  var_8_sub_122C((unsigned int)(__ROR4__(key[2], 3) - __ROL4__(key[3], 5)));
  var_4_sub_1209(c);
  *key ^= __ROR4__(0, 13);
  key[1] ^= __ROR4__(0, 15);
  key[2] ^= __ROL4__(0, 13);
  key[3] ^= __ROL4__(0, 11);
  return 0LL;
}

最終的にxorしたものと比較しているので、そのまま戻せる。flagの文字の最下位ビットが立っているかどうかで処理を変えるので、cの値は手で実行しながら埋めた。

from pwn import *

cmp = [0xDC, 0x86, 0x1A, 0x9A, 0xDD, 0x93, 0x9B, 0x35, 0xD3, 0x74, 0xDA, 0xEE, 0xE8, 0x5A, 0x3C, 0xC5, 0x1C, 0x64, 0x33, 0x47, 0xD2, 0x3B, 0x28, 0xF3, 0xCC, 0x5A, 0x48, 0x8B, 0x74, 0x0C, 0x4B, 0x87, 0x38, 0xD6, 0x80, 0x40, 0x51, 0xE6, 0x4A, 0x27, 0xA1, 0x73, 0x52, 0x0F, 0x93, 0x06, 0x54, 0x3D, 0x65, 0x13, 0xFB, 0xC8, 0x65, 0xAF, 0xD2, 0x67, 0xB3, 0x09, 0xEF, 0x7D, 0x23, 0xA6, 0x76, 0xE5, 0x13, 0x10, 0x13, 0xFF, 0x34, 0x8D, 0xAE, 0xD0, 0x9C, 0x2C, 0x4D, 0xF3, 0xA1, 0xBC, 0x46, 0x2F, 0x98, 0x87, 0xB6, 0x57, 0x1A, 0xA2, 0x17, 0xF1, 0xF0, 0xE5, 0xB0, 0xBA, 0x9B, 0x6D, 0xB5, 0xA7, 0xAC, 0x6A, 0x5E, 0xAC, 0xE8, 0xF6, 0x90, 0xD8, 0xB0, 0xA2, 0x99, 0x91]

key = bytearray(b'AlpacaHackRound8')

rol = lambda val, r_bits, max_bits: \
    (val << r_bits%max_bits) & (2**max_bits-1) | \
    ((val & (2**max_bits-1)) >> (max_bits-(r_bits%max_bits)))
ror = lambda val, r_bits, max_bits: \
    ((val & (2**max_bits-1)) >> r_bits%max_bits) | \
    (val << (max_bits-(r_bits%max_bits)) & (2**max_bits-1))

flag = b''

key0 = u32(key[0:4])
key1 = u32(key[4:8])
key2 = u32(key[8:12])
key3 = u32(key[12:16])

c = [0,1,1,0,0,0,0,0,0,1,1,1,1,1,1,1,1,0,0,1,0,0,0,1,0,0,0]

for i in range(len(c)):
    var_c = (rol(key0, 5, 32) + ror(key1, 3, 32)) & 0xffffffff
    var_8 = (ror(key2, 3, 32) - rol(key3, 5, 32)) & 0xffffffff
    var_4 = 0 ^ var_c ^ var_8
    # print(f'{var_c=:x}')
    # print(f'{var_8=:x}')
    # print(f'{var_4=:x}')

    # if var_4 & 1 == 0:
    if c[i] & 1 == 0:
        key0 ^= ror(var_8, 0xd, 32)
        key1 ^= ror(var_8, 0xf, 32)
        key2 ^= rol(var_c, 0xd, 32)
        key3 ^= rol(var_c, 0xb, 32)
    else:
        key0 ^= rol(var_8, 0xb, 32)
        key1 ^= rol(var_8, 0xd, 32)
        key2 ^= ror(var_c, 0xf, 32)
        key3 ^= ror(var_c, 0xd, 32)
    # print(f'{key0=:x}')
    # print(f'{key1=:x}')
    # print(f'{key2=:x}')
    # print(f'{key3=:x}')

    x = u32(bytes(cmp[i*4:i*4+4])) ^ var_4
    flag += x.to_bytes(4, 'little')
    print(flag)

vcipher

4バイトずつ比較されることはわかるので、flagの入力がどう比較されるかを観察すると、以下のように4ビット分ずらした上で1バイトずつ変化するのが見える。

0番目 -> ?????xx?
1番目 -> ???xx???
2番目 -> ?xx?????
3番目 -> x??????x

よって1バイトずつブルートフォースできる。実行は遅いが放置していると出てくる(こういうときに並列で回せるテンプレートを用意しておけると便利そうではある)。

import gdb

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

ror = lambda val, r_bits, max_bits: \
    ((val & (2**max_bits-1)) >> r_bits%max_bits) | \
    (val << (max_bits-(r_bits%max_bits)) & (2**max_bits-1))

correct_output = [0x345A7191, 0xDCC4950A, 0x8AD73F4E, 0x6006DEEE, 0xB474F6A4, 0x9620574D, 0x7FBA5668, 0x45CB397E]

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

e('file ./vcipher')
e('b *0x00005555555579ea')
e('commands\nsilent\nend')

flag = b'Alpaca{'

for i in range(100):
    for c in range(0x21, 0x7f):
        with open('in', 'wb') as f:
            f.write((flag + bytes([c])).ljust(32, b'A'))
        e('r < in')
        i = (len(flag)) // 4
        j = (len(flag)) % 4
        #print(i, j)
        for _ in range(i):
            e('c')
        rax = ror(p('$rax'), 4, 32)
        v = rax >> 8*j & 0xff
        output = ror(correct_output[i], 4, 32)
        output = output >> 8*j & 0xff
        # print(hex(v), hex(output))
        if v == output:
            flag += bytes([c])
            print(flag)
            break
    else:
        assert 0

subway

読んでいくと0と0x80000000でビットを表現して何かしら演算しているのがわかる。以下の流れで処理される。

• 0x159D: 入力をビットに変換
• 0x20FE: xを入力の4バイト分ずつとして(x * 0x215ABF3) ^ 0x856afcbfを計算する
• 0x167A: ごちゃごちゃ足したり引いたりする
• 0x21B1: 計算結果の比較

0x21B1での比較では、mulssの結果がそれぞれ0になるように選べばよい。ここは面倒なので動的にgdb scriptで求めた。

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 ./subway')
e('b *0x5555555561dd')
e('commands\nsilent\nend')
flag = 'AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA'
e(f'r {flag}')

b = []
bits = ''
for i in range(11):
    for j in range(32):
        # print(i, j)
        v = p('$xmm1.uint128')
        e('ni')
        result = p('$xmm1.uint128')
        if result == 0:
            bits = ('1' if v == 0 else '0') + bits
        else:
            bits = ('0' if v == 0 else '1') + bits
        if len(bits) == 8:
            b.append(bits)
            bits = ''
        e('c')
print(b)

あとは0x167Aのデコンパイル結果を持ってきてz3に投げる。

from z3 import *

s = Solver()

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

a1 = [BitVec(f'a1_{i}', 32) for i in range(11)]
v2 = [BitVec(f'v2_{i}', 32) for i in range(11)]

for i in range(11):
    a1[i] = (flag[i] * 0x215ABF3) ^ 0x856afcbf

def z_add(a, b):
    return a + b

def z_sub(a, b):
    return a - b

v2[0] = a1[0]
v2[1] = a1[1]
v2[2] = a1[2]
v2[3] = a1[3]
v2[4] = a1[4]
v2[5] = a1[5]
v2[6] = a1[6]
v2[7] = a1[7]
v2[8] = a1[8]
v3 = a1[9]
v2[9] = v3
v4 = a1[10]
v2[10] = v4
v2[9] = z_sub(v3, v4)
v2[10] = z_sub(v2[10], v2[5])
v2[9] = z_add(v2[9], v2[7])
v2[2] = z_add(v2[2], v2[4])
v2[1] = z_sub(v2[1], v2[4])
v2[4] = z_add(v2[4], v2[0])
v5 = z_add(v2[0], v2[8])
v2[0] = v5
v2[4] = z_sub(v2[4], v5)
v6 = z_add(v2[2], v2[0])
v2[2] = v6
v2[2] = z_sub(v6, v2[7])
v2[9] = z_sub(v2[9], v2[8])
v7 = z_add(v2[10], v2[6])
v2[10] = v7
v2[10] = z_add(v7, v2[9])
v2[5] = z_sub(v2[5], v2[6])
v2[1] = z_add(v2[1], v2[6])
v2[10] = z_sub(v2[10], v2[5])
v2[3] = z_add(v2[3], v2[8])
v2[7] = z_add(v2[7], v2[1])
v2[1] = z_sub(v2[1], v2[5])
v2[4] = z_sub(v2[4], v2[2])
v2[10] = z_add(v2[10], v2[0])
v2[5] = z_sub(v2[5], v2[8])
v2[10] = z_add(v2[10], v2[6])
v2[9] = z_sub(v2[9], v2[5])
v8 = z_sub(v2[3], v2[7])
v2[3] = v8
v2[3] = z_add(v8, v2[6])
v9 = z_add(v2[1], v2[7])
v2[1] = v9
v2[1] = z_add(v9, v2[9])
v2[3] = z_add(v2[3], v2[5])
v2[4] = z_sub(v2[4], v2[6])
v2[7] = z_sub(v2[7], v2[1])
v2[10] = z_sub(v2[10], v2[6])
v2[9] = z_sub(v2[9], v2[8])
v2[1] = z_sub(v2[1], v2[8])
v2[3] = z_sub(v2[3], v2[0])
v2[0] = z_sub(v2[0], v2[8])
v2[4] = z_sub(v2[4], v2[8])
v10 = z_add(v2[9], v2[7])
v2[9] = v10
v2[9] = z_add(v10, v2[5])
v2[0] = z_add(v2[0], v2[5])
v2[8] = z_sub(v2[8], v2[5])
v2[5] = z_add(v2[5], v2[6])
v11 = z_add(v2[0], v2[6])
v2[0] = v11
v2[0] = z_sub(v11, v2[6])
v2[4] = z_add(v2[4], v2[9])
v2[8] = z_add(v2[8], v2[10])
v2[6] = z_add(v2[6], v2[5])
v2[0] = z_add(v2[0], v2[7])
v2[8] = z_sub(v2[8], v2[3])
v2[0] = z_add(v2[0], v2[2])
v2[4] = z_sub(v2[4], v2[1])
v2[7] = z_add(v2[7], v2[1])
v12 = z_add(v2[4], v2[3])
v2[4] = v12
v2[8] = z_add(v2[8], v12)
v2[7] = z_sub(v2[7], v2[5])
v2[8] = z_sub(v2[8], v2[3])
v2[9] = z_add(v2[9], v2[4])
v2[4] = z_add(v2[4], v2[0])
v2[8] = z_sub(v2[8], v2[9])
v2[1] = z_add(v2[1], v2[9])
v2[5] = z_add(v2[5], v2[3])
v2[4] = z_add(v2[4], v2[8])
v2[7] = z_sub(v2[7], v2[9])
v2[8] = z_add(v2[8], v2[1])
v2[10] = z_sub(v2[10], v2[6])
v2[0] = z_sub(v2[0], v2[3])
v2[3] = z_sub(v2[3], v2[6])
v2[0] = z_sub(v2[0], v2[5])
v2[10] = z_sub(v2[10], v2[4])
v2[7] = z_sub(v2[7], v2[8])
v2[10] = z_add(v2[10], v2[6])
v2[1] = z_sub(v2[1], v2[6])
v2[4] = z_add(v2[4], v2[2])
v2[7] = z_sub(v2[7], v2[3])
v2[4] = z_sub(v2[4], v2[6])
v2[6] = z_sub(v2[6], v2[5])
v2[2] = z_sub(v2[2], v2[3])
v2[4] = z_add(v2[4], v2[6])
v2[9] = z_sub(v2[9], v2[7])
v2[8] = z_sub(v2[8], v2[3])
v2[5] = z_add(v2[5], v2[0])
v2[9] = z_add(v2[9], v2[1])
v2[4] = z_sub(v2[4], v2[10])
v2[0] = z_sub(v2[0], v2[3])
v13 = z_add(v2[2], v2[6])
v2[2] = v13
v2[2] = z_add(v13, v2[4])
v2[3] = z_sub(v2[3], v2[0])
v2[2] = z_sub(v2[2], v2[9])
v2[0] = z_add(v2[0], v2[8])
v14 = z_sub(v2[9], v2[6])
v2[9] = v14
v2[9] = z_sub(v14, v2[2])
v2[5] = z_sub(v2[5], v2[6])
v15 = z_add(v2[0], v2[2])
v2[0] = v15
v2[3] = z_sub(v2[3], v15)
v16 = z_add(v2[7], v2[4])
v2[7] = v16
v2[0] = z_add(v2[0], v16)
v2[3] = z_add(v2[3], v2[4])
v2[5] = z_add(v2[5], v2[10])
v2[10] = z_add(v2[10], v2[0])
v2[1] = z_sub(v2[1], v2[3])
v17 = z_sub(v2[2], v2[3])
v2[2] = v17
v2[2] = z_add(v17, v2[4])
v18 = z_sub(v2[0], v2[9])
v2[0] = v18
v2[0] = z_sub(v18, v2[4])
v2[10] = z_sub(v2[10], v2[4])
v2[6] = z_add(v2[6], v2[0])
v19 = z_add(v2[4], v2[3])
v2[4] = v19
v2[8] = z_sub(v2[8], v19)
v2[1] = z_add(v2[1], v2[0])
v2[9] = z_add(v2[9], v2[6])
v2[3] = z_sub(v2[3], v2[2])
v2[9] = z_add(v2[9], v2[2])
v2[2] = z_add(v2[2], v2[5])
v2[8] = z_sub(v2[8], v2[5])
v2[0] = z_add(v2[0], v2[9])
v2[6] = z_sub(v2[6], v2[5])
v2[1] = z_sub(v2[1], v2[9])
v2[5] = z_sub(v2[5], v2[7])
v2[4] = z_add(v2[4], v2[7])
v2[7] = z_add(v2[7], v2[2])
v2[8] = z_add(v2[8], v2[0])
v2[0] = z_add(v2[0], v2[4])
v20 = z_add(v2[5], v2[1])
v2[5] = v20
v2[5] = z_add(v20, v2[6])
v21 = z_add(v2[4], v2[8])
v2[4] = v21
v22 = z_add(v2[0], v21)
v2[0] = v22
v2[6] = z_add(v2[6], v22)
v2[0] = z_add(v2[0], v2[7])
v23 = z_add(v2[4], v2[9])
v2[4] = v23
v2[4] = z_sub(v23, v2[7])
v2[9] = z_sub(v2[9], v2[2])
v2[0] = z_sub(v2[0], v2[3])
v2[10] = z_sub(v2[10], v2[5])
v2[0] = z_sub(v2[0], v2[4])
v2[7] = z_sub(v2[7], v2[1])
v24 = z_add(v2[3], v2[0])
v2[3] = v24
v25 = z_add(v24, v2[6])
v2[3] = v25
v2[3] = z_add(v25, v2[4])
v2[6] = z_sub(v2[6], v2[10])
v26 = z_sub(v2[3], v2[7])
v2[3] = v26
v2[3] = z_add(v26, v2[0])
v2[8] = z_add(v2[8], v2[7])
v2[4] = z_add(v2[4], v2[0])
v2[8] = z_add(v2[8], v2[3])
v2[4] = z_add(v2[4], v2[6])
v2[1] = z_sub(v2[1], v2[0])
v2[2] = z_sub(v2[2], v2[9])
v2[7] = z_add(v2[7], v2[8])
v2[1] = z_sub(v2[1], v2[8])
v2[4] = z_sub(v2[4], v2[8])

x = ['10111000', '01001001', '01110111', '11011001', '10101000', '10100001', '10011000', '01010001', '11000000', '01000010', '00000000', '11000001', '01100100', '11001001', '11001001', '10011010', '11010100', '01010101', '11011111', '01100110', '01101100', '11001000', '00101011', '11100111', '01011001', '11110000', '00011001', '00101011', '10011101', '00110010', '11110011', '00101001', '01001101', '11101100', '10111000', '11011011', '01001000', '11110000', '10101010', '10101001', '11111111', '11111111', '00000101', '01100111']
for i in range(11):
    for j in range(4):
        bits = x[4*i+j]
        s.add(v2[i]>>(8*j) & 0xff == int(bits, 2))

assert s.check() == sat
m = s.model()
f = b''
for i in range(11):
    f += m[flag[i]].as_long().to_bytes(4, 'little')
print(f)