Microsoft：AIエージェントとLeanを使ってSymCryptのRust暗号を形式検証

1つではなく2つの保証レイヤー

形式検証とは、コードが仕様通りに動作することの数学的証明です——テストされたケースだけでなく、あらゆる可能な入力に対して。MicrosoftはSymCrypt——Windows、Azure、その他の製品を支える基盤暗号ライブラリ——に二重の保護を組み込みました：Rust言語はメモリ管理に関連したエラーの全カテゴリを排除し（メモリセーフティバグ）、一方Lean証明アシスタントは機能的正確性を確認します——アルゴリズムが標準の要求通りに正確に動作すること。

Leanは自身の信頼できるカーネルを通じて数学的証明を検証するツールです。選択されたシナリオをカバーするユニットテストとは異なり、Lean証明は絶対にすべての可能な入力をカバーします。この2つのレイヤーの組み合わせにより、検証済みコードは従来のアプローチよりもはるかに堅牢になります。

何が検証済みか？

Microsoftは、SHA-3（広く使用されているハッシュアルゴリズム）とML-KEM——NISTが2024年に標準化した後量子鍵交換アルゴリズム——の検証済みコードを発表しました。ML-KEMは特に重要です。今日ほとんどのインターネットトラフィックを保護するRSAとECDHを解読する可能性のある量子コンピュータの攻撃に耐えられるよう設計されているからです。

予定では、AES-GCM（対称暗号化）、FrodoKEM、ML-DSA——さらに2つの後量子アルゴリズム——も検証されます。これらのアルゴリズムすべてに共通しているのは、その複雑さとエラーの高いコストです。暗号における実装の欠陥は通常プログラムのクラッシュを引き起こすのではなく、悪用可能な静かな脆弱性を生み出します。

AIエージェントが証明記述を加速

暗号コードのLean証明を書くことは遅く、要求が高いです。Microsoftはこのプロセスを加速するためにAIエージェントを使用しています：エージェントが証明の候補を提案し、それがLeanの信頼できるカーネルを通じて独立して検証されます。通常のコード生成との重要な違いは、AIの出力が数学的チェックを通過しなければならない——正しそうに見えるだけでは不十分ということです。これは、AIエージェントのエラーが気づかれずに通過できないことを意味します。

SymCryptへの統合により、このアプローチは単なる学術実験ではなく、今日すでに実践的な意味を持ちます。Microsoftが使用するツールチェーン——Aeneas——はRustコードをLeanが分析できる形式に変換し、製品コードと形式手法の間のギャップを埋めます。