MicrosoftのSymCryptチームは、Rustで記述された暗号コードの形式検証のための新しい方法論を発表しました。この手法は、Lean証明アシスタントとAeneasツールチェーンを組み合わせ、公開標準（NIST仕様など）から導出された形式仕様に対する機能的正確性を保証します。暗号コードは現代のコンピューティングの基盤であり、わずかなミスが深刻な結果を招く可能性があります。従来のテストや監査だけでは不十分であり、形式検証が必要です。
まず、公開標準をLeanの形式仕様に変換します。この仕様は標準の構文に可能な限り近づけられ、監査が容易になります。例えば、ML-KEMの数論変換（NTT）では、標準の3重ループ構造をLeanでそのまま再現し、係数の更新も一致させています。仕様は実行可能であり、公式テストベクトルに対してテストできます。
次に、Aeneasを使用してRustコードを純粋関数的なLeanモデルに変換します。Rustの所有権システムにより、ポインタのエイリアシングや可変性の推論が簡略化されます。例えば、Rustのin-place配列更新関数は、Leanでは配列を明示的に受け取り返す関数になります。その後、モデルに定理を追加し、標準仕様を精緻化していることを証明します。
この検証作業はすでに実践的な成果を上げています。耐量子暗号アルゴリズムML-KEMとSHA-3の検証済みコードは、Windows Insiderビルドに出荷されました。SymCryptは同じワークフローをAES-GCM、FrodoKEM、ML-DSAなどの他のRustネイティブアルゴリズムにも拡張しています。
複数のアーキテクチャとハードウェア組み込み関数のサポートも重要です。SymCryptはx86-64やaarch64などの異なるプラットフォームで動作し、SSE2やNeonなどのSIMD命令を活用します。検証ツールチェーンは、各ターゲット向けにコードを複数回コンパイルし、モデルをマージすることで、静的ディスパッチを動的ディスパッチに変換します。組み込み関数は、小さなLean仕様またはRustコードでモデル化され、周囲の安全なRustコードはそれらのモデルに対して検証されます。
最後に、検証結果は自動生成されたダッシュボードを通じて開発者に公開されます。ダッシュボードは定理、前提条件、事後条件、カバーされる関数、信頼モデル、残りの仮定を開発者向けの用語で表示し、Leanを開かなくても検証状況を確認できます。これにより、形式検証はブラックボックスではなく、日常の開発フローに統合されたツールとなります。結論として、この方法論は、セキュリティを確保しながらも、実際の展開におけるパフォーマンスと柔軟性を両立させる、実用的な形式検証の道を提供します。