📘

セキュリティ・キャンプ2025全国大会応募課題を "2つ分" 晒してみる (Y1ゼミ, L1ゼミ)

2025/06/25に公開

 はじめに先日、セキュリティ・キャンプ2025 全国大会にて、「Code Sanitizer・Fuzzer自作ゼミ」に参加することになりました。
https://www.ipa.go.jp/jinzai/security-camp/2025/camp/zenkoku/index.html
セキュリティ・キャンプでは、"応募課題晒し"なる謎文化が存在しているようなので、私もこれに乗っかって晒そうと思います。

 ひとひねり(？)せっかくなら他人と違うことがしてみたいので、私は応募課題を 2つ 晒そうと思います。
私が応募したゼミは、以下の3つでした。
第1希望: Y1:Code Sanitizer・Fuzzer自作ゼミ
第2希望: Z1:プログラム難読化・解析ゼミ
第3希望: L1：Rust検証器自作ゼミ
このうち第1希望に通ったわけですが、第3希望のRust検証器自作ゼミの課題もかなり本腰入れて取り組んでいたので、同時に晒したいと思います。こちらも取り組んでいる中で、「こっちを第1希望にしていても良かったな〜〜」と思えるほど楽しい課題でした。セキュリティ・キャンプでは他のゼミの活動の様子を覗き見することができるようなので、積極的に活用していきたいと思います。ちなみに第2希望の応募課題に関しては今の自分にとっては難しく、最後まで完成させることは出来ませんでした。(興味はあったんですけどね！)

 Y1:Code Sanitizer・Fuzzer自作ゼミまずは実際に選考を通過したCode Sanitizer・Fuzzer自作ゼミから。

 設問1本講義の受講生には、大会期間中にサニタイザまたはFuzzer、あるいはその両方を受講生のすきな形で実装していただきます。

そのどちらをどのように実装していくかは事前学習期間中に話し合いながら決めていく予定ですが、現時点でのご興味をお伺いします。

サニタイザまたはFuzzerのうち、興味のあるほうを選択し、その理由を簡潔に述べてください。

また、特定のサニタイザやFuzzerを実装することに興味がある場合は、そのアイデアを教えてください。
現時点では、Fuzzer に興味があります。具体的には、単一のプログラムに対し Fuzzing を行って脆弱性を発見する Fuzzing ではなく、同じ目的を持って開発された複数のプログラムの、同じ入力に対する挙動の差に注目して脆弱性を発見する手法に興味を持っています。 

例えば、Rustlantis という Rust コンパイラの脆弱性を検査する Fuzzer がそのような特徴を持っています。Rustlantis は Rust の中間表現 (MIR) を自動生成する Fuzzer で、異なる Rust バックエンド (rustc、LLVM、Cranelift) に MIR を入力として与え出力された実行ファイルの実行結果を比較することで、コンパイラの挙動を検査することができます。また、Rustlantis は Rust において、ターゲットへの入力に MIR を採用した初めての Fuzzer です。MIR を扱うことによってプログラム中の未定義動作の有無を厳密に管理しやすく、実際に Rustlantis は未定義動作を含まず必ず終了することが保証された MIR を吐ける仕組みになっています。この特徴によって、異なるバックエンドでコンパイルされた実行ファイルを実行した際の結果に差分が生じた場合、それはプログラム側の問題ではなく「コンパイラ側のバグ」であると断定しやすくしているようです。 

対象への入力として常に valid な MIR を生成する Fuzzer という意味でも面白いですし、複数かつ特定のプログラムに対する専用の Fuzzer という意味でも面白いです。実際に Rustlantis のリポジトリを見ると、README に Rustlantis によって発見された Rust バックエンドの脆弱性が数多く載せられています (ソース)。 

Rust バックエンドに限らず、「同じ目的を持って開発された複数のプログラム」は、例えばブラウザエンジンや JavaScript エンジンなど沢山あると思うので、そのような特定のプログラムに対する専用の Fuzzer を作ってみたいです。できればキャンプの期間中に、実際に脆弱性を発見してみたいです。

 設問2以下の条件を満たす脆弱性報告を 1 つ選び、続く質問に答えてください。
CVE 識別番号が発行されている
2019 年以降に発見された (CVE-2019 以降)
C または C++で書かれたプログラムにおける未定義動作に起因する
Fuzzing により発見された
[質問]
脆弱性の原因となった未定義動作について、数文で簡単に説明してください。
動作が未定義であると明示的に定義している C または C++ 言語仕様のセクションはどれですか。> この際、正式な ISO の言語仕様を閲覧するためには高額な費用が必要となるため、無料で閲覧可能な working draft をバージョンを明示したうえで引用することとしてください。
Fuzzing に使用されたツールはどのようなものでしたか。
Fuzzing によって発見された面白い脆弱性の例として、CVE-2022-3602 を挙げます。この脆弱性を端的に説明すると、OpenSSL 内の Punycode デコーダに Off-by-one error が存在したことによって Buffer Overflow が発生する、というものです。OpenSSL が扱う X.509 証明書には、識別名やメールアドレス、ドメイン名、URI などに適用される名前制約があるのですが、そのうち、メールアドレスに対する Punycode のデコード処理に問題があり、Buffer Overflow が発生します。面白いのは、この脆弱性が典型的な Off-by-one error により引き起こされたものであるということです。
CVE-2022-3602 の実際の修正コミットは こちら にあります。個人的には、CVSS スコアは High であるのにも関わらず、修正コミットはたった 1byte であるのが面白ポイントだと思っています (Off-by-one error らしい)。
また、実際にこのような確保したバッファの領域を超える書き込みが未定義動作であるとする明示的な定義は、例えば C23 の最終ドラフトである WG14 N3096 の 6.5.6 Additive operators からも確認することができます。以下は、該当箇所の引用です。
If the pointer operand and the result do not point to elements of the same array object or one past the last element of the array object, the behavior is undefined. If the addition or subtraction produces an overflow, the behavior is undefined. If the result points one past the last element of the array object, it shall not be used as the operand of a unary * operator that is evaluated.
これはつまり、「配列オブジェクトの最後の要素の一つ先を指している場合、その動作は未定義」「加算または減算によってオーバーフローが発生した場合、動作は未定義」である、ということを表しています。また、付録の J.2 Undefined behavior にも、
An array subscript is out of range, even if an object is apparently accessible with the given subscript (as in the lvalue expression a[1][7] given the declaration int a[4][5]) (6.5.6).
との記述があります。よって、確保したバッファの領域を超えて書き込みを行うことは、C 言語の仕様において未定義であると言えます。
この脆弱性は、libFuzzer と Address Sanitizer を組み合わせた Fuzzing により発見されました。 (ソース)。この脆弱性は、原因が単純であって、更には OpenSSL に既に X.509 証明書を対象とした Fuzzing のテストが用意されていたのにも関わらず、それまでずっと未検出であったというところが興味深いです。入力 (X.509 証明書) が取りうる空間が膨大で既存の Fuzzing では適切に入力をカバー出来ていなかったことと、脆弱であった関数 ossl_punycode_decode が深い関数呼び出しの先にあったことが原因として挙げられています。実際に、ossl_punycode_decode を含め X.509 証明書の名前制約に関するコードには、元々行われていた Fuzzing では到達できていなかったようです。(ソース)。実際に CVE-2022-3602 を発見した Fuzzing では、有効な証明書や既知のマーカーを含む証明書を seed として基本的なパースを通過できるようにし、ossl_punycode_decode を含むより深いロジックに到達できる入力を効率的に生成できるようにしたり、X.509 証明書で用いられるエンコードや OID の辞書を使用した Grammar-based な Fuzzing を行うことで発見されています。Fuzzing 自体は万能ではなく、未到達のコードがあれば例え単純なものであっても脆弱性は残ってしまうことを示す良い事例であるなと思いました。 

ちなみに Google の OSS-Fuzz チームが 2023 年に発表した新しい Fuzzing の手法でも、CVE-2022-3602 を再発見することができたようです (ソース)。この手法では、LLM に fuzz target を自動生成させるというアプローチが取られていました。他にも、別の OSS に対する Fuzzing のケースでは、Coverage を最大 31 %向上させることができたようです。C 言語の残したレガシーなメモリ問題を現代の LLM が解決していく様子は、どこか趣を感じます。

 設問3コンパイラを自作した経験がある方は、そのソースコードを閲覧できる URL (GitHub リポジトリ等)を記入してください。

自作経験がない方でも、提出期間内に実装する時間と異常なまでのやる気がある場合はチャレンジしてくださっても大丈夫ですが、無理はなさらないでください。
（関数呼び出しが可能な程度完成度の）コンパイラの実装経験がある場合は、応募課題は以上となります。設問 4 以降は無回答として問題ありません。

実装経験がない方は、設問 4 に進んでください。本講義では、講師の用意したコンパイラの上にサニタイザ・Fuzzer を実装する形で進めることも可能です。コンパイラの実装経験がなくても全く問題はありません。
チュートリアルを触った程度であれば、低レイヤを知りたい人のための C コンパイラ作成入門 を過去に多少なぞったことがあります。あまり写経が好きではないので実際に書いたのは括弧付きの四則演算が行える程度のところまでですが (リポジトリ)、記事自体は関数呼び出しや型やポインタを扱うところまでは読了しています。関数呼び出しのプロローグやエピローグにおいて何が行われているか、レジスタの保存や復元、スタックの動作などはざっくりと理解しているつもりです。

 設問4アドレスサニタイザが以下の Heap Use-after-Free を検知できる仕組みを簡潔に説明してください。
#include "stdlib.h"
#include "stdio.h"

int main(void) {
    char* p1 = malloc(1);
    free(p1);
    printf("char: '%c'\n", *p1);
    return 0;
}
https://godbolt.org/z/PoP18P8We
Address Sanitizer は、プログラムのコンパイル時に、メモリの状態を記録する Shadow memory を操作する命令を追加で挿入し、malloc と free に関しては、Address Sanitizer の持つ専用の実装に置き換えられます。char* p1 = malloc(1); では、バッファの両端 1B に Redzone を配置して (実際には Shadow memory に両端のアドレスが Redzone であるという poison を記録して)、参照してはならない場所としてマークします。また、free(p1); では、すぐにはメモリを解放せずに p1 が使用していた領域を quarantine というキューにメモし (すぐに他の malloc で使わせないため)、Shadow memory にも Freed memory として記録します。このプログラムでは起こりませんが、quarantine がいっぱいになると、古いメモリから実際に解放していきます。また、*p1 のようなアドレス参照は、参照しようとしているアドレスの Shadow memory の poison を確認してから実際にアクセスを行うチェック付きの命令に置き換えられます。 

実行時には、free(p1); 時に p1 のアドレスに対応する Shadow memory の poison が Freed memory (0xFD) として記録します。次に、printf("char: '%c'\n", *p1); で p1 が参照されたタイミングで p1 の poison を検査し、0xFD を見つけて Heap Use-after-Free を検知します。その後は、適当なエラーレポートを吐いて終了します。 

以上が、Address Sanitizer が与えられたプログラムの Heap Use-after-Free を検知する仕組みです。

 設問 5本講義は C++を主に使用していきます。C/C++をはじめとした言語におけるプログラミング経験等を簡単に PR してください。

また、サニタイザや Fuzzer を使った経験があれば、そちらも記述してください。

応募期間中に取り組んでいただいた内容でも結構です。
課題 2 にて挙げた CVE-2022-3602 に関して、脆弱性を持っていた ossl_punycode_decode をほぼ同じシグニチャで小さく実装し直して、Address Sanitizer を使って Buffer Overflow を検知してみました。プログラムは以下の通りです。
#include <stdio.h>
#include <string.h>

int decode(const char *input, size_t input_len, char *output, size_t *out_len)
{
    size_t written_out = 0;
    size_t max_out = *out_len;

    for (size_t i = 0; i < input_len; ++i)
    {
        if (written_out > max_out)
            return 0;

        output[written_out++] = input[i];
    }

    *out_len = written_out;
    return 0;
}

int main(void)
{
    const char *input = "foobar";
    size_t input_len = strlen(input);

    char output[5];
    size_t out_len = sizeof(output);

    decode(input, input_len, output, &out_len);
    printf("Decoded string: %.*s\n", (int)out_len, output);

    return 0;
}
不正な境界チェックがあるのは、if (written_out > max_out) の部分です。これは、実際の修正コミット で修正された部分に対応するものです。この境界チェックは written_out が max_out を超えた場合に 0 を返すようになっていますが、このままでは written_out == max_out となった後も追加で 4byte (index 1 つ分) のコピー処理が走ってしまいます。Address Sanitizer を使ってこのプログラムを実行すると、以下のように Stack Buffer Overflow が検知されます。
実行環境: Linux 6.14.7-arch2-1, GCC 15.1.1
$ gcc main.c -fsanitize=address
$ ./a.out
=================================================================
==36042==ERROR: Address Sanitizer: stack-buffer-overflow on address 0x7b9487c00045 at pc 0x55823be582e3 bp 0x7ffc80c0d6c0 sp 0x7ffc80c0d6b0
WRITE of size 1 at 0x7b9487c00045 thread T0
    #0 0x55823be582e2 in decode (/tmp/a.out+0x12e2) (BuildId: f855e810268062c876f6ac4ec9f0719bb1b13e3d)
    #1 0x55823be5842e in main (/tmp/a.out+0x142e) (BuildId: f855e810268062c876f6ac4ec9f0719bb1b13e3d)
    #2 0x7f948a2376b4  (/usr/lib/libc.so.6+0x276b4) (BuildId: 468e3585c794491a48ea75fceb9e4d6b1464fc35)
    #3 0x7f948a237768 in __libc_start_main (/usr/lib/libc.so.6+0x27768) (BuildId: 468e3585c794491a48ea75fceb9e4d6b1464fc35)
    #4 0x55823be58114 in _start (/tmp/a.out+0x1114) (BuildId: f855e810268062c876f6ac4ec9f0719bb1b13e3d)

Address 0x7b9487c00045 is located in stack of thread T0 at offset 69 in frame
    #0 0x55823be5833b in main (/tmp/a.out+0x133b) (BuildId: f855e810268062c876f6ac4ec9f0719bb1b13e3d)

  This frame has 2 object(s):
    [32, 40) 'out_len' (line 27)
    [64, 69) 'output' (line 26) <== Memory access at offset 69 overflows this variable
HINT: this may be a false positive if your program uses some custom stack unwind mechanism, swapcontext or vfork
      (longjmp and C++ exceptions *are* supported)
SUMMARY: Address Sanitizer: stack-buffer-overflow (/tmp/a.out+0x12e2) (BuildId: f855e810268062c876f6ac4ec9f0719bb1b13e3d) in decode
Shadow bytes around the buggy address:
  0x7b9487bffd80: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x7b9487bffe00: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x7b9487bffe80: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x7b9487bfff00: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x7b9487bfff80: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
=>0x7b9487c00000: f1 f1 f1 f1 00 f2 f2 f2[05]f3 f3 f3 00 00 00 00
  0x7b9487c00080: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x7b9487c00100: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x7b9487c00180: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x7b9487c00200: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x7b9487c00280: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
Shadow byte legend (one shadow byte represents 8 application bytes):
  Addressable:           00
  Partially addressable: 01 02 03 04 05 06 07
  Heap left Redzone:       fa
  Freed heap region:       fd
  Stack left Redzone:      f1
  Stack mid Redzone:       f2
  Stack right Redzone:     f3
  Stack after return:      f5
  Stack use after scope:   f8
  Global Redzone:          f9
  Global init order:       f6
  Poisoned by user:        f7
  Container overflow:      fc
  Array cookie:            ac
  Intra object Redzone:    bb
  ASan internal:           fe
  Left alloca Redzone:     ca
  Right alloca Redzone:    cb
==36042==ABORTING
$
上記では、具体的に不正であった操作内容 (WRITE of size 1 at 0x7b9487c00045 thread T0) やスタックトレース、問題の起きた変数 ([64, 69) 'output' (line 26) <== Memory access at offset 69 overflows this variable)、Shadow memory の状態 (Shadow bytes around the buggy address: 以下) などが確認できました。Address Sanitizer はここで初めて使用したのですが、想像していたよりずっと多くの情報が出力されたので、感動しています。
なお、実際の修正コミットのように if (written_out > max_out) を if (written_out >= max_out) と変更することで、正常に動作する様子が確認できます。
--- main.c	2025-06-08 13:06:29.416615674 +0900
+++ fixed.c	2025-06-08 13:16:04.735554924 +0900
@@ -8,7 +8,7 @@

     for (size_t i = 0; i < input_len; ++i)
     {
-        if (written_out > max_out)
+        if (written_out >= max_out)
             return 0;

         output[written_out++] = input[i];
$ gcc fixed.c -fsanitize=address
$ ./a.out
Decoded string: fooba
$
また、C 言語自体のプログラム経験はあまりありませんが、C 言語を用いた軽い実験程度のものであれば、以下のような経験があります。
Linux において、Mount Namespace の分離による chroot 環境または pivot_root 環境からの jailbreak を試しました。(リポジトリ)
のちに大きめのコンテナランタイムを作るための PoC として、非特権コンテナランタイムを小さく実装しました。(リポジトリ)

OS in 1,000 Lines という、1000 行で実装する OS のチュートリアルをなぞりました。(リポジトリ)
private リポジトリではありますが、Linux カーネルに独自の小さいシステムコールを追加したり、独自の小さいデバイスドライバを C 言語で書いています。これは大学の主専攻実験で行っているもので、課題のページは こちら から閲覧することができます。
また、現在は C 言語をメイン言語としていないので C/C++ 自体にはあまり精通していませんが、キャンプが始まる時点で十分な C++ の実力を持ってればよい という事であれば、キャンプの講義までに講義を受講するのに十分なレベルまで習得することは十分可能であると考えています。
実際に、初めて触れるプログラム言語でも私は習得が早い方であると考えています。

例えば初めて書いた Go のプログラムは、一人で個人開発している SNS のバックエンドでした (リポジトリ)。ここで作った SNS は現在も 1 年以上運営していて、過去にはレバテック LAB 様からこちらの個人開発 SNS に関する取材をいただいています (実際の記事)。

また、初めて書いた Rust プログラムは、古典的なアルゴリズムを使用した対戦用のテトリス AI でした (リポジトリ)。それなりに動作するところまでは実装しています (実際に動作している様子)。Rust に関しては、その後に OCI Runtime Spec に (そこそこ) 準拠した非特権低レベルコンテナランタイムを書いています (リポジトリ)。
もし Sanitizer・Fuzzer 自作ゼミに参加できた場合は、大会期間までに C++ で Brainfuck インタプリタを実装するか、または小さめの仕様を持つ自作言語のコンパイラを実装したりして、C++ をある程度不自由なく書けるようにしておきたいと考えています。

 所感この課題に取り組むまで私は Sanitizer や Fuzzer についての知識がほとんどなかったのですが、実際に調べていく中で「はぇ〜〜面白！」みたいな興味をそそられる話が沢山出てきて楽しかったです。一つ調べたら芋づる式に気になる単語がボロボロ出てくるので、それらを調べていたらいつの間にか1文字も書かずに数時間が経過していたりしました。設問1も初めは「Sanitizer に興味がある」と書くつもりだったのですが、調べていくうちに さては Fuzzer も面白いな？？という気持ちになってきて、最終的に「Fuzzer に興味がある」と書いて出しました。

 L1：Rust検証器自作ゼミこちらのゼミは第3希望にしていたので実際に参加するわけではないのですが、せっかく書いたので晒します (仮にこちらを第1希望にしていたとして、選考に通っていたかどうかは未知数です)。

 [問 1] ビット演算の理解コンピュータの中では、整数は 2 進数の 0/1 のビット列で表現されています。こうしたビット列に対するビット毎の AND や XOR、ビットシフトといった「ビット演算」は効率よく実行できるため、広く活用されています。
例えば、次の関数 mod4 は、整数 n を 4 で割ったときの非負の余り (0 ～ 3) を返します。
fn mod4(n: i64) -> i64 { n & 3 }
なお、i64 は 64 ビット符号付き整数型で、& はビット毎の AND です。3 は 2 進数表現では 0b11 なので、この関数は n の下位 2 ビットを返しますが、これは 2 進数で考えると、n を 4 で割った非負の余り (0 ～ 3) に対応します。
それでは問題です。次の関数 skim を考えてみましょう。
fn skim(n: i64) -> i64 { n & -n }
この関数 skim は、端的に言うとどのような値を返す関数でしょうか。また、そのような動作をするのはなぜでしょうか。簡単に説明してください。
ヒント: 様々な値を skim に入れて、どういう動作をするか確かめてみると、様子がわかります。例えば、7, 8, -8, 12 を入れるとどうなるでしょうか。負の数をビット列で表現するための「2 の補数表現」についてもぜひ調べてみてください。
狙い: 入り組んだビット演算は、人間には一見分かりづらくバグの原因となる一方で、論理的には割と扱いやすいため、形式検証の良いテーマとなります。このゼミで扱う可能性も高いので、出題しました。
この関数 skim は、「整数 n の最下位に立っている 1 ビットだけを取り出した値」を返す関数です。例えば問題文の例である 7 のビット表現は 0b00..0111 であるので skim(7) は 0b00..0001 すなわち 1 を返し、12 のビット表現は 0b00..1100 であるので skim(12) は 0b00..0100 すなわち 4 を返します。
2 の補数表現では n のビット表現と -n のビット表現の和が 0 になるように作られていますが、n から -n を求める手段として、「反転して 1 を足す」という方法が知られています。したがって、n & -n は、n & (~n + 1) と同じ意味になります。ここで ~n は n のビットを反転させた値とします。
ここで、n のビット表現に注目します。当たり前ですが、n の最下位の 1 より下位のビットはすべて 0 です。そして ~n を計算すると、それらは全て 1 になります。n の最下位の 1 であった場所は、反転して 0 になります。次に、~n + 1 を計算すると、最下位の 1 より下位は繰り上がりで 0 に戻り、n の最下位の 1 であった位置も、1 に戻ります。この時点で、~n + 1 (つまり -n) のビット表現は、「n の最下位の 1 であった位置より上位のビットのみが反転された値」と言えます。最後に、n & -n を計算すると、n の最下位の 1 であった位置のみが残り、それ以外は 0 になります。したがって、skim(n) は n の最下位の 1 ビットだけを取り出した値を返す、ということが言えます。

 [問 2] 複雑な再帰関数の理解以下の関数 seven を考えてみましょう。
fn seven(n: i64) {
    if n <= 4 { n + 3 } else { seven (seven (n - 4)) }
}
不思議なことに、この関数 seven(n) は、n ≥ 4 で常に 7 を、n ≤ 3 で n + 3 を返します。これがなぜか、説明してください。
ヒント: 一見複雑ですが、小さい n から順に動作を追ってみると、様子が見えてきます。例えば、seven(7) はどういう動作になるでしょうか。次に、seven(11) はどういう動作になるでしょうか。さらに、seven(15) はどういう動作になるでしょうか。
狙い: 複雑な問題に取り組む胆力、論理的な思考力を見ています。また、検証器の実装では再帰をしばしば使うので、再帰への習熟も確認しています。
まず、場合分けして考えます。
n ≤ 4 の場合

seven(n) は n + 3 を返します。

4 < n ≤ 8 の場合

seven(n) = seven(seven(n - 4)) になります (= はここでは等価を表すものとします)。ここで、n - 4 <= 4 より、seven(n - 4) = (n - 4) + 3 = n - 1 です。したがって、seven(n) = seven(n - 1) になります。つまり、seven(n) = seven(n - 1) = ... = seven(4) になります。seven(4) は 7 を返すので、結果、seven(n) も 7 を返します。

8 < n の場合

seven(n) = seven(seven(n - 4)) になります。ここで n - 4 > 4 より、seven(n - 4) = seven(seven(n - 8)) と展開されます。n - 8 も 8 より大きい場合、seven(n - 8) = seven(seven(n - 12)) のように展開されます。このようにして seven(n) は seven(seven(...seven(n - 4k))) のように展開されていき、やがて、どこかのタイミングで n - 4k は 8 以下になります。8 以下の整数 m に対して seven(m) は 7 を返すので、seven(seven(...seven(n - 4k))) = seven(seven(...seven(7))) です。ここで、 seven(7) = 7 であるため、展開された seven(seven(...seven(7))) は最終的に 7 を返すことになります。

以上の説明から、seven(n) は n ≥ 4 のときは常に 7 を返し、n ≤ 3 のときは n + 3 を返すことが言えます。

 [問 3] RustHorn 流の預言の理解
 解説Rust では「借用」という機能により「可変参照」&'a mut T を作り、これを通して安全にメモリ上のデータを更新できます。しかし、これは従来の手法では検証が難しいものでした。Rust の所有権型システムは非常に強い制限を与えてくれるので、何か上手いことができそうです。
講師 松下 の研究「RustHorn」は、「預言 (prophecy)」という未来を先取りする技術で Rust プログラムをモデル化する手法を提案し、可変参照を使う Rust プログラムを一般に効率よく検証できるようにしました。Rust 半自動検証器 Creusot もこのアイデアを取り入れています。
RustHorn 流の預言による借用のモデル化を簡単に説明すると、以下のようになります。
預言を作る
借用を始める際に、「借用中に行われる更新の最終的な結果」を未確定な形で先取りした「預言」x を作る。可変参照 &'a mut T は現在の値 v と預言の値 x の組 (v, x) としてモデル化される。

所有権を捨てるときに預言の値を確定させる
可変参照 &'a mut T は所有権を捨てる際に、預言の値 x をその時点の値 v' へと確定させる、すなわち、そのときのモデルが (v', x) であれば x = v' という情報を得る。

借用終了後に預言の値を使う
貸し手は、借用のライフタイム 'a が終わって所有権を取り戻した際に、預言の値 x をその時点での値として使うことができる。


 問題それでは問題です。可変借用を扱う以下の Rust 関数を考えましょう。
fn take_max<'a>(ma: &'a mut i32, mb: &'a mut i32) -> &'a mut i32 {
    if *ma >= *mb { ma } else { mb }
}
fn inc_max(mut a: i32, mut b: i32) {
    { let mc = take_max(&mut a, &mut b); *mc += 7; }
    assert!((a - b).abs() >= 7);
}
なお、abs は絶対値を計算する関数です。
関数 inc_max は任意の入力 a, b について、assert! によるアサーションが成功して終了します (ただし、整数のオーバーフローは無視します)。これがなぜか、RustHorn 流の預言によるモデルを通して説明してください。
ヒント: 上の解説に加えて、以下の講演や論文などを参考にしてくださって構いません。
RustHorn JSSST 2020 トップカンファレンス特別講演
動画 https://www.youtube.com/watch?v=Ah_Bds6I_YI
スライド https://shiatsumat.github.io/talks/jssst2020-esop2020-rust-horn-talk.pdf

RustHorn ACM TOPLAS 2021 論文 https://dl.acm.org/doi/full/10.1145/3462205
Creusot RW 2021 講演 動画 https://www.youtube.com/watch?v=b8sBtmzq0FM
狙い: このゼミで自作する Rust 検証器で RustHorn 流の預言を扱う可能性が高いので、これを機にこの考え方を理解してもらいたい、という思いで出題しました。プログラムの動作を追って、落ち着いて考えていけば、きっとわかると思います。
RustHorn 流の預言によるモデルを用いて CHC (Constrained Horn Clause) を考えることで、与えられた Rust プログラムのアサーションが成功することを説明します。
まず、take_max から、以下のような CHC が得られます。
TakeMax(⟨a, a°⟩, ⟨b, b°⟩, r) ⇐ a ≥ b ∧ b° = b ∧ r = ⟨a, a°⟩ ...[1]

TakeMax(⟨a, a°⟩, ⟨b, b°⟩, r) ⇐ a < b ∧ a° = a ∧ r = ⟨b, b°⟩ ...[2]
上の式は take_max において *ma >= *mb であった場合を表しています。この場合、mb のライフタイムはここで終了するので、預言 b° は b に確定されます。返り値には ma が選択され、ma のライフタイムはまだ終了していないため、CHC の右辺では r = ⟨a, a°⟩ となります。 

下の式は take_max において *ma < *mb であった場合を表しています。上の式と同様に、預言 a° は a に確定され、CHC の右辺では r = ⟨b, b°⟩ となります。
次に、inc_max について考えます。{ let mc = take_max(&mut a, &mut b); *mc += 7; } の行は、mc のライフタイムがこのブロックに閉じることになるので、このブロックと inc_max 全体それぞれについて CHC を考えます。
inc_max 内のブロックについて CHC を考えると、以下のようになります。
Block(⟨a, a°⟩, ⟨b, b°⟩, r) ⇐ TakeMax(⟨a, a°⟩, ⟨b, b°⟩, ⟨c, c°⟩) ∧ c° = c + 7 ...[3]
Rust においてブロックは式なので、CHC の左辺では r を置いています。返り値はないので、右辺に r に関する制約はありません (厳密性を求めてしまいましたが、r を省略してしまっても良かったかもしれません)。また、TakeMax の結果として得られる値と預言値のペアを ⟨c, c°⟩ とすると、このブロックが終了する時点では、預言 c° は c + 7 に確定することになります。
そして、inc_max 全体について CHC を考えると、以下のようになります。
|a° - b°| >= 7 ⇐ Block(⟨a, a°⟩, ⟨b, b°⟩, r) ...[4]
inc_max では、 a と b のライフタイム終了時に両者の差の絶対値を assert しているので、左辺は |a° - b°| >= 7 となります。
また、後の証明のために、Rusthorn の預言モデルにおいて、以下を仮定しておきます。
⟨p, p°⟩ = ⟨q, q°⟩ ⇒ p = q ∧ p° = q° ...[5]
「現在の値と預言の値のペアが等しいならば、その要素同士も等しい」ということを仮定しています。恐らく私の理解が間違っていなければ、Rusthorn の預言モデルではこのような性質が成り立つはずです。
以上より、[1]~[5] の CHC が得られました。得られた CHC を整理していくと、
[3], [4] より、

|a° - b°| >= 7 ⇐ TakeMax(⟨a, a°⟩, ⟨b, b°⟩, ⟨c, c°⟩) ∧ c° = c + 7 ...[6]
[1], [2] より、

TakeMax(⟨a, a°⟩, ⟨b, b°⟩, r) ⇐ (a ≥ b ∧ b° = b ∧ r = ⟨a, a°⟩) ∨ (a < b ∧ a° = a ∧ r = ⟨b, b°⟩) ...[7]
[6], [7] より、

|a° - b°| >= 7 ⇐ (a ≥ b ∧ b° = b ∧ ⟨c, c°⟩ = ⟨a, a°⟩) ∨ (a < b ∧ a° = a ∧ ⟨c, c°⟩ = ⟨b, b°⟩) ∧ c° = c + 7
分配律より、

|a° - b°| >= 7 ⇐ (a ≥ b ∧ b° = b ∧ ⟨c, c°⟩ = ⟨a, a°⟩ ∧ c° = c + 7) ∨ (a < b ∧ a° = a ∧ ⟨c, c°⟩ = ⟨b, b°⟩ ∧ c° = c + 7)
ここで、仮定した [5] を用いると、

|a° - b°| >= 7 ⇐ (a ≥ b ∧ b° = b ∧ a° = a + 7) ∨ (a < b ∧ a° = a ∧ b° = b + 7) ...[8]
よって、与えられた Rust プログラムのアサーションは、[8] の CHC と同値であることになります。実際、[8] は (数学的考察を進めていけば) 恒真であると分かるので、与えられた Rust プログラムは任意の入力 a, b についてアサーションが成功すると言えます。
以上の考察より、与えられた Rust プログラムは任意の入力 a, b についてアサーションが成功して終了するということが、RustHorn 流の預言によるモデルを通して説明できました。

 [問 4] 自由記述セキュリティ・キャンプ 2025 のこのゼミで挑戦したいこと、参加にあたっての思い、自身の強みなどについて、自由に書いてください。
私は この Rust 検証器自作ゼミにおいて、「契約プログラミング Verifier」を学習目的で自作したいと考えています。
Rust を書く上で、数値の入力されうる範囲を型で制限することがよくあります。例えば、"ユーザーのランクは 100 までなので u8 で表現する" といった具合です。しかし、これには限界があります。u8 とはいえ、この場合 101~255 の値は invalid であるからです。また、取りうる invalid な値の範囲を完全に除外しきれている訳でもないという点では i32 や u32 と大差ないのに、i32 や u32 で扱っている他の数値と計算するたびにいちいち cast する必要があるといった問題もあります。さらに、ある関数がドメイン制約 (≒ ユーザーのランク) として常に valid (≒ 0~100) な u8 を返すことをコード上で明示的に表現することができません (これが今回解決したい課題です)。このような問題から、私は Rust に契約プログラミングの考え方を取り入れ、関数に対する前提条件 #[requires] と後続条件 #[ensures] によってドメイン制約を表現できるようにしたいと考えています。
このような契約プログラミングに関する Rust Verifier には既に Kani や Prusti などのツールが存在しますが、あくまで学習目的として、まずは小さく始めて、少しずつ自分の理解とともに拡張していけたらなと思います。私は SAT/SMT ソルバや形式検証に特別詳しいわけではなく、あくまでこのゼミの応募課題に取り組むにあたって調べながら学習した程度ですが、このゼミでの Verifier の自作を通して、Rust の所有権や中間表現 (MIR) について詳しくなりたいと考えています。具体的な実装や実現方法についてはまだまだ知識が疎いですが、セキュリティ・キャンプで助言を貰いながら、出来るところまで手を動かしてみたいです。
また、これまでも私は、興味を持ったテーマに対して自分の手で試行錯誤しながら学んできました。例えば、私は過去に、Rust で以下のようなものを作りました。
テトリス AI「Artemis」 

GitHub: https://github.com/n4mlz/Artemis 

私が初めて Rust で書いたプログラムです。テトリス AI を Rust で実装しました。去年の 11 月に開発しました。 

私がパソコンに興味を持ったきっかけは中学生の頃にテトリス AI を見てかっこいいと思ったことでした。その後、テトリス AI を何度か作ろうとしたことがあったのですが、大学に上がるまではほとんどプログラムを書くことはなく、上手く動作するテトリス AI を作ることはできませんでした。大学に上がってから、「今ならリベンジできるのではないか」と思い、Rust 言語のチュートリアルも兼ねて、テトリス AI を作りました。アルゴリズムについては、長年世界一位の強さを誇っていた強豪テトリス AI「Cold-Clear」のコードを参考にしています。また、テトリス AI に限らず、オセロや将棋の AI に使用されるアルゴリズムについても調べ、より広い知識からテトリス AI のアルゴリズムを改良しました。 

当時の試行錯誤の様子: https://x.com/n4mlz/status/1851921416482070586/
非特権環境で動作する低レベルコンテナランタイム「tiny-youki」 

GitHub: https://github.com/n4mlz/tiny-youki 

PDF: https://files.n4mlz.dev/special_seminar.pdf 

OCI Runtime Specification に (そこそこ) 準拠した、非特権環境で動作する Rust 製の低レベルコンテナランタイムです。今年の 1 月に開発しました。 

コンテナランタイムの実装は 100 行程度の簡単な実装デモか、または 40 万行ほどの runc などの実装はインターネットに転がっているのですが、その中間を満たす規模のコードはそこまで多くありませんでした。特に、非特権環境で動作するコンテナランタイムの実装は、ほとんどありませんでした。tiny-youki は、その両者の中間を目指し、既存のコンテナランタイムである youki をベースに、より小さい実装で 0 から書いたものです。シンプルで理解しやすいコードを目指し、コンテナランタイム自作に関する参考資料として活用してもらうことを目標にしました。OCI Runtime Specification (というコンテナランタイムの標準仕様) にそこそこ準拠しています。また、名前は実装の元になった youki にちなんで、「tiny-youki」としています。 

(参考) 私が完成を喜んでいる様子: https://x.com/n4mlz/status/1879570678086869508/
また個人開発としては Rust に限らず、幅広い範囲に触れています。例えば Web 開発では、「snooze」という SNS を一人で開発しました。
SNS「snooze」 

Web: https://snooze.page 

GitHub: https://github.com/n4mlz/sns-frontend, https://github.com/n4mlz/sns-backend 

snooze は「鍵垢しか存在しないクローズドな SNS」をコンセプトにした、新しいタイプの SNS です。バックエンドにはドメイン駆動設計を採用し、TypeScript と Golang で開発しました。この SNS は、私の「変わった特徴を持った SNS を作りたい」という日常のメモから始まり、Web アプリケーションとして初めて書いたものでした。企画からドメイン設計、API 設計、DB 設計、UI デザイン、開発、デプロイ、リリース、運用まで全て一人で行っており、コード全体では、約 1.5 万行程の規模となっています。 

また、2024 年 8 月にレバテックラボ様からこちらの snooze を題材とした取材をお受けしました。

https://levtech.jp/media/article/focus/detail_507/
このように、私は自分の知的好奇心に従って物事を追求し、実際に形のある成果としてアウトプットできることを強みとしています。まずは小さいケースから初めて、車輪の再発明を通じて物事を理解することが大好きです。

Rust Verifier においても、Rust の MIR を読み解いたり、型や所有権がどのように検証条件と結びつくのかを試行錯誤しながら学ぶ過程そのものに、大きな面白さとやりがいを感じられるだろうと期待しています。
また、現在は、Rust で自作 OS をしようとしています。今後は Rust をメイン言語として使用することを考えており、そのためにも、Rust の深部までもっと詳しくなりたいです。この Rust 検証器自作ゼミは私にとって、Rust の MIR や形式検証など、通常のプログラミングでは触れる機会の少ない内部構造を深く学べる、非常に貴重な機会になると思っています。本ゼミでの講師や参加者との議論を通して、自分一人では得られない視点や技術的な助言をいただきながら、今の自分の知識では到達できないところまで挑戦し、この夏を Rust に本気で向き合う有意義な時間にしたいです。
また、松下さんに質問があります。
応募課題の [問 3] RustHorn 流の預言の理解 で用いられた Rust のサンプルコードの assert が必ず成功することを、実際に Rusthorn を用いて検証してみようと思い、下記のような手順を試したのですが、上手くいきませんでした。
環境: Linux 6.14.7-arch2-1, Rust nightly-2022-01-22, Z3 4.8.12 (64 bit)
やったこと:
Rusthorn を clone
$ git clone https://github.com/hopv/rust-horn.git
Rust nightly-2022-01-22 のインストール
Rusthorn のリポジトリを見る限り、必要そうだったのでインストールしました。
$ rustup toolchain install nightly-2022-01-22
Z3 のインストール
$ sudo apt update
$ sudo apt install z3

rust-horn/rust-horn/Makefile の修正
環境変数の展開の記法にミスがあったため、以下のように修正しました。
diff --git a/rust-horn/Makefile b/rust-horn/Makefile
index 5db9b1a..dc4b7cd 100644
--- a/rust-horn/Makefile
+++ b/rust-horn/Makefile
@@ -13,7 +13,7 @@ try:
                name=$${file%.rs}; \
                cargo run --release \
                        "$$name.rs" -o "$$name.smt2" \
-                       -- -L $(RUST_LIB_PATH); \
+                       -- -L ${RUST_LIB_PATH}; \
        done

 clean:
課題 3 の Rust コードを rust-horn/rust-horn/sample/seccamp-3.rs に保存
Rusthorn では、main 関数に assert が書かれていることを前提にしているようでした。 

そのため、ここでは課題 3 の Rust コードをなるべく所有権の意味を保ったまま、Rusthorn が扱えるよう以下のように書き換えました。
fn rand<T>() -> T { unimplemented!() }

fn take_max<'a>(ma: &'a mut i32, mb: &'a mut i32) -> &'a mut i32 {
    if *ma >= *mb {
        ma
    } else {
        mb
    }
}

fn inc_max(mut a: i32, mut b: i32) {
    let mc = take_max(&mut a, &mut b);
    *mc += 7;
}

fn main() {
    let a = rand();
    let b = rand();
    inc_max(&mut a, &mut b);
    assert!((a - b).abs() >= 7);
}
ライフタイムに関しては、ほとんど意味が変わっていないと思います (実際に上記のプログラムに対して Rusthorn 流の預言モデルを用いた CHC を考えてみると、課題 3 と等価であると思います)。
Rusthorn の実行と Z3 による検証
make try を実行して Rusthorn を実行し、Z3 による検証を試みたところ、Z3 による出力は次のようになりました。
$ make try
$ for f in sample/*.smt2; do echo "=== $f ==="; z3 "$f"; echo; done
=== sample/inc-max-3-repeat-safe.smt2 ===
sat

=== sample/inc-max-3-repeat-unsafe.smt2 ===
unsat

=== sample/lists-3-inc-some-safe.smt2 ===
unsat

=== sample/lists-3-inc-some-unsafe.smt2 ===
unsat

=== sample/seccamp-3.smt2 ===
unsat

$
おそらく元から用意されているサンプルも、safe と付いているものは sat で、unsafe と付いているものは unsat になるように設計されていると思うのですが、課題 3 の Rust コード含め、実際に sat と判定されるものは一つだけでした。また、課題 3 の Rust コードも unsat と判定されてしまっています。
少なくとも課題 3 の Rust コードは inc_max のアサーションが必ず成功するはずなので sat と判定されるべきだと思うのですが、なぜ unsat と判定されてしまうのでしょうか。 

私の環境が悪いのか、あるいは Rusthorn の使い方が間違っているのか、あるいは Rusthorn のバグなのか教えていただきたいです。

 所感数学が得意なのもあって、割と前半に関しては書けた方なんじゃないかなと思います (特に問3)。また、問4で書いた Rusthorn に関する質問では、後日講師の松下さんに直接回答を頂けました (態々本当にありがとうございます！)。松下さんから頂いた回答をもここに晒すわけにはいかないので書けないのですが、内容としては、単純に問4の私の書いたコードが Rust として間違っている、ということでした。本当に自信満々に初歩的なミスをしてしまっていたようで、恥ずかしいです。
以下のように記述すると、課題3のRustコードが無事 z3 によって sat と判定されました。
fn rand<T>() -> T {
    unimplemented!()
}

fn take_max<'a>(ma: &'a mut i32, mb: &'a mut i32) -> &'a mut i32 {
    if *ma >= *mb {
        ma
    } else {
        mb
    }
}

fn inc_max(a: &mut i32, b: &mut i32) {
    let mc = take_max(a, b);
    *mc += 7;
}

fn main() {
    let mut a = rand();
    let mut b = rand();
    inc_max(&mut a, &mut b);
    assert!((a - b).abs() >= 7);
}
や〜、ちゃんと見直しておけば良かった。

 おわりに実は「応募締切3日前から『1日1つ全力で応募課題やる』を3日間やったら3つ応募課題出せるんでは？」みたいな謎戦略(？)で3日間大学に引きこもって缶詰みたいに応募課題だけやってたんですが、(2つしか書けなかったのは置いておいて) 意外となんとかなりましたね。締切駆動をするのはあまりオススメできませんが、私の応募課題晒しがどなたかの参考になれば嬉しいです。
今年は SecHack365 にも参加する (している) ので、SecHack365 × セキュリティ・キャンプの二刀流を頑張っていきたいです。うおお、体力 of 体力！💪💪
https://x.com/n4mlz/status/1936982157353976183

はじめに

ひとひねり(？)

Y1:Code Sanitizer・Fuzzer自作ゼミ

設問1

設問2

設問3

設問4

設問 5

所感

L1：Rust検証器自作ゼミ

[問 1] ビット演算の理解

[問 2] 複雑な再帰関数の理解

[問 3] RustHorn 流の預言の理解

解説

問題

[問 4] 自由記述

所感

おわりに

Discussion