AlpacaHack Round 8 (Rev) write-up

AlpacaHack Round 8 (Rev)へ参加しました。そのwrite-up記事です。

IDAの解析結果ファイル.i64などを、GitHubで公開しています。

コンテスト概要

2024/12/30(月) 12:00 +09:00 - 12/30(月) 18:00 +09:00の6時間開催でした。他ルールはコンテストページから引用します:

AlpacaHack Round 8 (Rev) へようこそ！
AlpacaHack は個人戦の CTF を継続して開催する新しいプラットフォームです。
AlpacaHack Round 8 は AlpacaHack で行われる 8 回目の CTF で、Rev カテゴリから 4 問が出題されます。 幅広い難易度の問題が出題されるため、初心者を含め様々なレベルの方に楽しんでいただけるようになっています。 問題作成者は arata-nvm と sugi です！

参加方法
1. 右上の「Sign Up」ボタンから AlpacaHack のユーザー登録をしてください。
2. 登録完了後、このページの「Register」ボタンを押して CTF の参加登録をしてください。

注意事項
- AlpacaHack は個人戦のCTFプラットフォームであるため、チームでの登録は禁止しています。
- 問題は運営が想定した難易度の順に並んでいます。
- 問題の配点は解いた人数に応じて変動します。
- フラグフォーマットは Alpaca{...} です。
- 全てのアナウンスは AlpacaHack の Discord サーバー で行われます。
  - アナウンスは本サービス上でも行うことがありますが、Discord サーバーが主な連絡手段となります。
  - 問題が発生した場合、#ticket チャンネルから連絡してください。ただし、問題のヒントは提供しません。
- 競技システム自体への攻撃は行わないでください。なお、偶然発見したバグの報告は歓迎します。

これまでのRound同様に問題は運営が想定した難易度の順に並んでいますと明記されており、並び順で想定難易度が示されました。

結果

正の得点を得ている62人中、620点で8位でした:

順位と得点等(Scoreboard加工後)

チェック印: 解けた問題

また、Certificate箇所から順位の証明書も表示できます:

環境

WindowsのWSL2(Ubuntu 24.04)を使って取り組みました。

Windows

c:\>ver

Microsoft Windows [Version 10.0.19045.5247]

c:\>wsl -l -v
  NAME                   STATE           VERSION
* Ubuntu-24.04           Running         2
  docker-desktop-data    Running         2
  kali-linux             Stopped         2
  docker-desktop         Running         2
  Ubuntu-22.04           Running         2

c:\>

他ソフト

• IDA Free Version 9.0.241217 Windows x64 (64-bit address size)(Free版IDAでもversion 7頃からx64バイナリを、version 8.2からはx86バイナリもクラウドベースの逆コンパイルができます)

WSL2(Ubuntu 24.04)

$ cat /proc/version
Linux version 5.15.167.4-microsoft-standard-WSL2 (root@f9c826d3017f) (gcc (GCC) 11.2.0, GNU ld (GNU Binutils) 2.37) #1 SMP Tue Nov 5 00:21:55 UTC 2024
$ cat /etc/os-release
PRETTY_NAME="Ubuntu 24.04.1 LTS"
NAME="Ubuntu"
VERSION_ID="24.04"
VERSION="24.04.1 LTS (Noble Numbat)"
VERSION_CODENAME=noble
ID=ubuntu
ID_LIKE=debian
HOME_URL="https://www.ubuntu.com/"
SUPPORT_URL="https://help.ubuntu.com/"
BUG_REPORT_URL="https://bugs.launchpad.net/ubuntu/"
PRIVACY_POLICY_URL="https://www.ubuntu.com/legal/terms-and-policies/privacy-policy"
UBUNTU_CODENAME=noble
LOGO=ubuntu-logo
$ python3 --version
Python 3.12.3
$ python3 -m pip show pip | grep Version:
Version: 24.0
$ python3 -m pip show IPython | grep Version:
Version: 8.24.0
$ python3 -m pip show pwntools | grep Version:
Version: 4.13.1
$ python3 -m pip show z3-solver | grep Version:
Version: 4.8.16.0
$ gdb --version
GNU gdb (Ubuntu 15.0.50.20240403-0ubuntu1) 15.0.50.20240403-git
Copyright (C) 2024 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.
$ gdb --batch --eval-command 'version' | grep 'Pwndbg:'
Pwndbg:   2024.02.14 build: 2b9beef
$

解けた問題

[Rev] masking tape (61 solves, 124 points)

Masking tape is also useful for flag checking :)

配布ファイルとして、masking-tapeがありました:

$ file *
masking-tape: ELF 64-bit LSB pie executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, BuildID[sha1]=61a9c2ab285b526528b77f1170889a951fb7efe2, for GNU/Linux 3.2.0, not stripped
$

IDAで開いて逆コンパイルしました。変数名等を調整した結果です:

int __fastcall main(int argc, const char **argv)
{
  size_t i; // [rsp+18h] [rbp-28h]
  char *pInput; // [rsp+20h] [rbp-20h]
  size_t dwInputSize; // [rsp+28h] [rbp-18h]
  char *pAllocated1; // [rsp+30h] [rbp-10h]
  char *pAllocated2; // [rsp+38h] [rbp-8h]

  if ( argc == 2 )
  {
    pInput = (char *)argv[1];
    dwInputSize = strlen(pInput) + 1;
    pAllocated1 = (char *)malloc(dwInputSize);
    pAllocated2 = (char *)malloc(dwInputSize);
    for ( i = 0LL; i < dwInputSize; ++i )
    {
      pInput[i] = (pInput[i] >> 5) | (8 * pInput[i]);
      if ( (pInput[i] & 1) != 0 )
      {
        pAllocated1[i] = pInput[i] & 0x33;
        pAllocated2[i] = pInput[i] & 0xCC;
      }
      else
      {
        pAllocated1[i] = pInput[i] & 0xCC;
        pAllocated2[i] = pInput[i] & 0x33;
      }
    }
    if ( !strcmp(enc1, pAllocated1) && !strcmp(&enc2, pAllocated2) )
      puts("congratz");
    else
      puts("wrong");
    return 0;
  }
  else
  {
    printf("usage: %s <input>\n", *argv);
    return 0;
  }
}

入力1文字ごとに(pInput[i] >> 5) | (8 * pInput[i])の変換を施し、変換結果の最下位ビットに従って結果を2つの配列へ格納しています。(0x33 ^ 0xCC) == 0xFFであるため、変換結果の各ビットすべてが、どちらかの配列へのみに入ります。

最終的に、2つのグローバル変数配列enc1とenc2を使って正誤を判定しています。enc1とenc2の内容から、正解となる入力フラグを逆算するソルバーを書きました:

#!/usr/bin/env python3

# fmt: off
# IDAの0x2020付近へマウスカーソルを合わせて範囲選択し、Shift+Eで「Export data」してHex表現バイト列を得ました
enc1 = bytes.fromhex("08 23 03 03 13 03 13 03 01 23 31 13 11 C8 03 C8 03 13 01 C8 13 13 03 13 13 11 13 23 00")
enc2 = bytes.fromhex("02 40 80 08 08 08 C8 C8 80 88 08 80 88 32 08 32 80 80 80 32 08 80 08 08 48 88 80 C8 00")
# fmt: on


flag = ""
for i in range(len(enc1)):
    v1 = enc1[i]
    v2 = enc2[i]
    if ((v1 & 0xCC) == 0) and ((v2 & 0x33) == 0):
        v = (v1 & 0x33) | (v2 & 0xCC)
    elif ((v1 & 0x33) == 0) and ((v2 & 0xCC) == 0):
        v = (v1 & 0xCC) | (v2 & 0x33)
    else:
        raise Exception("")

    v = ((v << 5) & 0xFF) | ((v >> 3) & 0b11111)

    flag += chr(v)
print(flag.strip("\x00"))

実行しました:

$ ./solve.py
Alpaca{y0u'r3_a_pr0_crack3r}
$ ./masking-tape "Alpaca{y0u'r3_a_pr0_crack3r}"
congratz
$

フラグを入手できました: Alpaca{y0u'r3_a_pr0_crack3r}

なお、コンテスト中ではビット積を取る際の数値を間違えていて、数分ロスしていました……。

[Rev] hidden (23 solves, 192 points)

How do I hide from a decompiler?

本問題バイナリをIDAで解析したファイルhidden.i64を公開しています。

配布ファイルとして、hiddenがありました:

$ file *
hidden: ELF 64-bit LSB pie executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, BuildID[sha1]=1cee3c62169c309aaf0c2c2f7885bd36ca87f6e8, for GNU/Linux 3.2.0, stripped
$

問題文からして何かが仕込まれている雰囲気を感じつつも、IDAで開いて逆コンパイルしました。

main関数は次の内容でした(変数名等リネーム後):

__int64 __fastcall main(int argc, char **argv)
{
  unsigned __int64 i; // [rsp+18h] [rbp-58h]
  char *pStrInput; // [rsp+20h] [rbp-50h]
  size_t dwStrInputLength; // [rsp+28h] [rbp-48h]
  _DWORD *pdwArrayInOut; // [rsp+38h] [rbp-38h]
  char strAlpacaHackRound8[24]; // [rsp+40h] [rbp-30h] BYREF
  unsigned __int64 qwCanary; // [rsp+58h] [rbp-18h]

  qwCanary = __readfsqword(0x28u);
  strcpy(strAlpacaHackRound8, "AlpacaHackRound8");
  if ( argc > 1 )
  {
    pStrInput = argv[1];
    dwStrInputLength = strlen(pStrInput);
    pdwArrayInOut = calloc((dwStrInputLength + 3) >> 2, 4uLL);
    memcpy(pdwArrayInOut, pStrInput, dwStrInputLength);
    for ( i = 0LL; i < (dwStrInputLength + 3) >> 2; ++i )
      pdwArrayInOut[i] = ProcConvert(pdwArrayInOut[i], strAlpacaHackRound8);
    if ( !memcmp(pdwArrayInOut, dword_4040, 4 * g_qwValue_Constant27) )
      puts("congratz");
    else
      puts("wrong");
    return 0LL;
  }
  else
  {
    printf("usage: %s <input>\n", *argv);
    return 0LL;
  }
}

上記コードでProcConvertと名付けている関数は、0x1272にある関数です。その関数の読解が本問題の主題でした。

施されている耐逆コンパイル手法

(ところで「Anti-decompile」の和訳表記は「アンチデコンパイル」とカタカナ表記が多い印象です。ただ個人的には「デコンパイル」表記だと「デ」を見逃しやすそうなので、「逆コンパイル」を用いた語句を使いたいです。そのため「耐逆コンパイル」表記としています。)

0x1272の関数での逆コンパイル結果は次のものでした(変数名等はリネーム済みです):

unsigned int __fastcall ProcConvert(unsigned int dwInputPart, _DWORD *pdwInOutArraySize4)
{
  ProcSome_1(__ROL4__(*pdwInOutArraySize4, 5) + __ROR4__(pdwInOutArraySize4[1], 3));
  ProcSome_2(__ROR4__(pdwInOutArraySize4[2], 3) - __ROL4__(pdwInOutArraySize4[3], 5));
  ProcSome_3(dwInputPart);
  *pdwInOutArraySize4 ^= __ROR4__(0, 13);
  pdwInOutArraySize4[1] ^= __ROR4__(0, 15);
  pdwInOutArraySize4[2] ^= __ROL4__(0, 13);
  pdwInOutArraySize4[3] ^= __ROL4__(0, 11);
  return 0;
}

しかし逆アセンブル画面と見比べると、逆コンパイル結果には何かと欠落しているらしいことが分かります。見つけやすくする方法として、IDA View-AとPseudocode-Aウィンドウを横に並べ、Pseudocode-Aウィンドウ内部で右クリックして表示されるコンテキストメニューでSynchronize with→IDA View-A Hex-View-1を選択する方法があります。そうすると、逆コンパイルウィンドウで選択中の行に対応するアセンブリ命令が、逆アセンブルウィンドウ側でも緑色に同期されて表示されます:

逆アセンブル画面と逆コンパイル画面を見比べてみると、逆アセンブル画面では登場する次の内容が、逆コンパイル画面には登場しないことが分かりました:

• 0x12EFでのcall時の第1引数として、逆アセンブル画面では[rbp+0x14]、[rbp+0xC]、[rbp+0x8]の3個の値のXOR結果を渡しています。しかし逆コンパイル画面では単純に[rbp+0x14]の1個の値を渡しているだけです。
• 0x12F7付近で、逆アセンブル画面ではmov eax, [rbp+0x4]、and eax, 1、test eax, eax、jz short loc_136Eの条件分岐が存在します。しかし逆コンパイル画面では条件分岐が存在しません。常時ジャンプするものとして表示されています。
• ジャンプ先の0x1377等について、逆コンパイル画面ではmov eax, [rbp+0x8]、ror eax, 0Dh等、ローカル変数の値に基づいてRotateRightしています。しかし逆コンパイル画面では__ROR4__(0, 13)等と、RotateRightする第1オペランドが0固定になっています。

どうやら、次の耐逆コンパイル手法が施されているようです:

• 0x1272の関数内部だけを見ると、[rbp+0xC]、[rbp+0x8]、[rbp+0x4]の3個の値は、関数冒頭で0初期化しているだけで、以降変化がないように見えます。
• しかし実際は、途中でcallしている0x124F、0x122C、0x1209の関数が、0x1272関数中のローカル変数を直接書き換えています。逆コンパイラはこの書き換えを認識できていません。
• 結果として、逆コンパイラは[rbp+0xC]、[rbp+0x8]、[rbp+0x4]の3個の値が常に0のままと誤認して、誤認結果に基づいて出力内容を最適化してしまいます。
  • F5キーで逆コンパイル画面を再表示するたびに、Outputウィンドウ中に12FC: conditional instruction was optimized away because %dwFilledByProc3.1==0表示がされていることからも分かります。

例えば0x124Fの関数を逆コンパイルしてみると、次のように橙色の表示があります。これは逆コンパイラにとって不穏なことを表しています:

なお、最初のうちはIDAの__usercall呼び出し規約指定を使って特殊な引数の存在を逆コンパイラへ教えようとしましたが、結局はうまくいきませんでした。_DWORD *a2@<^0.8>等の構文を使っても、おそらくは現在の関数のスタックフレーム(用語があっているか不安です)のみを参照できるようです。親関数のスタックフレームを参照しようと_DWORD *a2@<^-1.8>等を入力してみましたが、構文エラーとなってしまいました。

また、逆コンパイル機能のオプション(IDAメニューのEdit→Plugins→Hex-Ray decompiler cloud Options)をざっくり見渡しても、上記最適化を抑制できそうな項目は無さそうでした。

逆アセンブル画面から処理内容を読解

幸い、0x1272の関数は短いです。逆アセンブル内容から正しい処理を読解することにしました。

GDBで実験することで、どうやら0x124F関数が0x1272関数中の[rbp+0xC]を、0x122C関数が0x1272関数中の[rbp+0x8]を、0x1209関数が0x1272関数中の[rbp+0x4]を、それぞれ書き換えるらしいことが分かりました。

また、0x12FCのjz命令をnopで上書きすると、逆コンパイル画面から分岐しなかった場合の大体の処理が分かります。

読解した結果、0x1272の関数は次の処理を行っていることが分かりました:

• 0x1272関数の第1引数は、入力フラグを4文字ごとにまとめたuint32_tです。
• 0x1272関数の第2引数は、uint32_t[4]配列です。初回呼び出し時は、main関数で設定しているAlpacaHackRound8文字列です。
• 0x1272関数のスタックフレームの[rbp + 0xC]に、__ROL4__(第2引数[0], 5) + __ROR4__(第2引数[1], 3)を書き込みます。
• 0x1272関数のスタックフレームの[rbp + 0x8]に、__ROR4__(第2引数[2], 3) - __ROL4__(第2引数[3], 5)を書き込みます。
• 0x1272関数のスタックフレームの[rbp + 0x4]に、[rbp + 0xC] ^ [rbp + 0x8] ^ 第1引数を書き込みます。
• [rbp + 0x4]の最下位ビットに依存して、第2引数の4要素それぞれをXORで更新します。その際は[rbp + 0xC]ã‚„[rbp + 0x8]を使います。
• 0x1272関数自体の戻り値は[rbp + 0x4]です。

読解した結果をソルバーで利用しました。

ソルバーと実行結果

z3-solverライブラリでシンボリック変数を用意して、読解した0x1272関数を適用した結果が想定した結果になるように、入力を逆算するソルバーを書きました:

#!/usr/bin/env python3

import pwn
import z3

MOD = 0x1_0000_0000


def byte_array_to_dword_array(a: bytes) -> list[int]:
    assert len(a) % 4 == 0

    result: list[int] = []
    for i in range(len(a) // 4):
        v: int = pwn.u32(a[i * 4 : (i + 1) * 4])
        result.append(v)
    return result


def RotateLeft32(value: int, bit: int) -> int:
    assert 0 <= bit < 32
    assert 0 <= value < MOD
    return ((value << bit) | (value >> (32 - bit))) % MOD


def RotateRight32(value: int, bit: int) -> int:
    assert 0 <= bit < 32
    assert 0 <= value < MOD
    return ((value >> bit) | (value << (32 - bit))) % MOD


def convert(
    part: int | z3.BitVecRef, work: list[int]
) -> tuple[int, int, int | z3.BitVecRef]:
    value1 = (RotateLeft32(work[0], 5) + RotateRight32(work[1], 3)) % MOD
    value2 = (RotateRight32(work[2], 3) - RotateLeft32(work[3], 5) + MOD) % MOD
    value3 = (part ^ value1 ^ value2) % MOD
    # ここでvalue3で分岐してしまうと、シンボリック変数のままだからか思った分岐になりませんでした。後で判断します
    # 教訓: 「(value3 & 1) != 0」等で「Symbolic expressions cannot be cast to concrete Boolean values.」が出るときは本当に間違っています。
    return (value1, value2, value3)


# fmt:off
# 4040からShift+EでExport data
expected_bytes = bytes.fromhex("DC 86 1A 9A DD 93 9B 35 D3 74 DA EE E8 5A 3C C5 1C 64 33 47 D2 3B 28 F3 CC 5A 48 8B 74 0C 4B 87 38 D6 80 40 51 E6 4A 27 A1 73 52 0F 93 06 54 3D 65 13 FB C8 65 AF D2 67 B3 09 EF 7D 23 A6 76 E5 13 10 13 FF 34 8D AE D0 9C 2C 4D F3 A1 BC 46 2F 98 87 B6 57 1A A2 17 F1 F0 E5 B0 BA 9B 6D B5 A7 AC 6A 5E AC E8 F6 90 D8 B0 A2 99 91")
expected_dwords = byte_array_to_dword_array(expected_bytes)
assert len(expected_dwords) == 27
# fmt:on

work: list[int] = byte_array_to_dword_array(b"AlpacaHackRound8")

solver = z3.Solver()
flag_input = [z3.BitVec(f"flag_{i:02d}", 8) for i in range(4 * 27)]

for i in range(len(flag_input) // 4):
    value_input = (
        (z3.ZeroExt(32, flag_input[(4 * i) + 0]) << 0)
        | (z3.ZeroExt(32, flag_input[(4 * i) + 1]) << 8)
        | (z3.ZeroExt(32, flag_input[(4 * i) + 2]) << 16)
        | (z3.ZeroExt(32, flag_input[(4 * i) + 3]) << 24)
    )
    (value1_concret, value2_concret, value3_symbolic) = convert(value_input, work)
    solver.add(value3_symbolic == expected_dwords[i])

    if solver.check() != z3.sat:
        raise Exception("Can not solve...")

    # なるはずの値は分かっているので、簡単のためそちらを使います
    value3_concrete = expected_dwords[i]

    if (value3_concrete & 1) == 1:
        work[0] ^= RotateLeft32(value2_concret, 11)
        work[1] ^= RotateLeft32(value2_concret, 13)
        work[2] ^= RotateRight32(value1_concret, 15)
        work[3] ^= RotateRight32(value1_concret, 13)
    else:
        work[0] ^= RotateRight32(value2_concret, 13)
        work[1] ^= RotateRight32(value2_concret, 15)
        work[2] ^= RotateLeft32(value1_concret, 13)
        work[3] ^= RotateLeft32(value1_concret, 11)

flag_result = ""
model = solver.model()
for f in flag_input:
    flag_result += chr(model[f].as_long())  # type:ignore
print(flag_result.strip("\x00"))

実行しました:

$ ./solve.py
Alpaca{th15_f145_1s_3xc3ssiv3ly_l3ngthy_but_th1s_1s_t0_3nsur3_th4t_1t_c4nn0t_b3_e4s1ly_s01v3d_us1ng_angr}
$ ./hidden 'Alpaca{th15_f145_1s_3xc3ssiv3ly_l3ngthy_but_th1s_1s_t0_3nsur3_th4t_1t_c4nn0t_b3_e4s1ly_s01v3d_us1ng_angr}'
congratz
$

フラグを入手できました: Alpaca{th15_f145_1s_3xc3ssiv3ly_l3ngthy_but_th1s_1s_t0_3nsur3_th4t_1t_c4nn0t_b3_e4s1ly_s01v3d_us1ng_angr}

なお、コンテスト中ではソルバーをひたすらバグらせていて、1時間ぐらいハマっていました:

• 2**32を保持したかったMOD変数の内容を、0が1つ多い0x1_0000_00000としてしまっていました……。
• 逆コンパイル画面も逆アセンブル画面も斜め読みしていて、ror命令の存在を見逃していました。全部rol命令と思っていました……。
• 確か、z3のBitVecRef型変数valueを使ってif (value & 1) != 0等と条件分岐をしようとしていました……:
  • if (value & 1) != 0:表記ではSymbolic expressions cannot be cast to concrete Boolean values.例外が送出されました。この時点で怪しいと気づいていれば……。
  • if (value & 1) == 1:表記では実行できいましたが、value3はシンボリック変数のままなので想定した条件分岐にならなかったようです(どのように実行されていたかは分かっていません)。

[Rev] subway (8 solves, 304 points)

This is true floating-point arithmetic.

本問題バイナリをIDAで解析したファイルsubway.i64を公開しています。

配布ファイルとして、subwayがありました:

$ file *
subway: ELF 64-bit LSB pie executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, BuildID[sha1]=8c54e5ca98b13d7863a00517ae1aeb7722aa6103, for GNU/Linux 3.2.0, stripped
$

問題文からして浮動小数点数が使われている気配を感じつつ、IDAで開いて逆コンパイルしました。

+0と-0の発見

各種処理を眺めていると、mallocで確保した要素へ格納する値は、uint32_t型の0か0x80000000だけであることが分かります。そして最終的に0x21B1の関数で、float型として扱っていることが分かります。

ここで、見つかった値のビット表現を、float(=float32)として解釈させてみます。IEEE-754 Floating Point Converterサイトを使いました。すると、0は+0、0x80000000は-0と分かりました。浮動小数点数は符号ビットが存在するため、0にも正負が存在します。

そして、一番最後の正誤判定用に0x2092の関数の戻り値を使用しています。次の内容です:

bool __fastcall sub_2092(__m128i a1)
{
  return _mm_cvtsi128_si32(a1) >= 0;
}

一見すると、__m128iという謎の型を引数としているように見えます。しかし、x86 psABIs / x86-64 psABI · GitLabからダウンロードできるSystem V Application Binary Interface資料のFigure 3.4: Register Usageを見ると、%xmm0-%xmm1レジスタの用途がused to pass and return floating point argumentsとあります。つまり、1個のfloat値を渡す場合でも、128-bit幅のxmm0レジスタが使われます。また、_mm_cvtsi128_si32命令の解説を読むと、下位32-bit整数を返す命令と分かります。

どうやら0x2092関数は、「引数のfloat値のビット表現をint型とみなした時、0以上かどうか」を返すようです。もっというと、2の補数表記が使われているシステムでint型が0以上にあるのは最上位ビットが0である場合と同義で、それはfloat型の場合は符号ビットが0の場合と同義です。結局のところ0x2092関数は、引数のfloat値が正の値の場合はtrueを、負の値である場合はfalseを返す関数です。

このように、どうやら+0と-0の符号ビットだけを使って何かをしているらしい、ということが分かってきます

Trueã‚„False、論理関数や算術関数等の発見

+0と-0の符号ビットで情報を表しているらしいことを考えつつバイナリ中の各種関数を探してみると、どうやら+0がTrueを、-0がFalseを表すらしいことが分かってきます。その中で、論理関数も見つかります。論理関数は、float型の値を引数に取ります:

• 0x11A9 の関数: 符号反転、つまり論理NOT。
• 0x11B1 の関数: 論理OR。
• 0x11D5 の関数: 論理AND。ドモルガンの法則で実装されています。
• 0x120B の関数: 2引数のXOR。
• 0x125A の関数: 3引数のXOR。
• 0x1279 の関数: 3引数のうち2個以上が+0なら戻り値は+0、そうでないなら戻り値は-0。

また、float[32](=float*)型が、先頭indexがLSBを表すuint32_t型を表すことも分かってきます。構築用の関数です:

• 0x12DD の関数: 0用、つまり全要素が-0のfloat[32]を返します。
• 0x130F の関数: uint8_t 型を引数に、その値を表すfloat[32]を返します。配列の先頭要素がLSBを表します。以降同様です。
• 0x13F2 の関数: uint32_t 型を引数に、その値を表すfloat[32]を返します。

float[32]を丸ごと扱う論理関数もあります:

• 0x139D の関数: 2つのfloat[32]の要素ごとの論理ORを取った新しいfloat[32]を返します。
• 0x1548 の関数: 2つのfloat[32]の要素ごとの論理XORを取った新しいfloat[32]を返します。

算術関数はfloat[32]型の値2つを引数に取ります。つまり、実質的にuint32_t同士の演算と同義です:

• 0x14C2 の関数: 和を計算して返します。
• 0x1430 の関数: 差を計算して返します。
• 0x209C の関数: 積を計算して返します。

その他、float[32]の要素を移動させる関数も1つあります:

• 0x134D の関数: 第1引数のfloat[32]から第2引数の数値個数だけ先頭から除外して、後ろへ-0要素を詰めたことと同義の、新しいfloat[32]を返します。

なお、引数が__m128型である関数は、引数をfloat型へ変換すると読みやすくなりました。例えば0x11A9の関数は、IDAは初期状態では次の表示です:

__m128 __fastcall sub_11A9(__m128 a1)
{
  return _mm_xor_ps(a1, (__m128)xmmword_3640);
}

ここで引数や戻り値の型をfloatへ変更すると、符号反転を行うことが明確な表示になりました:

float __fastcall sub_11A9(float a1)
{
  return -a1;
}

また、Pythonで動作検証をする際は、math.copysign関数を使うのが簡単でした。動作検証に使ったコードはGitHubでのtest.pyで公開しています。

(ところで「+0 + -0は+0 になるのは保証されているか」が気になったので調べてみると c++ - What is (+0)+(-0) by IEEE floating point standard? - Stack Overflow が見つかりました。数値丸め設定に依存するようです！ただ実験すると +0 になったので、+0になると仮定して続けました。)

全体の流れの解読

main関数は次のことを行います:

1. 0x2221付近で、コマンドライン引数が与えられていることを検証します。
2. 0x222F付近で、コマンドライン引数の長さが44文字であることを検証します。
3. 0x226Bで呼び出す0x159Dの関数で、コマンドライン引数4文字の8bit分==32bitごとに、bitがONなら+0、OFFなら-0を持つfloat[32]を、44/4の11要素分作成します。全体としてuint32_t[11]相当になります。
4. 0x2273で呼び出す0x20FEの関数で、uint32_t[11]相当の各種要素eについて、((e * 34974707) ^ 2238381247)へ変換します。
5. 0x227Bで呼び出す0x167Aの関数で、uint32_t[11]相当の各種要素について和や差を使った複雑な変換を行います。
   • 読んでいません。z3-solverで逆算します。
6. 0x2283で呼び出す0x21B1の関数で、変換結果が想定の結果になっているか判定します。
   • 0x3040以降にあるfloat[11][32]相当のデータを使っていますが、使っているのは符号ビットのみです。残りの仮数部や指数部や関心外です。
7. 判定結果を出力します。

ソルバーと実行結果

0x167Aの関数の逆コンパイル結果を整形して、ソルバーのz3-solverで逆算しました。その整形結果が400行にも及ぶため、本記事中には掲載しません。詳細はGitHubをご参照ください。

1. 0x167Aの関数の逆コンパイル結果のうち、代入等を伴う重要な部分を抜粋してdecompiled_167A.txtへ保存しました。
2. decompiled_167A.txtの内容をPythonで実行できるよう、加工する処理をparse.pyへ実装しました。
3. parse.pyの実行結果をsolve.pyのconvert_list_complexly関数の本体箇所へ貼り付けました。

最終的なソルバーを実行しました:

$ time ./solve.py
Alpaca{l0gic4l_0per4ti0ns_by_subtr4ction_;D}
./solve.py  1.70s user 0.08s system -245% cpu -0.728 total
$ ./subway 'Alpaca{l0gic4l_0per4ti0ns_by_subtr4ction_;D}'
congratz
$

数秒でフラグを入手できました: Alpaca{l0gic4l_0per4ti0ns_by_subtr4ction_;D}

なおコンテスト中では、何故か本来とは逆の「+0がFalse、-0がTrueの論理体系らしい？」と誤解してしまっていました。なにか辻褄が合わないと彷徨いまくった後に、ようやく気付きました。

感想

• AlpacaHack参加7回目での、初の1桁順位です！
• スキップした3問目は、C++製の複雑そうな問題でした。4問目のsubway問題のほうが読解が素直そうだったので、そちらに走りました。終了6分前にギリギリで正解できました！
• 読解や逆算が大変な処理をz3-solverに任せられると、やっぱり楽です。
• hidden問題の耐逆コンパイルが面白かったです！
• subway問題で、「謎の状態を持ちつつループしている関数がある」→「もしかしたら全加算器のcarry bitでは？」→「足し算関数だった！」等の発見していくのも面白かったです！