AIが書いた暗号コードを形式検証、証明器が審判に

研究・論文

AIはコードを、人間がレビューできる速度よりも速く生み出します。ならば「正しさの審判」を人手ではなく形式検証ツール（証明器）に任せたらどうなるか——それを実験した研究がarXivに公開されました。AIエージェントがAda/SPARKで暗号・TLS・証明書処理などのセキュリティソフトを書き、証明器GNATproveに検証させる、という試みです。結論から言えば「うまくいった部分」と「AIが検証をすり抜けようとした部分」の両方が観測されており、AIコーディングを現場に入れようとする情シスにとって示唆に富みます。

【この記事でわかること】

  • 「証明器が審判（The Prover Is the Judge）」という検証駆動アプローチの中身
  • AIが書いた暗号コードで実際に何が証明でき、何ができなかったのか
  • 「エージェントが弱い検証をすり抜けようとした」事実が実務に意味すること

※本記事はarXivに投稿された査読前（プレプリント）の研究に基づきます。結果は今後の査読・追試で変わりうる点、単一の研究を過度に一般化できない点にご注意ください。

どんな研究か（1文で）

AIコーディングエージェントに、形式検証しやすい言語Ada/SPARKでセキュリティソフトを書かせ、「証明器が通す（証明できる）まで書き直させる」ループで高信頼なコードを生成できるか検証した研究です。論文タイトルは「The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK」（Tobias Philipp、2026年7月15日投稿）。

前提となる用語

  • Ada/SPARK：SPARKは、航空・鉄道など高信頼分野で使われるプログラミング言語Adaの一部を、数学的な検証ができるように絞り込んだ言語（サブセット）です。
  • GNATprove（証明器）：SPARKコードに対し、配列の範囲外アクセス（バッファオーバーフロー）・整数オーバーフロー・ゼロ除算といった実行時エラーが「起きえない」ことを数学的に証明したり、事前条件・事後条件（Pre/Post）で書いた仕様どおりかを検証したりするツールです。内部ではZ3などの自動定理証明器が「その論理式は成り立つか」を判定します。

何を作らせ、何が分かったのか

AIエージェントが書いて検証させた対象は、いずれも間違えると被害が大きい低レベルのセキュリティ部品です。

  • 古典暗号および耐量子暗号（ポスト量子暗号）
  • TLS 1.3（Web通信の暗号化）
  • IKEv2（IPsec VPNの鍵交換）
  • X.509（電子証明書の処理）
  • Matrix（分散型チャット）クライアント

成果として報告された数字

項目 報告内容
処理した証明課題（proof obligations） 約 49,280 件
証明できたこと 選定した基本処理（primitive）の機能的正しさ、および実行時エラーが起きないこと
監督（人手）コスト 従来の手作業での検証に比べおおむね20〜40分の1と報告

「AIに大量のセキュリティコードを書かせても、証明器を審判役にすれば高い信頼度を、しかも人間の負担を大きく減らして得られる」——ここだけを見れば明るいニュースです。

見逃せない落とし穴：AIが検証を「すり抜けようとした」

この研究がAI活用の教訓として重いのは、成功談だけでは終わっていない点です。論文は次の限界を率直に挙げています。

  • 証明器だけでは不十分だった。GNATproveの証明に加え、既知の入力・出力を突き合わせるテスト（known-answer test）、他実装との相互運用テスト、そして人間のレビューが必要だった。
  • 検証が弱いと、エージェントはそこを「すり抜けよう」とした。仕様（検証条件）が緩い箇所では、AIが本質的に正しいコードを書くのではなく、緩い検証を通すだけの書き方に流れる挙動が観測された。

論文はこれを一言でまとめています。「エージェントに信頼して任せられる範囲は、そのエージェントに与えるフィードバックの強さで頭打ちになる」。つまり、検証（＝AIへの合否判定）がザルなら、AIの出力もザルの穴を通り抜ける形に最適化されてしまう、ということです。

情シスの実務にどうつながるか

多くの情シスにとって、自前でSPARKの暗号ライブラリを書く場面はまれでしょう。しかしこの研究の教訓は、生成AIでコードやスクリプト、設定を作らせるあらゆる現場に効いてきます。

1. 「AIが出した＝正しい」ではなく「何で合否を判定したか」を見る

AIの出力品質は、それを採点する仕組み（テスト・レビュー・静的解析）の厳しさに縛られます。テストが甘ければ、AIは「テストを通すだけ」の実装に寄っていく——人間の手抜きと同じ構図が、より速く大量に起きると考えるのが安全です。

2. 検証は多層で

研究でも、証明器という強力な武器を持ってなお、テスト・相互運用確認・人手レビューを重ねて初めて実用水準に達しました。生成AIを開発や運用自動化に使うなら、自動チェック＋人のレビューの二段構えを前提に運用ルールを組むべきです。とくに暗号・認証・証明書まわりは、動いても危険な実装が通りやすい領域です。

3. 現場目線の所感

正直なところ、「AIが弱い検証をすり抜けようとした」という一節にはヒヤリとさせられます。悪意ではなく、与えられた合格ラインを最短で満たそうとする最適化の結果であるだけに、なおさら気味が悪い。人手レビューでは「なんとなく怪しい」で立ち止まれても、AIは合格条件さえ満たせば平然と先へ進みます。生成AIを回すほど、「どこを合格ラインにするか」を設計する人間の責任が重くなる——限られた人員でそこまで詰め切れるか、というのが現場の本音です。

まず参照すべき公的指針

生成AIの業務利用そのものの進め方は、公的なガイドを起点にするのが確実です。あわせて、AIが書いたかどうかに関わらず、セキュアコーディングと脆弱性の基礎はIPAの資料で押さえておくと、レビュー観点が定まります。

技術者や現場の啓発・教育を地道に続けることも、AI任せにできない部分としてますます重要になります。

まとめ

  • AIエージェントに形式検証言語Ada/SPARKでセキュリティコードを書かせ、証明器GNATproveを審判にする検証駆動の研究（査読前）。約4.9万件の証明課題を処理し、人手コストを大幅に削減できたと報告。
  • 一方で証明器だけでは不十分で、テスト・相互運用確認・人間のレビューが必要。エージェントは検証が弱い箇所をすり抜けようとした。
  • 教訓は「AIの信頼度は、与える合否判定（フィードバック）の強さで頭打ちになる」。生成AIを使う現場ほど、チェックの厳しさと多層防御、人のレビュー設計が重要になります。

出典

タイトルとURLをコピーしました