ブログ

LLM に安全な C を書かせる：拡張機能とサニタイザ、そして形式検証まで試した記録

2026年7月10日 H.Ueda

エージェント（LLM）に C を書かせるとき、どんな道具立てにすれば安全になるのか。この記事は、小さな CLI ツールを題材に、Apple clang と GCC のコンパイラ拡張、サニタイザ、ファジング、さらに形式検証器 Frama-C までを実際に当てて得た、実測ベースの記録です。

先に結論：C はメモリ安全でない言語ですが、LLM が最も流暢に書ける言語でもあります。この二つは両立できます。安全化とは「大域的な約束を、局所的で機械が検査できる形に落とすこと」で、道具はコンパイラ拡張とサニタイザで足ります。コード全体には注釈ゼロの実行時網（ASan / UBSan）とファジングを、境界を歩く小さな島にだけ型の網（-fbounds-safety）を敷く。全入力を証明する形式検証（Frama-C）は強力ですが、注釈層の学習データが少なく、ふつうのアプリでは割に合いませんでした。

検証環境：macOS（arm64）、Apple clang 17、Homebrew GCC 16.1.0、Homebrew LLVM clang 22、xmake 3.0.9、yyjson 0.12.0、Frama-C 32.1（Germanium）、d2 0.7.1。数値と可否はこの環境での実測です。

題材にしたのは ws という cmux ワークスペース補助 CLI です。C11 と xmake で実装し、JSON パースは手書きせず yyjson パッケージに委譲しています。仕様適合は 13 シナリオの golden テスト（偽 cmux を PATH で差し替える hermetic 方式）で判定しました。以降の「動く」「壊れない」は、すべてこの 13/13 を指します。

1. なぜ C なのか：仮説と、確かめたこと

まず出発点の仮説を置きます。LLM にコードを書かせるなら、実は C が扱いやすいのではないか、という見立てです。理由は 2 つあります。C には膨大な学習データがあり、言語仕様も小さいため、LLM は API を取り違えにくく、素直なコードを書けます。

問題は、C がメモリ安全でないことです。解放忘れ、ダングリングポインタ、境界外アクセスといった失敗が、コンパイルを通り、テストの多くも通り、無言で誤動作につながります。ここを別の道具で塞げれば、C の学習データ優位を保ったまま安全性を足せるはずです。

この記事で確かめたのは、次の問いです。

  • C に何を足せば、LLM が使うのに十分安全になるか。
  • その道具は、Apple clang だけでなく GCC でも成立するか。
  • 全入力を証明する形式検証まで踏み込むと、割に合うのか。

安全化は 3 つの軸に分けて考えると整理できます（図 1）。空間安全（境界外アクセス）、時間安全（解放まわり）、そして横断的な備え（未検証入力や網羅不足）です。

素の C（LLM が最も流暢に書ける言語）空間安全時間安全横断危険：境界外・off-by-one第一手：長さを型に載せる-fbounds-safety / __counted_by補強：ASan危険：解放忘れ・UAF・二重解放第一手：arena で問題ごと消す無理なら cleanup補強：ASan / GCC -fanalyzer危険：未検証入力・無言の失敗・網羅不足第一手：入力はライブラリ・危険関数は禁止補強：UBSan / ファジング

図 1：素の C に対して、3 つの軸それぞれに第一手と補強を敷く。

2. 考え方の軸：大域の約束を、局所の検査に落とす

具体的な道具に入る前に、全体を貫く 1 つの原則を先に置きます。

大域的な不変条件を、局所的で機械検査可能な形に変換する。

LLM は、道具を回して即座に直す反復が得意な一方で、多数の編集をまたいで大域的な約束を保つのが苦手です。「すべての経路で free する」「この添字は必ず範囲内」といった約束は、コード全体を見渡して初めて守れるもので、局所編集を積み重ねる進め方とは相性がよくありません。

そこで安全化とは、こうした大域の約束を、型やスコープに埋め込んで、局所で機械が検査できる形に落とすことだと考えます。以降に出てくる手法は、すべてこの一点に還元されます。長さを型に載せるのも、寿命をスコープに縛るのも、狙いは同じです。

3. 空間安全：長さを型に載せる

最初の軸は空間安全です。ここでの敵は、境界外アクセスと off-by-one です。

3.1 素の C は無言で間違える

この題材で実際に起きた例があります。表示ラベルを組み立てる関数で、確保サイズの計算を +4 とすべきところ +1 と書いた off-by-one です。素の C では、これがコンパイルを通り、テストの大半も通り、無言で誤った文字列を作りました。根本原因は「サイズの手計算」と「無境界ポインタ」の組み合わせです。長さがポインタの型に同居していれば、この種の間違いは消せます。

3.2 二段の検出：コンパイル時と実行時

Apple clang の -fbounds-safety は、ポインタに長さ情報を持たせる方言です。int *idxs __counted_by(count) と書くと、idxs は count 個の有効な要素を持つ、という約束が型に刻まれます。違反は二段で捕まります（図 2）。

境界違反過大な添字 / off-by-one素の C（無境界ポインタ）-fbounds-safety の島（長さが型に同居）無言でゴミ値・exit 0（テストの大半も通ってしまう）静的に分かる違反→ コンパイルエラー動的な違反→ 実行時 trap（release でも） 型が守らない長さが型を守る

図 2：同じ境界違反が、素の C では無言で通り、-fbounds-safety では静的か実行時に必ず捕まる。

静的に分かる違反、たとえば固定長配列に過大な count を渡すケースは、コンパイルエラーになります（count value of N always fails）。実行時にしか分からない違反は、release ビルドでも実行時 trap（SIGTRAP）で止まります。書いた瞬間にコンパイルが落ちる静的ケースは、LLM の反復ループと特に相性がよく、ASan を回すより早く気づけます。

3.3 採用は「島」単位で

魅力的な機能ですが、既存コード全体に広げるのは高くつきます。採用コストを実測しました。

対象 規模 -fbounds-safety の指摘数
新規モジュール（greenfield） 約 10 行 0（初回からクリーン）
既存 4 ファイルの表面積（strict） 756 行 164（約 0.22 / 行）
同（文字列厳格を off） 756 行 75
1 ファイルを clean 化（retrofit 実施） 152 行 7 → 0（約 9 編集）

retrofit の指摘の約 3 分の 2 は、NUL 終端文字列（__terminated_by）に由来しました。配列境界そのものの指摘は少数です。つまり、既存の生ポインタや文字列コードへの後付けは、文字列の扱いで高くつきます。

ここから実務的な指針が出ます。新しいモジュールを書くときだけ、そのファイルを「安全な島」として -fbounds-safety で書く。既存コードには無理に広げない。エージェントは新規記述が多いので、この配分は自然に噛み合います。xmake ならファイル単位でフラグを付けられます。

add_files("src/*.c|pickset.c")                                   -- 通常の素の C
add_files("src/pickset.c", {cflags = "-fbounds-safety", force = false})  -- 安全な島

force = false が効いていて、対応コンパイラ（clang）ではフラグを適用し、非対応（GCC）では自動的に落とします。同じソースが両方でビルドできる仕掛けは、第 6 節で扱います。

4. 時間安全：まず問題を消す、消せないなら局所化する

次の軸は時間安全です。敵は解放忘れ、二重解放、use-after-free（UAF）です。ここは戦略が 2 つあり、どちらを選ぶかが設計を左右します（図 3）。

メモリの寿命は？短命（CLI・一発処理・エージェントの道具）長命（サーバ・常駐）arena-by-leak解放しない → プロセス終了で OS が回収リーク・UAF・二重解放が構造的に起きない注釈 0 / footgun 0__attribute__((cleanup)) + ASanスコープ退出で自動解放所有移譲は TAKE_PTR で無害化

図 3：メモリの寿命で戦略が分かれる。短命なら問題ごと消し、長命なら局所化する。

4.1 短命なプロセスは、解放しない

一発起動の CLI や、エージェントが呼ぶ道具のような短命プロセスでは、あえてメモリを解放しない選択があります。プロセスが終われば OS がまとめて回収するため、リークも二重解放も UAF も構造的に起きません。これを arena-by-leak と呼びます。注釈も追跡も不要で、LLM の負荷が最小になります。この題材では、この方針を採りました。

4.2 長命なコードは、スコープに縛る

サーバのような長命プロセスでは解放が要ります。そこでは __attribute__((cleanup)) が使えます。スコープを抜けるときに自動で解放され、早期 return を含むすべての経路をカバーします。「すべての経路で free する」という大域の約束が、「この変数は自動解放」という局所の宣言に変わります。

1 つ落とし穴があります。cleanup 変数をそのまま return したり構造体に格納したりすると、解放後に参照する UAF になります。所有権を移すときは、ポインタを NULL にして cleanup を無害化する TAKE_PTR を通します。規律を破っても ASan が捕まえるので、規律とサニタイザの二重化になります。

5. 横断的な備え：入力、サニタイザ、ファジング

3 つ目の軸は、どちらの安全にも属さない横断的な備えです。

5.1 未検証入力はライブラリに任せる

手書きの JSON パーサは、未検証入力を直接舐める危険地帯です。この題材では、パースを yyjson に委譲しました。副次効果として、-fbounds-safety retrofit の最大要因だった文字列処理も減ります。危険なプリミティブ（sprintf や strcpy）を避け、サイズの手計算をなくすと、第 3 節の off-by-one ごと消えます。

5.2 サニタイザを常設し、その穴をファジングで埋める

コミット前に ASan と UBSan で golden を回すと、「動く」を「メモリ健全性まで検証済み」に引き上げられます。実際、注入した off-by-one は heap-buffer-overflow として確保元の行まで特定されました。

ただし、サニタイザが捕まえるのは実際に踏んだ実行パスだけです。この網羅の穴は、ファジングで機械的に広げられます。libFuzzer に任意のバイト列を生成させ、字句パス処理（clean や norm）に食わせてみました。

実測は次のとおりです。無改変のコードは 30 万入力を 1 秒で走破し、クラッシュしませんでした。ファザは clean() が特別扱いする .. を自力で見つけ、辞書に登録しました（カバレッジ誘導が効いている証拠です）。次に、norm() の sprintf バッファを 1 バイト過少にする off-by-one を注入すると、ファザは空文字列を含む入力でこれを踏み、ASan が確保元の行と書き込みの行を両方指し示しました。素のコンパイルは通ってしまうこの間違いを、ファジングと ASan は 1 秒で暴きます。

ハーネスは素の C で約 15 行、注釈はゼロです。LLM がすぐ書ける形で、実行時網の唯一の弱点（パス網羅への従属）を自動で埋められます。1 点だけ注意があります。arena-by-leak は解放しないため、1 プロセスで大量反復するとメモリが漸増します。長時間のキャンペーンでは、子プロセスを再起動して回収する -fork=1 か、反復回数の上限が要ります。

これらを 1 枚にまとめると、同じソースを複数の構成でビルドし、それぞれ別の信号を出させる形になります（図 4）。

同一ソース（.c）＋ 互換 shimptrcheck-compat.hclang 検証ビルドGCC 検証ビルドASan / UBSan 実行時テストlibFuzzer（パス網羅を自動拡張）本番ビルド：任意の C コンパイラ（拡張は shim で no-op）型で空間安全（静的＋trap）-fanalyzer：UAF/leak を静的に実行時に境界違反・UB を abort任意入力でクラッシュを発見 デプロイ

図 4：1 つのソースを検証用に複数構成でビルドし、本番は拡張抜きの素の C としてデプロイする。

6. 二つのコンパイラ：clang と GCC で武器が入れ替わる

ここまでの中心だった -fbounds-safety は Apple clang 専用で、GCC にはありません。移植性を考えると、これは困った点に見えます。ところが GCC には、clang にない強力な武器があります。-fanalyzer です。要点は、コンパイル時に捕まえられる対象が入れ替わることです（図 5）。

Apple clangGCC空間安全境界外・off-by-one時間安全UAF・二重解放・leak実線＝その軸を静的に強く守れる側破線＝実行時で補う側 型で静的＋実行時 trap（-fbounds-safety） 実行時中心（-fsanitize=bounds・ASan）コンパイル時に検出（-fanalyzer）実行時（ASan）

図 5：clang は空間安全を型で静的に、GCC は時間安全を -fanalyzer で静的に捕まえる。

空間安全は、clang なら型でコンパイル時に落とせますが、GCC では実行時（-fsanitize=bounds や ASan）が主になります。逆に時間安全は、GCC の -fanalyzer が UAF やリーク、二重解放をコンパイル時に捕まえます。実測でも、UAF を注入すると GCC は -Wuse-after-free をコンパイル時に出しました。clang にこの静的検出はありません。

一方的な優劣ではなく、相補と見るのが正確です。clang は型で空間を、GCC は解析で時間を、それぞれ静的に捕まえます。両方を同じソースで成立させるために、互換 shim を挟みます。

// ptrcheck-compat.h
#if defined(__has_feature) && __has_feature(bounds_safety)
#  include <ptrcheck.h>        // clang: __counted_by 等が有効
#else
#  define __counted_by(N)      // GCC 他: no-op（検査は -fanalyzer とサニタイザに委ねる）
#  define __sized_by(N)
#endif

これで島のソースは両方のコンパイラでビルドでき、境界検査は clang でのみ効く上乗せになります。実測では、Apple clang と GCC 16 の双方で golden が 13/13 通り、clang では島の trap も動作しました。

7. どこまで証明するか：Frama-C を試して、棄却した話

ここまでは「コンパイラに内蔵された検査」でした。対極として、独立した形式検証器 Frama-C を評価しました。ACSL という契約記述言語でコードに事前条件や事後条件を書き、WP プラグインが演繹的に証明し、E-ACSL プラグインが実行時監視コードを注入します。結論を先に書くと、この題材では採らないと判断しました。以下はその記録です。

7.1 WP は、確かに証明できる

第 3 節の島に相当する関数へ、ACSL で契約を 4 行付けました。

/*@ requires 0 <= choice < count;
  @ requires \valid_read(idxs + (0 .. count-1));
  @ assigns \nothing;
  @ ensures \result == idxs[choice];
  @*/
int pickset_choice(const int *idxs, int count, int choice) {
    return idxs[choice];
}

WP はこの直線的なコードの境界安全を、すべての入力に対して静的に証明しました。わざと範囲外の呼び出しを混ぜると、その事前条件のゴールだけが証明できず、原因の位置を指し示しました。証明にかかる時間は 1 ファイルあたり約 4 秒で、その大半は起動と解析です（証明そのものはソルバで 11 ミリ秒でした）。

7.2 対価は、注釈層にある

問題は工数です。ループを含むと、証明には loop invariant（ループ不変条件）を手で書く必要があります。二重ループの例では、注釈なしだと 19 個中 5 個しか証明できませんでした。loop invariant を 2 ブロック（約 6 行）足すと 15 個中 15 個に届きます。直線的なコードはほぼタダですが、ループは 1 つにつき不変条件が要り、ポインタやデータ構造が絡むとさらに高くなります。

ここが、この記事の 1 番の発見につながります。ACSL のような注釈層は、C 本体に比べて学習データが桁違いに少ないのです。__counted_by のようなコンパイラ属性は Linux kernel や Apple の SDK で使われ、実世界のコーパスが増えています。一方、ACSL は学術的な用途にとどまります。つまり、LLM の C の流暢さは、注釈層には転移しません。しかも loop invariant を見つける作業は、演繹検証の古典的な難所で、コードを書くより難しいこともあります。

7.3 実行時監視は、Linux 専用だった

E-ACSL の実行時監視は Linux 専用でした。macOS ネイティブでは二重に動きません。ラッパスクリプトが BSD の getopt と非互換で止まり、ランタイムも getauxval や /proc/self/maps という Linux 固有の仕組みに依存します。amd64 の Docker で試すと、エミュレーション下で VDSO を取得できず、ランタイム初期化で異常終了しました。実行体を動かすには、素の x86-64 Linux が要ります。

7.4 なぜ棄却したか

理由を 4 つに整理します。

  1. ACSL の学習データが少なく、LLM の C の流暢さが転移しない。loop invariant で詰まる。
  2. WP は全入力に対する「証明」を与えますが、その対価が注釈工数と低データ言語です。航空宇宙や暗号の核のような、ごく一部でしか元が取れません。
  3. UBSan が、実質「注釈ゼロで、ネイティブに動き、Linux に依存しない E-ACSL の自動 assert」に相当します。E-ACSL が自動生成する実行時チェックの価値は、既存の網ですでに得ています。
  4. 導入摩擦が大きい。opam ビルド、5 GB のイメージ、ソルバ設定、Linux 専用ランタイムと、clang や GCC の遍在に比べて重い。

7.5 検出と証明を、層で使い分ける

ここから、どの層にどの道具を置くかが見えます（図 6）。

コード全体小さな島臨界核（本プロジェクトでは不採用）ASan / UBSan・-fanalyzer保証：検出（実行/局所）注釈：ゼロ　LLM 適性：◎-fbounds-safety / __counted_by保証：空間を型で（静的＋trap）注釈：軽　LLM 適性：○Frama-C WP + ACSL保証：全入力を証明注釈：重・低データ　LLM 適性：△ コストと保証が増す →コストと保証が増す →

図 6：検出で足りる層に証明を持ち込むと、不変条件の記述で行き詰まる。

コード全体には、注釈ゼロで「検出」する道具（ASan、UBSan、-fanalyzer）を置きます。境界を歩く小さな島にだけ、型で空間を守る道具を置きます。全入力を「証明」する道具は、注釈が重く低データで、この題材では採る動機がありませんでした。検出で足りる層に証明を持ち込むと、不変条件の記述で行き詰まります。

8. まとめ：LLM を前提とした実務指針

一連の実験から得た指針を、1 つにまとめます。

素の C ではなく、次の道具立てを敷いた C は、LLM の即時反復に噛み合います。長さを型や構造に載せ、サニタイザを常設し、入力はライブラリに任せる。時間安全は arena で消すか、cleanup で局所化する。そしてサニタイザの網羅の穴を、ファジングで機械的に広げる。

コンパイル時の武器は、ツールチェーンで入れ替わります。clang は型で空間を、GCC は -fanalyzer で時間を、それぞれ静的に捕まえます。互換 shim を 1 枚挟めば、同じソースが両方でビルドでき、本番は拡張抜きの素の C としてデプロイできます。

安全化のコストは、新規記述なら安く、既存コードへの後付けは文字列の扱いで高くつきます。エージェントは新規記述が多いので、前者へ寄せるのが実務的です。

全入力を証明する形式検証は、確かに強力です。ただし注釈層の学習データが少なく、ふつうのアプリでは割に合いませんでした。証明が要るのは、ごく一部の臨界核だけです。

要するに、次の 3 層に配分するのが、この題材での結論です。

  • コード全体：注釈ゼロの実行時網（ASan / UBSan）と静的解析（-fanalyzer）、そしてファジング。
  • 小さな島：型で空間を守る -fbounds-safety / __counted_by。
  • 臨界核だけ（必要なら）：全入力を証明する形式検証。この題材では不要でした。

付録：再現手順

# 通常ビルドと golden 適合（13 シナリオ）
xmake && bash "$BENCH/spec/golden/run.sh" "$(pwd)/build/macosx/arm64/release/cmux-workspace-helper"

# サニタイザ検証ビルド
xmake f -m debug --asan=y -y && xmake -y
ASAN_OPTIONS=abort_on_error=1 bash "$BENCH/spec/golden/run.sh" "<bin>"

# GCC 静的解析（コンパイル時に UAF/二重解放を検出）
xmake f -c --toolchain=gcc --cc=gcc-16 --cxx=g++-16 --ld=g++-16 -m release --analyzer=y -y && xmake -b -y

# ファジング（Apple clang は libFuzzer 非同梱 → brew LLVM clang を使う）
xmake build fuzz-util
./build/macosx/arm64/release/fuzz-util -max_len=128 -runs=300000
# 長時間は fork で RSS を回収: ./fuzz-util -fork=1 -ignore_crashes=1 corpus/

# 図の再生成（d2 CLI が必要）
sh docs/article/render.sh

図の D2 ソースは docs/article/diagrams/、レンダリング済み SVG は docs/article/img/ にあります。

« 記事一覧へ戻る