Global Cyber Skills Benchmark 2025 Operation Blackout 紹介 + ShadowLabyrinth 問題 Writeup

概要

• Hack The Box 社主催の CTF イベント Global Cyber Skills Benchmark 2025 Operation Blackout で、弊社チームは全体 43 位、日本国内 4 位の成績を収めました。
• 本記事では Reversing ジャンル最難関の ShadowLabyrinth 問題を解説します。(amd64 ELF + 独自 VM コード)

はじめに

こんにちは、研究開発部の末廣です。Hach The Box 社主催の CTF イベント Global Cyber Skills Benchmark 2025 Operation Blackout ¹に、 NFLabs. 社員およびインターン生で参加しました。メンバー間で知恵を出し合い、協力した結果、全 103 フラグ中 80 フラグを獲得でき、全 796 チーム中全体 43 位、日本国内 4 位の成績を収めました。

当社のエンジニアとインターン生16名が #HackTheBox Global Cyber Skills Benchmark 2025 に挑戦し、103フラグのうち 80フラグを獲得し、成績は796チーム中43位（国内4位）でした🚩
全16ジャンルに幅広く取り組み、4ジャンルで完答しました。当社は今後も #CTF に挑戦し、スキルを磨いていきます。 pic.twitter.com/BaeiJMzdw5

— エヌ・エフ・ラボラトリーズ (@NFLaboratories) June 4, 2025

本記事では私が解いた問題のうち、最も正解チーム数が少ない問題を解説します。

コンテストの特徴

本コンテストは、 Hack The Box 社が毎年開催している企業対抗の CTF です。昨年までは HTB Business CTF 2024² という名称でした。今年から Global Cyber Skills Benchmark に名称が変化しました。

本コンテストの特徴として、企業対抗という点があります。コンテスト参加者は会社のメールアドレスで認証して、各会社のチームへ参加します。

コンテストの出題内容

コンテストの開催期間は 2025/05/23(金) 22:00 ～ 2025/05/27(火) 22:00 (JST) の、土日をまるまる含む 4 日間にわたる開催です。特筆すべきは扱うジャンルの幅広さで、次の全 16 ジャンルが出題されました。

• Fullpwn
• Web
• Pwn
• Crypto
• Reversing
• Forensics
• Coding
• Mobile
• OSINT
• Blockchain
• Hardware
• Cloud
• ICS
• ML
• AI
• Secure Coding

各ジャンルで 1 ～ 5 個の問題が出題されており、合計 66 問あります。この中の Fullpwn ジャンルはいわゆる Boot2Root 系のペネトレーションテスト系の問題で、全 4 問それぞれで user 権限用のフラグと root 権限用のフラグの 合計 2 個が設定されています。また Forensics ジャンルでは全 5 問それぞれで攻撃の痕跡が残ったファイルが与えられ、各ファイルから 5 ～ 10 個の指定された痕跡を探す内容です。コンテスト全体として合計 103 個もののフラグが設定されています。

コンテスト終了後に公式 Writeup³ が GitHub で公開されており、本記事執筆時点では 12 ジャンルの問題が解説されています。コンテスト時に配布されたファイルは GitHub では含まれていませんが、公式の解説を一読いただけると、本コンテストの特色等を御理解いただけると思います。

[Reversing] ShadowLabyrinth [hard]

Reversing ジャンルの中で最難関の問題です。コンテスト終了時点での正確な正解チーム数は分かりませんが、終了後のスコアボードから閲覧できる上位 100 チームの正解問題内容を調べると、本問題の正解チーム数は 20 チームほどのようです。

次の 2 個のファイルが与えられます。

1. shadow_labyrinth: amd64 の ELF 実行形式。後述するように file.bin 内容を復号して、独自 VM コードとして実行する機能を持ちます。
2. file.bin: 暗号化された独自 VM コード。

本問題は、いわゆるフラグチェッカー問題です。shadow_labyrinth バイナリを実行すると文字列を入力でき、正しいフラグか誤っているかを出力する機能を持ちます。

正しいフラグを求めるために、 shadow_labyrinth バイナリの処理を読み解いていきました。

main 関数の内容把握

shadow_labyrinth バイナリの main 関数の内容は次のような内容です。

int main()
{
  char input[104]; // [rsp+0h] [rbp-78h] BYREF
  unsigned __int64 canary; // [rsp+68h] [rbp-10h]

  canary = __readfsqword(0x28u);
  memset(input, 0, 90);
  puts("[Central Command Node]: Motion triggered! Labyrinth entrance...");
  fgets(input, 89, stdin);
  if ( strlen(input) == 88 )
  {
    if ( input[0] == 'H' || input[1] == 'T' || input[2] == 'B' || input[3] == '{' || input[87] == '}' )
    {
      input[87] = 0;
      CheckInputAndWriteResult(&input[4]);
      return 0;
    }
    puts("Invalid flag.");
  }
  else
  {
    puts("Invalid flag length.");
  }
  return 1;
}

次のことを行います。

• 入力が 88 文字であることを検証。
• 入力が HTB{ から始まり } で終わるようなことを検証。
  • 各種条件が || 演算子で判定されているため、実際は検証している文字 5 個のうち 1 箇所でも適合すれば、後続の判定処理を行います。しかし本コンテンストのフラグフォーマットは HTB{ で始まり } で終わる形式で統一されているため、おそらく当該条件は && 演算子で判定することが本来意図と思われます。
• 上記 2 つ両方の検証が通った場合に、 RVA 0x1660 の関数でフラグ文字列の波括弧 {} 内部の 83 文字を検証します。

フラグ波括弧内部の先頭 48 文字の解明

shadow_labyrinth バイナリの RVA 0x1660 の関数では、次の 3 つの処理行います。

1. フラグ波括弧内部のうち先頭 48 文字の内容を検証
2. file.bin 内容を読み込み、その検証済みの 48 文字の内容を使って復号
3. 復号結果を独自 VM コードとして実行し、フラグ波括弧内部のうち残りの 35 文字を検証

先頭 48 文字検証処理は次の内容です。

1. .rodata セクションにある配列の内容を使って 48 文字を入れ替え。 S-box を使って実現しています。
2. 48 文字並び替え後の内容について 4 文字ごとに、「各種文字 * 配列由来の係数」の総和が「別の配列由来の内容」であることを検証。

各種配列の内容は固定であるため、静的解析ツールで抽出できます。後は上記検証を突破する 48 文字の入力を求める必要があります。今回は SMT solver である z3⁴ を使って求解しました。

#!/usr/bin/env python3


import pwn
import z3


def parse_as_qword_array(hex_data: str, sign: str) -> list[int]:
    b = bytes.fromhex(hex_data)
    assert len(b) % 8 == 0
    result = []
    for i in range(len(b) // 8):
        result.append(pwn.u64(b[8 * i : 8 * (i + 1)], endianness="little", sign=sign))
    return result


def parse_as_dword_array(hex_data: str) -> list[int]:
    b = bytes.fromhex(hex_data)
    assert len(b) % 4 == 0
    result = []
    for i in range(len(b) // 4):
        result.append(
            pwn.u32(b[4 * i : 4 * (i + 1)], endianness="little", sign="signed")
        )
    return result


solver = z3.Solver()
flag_total_list_symbol = [z3.BitVec(f"flag_{i:02d}", 8) for i in range(88)]
for f in flag_total_list_symbol:
    solver.add(f >= 0x20)
    solver.add(f < 0x7F)
solver.add(flag_total_list_symbol[0] == ord("H"))
solver.add(flag_total_list_symbol[1] == ord("T"))
solver.add(flag_total_list_symbol[2] == ord("B"))
solver.add(flag_total_list_symbol[3] == ord("{"))
solver.add(flag_total_list_symbol[87] == ord("}"))

flag_core_list_symbol = flag_total_list_symbol[4:-1]

sbox_list = bytes.fromhex(
    "10 19 20 05 00 2D 26 02 0E 28 18 11 07 21 17 1D 27 0F 23 15 2E 1A 13 2F 2B 14 0D 1F 01 16 2C 2A 1E 08 22 0B 12 1B 0C 09 29 24 04 1C 03 06 25 0A"
)
assert len(sbox_list) == 48
assert len(set(sbox_list)) == 48

flag_sboxed_list_symbol = [
    flag_core_list_symbol[sbox_list[i]] for i in range(len(sbox_list))
]

multiplier_list = parse_as_qword_array(
    "92 34 D1 97 80 B7 0D C3 3A FB 54 5E 48 48 31 41 8D A4 B9 67 F5 8D 96 B6 92 BC 64 79 91 C5 62 88 07 64 D6 68 40 F9 92 4A 07 F8 47 3A 0B A6 1F EB 91 3A 6F 0C 3B 3A DB 32 F3 3A 82 6E FC 4C 29 CA 8B 83 BD 6C F0 96 29 5E 96 15 0E CE 3C F7 BC 95 B5 C8 C9 B4 94 1B 24 E4 97 5F C5 12 B2 9F 51 5A 53 CA E7 E8 E8 F8 04 19 F6 18 9F 53 B8 61 3E 57 1A EC 33 73 B3 13 8B 81 38 8C 62 5A CF 5F EC 52 9B 45 62 16 F6 B6 EE FA 0E 6B 47 18 25 46 16 F8 9B FC D9 23 EC 26 3A D0 1B 90 2E F9 FD C2 2D FC 5B 74 C7 2B A4 B6 C0 B8 8F A5 FF F8 38 A1 F1 6B 8D 48 01 1C FC B1 6E 66 75 E9 AB 4E EB AB 6A FD F8 FF 13 A6 48 26 B6 7D 6C 14 F3 7D 2C 79 15 56 0C B8 8E 46 EB 3A 70 5F EF 2F D7 73 F1 4C C3 E6 4F 3E 1F E4 DF 67 08 A8 68 4D A3 9B 7C 8D 16 B7 37 A8 73 3E AE 7B 39 44 A5 8E 3B B3 7C 7A 7B 22 83 B0 0E 05 B0 F5 E6 A3 BB 8E DF CD 8E C5 C0 3A 93 9B F7 CE 21 A6 83 C4 51 4B BF 02 25 CA 21 95 BF E0 67 E5 42 40 55 11 5E D5 9C A6 BB 51 C5 1B 4D 48 09 0A B6 5A 01 13 0B 58 48 AE AB EF 1A C4 C7 8E 79 DD 93 68 57 BB 89 A6 7C 77 08 C9 F5 FA B8 48 A3 07 16 48 07 E7 3E BF 8A D2 99 77 C5 70 C6 DD EF A9 3A 33 8F 3A E4 9E E4 44 F0 2B AC F9 44 3B E1 67 D0 13 72 CA 18 7F B2 4B F9 92 33 33",
    sign="signed",
)
assert len(multiplier_list) == 48
expected_sum_list = parse_as_qword_array(
    "79 53 8A 8D CD 9A 93 B8 DF 35 4B B4 31 81 DC B2 83 1B 41 89 37 F9 87 92 B8 27 61 8B 32 26 7C 93 DB AD 76 81 B3 85 65 A3 D2 62 A3 B4 0E CF 88 AA 87 AA 5A 69 CD 5A 88 70 7C 69 16 5C F8 38 7D 8E 0A 6F 8A BC 36 01 87 1C 1A 02 F0 97 2A 0C 05 B7 12 EF 73 27 65 C5 B7 23 FC EC 3C 4D 75 F2 E4 6A",
    sign="unsigned",
)
assert len(expected_sum_list) == 12

for i in range(len(expected_sum_list)):
    total = 0
    for j in range(4):
        indexInner = i * 4 + j
        total += (
            z3.ZeroExt(64, flag_sboxed_list_symbol[indexInner])
            * multiplier_list[indexInner]
        )
    # 求解にはこのビット積が重要でした
    solver.add((total & 0xFFFFFFFF_FFFFFFFF) == expected_sum_list[i])

# フラグの残り35文字はVMで判断
for i in range(48, len(flag_core_list_symbol)):
    solver.add(flag_core_list_symbol[i] == ord("?"))

if solver.check() == z3.sat:
    model = solver.model()
    for f in flag_total_list_symbol:
        print(chr(model[f].as_long()), end="")
    print()

実行すると 20 秒ほどで HTB{by_4dd1ng_nd_multiply1ng_w3_pl4y_4_l1ttl3_m3l0dy???????????????????????????????????} の結果を得られます。目的の、波括弧内部先頭 48 文字が by_4dd1ng_nd_multiply1ng_w3_pl4y_4_l1ttl3_m3l0dy であることを求められました。

復号後の独自 VM コード内容をダンプ

shadow_labyrinth バイナリの RVA 0x1724 から、上で求めた波括弧内部先頭 48 文字の内容を使って file.bin 内容を復号します。復号は次の手順で行います。

1. 波括弧内部の 33～48 文字目を使ってマルチバイト XOR。
2. 波括弧内部の 1～32 文字目を鍵、固定配列内容を IV とする AES256-CBC で復号。
3. zlib の uncompress 関数を使って伸長。

file.bin 復号後内容を取得する方法として、今回は gdb コマンドによるデバッグを使いました。次の手順で復号後内容を vmcode.bin として保存します。

1. gdb shadow_labyrinth で起動。
2. break uncompress コマンドで uncompress 関数呼び出し時にブレークするよう設定。
3. run コマンドでデバッグ実行開始。
4. 入力として、上で求めた HTB{by_4dd1ng_nd_multiply1ng_w3_pl4y_4_l1ttl3_m3l0dy???????????????????????????????????} を設定。
5. uncompress 関数でブレークするので、 finish コマンドで uncompress 関数から戻るまで実行継続。
6. 復号後内容を含む VM 実行状態構造体の先頭アドレスが rbx レジスタに格納されているため、 dump binary memory vmcode.bin $rbx ($rbx+0x100000) コマンドで vmcode.bin ファイルへ保存。

独自 VM コード内容をトレース出力するも理解が追いつかず

shadow_labyrinth バイナリの RVA 0x18d0 からが、独自 VM コードを実行する処理です。オペコードは 16 種類あり、それぞれ RVA 0x3ce0 にある関数ポインターの配列を使って、各種オペコードの処理を実現しています。また、各種オペコードの処理を解析するうちに、 VM 実行状態は次の構造体で表されると分かりました。

struct VmContext
{
    uint32_t dwMemoryMapSize[0x100000];
    int32_t dwRegisters[51];
    char strCopiedInput[36];
    int32_t dwInstructionCounter;
    uint8_t bZeroFlag; // ZF
};

16 種類のオペコードは次の内容です。

• オペコード 0: 指定レジスタ内容を 0 に設定。
• オペコード 1: 指定レジスタ内容を 1 に設定。
• オペコード 2: 指定レジスタ内容へ即値を加算。
• オペコード 3: 指定レジスタ内容から即値を減算、 ZF を設定。
• オペコード 4: 指定レジスタ内容を別レジスタ内容で左シフト。
• オペコード 5: 指定レジスタ内容へ別レジスタ内容を加算。
• オペコード 6: 指定レジスタ内容から別レジスタ内容を減算、 ZF を設定。
• オペコード 7: 指定レジスタ内容を別レジスタ内容で XOR。
• オペコード 8: 指定レジスタ内容を、独自 VM 中メモリマップの指定アドレスへ書き込み、 Store。
• オペコード 9: 独自 VM 中メモリマップの指定アドレス内容を、指定レジスタへ書き込み、 Load。
• オペコード 10: ZF が 1 ならジャンプ。
• オペコード 11: ZF が 0 ならジャンプ。
• オペコード 12: 無条件ジャンプ。
• オペコード 13: 入力フラグの波括弧内部後ろ 35 文字中の 1 文字を、レジスタ 35 にコピー。
• オペコード 14: 独自 VM 中メモリマップの指定アドレス以降の内容を文字列として出力、 puts。
• オペコード 15: プロセス終了。

まずは適当な入力について実行 VM コードをトレースして確認するために、次の gdb スクリプトを書いて解析することを試みました。

#!/usr/bin/env python3
# gdb -x gdb_script.py -q ./shadow_labyrinth

import gdb

TEST_FLAG = "HTB{by_4dd1ng_nd_multiply1ng_w3_pl4y_4_l1ttl3_m3l0dy???????????????????????????????????}"
INPUT_FILE_NAME = "./gdb_input_file.txt"
with open(INPUT_FILE_NAME, "w") as f:
    f.write(TEST_FLAG)

gdb.execute("break uncompress")
gdb.execute(f"run < {INPUT_FILE_NAME}")
gdb.execute("finish")

# RVA 0x18c8 にいるはず
addr_after_uncompress = int(gdb.parse_and_eval("$rip"))
print(f"{addr_after_uncompress = :016x}")
addr_after_fetch_opcode = addr_after_uncompress - 0x18C8 + 0x18E8

gdb.execute(rf"""dprintf *{hex(addr_after_fetch_opcode)}, "%04x: opcode %02d \n", ($edx-1), $eax """)
gdb.execute("continue")
gdb.execute("exit")

しかし上記スクリプトで実行時トレースを取得すると、 30 万回以上の独自 VM コードを実行することが判明しました。このままでは内容理解が困難であるため、別のアプローチを考えました。

「独自 VM コード内容を C コードへ変換 → C コンパイラによる最適化」という難読化解除方法

様々な試行錯誤を重ねると、次のことが分かりました。

• 独自 VM のメモリマップの用途が、コード部分とデータ部分で使用アドレスが完全に分かれています。そのため「独自 VM コード実行中にコード部分を自己書き換え」は考慮不要です。
• 同様に、オペコード 14 での文字列出力用のアドレスは、メモリマップ中に最初から平文で存在しています。
• 出力に影響する分岐は最後のみであり、何らかの計算結果によって正解か失敗かの出力が変化します。

独自 VM コードの見通しを良くするため、次の方針を考えました。

1. 独自 VM コードを C 言語ソースコードへ変換。
2. 変換後 C 言語ソースコードを、 C コンパイラで最適化しつつコンパイル。
3. コンパイル後のバイナリを逆コンパイルして確認。

最終的な、独自 VM コードを C 言語ソースコードへ変換するスクリプトを次に示します。

#!/usr/bin/env python3
# ./translate.py && gcc -no-pie -Os -o generated-no-pie-smalled generated.c
import pwn

with open("vmcode.bin", "rb") as f_in:
    vm_code = f_in.read()

MIN_MEMMAP = 126842
MAX_MEMMAP = MIN_MEMMAP + 2000

int32_memory_map_content = []
for i in range(len(vm_code) // 4):
    int32_memory_map_content.append(
        pwn.u32(vm_code[4 * i : 4 * (i + 1)], endianness="little", sign="signed")
    )
int32_memory_map_content = int32_memory_map_content[MIN_MEMMAP:MAX_MEMMAP]

with open("generated.c", "w") as f_out:
    f_out.write(
        """
#include<stdio.h>
#include<stdlib.h>
#include<stdint.h>
void __attribute__((noinline,noclone)) succeeded() {
    puts("Succeeded!");
}
void __attribute__((noinline,noclone)) failed() {
    puts("Failed...");
}
void print_string(uint32_t* addr)
{
  uint32_t i;
  for ( i = *addr; *addr; i = *addr )
  {
    ++addr;
    putc((char)i, stdout);
  }
}
int main()
{
    int32_t dwMemoryMap[10000] = {"""
        + ",".join(map(lambda v: hex(v), int32_memory_map_content))
        + """};
    int32_t registers[50] = {};
    uint8_t bZero = 0;
    char strFlag[36] = {};
    int32_t strFlagIndex = 0;
    scanf("%s", strFlag);

"""
    )
    ip = 0

    min_load_store_addr = 2**32
    max_load_store_addr = 0
    while ip < 0x7BDE7:  # 最後にexitで終わる。その後は変換不要
        opcode = vm_code[ip]
        ip += 4
        arg_1 = pwn.u32(vm_code[ip + 0 : ip + 4], endianness="little", sign="signed")
        arg_2 = pwn.u32(vm_code[ip + 4 : ip + 8], endianness="little", sign="signed")

        f_out.write(f"label_{hex(ip // 4 - 1)}: ")
        match opcode:
            case 0:
                f_out.write(f"registers[{arg_1}] = 0;\n")
                ip += 4
            case 1:
                f_out.write(f"registers[{arg_1}] = 1;\n")
                ip += 4
            case 2:
                f_out.write(f"registers[{arg_1}] += {hex(arg_2)};\n")
                ip += 8
            case 3:
                f_out.write(f"registers[{arg_1}] -= {hex(arg_2)}; bZero = (registers[{arg_1}] == 0);\n")
                ip += 8
            case 4:
                f_out.write(f"registers[{arg_1}] <<= {hex(arg_2)};\n")
                ip += 8
            case 5:
                f_out.write(f"registers[{arg_1}] += registers[{arg_2}];\n")
                ip += 8
            case 6:
                f_out.write(f"registers[{arg_1}] -= registers[{arg_2}]; bZero = (registers[{arg_1}] == 0);\n")
                ip += 8
            case 7:
                f_out.write(f"registers[{arg_1}] ^= registers[{arg_2}];\n")
                ip += 8
            case 8:
                addr = arg_2 + ip // 4 + 2 - MIN_MEMMAP
                max_load_store_addr = max(max_load_store_addr, addr)
                min_load_store_addr = min(min_load_store_addr, addr)
                f_out.write(f"dwMemoryMap[{hex(addr)}] = registers[{arg_1}];\n")
                ip += 8
            case 9:
                addr = arg_2 + ip // 4 + 2 - MIN_MEMMAP
                max_load_store_addr = max(max_load_store_addr, addr)
                min_load_store_addr = min(min_load_store_addr, addr)
                f_out.write(f"registers[{arg_1}] = dwMemoryMap[{hex(addr)}];\n")
                ip += 8
            case 10:
                f_out.write(f"if (bZero) {{ goto label_{hex(ip // 4 - 1 + arg_1)}; }}\n")
                ip += 4
            case 11:
                f_out.write(f"if (!bZero) {{ goto label_{hex(ip // 4 - 1 + arg_1)}; }}\n")
                ip += 4
            case 12:
                f_out.write(f"goto label_{hex(ip // 4 - 1 + arg_1)};\n")
                ip += 4
            case 13:
                f_out.write("registers[35] = strFlag[strFlagIndex++];\n")
                ip += 0
            case 14:
                addr = arg_1 + ip // 4 + 1
                match addr:
                    case 0x1EFE3:
                        f_out.write("succeeded();\n")
                    case 0x1F014:
                        f_out.write("failed();\n")
                    case _:
                        raise Exception("Not covered")

                ip += 4
            case 15:
                f_out.write("exit(0);\n")
            case _:
                raise Exception("Not Implemented...")

    f_out.write("""
    return 0;
}
""")

工夫した点です。

• すべての変数をローカル変数とすることで、コンパイラの最適化を促進しました。
• 「最終状態の出力」等を一切行わないことで、途中状況の保存等を不要にすることでも、コンパイラの最適化を促進しました。

最適化オプション込みでコンパイルした結果を逆コンパイルすると、次のような処理が目に留まりました。

  v7 = 218 * input[34]
     + 90 * input[28]
     + 94 * input[27]
     + 215 * input[26]
     + 222 * input[11]
     + 70 * input[10]
     + 133 * input[9]
     + 292 * input[1]
     + 187 * input[0]
     + 260 * input[2]
     + 157 * input[3]
     + 186 * input[4]
     + 106 * input[5]
     + 211 * input[6]
     + 241 * input[7]
     + 191 * input[8]
     + 124 * input[12]
     + 132 * input[13]
     + (input[14] << 8)
     + 157 * input[15]
     + 282 * input[16]
     + 242 * input[17]
     + 220 * input[18]
     + 113 * input[19]
     + 297 * input[20]
     + 105 * input[21]
     + 63 * input[22]
     + 214 * input[23]
     + 223 * input[24]
     + 203 * input[25]
     + 79 * input[29]
     + 69 * input[31]
     + 262 * input[32]
     + 267 * input[33] != 636090;

長い内容ですが、よく読むと次のことが分かります。

• 1 箇所だけ (input[14] << 8) と左シフト演算が使われています。これは 256 * input[14] の最適化結果です。
• 全体として、フラグの波括弧内部の後ろ 35 文字 の各文字についての定数倍の総和が、固定値であるかどうかを判断しています。これは、各種入力を 1 つのベクトルと考えたとき、とあるベクトルとの内積が、特定の値であるかを判断していることになります。

逆コンパイル結果を眺めると 35 個ある処理すべてが同様の判定であり、すべての判定について内積が固定値と一致している場合に正解と判定していることが分かりました。すなわち 35 連立 1 次方程式を解けば、正解のフラグが分かるようです。

35 連立 1 次方程式の求解

逆コンパイル結果をテキスト処理して、行列やベクトルをパースしました。その後の連立方程式を解く方法として、数学ソフトウェアである Sage⁵ を使用しました。 Sage は Python の拡張であるかのように、行列計算等を記述できます。

今回の連立方程式では係数が最大でも 300 未満のようで、フラグの各種数値は 0x20～0x7E と想定できることから、要素数 35 であるベクトルの内積は最大でも 1344000 程度であるため、 VM 実行状態のレジスタサイズである int32_t の値域に収まっておりオーバーフローしないことが見積もれます。そのため Sage の整数環である ZZ の範疇で求解しました。

最終的な Sage スクリプトのソルバーを次に示します。

#!/usr/bin/env sage

import re

z3_code = """
v7 = (
    218 * input[34]
    + 90 * input[28]
    + 94 * input[27]
    + 215 * input[26]
    + 222 * input[11]
    + 70 * input[10]
    + 133 * input[9]
    + 292 * input[1]
    + 187 * input[0]
    + 260 * input[2]
    + 157 * input[3]
    + 186 * input[4]
    + 106 * input[5]
    + 211 * input[6]
    + 241 * input[7]
    + 191 * input[8]
    + 124 * input[12]
    + 132 * input[13]
    + (input[14] << 8)
    + 157 * input[15]
    + 282 * input[16]
    + 242 * input[17]
    + 220 * input[18]
    + 113 * input[19]
    + 297 * input[20]
    + 105 * input[21]
    + 63 * input[22]
    + 214 * input[23]
    + 223 * input[24]
    + 203 * input[25]
    + 79 * input[29]
    + 69 * input[31]
    + 262 * input[32]
    + 267 * input[33]
    != 636090
)
以降同様に逆コンパイル結果から 35 個の式の内容を貼り付けます
"""

SIZE = 35
matrix: list[list[int]] = []
matrix_current: list[int] = [0] * SIZE
v: list[int] = []
for line in z3_code.splitlines():
    line = line.strip()
    if not line:
        continue
    if line == "(":
        continue
    if line == ")":
        continue

    print(line)

    succeeded = False
    if re.match(r"^\w+ \= \($", line):
        succeeded = True
    m = re.search(r"^\s*(?:\+ )?input\[(\d+)\]$", line)
    if m:
        index = int(m.group(1))
        assert 0 <= index < SIZE
        matrix_current[index] = 1
        succeeded = True
    m = re.search(r"^\s*(?:\+ )?(\d+) \* input\[(\d+)\]$", line)
    if m:
        succeeded = True
        amp = int(m.group(1))
        index = int(m.group(2))
        assert 0 <= index < SIZE
        matrix_current[index] = amp
    m = re.search(r"^\s*(?:\+ )?\(input\[(\d+)\] << (\d+)\)$", line)
    if m:
        succeeded = True
        index = int(m.group(1))
        bit = int(m.group(2))
        assert 0 <= index < SIZE
        matrix_current[index] = 1 << bit
    m = re.search(r"^\s*!= (\d+)$", line)
    if m:
        # 1個の連立方程式の終わり
        succeeded = True
        value = int(m.group(1))

        matrix.append(matrix_current)
        v.append(value)
        matrix_current = [0] * SIZE  # 方程式で使用されない要素もある
    assert succeeded


assert len(matrix) == SIZE

print(matrix)
print(v)

A = Matrix(ZZ, matrix)
v = vector(ZZ, v)
x = A.solve_right(v)
print(x)
for elem in x:
    print(chr(int(elem)), end="")
print()

なお、最終的なパース結果の行列は次のようになりました。

A = [[187, 292, 260, 157, 186, 106, 211, 241, 191, 133, 70, 222, 124, 132, 256, 157, 282, 242, 220, 113, 297, 105, 63, 214, 223, 203, 215, 94, 90, 79, 0, 69, 262, 267, 218], [184, 72, 4, 8, 123, 117, 208, 45, 79, 188, 42, 0, 257, 103, 91, 79, 144, 174, 237, 224, 240, 4, 18, 130, 1, 244, 62, 220, 63, 30, 162, 101, 154, 296, 295], [211, 157, 16, 183, 1, 95, 72, 166, 145, 113, 199, 90, 192, 210, 0, 265, 182, 256, 293, 97, 53, 26, 256, 100, 49, 242, 244, 95, 108, 211, 0, 40, 251, 43, 208], [196, 286, 52, 87, 57, 7, 203, 296, 272, 188, 152, 209, 266, 0, 158, 174, 115, 167, 258, 172, 105, 94, 18, 212, 130, 70, 205, 224, 291, 26, 235, 293, 103, 186, 178], [45, 229, 279, 183, 189, 252, 268, 78, 118, 124, 74, 36, 292, 299, 230, 289, 12, 12, 250, 81, 78, 276, 115, 98, 237, 17, 0, 235, 129, 152, 46, 165, 258, 126, 131], [75, 188, 29, 18, 213, 208, 121, 195, 115, 288, 159, 166, 97, 96, 149, 106, 101, 148, 246, 5, 262, 50, 61, 253, 0, 243, 89, 15, 87, 104, 20, 209, 130, 195, 169], [294, 112, 298, 15, 99, 60, 148, 280, 265, 258, 17, 281, 72, 14, 17, 235, 72, 297, 179, 138, 246, 175, 133, 150, 3, 184, 80, 130, 91, 5, 117, 284, 227, 143, 116], [281, 123, 291, 110, 116, 87, 13, 150, 7, 157, 256, 18, 111, 251, 54, 109, 227, 205, 289, 256, 151, 270, 165, 247, 197, 58, 69, 20, 67, 234, 58, 249, 29, 184, 107], [236, 183, 237, 10, 8, 48, 276, 142, 149, 127, 64, 106, 103, 136, 220, 200, 97, 41, 14, 215, 248, 114, 260, 134, 178, 214, 58, 188, 43, 280, 247, 204, 1, 94, 214], [131, 296, 72, 237, 294, 146, 79, 285, 129, 27, 108, 278, 261, 194, 164, 186, 128, 252, 128, 253, 174, 271, 274, 229, 80, 16, 126, 74, 86, 71, 52, 15, 26, 50, 95], [161, 230, 11, 242, 39, 58, 193, 294, 181, 1, 109, 273, 268, 167, 56, 1, 19, 241, 82, 233, 85, 151, 132, 108, 276, 223, 289, 78, 211, 93, 17, 24, 27, 225, 145], [237, 126, 106, 225, 139, 239, 86, 210, 235, 156, 256, 119, 242, 107, 27, 197, 125, 36, 7, 231, 52, 284, 239, 3, 107, 210, 31, 166, 79, 71, 45, 235, 65, 156, 194], [139, 94, 143, 223, 212, 35, 212, 88, 293, 186, 144, 299, 53, 194, 259, 167, 21, 165, 157, 93, 221, 269, 282, 251, 72, 272, 129, 176, 237, 160, 285, 156, 270, 259, 30], [112, 185, 190, 266, 286, 206, 241, 286, 84, 255, 38, 128, 56, 60, 150, 46, 99, 137, 128, 288, 159, 259, 22, 256, 47, 201, 38, 166, 16, 203, 230, 210, 282, 111, 211], [151, 148, 70, 91, 191, 211, 224, 248, 208, 176, 9, 138, 277, 168, 232, 10, 190, 67, 235, 108, 102, 106, 152, 73, 6, 291, 124, 94, 235, 88, 123, 129, 298, 184, 269], [292, 162, 128, 221, 40, 82, 126, 96, 154, 123, 60, 288, 98, 273, 264, 205, 25, 135, 155, 183, 120, 36, 43, 208, 192, 284, 245, 12, 107, 289, 69, 40, 113, 106, 222], [183, 65, 118, 113, 7, 46, 296, 96, 129, 102, 173, 21, 119, 146, 192, 51, 14, 253, 38, 299, 294, 183, 228, 126, 207, 198, 244, 260, 269, 284, 99, 189, 147, 256, 213], [192, 167, 21, 22, 99, 4, 292, 39, 214, 173, 169, 44, 192, 147, 33, 130, 168, 21, 70, 163, 78, 248, 285, 43, 212, 98, 252, 102, 66, 117, 270, 160, 131, 286, 10], [1, 257, 139, 298, 37, 178, 142, 214, 293, 104, 203, 100, 60, 255, 153, 204, 32, 106, 96, 3, 103, 101, 264, 281, 289, 155, 263, 290, 155, 69, 233, 149, 8, 207, 82], [296, 209, 122, 100, 127, 162, 187, 289, 173, 240, 179, 253, 77, 153, 129, 51, 123, 94, 57, 142, 105, 114, 115, 8, 127, 15, 103, 117, 243, 288, 228, 292, 183, 126, 95], [138, 282, 170, 160, 196, 61, 93, 296, 83, 137, 178, 209, 95, 271, 212, 226, 13, 272, 56, 83, 90, 224, 128, 173, 162, 111, 151, 227, 107, 174, 25, 24, 46, 193, 34], [7, 284, 70, 235, 137, 298, 72, 90, 82, 60, 228, 262, 4, 186, 229, 175, 266, 102, 158, 163, 202, 153, 16, 67, 240, 142, 179, 55, 191, 16, 177, 214, 255, 281, 263], [154, 122, 295, 253, 5, 255, 24, 184, 156, 38, 70, 51, 106, 71, 130, 255, 68, 114, 208, 163, 167, 193, 69, 138, 236, 182, 101, 167, 291, 207, 280, 153, 50, 22, 31], [251, 128, 279, 67, 170, 232, 29, 196, 104, 295, 85, 284, 66, 198, 203, 238, 255, 294, 246, 123, 155, 21, 134, 5, 121, 52, 150, 293, 63, 90, 204, 79, 92, 294, 244], [186, 21, 29, 61, 15, 204, 156, 232, 42, 217, 178, 38, 73, 283, 43, 210, 259, 5, 241, 146, 87, 193, 31, 143, 166, 222, 249, 162, 91, 175, 49, 145, 236, 37, 282], [82, 252, 216, 113, 271, 152, 102, 32, 130, 77, 130, 139, 102, 206, 16, 84, 242, 20, 279, 277, 32, 107, 67, 164, 195, 149, 37, 96, 218, 287, 198, 19, 212, 283, 283], [60, 40, 37, 148, 244, 100, 168, 244, 45, 20, 223, 263, 248, 173, 44, 162, 53, 125, 184, 131, 5, 205, 201, 290, 246, 100, 9, 276, 249, 232, 276, 121, 128, 159, 119], [92, 176, 276, 275, 43, 7, 4, 199, 38, 150, 221, 93, 214, 120, 26, 145, 273, 281, 50, 235, 214, 288, 90, 263, 231, 126, 25, 97, 186, 170, 174, 78, 201, 194, 11], [150, 74, 145, 202, 68, 240, 15, 131, 220, 28, 3, 35, 217, 137, 250, 78, 182, 177, 146, 194, 12, 137, 133, 268, 234, 74, 162, 36, 253, 94, 219, 85, 10, 218, 278], [98, 12, 46, 148, 154, 226, 151, 213, 130, 243, 86, 89, 113, 61, 3, 73, 58, 48, 32, 23, 145, 116, 81, 68, 256, 76, 197, 149, 290, 80, 68, 238, 190, 1, 98], [197, 21, 98, 288, 177, 87, 60, 150, 47, 116, 169, 221, 29, 128, 186, 45, 266, 65, 245, 299, 272, 193, 174, 175, 102, 253, 156, 13, 26, 200, 279, 80, 120, 196, 43], [165, 19, 125, 213, 252, 58, 241, 151, 101, 238, 289, 209, 181, 236, 50, 260, 232, 276, 168, 187, 98, 248, 207, 210, 129, 41, 152, 286, 188, 80, 177, 161, 271, 163, 145], [134, 156, 265, 26, 249, 245, 286, 187, 275, 99, 155, 127, 65, 148, 33, 2, 131, 238, 7, 129, 149, 91, 25, 161, 34, 275, 97, 106, 194, 46, 115, 297, 140, 240, 146], [49, 136, 163, 132, 283, 129, 169, 130, 2, 289, 93, 187, 11, 279, 62, 88, 131, 168, 247, 248, 28, 208, 293, 288, 276, 114, 275, 100, 283, 41, 294, 60, 277, 64, 79], [272, 20, 183, 288, 215, 241, 59, 227, 77, 112, 75, 222, 211, 177, 273, 295, 78, 98, 172, 215, 151, 165, 232, 65, 269, 5, 154, 92, 47, 271, 99, 89, 156, 230, 82]]
v = [636090, 419918, 473345, 569425, 540335, 478567, 517711, 526162, 490345, 529536, 495033, 500970, 608292, 565270, 547687, 505882, 556709, 466029, 541989, 543512, 504443, 558774, 481496, 563443, 475833, 518187, 509866, 519179, 491299, 417961, 506039, 604004, 514020, 544304, 564033]

実行して連立方程式を解くと _tuturututu_n3v3r_g0nna_g1v3_y0u_up が得られます。

得られたフラグ

判明した次の内容を組み合わせます。

• main 関数で調べる 5 文字
• RVA 0x1660 の関数 1 段階目の処理を解析して得られた、フラグの波括弧内部の先頭 48 文字
• 復号した file.bin 内容の独自 VM コード内容を解析して得られた、フラグの波括弧内部の残り 35 文字

結果、フラグが HTB{by_4dd1ng_nd_multiply1ng_w3_pl4y_4_l1ttl3_m3l0dy_tuturututu_n3v3r_g0nna_g1v3_y0u_up} と分かります。

おわりに

本コンテストは、開催期間が長く出題ジャンル数や問題数が多いため、お祭りのようなイベントでした。社内から部門を超えて様々なメンバーが参加しており、面白い時間になりました。

最後になりましたが本記事で紹介している内容が、コンテストの雰囲気や、問題への取り組み方等の参考になれば幸いです。

---

1. https://www.hackthebox.com/events/global-cyber-skills-benchmark-2025↩
2. https://www.hackthebox.com/blog/business-ctf-2024-the-vault-of-hope-recap↩
3. https://github.com/hackthebox/business-ctf-2025↩
4. https://www.microsoft.com/en-us/research/project/z3-3/↩
5. https://doc.sagemath.org/html/en/tutorial/index.html↩