HackIT CTF 2017 rev200 writeup

問題

Description: You haxor, come on you little sciddie… debug me, eh? You fucking little lamer… You fuckin’ come on, come debug me! I’ll get your ass, you jerk! Oh, you IDA monkey! Fuck all you and your tools! Come on, you scum haxor, you try to reverse me? Come on, you asshole!!

rev200.efiというefiファイルが与えられる。

$ file rev200.efi 
rev200.efi: PE32+ executable (DLL) (EFI application) x86-64 (stripped to external PDB), for MS Windows

解く

シンボル付きのバイナリなので読みやすい。efi_main()を見ると、InitializeLib()でライブラリの初期化とInput()で入力の受け付けを行っているのが分かる。Inputの直後でalgo()をcallしていてあやしい。

algo()を見るとCorrect、Wrongを出力していて、ここで入力値のチェックをしていると分かる。algo()をhopperでデコンパイルすると以下のようになった。

int algo(int arg0) {
    rsp = rsp - 0x180;
    rbp = rsp + 0x80;
    arg_32 = arg0;
    for (arg_-1 = 0x0; arg_-1 <= 0x13; arg_-1 = arg_-1 + 0x1) {
            *(int32_t *)(rbp + sign_extend_32(arg_-1) * 0x4 + 0x90) = *(int8_t *)(arg_32 + sign_extend_64(arg_-1)) & 0xff & 0xff;
    }

    for (arg_-1 = 0x0; arg_-1 <= 0x13; arg_-1 = arg_-1 + 0x1) { // check input
            *(int32_t *)(rbp + sign_extend_32(arg_-1) * 0x4 + 0x90) = (((*(int32_t *)(rbp + sign_extend_32(arg_-1) * 0x4 + 0x90) ^ 0xc) + 0x6 ^ 0xd) + 0x7 ^ 0xe) + 0x8;
            *(int32_t *)(rbp + sign_extend_32(arg_-1) * 0x4 + 0x40) = (((*(int32_t *)(rbp + sign_extend_32(arg_-1) * 0x4 + 0x40) ^ 0xf) + 0x9 ^ 0x10) + 0xa ^ 0x11) + 0xb;
    }

    for (arg_28 = 0x0; arg_28 <= 0x13; arg_28 = arg_28 + 0x1) {
            *(int32_t *)(rbp + sign_extend_32(arg_28) * 0x4 + 0xffffffffffffffa0) = *(int32_t *)(rbp + sign_extend_32(arg_28) * 0x4 + 0x90);
    }

    for (arg_29 = 0x14; arg_29 <= 0x27; arg_29 = arg_29 + 0x1) {
            *(int32_t *)(rbp + sign_extend_64(arg_29 + 0xffffffffffffffec) * 0x4 + 0x40) = *(int8_t *)(arg_32 + sign_extend_64(arg_29)) & 0xff & 0xff;
    }
    for (arg_-1 = 0x14; arg_-1 <= 0x27; arg_-1 = arg_-1 + 0x1) {
            *(int32_t *)(rbp + sign_extend_32(arg_-1) * 0x4 + 0xffffffffffffffa0) = *(int32_t *)(rbp + sign_extend_32(arg_-1 - 0x14) * 0x4 + 0x40);
    }

    if (memcmp(&var_-96, correct, 0xa0) == 0x0) {
            rax = Print(u"\nCorrect\n", correct, 0xa0, r9);
    }
    else {
            rax = Print(u"\nWrong\n", correct, 0xa0, r9);
    }
    return rax;
}

入力値をxorしたあと、memcmpでcorrectと比較している。 総当りで解くsolverを書いた。

# coding: UTF-8

correct = [104, 60, 121, 113, 99, 124, 129, 146, 146, 101, 101, 147, 146, 73, 121, 146, 56, 108, 60, 111, 123, 135, 88, 85, 137, 90, 89, 126, 126, 107, 135, 108, 87, 108, 107, 88, 89, 90, 90, 111];
flag = ""

for i in range(20):
    for j in range(256):
        if ((((((j ^ 0xc) + 6) ^ 0xD) + 7) ^ 0xe) + 8) == correct[i]:
            flag += chr(j)

for i in range(20):
    for j in range(256):
        if (((((j ^ 0xf) + 9) ^ 0x10) + 10) ^ 0x11) + 11 == correct[i+20]:
            flag += chr(j)
   
print(flag)

z3pyを使っても解くことができる

# coding: UTF-8

from z3 import *

FLAG_LENGTH = 40
correct = [104, 60, 121, 113, 99, 124, 129, 146, 146, 101, 101, 147, 146, 73, 121, 146, 56, 108, 60, 111, 123, 135, 88, 85, 137, 90, 89, 126, 126, 107, 135, 108, 87, 108, 107, 88, 89, 90, 90, 111];

s = Solver()
text = []

for i in range(FLAG_LENGTH):
    text.append(BitVec(i, 8))
    s.add(And(text[i] >= 0x20, text[i] < 0x7f)) # in printable ascii

for i in range(20):
    s.add(((((((text[i] ^ 0xC) + 6) ^ 0xD) + 7) ^ 0xE) + 8) == correct[i])

for i in range(20, 40):
    s.add((((((text[i] ^ 0xF) + 9) ^ 0x10) + 10) ^ 0x11) + 11 == correct[i])

if s.check() == sat:
    m = s.model()
    flag = ''
    for i in range(FLAG_LENGTH):
        flag += chr(int(str(m[text[i]])))

    print(flag)

$ python solver.py 
h4ck1t{ff77af3cf8d4e1e67c4300aeb5ba6344}