NFLabs. エンジニアブログ

セキュリティやソフトウェア開発に関する情報を発信する技術者向けのブログです。

SECCON CTF 13 予選に参加しました! + F is for Flag Writeup

概要

  • SECCON CTF 13 予選で Team Enu は、グローバル 653 チーム中 36 位、国内 303 チーム中 9 位の成績を収めました。決勝へ進出します!
  • 本記事では、reversing ジャンルの F is for Flag 問題を解説します。

はじめに

この記事は、NFLaboratories Advent Calendar 20241 1 日目の記事です。

こんにちは、研究開発部の末廣です。弊社 NFLabs. は、情報セキュリティコンテストイベント SECCON2 のブロンズスポンサーとして協賛しています3

その SECCON の CTF イベント SECCON CTF 13 予選4 に、 NTT グループ有志と、募集5に応募いただいた学生の合同チーム Team Enu6 で参加しました。結果、グローバル 653 チーム中 36 位、国内 303 チーム中 9 位の成績を収めました。この順位は予選を突破して決勝へ進出できる順位です。 Team Enu が SECCON CTF 決勝へ出場するのは2年ぶりです!

筆者は reversing ジャンルの F is for Flag 問題で得点に貢献できました。 Writeup として、本記事ではその問題を解説します。

F is for Flag

amd64 ELF バイナリのフラグチェッカー問題です。実行すると文字列を入力でき、入力した文字列がフラグと一致するかどうかを出力する機能を持つバイナリです。

バイナリを解析すると、入力が正しいフラグかどうかを以下の流れで検証していると分かりました。

  1. 入力内容が 64 文字であることを検証
  2. 入力内容 64 文字を、 4 文字ごとに unsigned int すなわち uint32_t へまとめることで、 16 要素のリストへ変換
  3. 以下の処理を 1 ラウンドとして、 8 ラウンド分ループして変換
    1. リストの 16 要素それぞれについて、 1-nibble 単位で Sbox を使って置き換え
    2. リストの 16 要素それぞれについて、 0x4E6A44B9 を掛ける
    3. リストの 16 要素それぞれについて、現在ラウンド数と 16 要素それぞれの index に依存して、以下のどちらかの処理を実行
      • その index の元の値をそのまま使用、 new_list[index] := old_list[index]
      • 以下の 4 要素の XOR 値を使用、 new_list[index] := v3 ^ v2 ^ v1 ^ v0
        1. v3 := RotateLeft32(old_list[(index + 3) % 16], 29)
        2. v2 := RotateLeft32(old_list[(index + 2) % 16], 17)
        3. v1 := RotateLeft32(old_list[(index + 1) % 16], 7)
        4. v0 := old_list[index]
  4. 変換結果のリストの 16 要素それぞれが、それぞれ特定の内容なら正解と判定

ラウンド中で行っている 3 個の処理はそれぞれ逆変換が存在するため、 8 ラウンド全体についても逆変換できます。そのため最後に比較している内容へ逆変換を施すことで、正解となるフラグを逆算できます。

バイナリの特徴

以降、バイナリ中の相対仮想アドレス (RVA) を 048c 形式で表記します。なお PIE が有効なバイナリであるため、表層解析や静的解析でも各種アドレスは RVA として表示されます。

本問題のバイナリは、次の特徴を持っています。

  • C++ 製かつ not stripped
  • 最適化未実施
  • 値の型として variant 型を使用
  • function やラムダ式を多用
  • 条件分岐を 1 つの関数へ集約
  • 相互再帰によるループの実現

C++ 製かつ not stripped

本問題のバイナリは not stripped であり、シンボル情報が残っています。そのため、使用している標準ライブラリ関数は完全に判明し、本問題固有のアプリケーションコードで使われている関数名も分かります。また、 C++ 製バイナリであることから、各種関数のシンボル名には関数引数の型などの情報がエンコードされています(mangling) 。 mangling されたシンボル名を C++ 方式の型表記へ変換 (demangle) するには、 c++filt7 コマンドで実現できるため、バイナリで使用している型が分かりやすい特徴を持ちます。

一方で、本問題では非常に複雑な型を使用しています。そのため demangle 結果が非常に長くなる場合があります。

例えば、 _ZZ4mainENKUlSt7variantIJjNSt7__cxx1112basic_stringIcSt11char_traitsIcESaIcEEESt10shared_ptrI4ConsEEESt8functionIFS9_vEESC_E_clES9_SC_SC_ というシンボル名は、 main::{lambda(std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >, std::function<std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> > ()>, std::function<std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> > ()>)#1}::operator()(std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >, std::function<std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> > ()>, std::function<std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> > ()>) const へ demangle されます。

別の例として、 _ZSt8__invokeIRK3fixIZ4mainEUlT_St7variantIJjNSt7__cxx1112basic_stringIcSt11char_traitsIcESaIcEEESt10shared_ptrI4ConsEEESC_SC_E_EJSC_RSC_SC_EENSt15__invoke_resultIS1_JDpT0_EE4typeEOS1_DpOSJ_ というシンボル名は、 std::__invoke_result<fix<main::{lambda(auto:1, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >)#1}> const&, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >&, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> > >::type std::__invoke<fix<main::{lambda(auto:1, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >)#1}> const&, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >&, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> > >(fix<main::{lambda(auto:1, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >)#1}> const&, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >&&, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >&, std::variant<unsigned int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::shared_ptr<Cons> >&&) へ demangle されます。

デバッガによっては、関数のシンボル名を demangle して表示する機能を持ちます。通常のバイナリでは demangle された状態の方が読みやすいのですが、本問題のバイナリでは途方もない長さの demangle 結果が表示されることでデバッガ本来の出力が埋もれやすいです。

最適化未実施

C++ コンパイラには、オプションとして最適化レベルを指定可能なものが多いです。最適化を有効にすると関数のインライン展開や未使用変数の削除等により、実行速度向上やバイナリサイズ削減を重視するコンパイルが可能です。しかし本問題のバイナリでは、どうやら最適化が実施されていない模様です。

関数引数を追跡した結果、実際は未使用であるため追跡する必要がなかったと分かることがありました。また、引数 5 個ほどを受け取って別の関数へ転送するだけの関数が 3 段階挟まっていることがあり、関数引数の型や便宜上の名前を伝搬させていくことが大変でした。加えて、 Perfect forwarding8 で使われる std::forward9 関数は引数をそのまま返すだけですが、本バイナリでは呼び出し箇所が多数存在していて引数と戻り値が見た目上分断されるため、その意味でも解析しづらい面がありました。

値の型として variant 型を使用

本バイナリでは、フラグ入力を受け取る箇所以外のほぼ全てで、std::variant10 型を使用しています。上の demangle 結果にも登場している通り、 vairant 型のテンプレート型引数はシンボル情報から分かります。本バイナリの場合、次の 3 個の型を統合するために variant 型を使用しています。

  1. unsigned int 型。この型は、各種変換途中や、最後に比較する値として使われます。また、比較演算子結果等の bool 型の値を保持するためにも使われます。
    • 15D54 の関数で unsigned int 型から構築します。
    • 16672 の関数で bool 型から構築します。
  2. std::string 型。この型は、フラグ入力として入力された内容を保持するために使われます。
    • 16AAA の関数で string から構築します。
    • 1C03E の関数で char* から構築します。
  3. std::shared_ptr<Cons> 型。この型は、実質的に struct { unsigned int head; Cons tail; } の Consセルを使ったリストを表現するために使われています。
    • 3BC0の関数で、Consセルを構築します。
    • 使用箇所は次の関数です。
      • 3C38 の関数で Consセルから head 部分を取得します。
      • 3C78 の関数で Consセルから tail 部分を取得します。
      • 3DF83F7A の関数で Consセルのリストから index 番目の head を取得します。後述の方法で、 76FC74EE の関数で相互再帰することで、ループします。

本問題の様々な関数で、この variant 型を扱います。使用箇所によっては、特定の variant 型変数は必ず unsigned int 型を所持している等の前提で使用しているため、各種 variant 型変数が扱う値を追跡することが重要です。本記事ではこの variant 型に複数回言及するため、便宜上 ChallengeVariant という名前で扱います。

using ChallengeVariant = std::variant<unsigned int, std::string, std::shared_ptr<Cons>>;

function やラムダ式を多用

上の demangle 結果にも登場している通り、本バイナリでは std::function11 を使用しています。 function へ格納する関数オブジェクトは、シンボル名から判断するにすべてラムダ式12であり、かつ変数の参照キャプチャを行っているらしいラムダ式ばかりです。

変数キャプチャを行うラムダ式から function オブジェクトを構築する場合、各ラムダ式用の構造体を引数として取るような処理となるようです。例えば main 関数の 67D7 付近で、 549E 関数用の function オブジェクトを構築する箇所は、次のような処理を行っています。

// 解析時に定義した、ラムダ式でキャプチャしている内容を表現するための構造体
struct LambdaParam_549E
{
    const LambdaParam_CAEE *p_lambda_param_CAEE;
    const LambdaParam_C2A6 *p_lambda_param_C2A6;
    const LambdaParam_BAD8 *p_lambda_param_BAD8;
    const std::string *p_std_string_input;
    const ChallengeVariant *p_variant_cons16_expected_result;
};

// キャプチャ内容を構造体で準備しています
// ラムダ式内部で更に別のラムダ式を呼び出す場合は、構造体を入れ子で扱います
lambda_param_549E.p_lambda_param_CAEE = &lambda_param_CAEE;
lambda_param_549E.p_lambda_param_C2A6 = &lambda_param_C2A6;
lambda_param_549E.p_lambda_param_BAD8 = &lambda_param_BAD8;
lambda_param_549E.p_std_string_input = &std_string_input;
lambda_param_549E.p_variant_cons16_expected_result = &variant_cons16_expected_result;
// function オブジェクトのコンストラクタ呼び出し時にキャプチャ内容を渡します
// なお、最終的に 549E 関数を呼び出すための関数ポインタはコンストラクタ内部で設定しています
StdFunctionConstructorForLambda549E(
    &std_function_lambda_549E_set_0_if_correct_input,
    &lambda_param_549E);

バイナリを解析する中で、ラムダ式用の構造体を 23 種類定義して解析を進めました。

条件分岐を1つの関数へ集約

本バイナリの、標準ライブラリ部分を除外したアプリケーションコード部分で、いわゆる if-else 文による条件分岐は 3B3C でのみ登場します。 3B3C の関数を C++ で表現すると、次のようになります。

void IfThenElse(
    ChallengeVariant *p_variant_result,
    const void *not_used,
    const ChallengeVariant &variant_condition,
    const std::function<void(ChallengeVariant*)> &func_if_true,
    const std::function<void(ChallengeVariant*)> &func_if_false)
{
    if (std::get<0>(variant_condition) != 0)
    {
        func_if_true(p_variant_result);
    }
    else
    {
        func_if_false(p_variant_result);
    }
}

function 型 2 つと条件分岐用の variant 型を引数に取り、結果を variant 型ポインタへ書き込むことで、呼び出し元に値を返す機能を持ちます。本バイナリのアプリケーションコード部分は、すべての条件分岐を 3B3C の関数で行います。

なお、各種 variant の加算や減算等を行う関数でも、第 2 引数は未使用の関数ばかりでした。出力用 variant 型引数を取る際の、コンパイラ都合によるものと考えています。

相互再帰によるループの実現

本バイナリの、標準ライブラリ部分を除外したアプリケーションコード部分には、いわゆる for 文や while 文によるループは全く登場しません。本バイナリのループは、関数の再帰呼び出しと、前述の条件分岐用関数による再帰終端判定で実現しています。

ループ処理を 1 段階進めるだけでも、ループの終了判定を行う関数と、ループカウンタを増やしつつループ本体処理を行う関数の 2 つに分かれています。そのため解析時は、ループ全体として何を実現しているのかを追跡することが重要です。

例えば、 76FC74EE の関数で相互再帰することで Consセルのリストから index 番目の head を取得する処理は、次のようになっています。

// 指定 index 番目の head を取得する処理の、ループ終了判定を行う関数です
ChallengeVariant *Lambda76FC_GetNthHead_CheckLoopCondition(
    ChallengeVariant *p_variant_result,
    const LambdaParam_76FC *p_lambda_param_76FC,
    const LambdaParam_76FC *p_lambda_param_76FC_1, // 第 2 引数と同一オブジェクトのアドレスを第 3 引数でも取っています
    const ChallengeVariant *p_variant_cons_list, // この Consセルのリストが処理対象です
    const ChallengeVariant *p_variant_loop_limit_for_76FC, // 目標のループ回数で、再帰中不変です
    const ChallengeVariant *p_variant_loop_count_for_76FC) // 現在のループ回数で、相互再帰 1 回で 1 増加します
{
    // ローカル変数定義、省略

    // ループ本体処理とループカウンタ増加を担う関数オブジェクトを構築
    maybe_not_used_0 = p_lambda_param_76FC->maybe_not_used_0;
    p_lambda_param_74EE.pp_lambda_param_76FC = &p_lambda_param_76FC_1;
    p_lambda_param_74EE.maybe_not_used_8 = p_lambda_param_76FC->maybe_not_used_18;
    p_lambda_param_74EE.p_variant_cons_list = p_variant_cons_list;
    p_lambda_param_74EE.p_variant_loop_limit_for_76FC = p_variant_loop_limit_for_76FC;
    p_lambda_param_74EE.maybe_not_used_20 = p_lambda_param_76FC->maybe_not_used_20;
    p_lambda_param_74EE.p_variant_loop_count_for_76FC = p_variant_loop_count_for_76FC;
    StdFunctionConstructorForLambda74EE(
        &std_function_lambda_74EE_loop_body_wrapper,
        &p_lambda_param_74EE);

    // ループ最後に Consセルの head を返すための関数オブジェクトを構築
    lambda_param_72B4.p_not_used = p_lambda_param_76FC->maybe_notused;
    lambda_param_72B4.p_variant_cons_list = p_variant_cons_list;
    StdFunctionConstructorForLambda72B4(
        &std_function_lambda_72B4_cons_cell_get_head,
        &lambda_param_72B4);

    // ループ終了条件を満たしているか判定
    notUsed_8 = p_lambda_param_76FC->notUsed_8;
    MayBe_CopyVariant(
        &variant_loop_limit_for_76FC,
        p_variant_loop_limit_for_76FC);
    MayBe_CopyVariant(
        &variant_loop_count_for_76FC,
        p_variant_loop_count_for_76FC);
    Calculate_Equal(
        &variant_has_reach_loop_limit,
        notUsed_8,
        &variant_loop_count_for_76FC,
        &variant_loop_limit_for_76FC);

    // ループ終了条件を満たしていればループ最後の処理を、満たしていなければループ本体を、 function 経由で実行
    IfThenElse(
        p_variant_result,
        maybe_not_used_0,
        &variant_has_reach_loop_limit,
        &std_function_lambda_72B4_cons_cell_get_head,
        &std_function_lambda_74EE_loop_body_wrapper);

    // ローカル変数のデストラクタ呼び出し、省略

    return p_variant_result;
}

// 指定 index 番目の head を取得する処理の、ループ本体を行う関数です
// Consセルの tail 取得と、ループカウンタのインクリメントを行います
ChallengeVariant *ProcLambda_74EE_GetNthHead_LoopBody(
    ChallengeVariant *p_variant_result,
    const LambdaParam_74EE *p_lambda_param_74EE)
{
    // ローカル変数定義、省略

    // ループカウンタをインクリメント
    pp_lambda_param_76FC = p_lambda_param_74EE->pp_lambda_param_76FC;
    not_used = p_lambda_param_74EE->maybe_not_used_20;
    value1 = 1;
    VariantConstructorFromUnsignedInt(
        &variant_value1,
        &value1);
    MayBe_CopyVariant(
        &variant_loop_count_for_76FC,
        p_lambda_param_74EE->p_variant_loop_count_for_76FC);
    Calculate_Add(
        &variant_loop_count_for_76FC_incremented,
        not_used,
        &variant_loop_count_for_76FC,
        &variant_value1);

    // Consセルの tail をたどる
    p_variant_loop_limit_for_76FC = p_lambda_param_74EE->p_variant_loop_limit_for_76FC;
    maybe_not_used_8 = p_lambda_param_74EE->maybe_not_used_8;
    MayBe_CopyVariant(
        &variant_cons_list,
        p_lambda_param_74EE->p_variant_cons_list);
    ConsCell_GetTail(
        &variant_cons_tail,
        maybe_not_used_8,
        &variant_cons_list);

    // 更新後の状態でループ終了条件を相互再帰で再評価
    Lambda76FC_GetNthHead_CheckLoopCondition_Wrapper(
        p_variant_result,
        pp_lambda_param_76FC,
        &variant_cons_tail,
        p_variant_loop_limit_for_76FC,
        &variant_loop_count_for_76FC_incremented);

    // ローカル変数のデストラクタ呼び出し、省略

    return p_variant_result;
}

実行内容詳細

解析結果の総まとめとして、各種処理をどのアドレスで行っているかを詳細に記述します。

  1. main 関数の 5706 で、フラグ入力
  2. main 関数の 570B5B8D で、正解判定として最後に比較するための Consセルのリストを構築
  3. main 関数の 5D6C61EE で、 sbox 用 Consセルのリストを構築
  4. main 関数の 63CD66E9 で、直接的または間接的に使用するラムダ式のための、各種キャプチャ用構造体を準備
    • この中に、入力文字列、正解判定用 Consセルのリスト、 Sbox 用 Consセルのリストを含みます
  5. main 関数の 6784 で、入力内容が 64 文字であるか判定
  6. main 関数の 67AF から呼び出す 3B3C の条件分岐関数で、入力が 64 文字である場合は 549E 関数でさらなる判定を開始
    1. 5508 から呼び出す関数で、 BAD8B0F8A6DE の関数でループしつつ入力内容 64 文字を 4 文字ごとに unsigned int すなわち uint32_t へまとめることで、 16 要素の Consセルのリストへ変換
    2. 551B から呼び出す関数で、 C2A6C040 の関数でループしつつ、次の内容 1 回を 1 ラウンドとして、 8 ラウンド分ループして変換
      1. C11F から呼び出す関数で、 887085F8 の関数で外側ループ、 812C7B70 の関数で内側ループをしつつ、 Consセルのリストの各要素を 1-nibble 単位で Sbox を使って置き換え
      2. C138 から呼び出す関数で、 8FB48CF4 の関数でループしつつ、 Consセルのリストの各要素へ 0x4E6A44B9 を掛ける
      3. C154 から呼び出す関数で、 A3B09994 の関数でループしつつ、現在ラウンド数と現在のループ index へ依存して、以下のどちらかの処理を実行
        • 949A の関数では、その index の元の値をそのまま使用、 new_list[index] := old_list[index]
        • 96D64278 の関数で、次の 4 要素の XOR 値を使用、 new_list[index] := v3 ^ v2 ^ v1 ^ v0
          1. v3 := RotateLeft32(old_list[(index + 3) % 16], 29)
          2. v2 := RotateLeft32(old_list[(index + 2) % 16], 17)
          3. v1 := RotateLeft32(old_list[(index + 1) % 16], 7)
          4. v0 := old_list[index]
    3. 5534 から呼び出す関数で、 CAEEC888 の関数でループしつつ、変換結果が特定の内容と一致するなら 0 に、不一致なら 1 に判定結果を設定
  7. main 関数の 67D7 で、判定結果が 0 なら正解時用の、それ以外なら失敗時用の文字列を、出力内容として設定
  8. main 関数の 67ED で、設定した文字列を出力

フラグ計算ソルバ

フラグを逆算して計算するPythonコードを以下に記載します。

import z3

# (ラウンド数, リスト中index)の組について、9F29での分岐を表すテーブルです
CONDITION_TABLE_9F29 = {
    (0, 0): 0,
    (0, 1): 0,
    (0, 2): 0,
    (0, 3): 0,
    (0, 4): 0,
    (0, 5): 0,
    (0, 6): 0,
    (0, 7): 0,
    (0, 8): 0,
    (0, 9): 0,
    (0, 10): 0,
    (0, 11): 0,
    (0, 12): 0,
    (0, 13): 1,
    (0, 14): 1,
    (0, 15): 1,
    (1, 0): 1,
    (1, 1): 0,
    (1, 2): 0,
    (1, 3): 0,
    (1, 4): 0,
    (1, 5): 0,
    (1, 6): 0,
    (1, 7): 0,
    (1, 8): 0,
    (1, 9): 0,
    (1, 10): 0,
    (1, 11): 0,
    (1, 12): 0,
    (1, 13): 0,
    (1, 14): 1,
    (1, 15): 1,
    (2, 0): 1,
    (2, 1): 1,
    (2, 2): 0,
    (2, 3): 0,
    (2, 4): 0,
    (2, 5): 0,
    (2, 6): 0,
    (2, 7): 0,
    (2, 8): 0,
    (2, 9): 0,
    (2, 10): 0,
    (2, 11): 0,
    (2, 12): 0,
    (2, 13): 0,
    (2, 14): 0,
    (2, 15): 1,
    (3, 0): 1,
    (3, 1): 1,
    (3, 2): 1,
    (3, 3): 0,
    (3, 4): 0,
    (3, 5): 0,
    (3, 6): 0,
    (3, 7): 0,
    (3, 8): 0,
    (3, 9): 0,
    (3, 10): 0,
    (3, 11): 0,
    (3, 12): 0,
    (3, 13): 0,
    (3, 14): 0,
    (3, 15): 0,
    (4, 0): 0,
    (4, 1): 1,
    (4, 2): 1,
    (4, 3): 1,
    (4, 4): 0,
    (4, 5): 0,
    (4, 6): 0,
    (4, 7): 0,
    (4, 8): 0,
    (4, 9): 0,
    (4, 10): 0,
    (4, 11): 0,
    (4, 12): 0,
    (4, 13): 0,
    (4, 14): 0,
    (4, 15): 0,
    (5, 0): 0,
    (5, 1): 0,
    (5, 2): 1,
    (5, 3): 1,
    (5, 4): 1,
    (5, 5): 0,
    (5, 6): 0,
    (5, 7): 0,
    (5, 8): 0,
    (5, 9): 0,
    (5, 10): 0,
    (5, 11): 0,
    (5, 12): 0,
    (5, 13): 0,
    (5, 14): 0,
    (5, 15): 0,
    (6, 0): 0,
    (6, 1): 0,
    (6, 2): 0,
    (6, 3): 1,
    (6, 4): 1,
    (6, 5): 1,
    (6, 6): 0,
    (6, 7): 0,
    (6, 8): 0,
    (6, 9): 0,
    (6, 10): 0,
    (6, 11): 0,
    (6, 12): 0,
    (6, 13): 0,
    (6, 14): 0,
    (6, 15): 0,
    (7, 0): 0,
    (7, 1): 0,
    (7, 2): 0,
    (7, 3): 0,
    (7, 4): 1,
    (7, 5): 1,
    (7, 6): 1,
    (7, 7): 0,
    (7, 8): 0,
    (7, 9): 0,
    (7, 10): 0,
    (7, 11): 0,
    (7, 12): 0,
    (7, 13): 0,
    (7, 14): 0,
    (7, 15): 0,
}

UINT32_MOD = 0x1_0000_0000
CONS_LIST_LENGTH = 16

def RotateLeft32(x: int, bit: int) -> int:
    MASK = UINT32_MOD - 1
    if isinstance(x, int):
        assert 0 <= x <= MASK
        assert 0 <= bit <= 31
        return ((x << bit) & MASK) | (x >> (32 - bit))
    else:
        return ((x << bit) & MASK) | z3.LShR(x, 32 - bit)

SBOX = [3, 14, 1, 10, 4, 9, 5, 6, 8, 11, 15, 2, 13, 12, 0, 7]
assert len(SBOX) == 16

def create_inv_sbox() -> list[int]:
    result = [-1] * 16
    for i, x in enumerate(SBOX):
        result[x] = i
    return result

INV_SBOX = create_inv_sbox()
for i in range(CONS_LIST_LENGTH):
    assert i == INV_SBOX[SBOX[i]]

def convert_input_string_to_cons_list(flag: str) -> list[int]:
    assert len(flag) == CONS_LIST_LENGTH * 4
    result = []
    for i in range(len(flag) // 4):
        temp = 0
        for j in range(4):
            temp |= ord(flag[4 * i + j]) << (j * 8)
        result.append(temp)
    return result

def print_cons_list(current: list[int]):
    for i in range(len(current)):
        for j in range(4):
            c = chr(current[i] >> (j * 8) & 0xFF)
            print(c, end="")
    print()

def transform(cons_list: list[int]) -> list[int]:
    assert len(cons_list) == CONS_LIST_LENGTH
    for round_index in range(8):
        cons_list = [substitute_nibbles(x) for x in cons_list]
        cons_list = [multiply_0x4E6A44B9(x) for x in cons_list]
        cons_list = mix_elements(cons_list, round_index)
    return cons_list

def inv_transform(cons_list: list[int]) -> list[int]:
    assert len(cons_list) == CONS_LIST_LENGTH
    for round_index in range(7, -1, -1):
        cons_list = inv_mix_elements(cons_list, round_index)
        cons_list = [inv_multiply_0x4E6A44B9(x) for x in cons_list]
        cons_list = [inv_substitute_nibbles(x) for x in cons_list]
    return cons_list

def substitute_nibbles(value: int) -> int:
    assert 0 <= value < UINT32_MOD
    result = 0
    for nibble_index in range(8):
        x = (value >> (nibble_index * 4)) & 0xF
        result |= SBOX[x] << (nibble_index * 4)
    return result

def inv_substitute_nibbles(value: int) -> int:
    assert 0 <= value < UINT32_MOD
    result = 0
    for nibble_index in range(7, -1, -1):
        x = (value >> (nibble_index * 4)) & 0xF
        result |= INV_SBOX[x] << (nibble_index * 4)
    return result

def multiply_0x4E6A44B9(value: int) -> int:
    return (value * 0x4E6A44B9) % UINT32_MOD

def inv_multiply_0x4E6A44B9(value: int) -> int:
    inv_0x4E6A44B9 = pow(0x4E6A44B9, -1, UINT32_MOD)
    return (value * inv_0x4E6A44B9) % UINT32_MOD

def mix_elements(cons_list: list[int], round_index: int) -> list[int]:
    assert len(cons_list) == CONS_LIST_LENGTH
    result: list[int] = []
    for list_index in range(CONS_LIST_LENGTH):
        if CONDITION_TABLE_9F29[(round_index, list_index)]:
            result.append(cons_list[list_index])
        else:
            next1 = RotateLeft32(cons_list[(list_index + 3) % 16], 29)
            next2 = RotateLeft32(cons_list[(list_index + 2) % 16], 17)
            next3 = RotateLeft32(cons_list[(list_index + 1) % 16], 7)
            next4 = cons_list[(list_index + 0) % 16]  # rotateなし。
            next_xor = next1 ^ next2 ^ next3 ^ next4
            result.append(next_xor)
    return result

def inv_mix_elements(cons_list: list[int], round_index: int) -> list[int]:
    assert len(cons_list) == CONS_LIST_LENGTH
    solver = z3.Solver()
    bit_vec_list = [z3.BitVec(f"previous[{i}]", 32) for i in range(CONS_LIST_LENGTH)]

    for list_index in range(CONS_LIST_LENGTH - 1, -1, -1):
        if CONDITION_TABLE_9F29[(round_index, list_index)]:
            solver.add(bit_vec_list[list_index] == cons_list[list_index])
        else:
            next1 = RotateLeft32(bit_vec_list[(list_index + 3) % 16], 29)
            next2 = RotateLeft32(bit_vec_list[(list_index + 2) % 16], 17)
            next3 = RotateLeft32(bit_vec_list[(list_index + 1) % 16], 7)
            next4 = bit_vec_list[list_index]  # rotateなし。
            next_xor = next1 ^ next2 ^ next3 ^ next4
            solver.add(next_xor == cons_list[list_index])

    assert solver.check() == z3.sat

    model = solver.model()
    candidate = [model[a].as_long() for a in bit_vec_list]

    # 2個目の解が無いことを検証
    block = []
    for i in range(CONS_LIST_LENGTH):
        block.append(bit_vec_list[i] != candidate[i])
    solver.add(z3.Or(block))
    assert solver.check() != z3.sat

    return candidate

EXPECTED_RESULT = [
    0x11793013,
    0x88D2EC9B,
    0x2C0CCCDD,
    0x97AEF869,
    0x34BC7C60,
    0xF86C82D7,
    0x927B5BD9,
    0xD5689A8C,
    0x451F151A,
    0xF389C4A,
    0xD2C1D5AF,
    0x82841CF4,
    0xBD18775A,
    0xBE8AFE4D,
    0x1904C652,
    0xB7E9A2A4,
]
assert len(EXPECTED_RESULT) == CONS_LIST_LENGTH
print_cons_list(inv_transform(EXPECTED_RESULT))

実行すると、フラグが SECCON{fUnCt10n4l_pRoGr4mM1n6_1s_pR4c7iC4lLy_a_pUr3_0bfu5c4T1oN} と分かります。

おわりに

コンテスト期間中、筆者は本記事で紹介した問題に多くの時間を費やしました。最終的に解析が完了し、正解することはできましたが、より効率的に解析する方法を身に着けていきたいです。一方で、フラグ内容が表す通り、問題バイナリは関数型プログラミング手法で実装されています。C++で関数型プログラミングを実装した場合の構造が理解できて、非常に面白く感じました。

チームとしては、様々なメンバーが幅広いジャンルで正解していったことで、決勝へ出場できる順位を達成できました。ひとえにチームメンバーのおかげです。 筆者自身は SECCON CTF 決勝への出場経験はまだありませんが、もし出場できるなら精一杯頑張ります!

最後になりましたが本記事で紹介している内容が、問題へ取り組んだ方や、これから CTF を始めようと考える方の参考になれば幸いです。