SymCrypt の Rust 暗号化検証：標準からコードへ、AI エージェントの活用

Rust、Lean、Aeneas、そして AI エージェントが、本番環境の暗号化アルゴリズムに対する形式検証をどのようにスケーラブルにしているか

一目でわかるポイント

• SymCrypt は、Rust、Aeneas、Lean を活用した新しい形式検証済み暗号技術の開発により、より高いセキュリティ保証を提供します。
• 量子耐性暗号など、標準アルゴリズムをコードが安全かつ正確に実装していることを証明しています。
• 今回はまず SHA-3 と ML-KEM の検証済みコード、仕様、プロパティ、そして証明を公開します。
• Aeneas は Rust コードの大部分を検証可能にし、Lean による効率的な自動化で証明作業をサポートします。
• エージェントを活用することで、独立して検証可能な証明を記述し、自動化のスケーラビリティを実現しています。

形式検証への導入と動機

暗号化コードは、現代コンピューティングの基盤を支えています。OS、クラウドサービス、ファームウェア、メッセージングシステム、そしてそれらを繋ぐプロトコルを保護する役割を果たします。しかし、些細なミスが取り返しのつかない結果を招くこともあります。演算のわずかな誤り、境界チェックの抜け落ち、あるいは状態遷移の不備などによって、設計そのものは正しくてもセキュリティが崩壊してしまうのです。

テストや監査は依然として不可欠ですが、それだけでは不十分です。暗号化実装は往々にして最適化されており、定時実行（constant-time）に設計され、アーキテクチャ固有の特性を持ち、あえて低レベルなコードになっています。標準規格に記載されるクリーンなアルゴリズムそのままのコードが shipped されることは稀で、実際には削減処理やビット操作、SIMD イントリンシック、細かく調整されたループ、そして多様な環境への移植性を担保するレイヤーなどが含まれています。

形式検証（formal verification）は、テストだけに頼るのではなく、機械による証明の展開によってこのギャップを埋めます。単にコードが通常通り正しく動作するかを確認するだけでなく、指定された事前条件を満たすすべての入力に対して、厳密な数学的仕様を実装することで保証します。

昨年 6 月、マイクロソフトは、Windows や Azure など幅広い製品・サービスで利用されている暗号化プロバイダー「SymCrypt」において、Rust で記述された新アルゴリズムを形式検証する方針を発表しました。新しい暗号化実装は安全な Rust で記述され、その後 Lean（外部リンク）という形式証明フレームワークと Aeneas（外部リンク）ツールチェーンを用いて検証されます。特に重要なのがポスト量子暗号（post-quantum cryptography）です。ここでは複雑なアルゴリズムを高速かつ安全に実装する必要性が高いため、このアプローチが特に有効です。

この組み合わせにより、2 層の保証が得られます。Rust の言語ルールが広範なメモリ安全性バグを防ぎ、一方 Lean による証明は標準規格から導き出された形式仕様に対して機能的な正しさを確立します。

その結果、本番環境向けの暗号化に対する新しい検証手法が確立されました。これは、開発者がコードを書き進める過程で検証を行い、パフォーマンスを重視した実装の選択を維持しつつ、進化し続けるコードベースに追いつける規模で証明プロセスを拡張可能にするものです。

image図 1. ソフトウェア検証におけるエージェント（確率的な青い要素）とツール（アルゴリズム的な緑の要素）。人間の役割は、規格の形式化と主要な性質のレビューに集中します。エージェントが証明や中間的な性質を記述します。一方、コンパイル、コード抽出、および証明の検証は決定論的であり、エージェントによるものではない。

SymCrypt における検証の現状

私たちは、形式仕様書と証明を含む SymCrypt のブランチ（外部リンク）をオープンソース化しました。この公開ブランチでは、検証対象となる Rust アルゴリズムの実装とともに、その証明アーティファクトも同時に公開されています。これにより、本番環境向けの暗号化コードに対してこの手法がどのように適用されるかが具体例として示されます。SymCrypt は単なる研究用のプロトタイプではありません。Windows や Azure Linux などの製品やサービスで広く利用されている、Microsoft のオープンソース暗号化ライブラリです。

今回のリリースでは、現在 Windows のインサイダービルドで使用されている Rust 製の ML-KEM および SHA3 コードに対する完全な証明が含まれています。SymCrypt では、この Rust、Lean、Aeneas を活用したワークフローをより多くの Rust ネイティブアルゴリズムへ拡大し、Windows や Linux の本番環境向けに統合しています。具体的には、AES-GCM、FrodoKEM、ML-DSA などの検証済み Rust コードが対象です。

本稿では、この SymCrypt の取り組みを具体例として取り上げ、公的な規格から実行可能な Lean 仕様へと至るプロセスを紹介していきます。

規格を形式化された Lean 仕様に落とし込む

最初のステップは、「アルゴリズムが本来果たすべき役割」を形式化することです。暗号プリミティブにおいては、信頼できる情報源となるのは通常、公的な規格です。NIST の仕様書や IETF の RFC、あるいは慎重にレビューされたアルゴリズムの記述などがこれに当たります。

我々のアプローチでは、Lean による仕様が元の規格と可能な限り近い形になるよう設計されています。規格でループ処理や配列の更新、数学的な演算が記述されている場合、Lean のモデルも同様の構造を踏襲します。この構文上の近接性は非常に重要です。規格と Lean モデルを並べて比較できるため、監査担当者が仕様書を検証しやすくなるからです。

Lean を使えば、実行可能な仕様も記述できます。つまり、形式化されたモデルを公式のテストベクトルに対して実行することで、転記ミスやオフバイワンエラー、あるいは仕様の誤解などを検出できるのです。

ML-KEM のようなアルゴリズムにおいては、さらに踏み込んで高レベルな数学的性質も証明可能です。例えば、数論変換（NTT）の形式モデルが、関連する多項式環上での意図された演算と一致することを示すことができます。

代表的な例として、ML-KEM に含まれる数論変換（NTT）があります。標準仕様では、このアルゴリズムは 256 個の係数を q で割った余り空間で行うインプレース変換として記述されており、定数 ζ（= 17）のべき乗を用いて係数のペアを更新する 3 つのネストされたループで構成されています。

以下に、NIST 標準を Lean で直接翻訳した例を示します。原文の構文に極力忠実に従うよう努めています。

この Lean の実装は、意図的に標準仕様の構造を模倣しています。同じループ構造、同じ ζ（ゼータ）の選択ロジック、そして同じ係数更新処理を採用しており、人間による行ごとの精査が容易になっています。同時に、これは実行可能であり、数学的な型を使用しているため、既知のベクトルを用いたテストや、NTT の代数的意味に関する高レベルな定理との接続も可能です。

要するに、この Lean による仕様は、暗号技術者にも証明エンジニアにもレビュー可能なほど標準仕様に忠実でありながら、簡潔で実行可能、かつ数学的な意味を持つモデルとなっています。

形式仕様とコードの連携

仕様が正式に策定された後、次なる課題はそれを実装へと結びつけることです。開発者に検証専用の言語へ生産コードを書き換えるよう求めたり、製品チームが引き継ぐ必要があるコードを生成したりするわけではありません。むしろ、エンジニアが実際に記述した Rust コードそのものを検証対象とします。

Aeneas は、Rust の中間レベル表現を純粋な Lean モデルへと変換することでこれを実現しています。ここで重要なのが、Rust が持つ所有権（ownership）と借用（borrowing）のルールです。これらの仕組みにより、ポインタのエイリアシングやライフタイム、そして不変性に関する複雑な推論を安全に排除でき、C 言語スタイルのコード検証で生じる膨大なコストを大幅に削減できます。

例えば、配列をインプレースで更新する Rust 関数は、Lean では明示的に引数として受け取り、結果として純粋な配列を返す関数へと変換されます。ミュータブルな借用も値の変換として扱われます。これにより、本質的な動作は維持しつつ、証明エンジニアが推論しやすい機能的なモデルを提供します。

Lean 上でこの関数が定義されると、それが形式仕様を精緻化（refine）していることを示す定理が付与されます。つまり、必要な範囲や妥当性条件を満たすすべての入力に対して、実装関数は標準から導出された Lean の仕様と同じ数学的結果を返すことになります。

このアプローチにより、責任の所在が明確に分離されます。ソフトウェアエンジニアは、慣習的でパフォーマンスの高い Rust コードをそのまま書き続けることができます。一方、形式検証エンジニアは生成された Lean モデルを対象に、その性質に関する定理の証明を行います。Rust のコードと証明書は並行して存在しますが、証明の負担によってコードが不自然な形に変えられてしまうことはありません。

NTT（数変換）の例に戻りましょう。Rust での実装は、可変借用を用いて配列をインプレースで更新する fn ntt(&mut [u16; 256]) という関数です。これに対し、Lean への翻訳では純粋な関数として扱われ、更新後の配列を直接返す ntt : Array U16 256#usize → Result (Array U16 256#usize) という形になります。ここで Result タイプでラップしているのは、Rust の関数がパニックを起こしうるという事実を明示的に表現するためです。

この場合の定理は、「配列が整形式の不変条件（有効な多項式を表すことを保証する）を満たすならば、Rust 版の ntt を実行した結果は、数学的な仕様 Spec.ntt の結果に対応する整形式の表現となる」というものです。ただし、これは低レベルな配列から高レベルな多項式への変換を考慮した上での話です。

実際の暗号化コードにあるすべての関数にこれを適用するには、相当な自動化が必要です。Lean の拡張性を活用することで、記号的実行や算術演算、配列操作、ビットベクトル推論のためのタクティクスを組み合わせた、段階的な自動化基盤を構築できます。その作業感はデバッグに近いものになります。自動化が日常的な証明の義務を処理し、エンジニアは自動では解決できない目標に対してのみ、検証と改善を行うのです。

インストリンシック関数と複数アーキテクチャへの対応

本番環境での暗号化処理において、ハードウェアを無視することはできません。SymCrypt は、組み込みシステムやカーネルコンテキストからクラウドサービスに至るまで、あらゆる環境で動作する必要があります。また、利用可能な場合はプラットフォーム固有の命令、特に SIMD インストリンシック関数やアーキテクチャに最適化されたパスを活用できることが求められます。

したがって、移植可能な参照実装のみを対象とした検証では不十分です。実際に製品として出荷されるコード、つまりディスパッチロジック、最適化ルーチン、ターゲット固有のバリアントを含めたすべてのコードを検証する必要があります。

以下のコードは、NTT 内部で利用されている ntt_layer 関数を基に作成されています。この関数は x86-64 と aarch64 でコンパイル方法が異なり、ターゲット固有の実装か移植可能な実装かを動的に切り替えるディスパッチを実現しています。x86-64 では SSE2 命令の利用可否を確認し、aarch64 では Neon の利用可否をチェックします。

.gist .gist-meta {

display: none !important;

}

rustc の出力は本質的にターゲット固有のものであるため、検証が必要な各コンパイルターゲットに対してコードを複数回コンパイルし、対応するモデルをマージしてから処理を進めます。実質的には、このマージ操作により、Rust コード内の cfg 属性によって許可されていた静的ディスパッチが、Lean モデル上では x86-64 と aarch64 の間における最初の動的ディスパッチ層へと変換されます。

Rust コードの挙動に従い、これらのターゲット固有モデルはさらに、XMM、Neon、および汎用実装に対応するモデルに対して動的にディスパッチを行います。

イントリンシック（内在関数）には、やや異なる扱いが必要です。生ポインタを操作したりプラットフォーム固有の命令を公開したりする一部の低レベルラッパーは、小さく注意深くレビューされた Lean の仕様によってモデル化されます。一方、他のものは Rust コードとしてモデル化され、ハードウェアのリファレンスドキュメントと照合してテストした後に翻訳・検証されます。その後、周囲の安全な Rust コードがこれらのモデルに対して検証されます。これにより、信頼できる範囲を狭く保ちつつ、ハードウェアアクセラレーションによるパフォーマンス向上のメリットは維持されます。

重要な点は、形式検証を行っても最適化を諦める必要がないということです。この手法は、イントリンシックやディスパッチ、プラットフォーム固有の実装など、本番環境コードが持つ複雑さをそのまま保持しつつ、単一の監査可能な正しさの証明を実現するように設計されています。

形式保証をコード開発者に反映させる

エンジニア組織において形式検証がスケーラブルに機能するためには、開発者が「何が証明されたのか」を理解できる必要があります。リポジトリ内に証明が存在するだけでは不十分です。その保証は可視化され、レビュー可能であり、エンジニアが維持しているコードと同期されているものでなければなりません。

これを支えるため、検証結果を自動生成されたダッシュボードを通じて公開しています。これらのダッシュボードでは、定理を開発者が理解しやすい用語で要約します。具体的には、事前条件、事後条件、対象となる関数、信頼できるモデル、そして残りの仮定です。エンジニアが何を確認したかを知るために、わざわざ Lean を開く必要はありません。例えば、以下の画面は ntt 関数に関するダッシュボードの表示例です。

image図 2. Rust 関数 mlkem.ntt が NIST 規格で指定された NTT を正しく実装していることを示す定理のダッシュボードページ。

仕様に含まれる定理の内容は、明確に提示されています。Lean の形式開発に含まれる定理文では、水平線の上に事前条件と入力、その下に事後条件を配置することで区別し、Rust と Lean の定義へリンクする完全修飾名を使用しています。

このフィードバックループは、内在関数（イントリック）やターゲット固有のコード、境界条件に関する前提をレビューする際に特に役立ちます。暗号化開発者は例えば、定理が自らが期待するコードの保証を完全に捉えているかを確認でき、形式的な記述が弱すぎる場合や、事前条件に誤りがあることに気づくことができます。

ダッシュボードはまた、検証を継続的な開発プロセスと統合します。Rust コードが変更されれば、Lean のモデルや証明も再生成・再実行可能です。証明が破綻した際、その失敗はシグナルとなります：実装側に変更があり証明の更新が必要なのか、それとも仕様との実際の乖離が露呈したのかを判断する手がかりになるのです。

これにより、形式的検証は単発の研究成果物から、エンジニアリングワークフローの一部へと進化します。

エージェントによる証明

従来のタクティクスを超えた自動化、つまり AI エージェントという最後の要素です。Lean は、証明が小さな信頼できるカーネルによって機械的にチェックされるため、この用途に非常に適しています。エージェントは証明スクリプトを提案できますが、その妥当性は Lean が独立して検証します。

私たちはエージェントを 2 つの場所で活用しています。第一に、標準仕様を Lean の仕様に翻訳する際の支援です。生成された仕様は実行可能であり、元の標準と整合し、公式ベクトルでテストされ、数学的定理によって裏付けられ、実装よりもはるかに簡潔であるため、エージェントが草案作成に関与したとしても、徹底的な監査が可能になります。

第二に、エージェントは証明の作成と維持を支援します。適切なライブラリ、戦術（タクティクス）、例、ドキュメントが整っていれば、エージェントは膨大な証明作業を処理できます。具体的には、生成されたモデルを展開したり、ヘルパー関数の仕様を適用したり、算術的な義務を解決したり、リファクタリング後の証明を修復したりする役割を果たします。

これは特に強力です。なぜなら、Rust のコードと Lean の証明は分離されているからです。エージェントは、証明を通すために生産環境の Rust 実装に注釈をつけたり修正を加えたりする必要はありません。彼らはあくまで証明側で動作し、その結果が Lean によって検証され、最終的な定理が望ましい保証を述べている一方で、未審査の仮定を導入していない場合にのみ承認されます。

実際には、これにより検証のコスト構造が変わります。以前は専門家の数ヶ月にわたる努力が必要だった作業が劇的に短縮できます。証明エンジニアの役割は、手動で一つひとつ証明を書くことから、仕様の設計、自動化の整備、定理文のレビュー、そしてエージェントを導いて証明を完了させることへとシフトします。

結論

検証済み暗号化技術はこれまで、厳しいトレードオフに直面してきました。最も強力な保証を提供するのは、専門的なツールチェーンや生成されたコード、そして製品チームが導入しにくいワークフローによるものでした。しかし、Rust、Lean、Aeneas、そしてエージェントによる証明自動化の組み合わせにより、私たちはそのトレードオフを再考することが可能になりました。

標準規格からコードまで、Rust の暗号化を形式検証するアプローチは、検証可能な仕様を規格から導出し、最適化されたマルチアーキテクチャ実装をサポートし、証明結果を開発者にフィードバックすることで、暗号工学における通常の工程の一部として確立され得ます。これは単なる事後の研究活動ではなく、開発プロセスに組み込まれるべきものです。

これが長期的な展望です。機械による検証証拠を伴いながら、標準規格を実装したことを保証し、かつ高速で移植性が高く、保守が容易で、開発者が主体となる暗号化コードの実現です。

本記事は Microsoft Research の投稿「Verifying Rust cryptography in SymCrypt, from standards to code」の続編（13/13）として掲載されました。