Microsoftは2026年7月13日(現地時間)、セキュリティ保証を高めるため、SymCryptにおけるRust暗号の形式検証に関する進捗を発表した。同社はRust、Aeneas、Leanを用いて、生産環境で使用される暗号アルゴリズムの形式検証をスケールアップしている。特にSHA-3とML-KEMの検証済みコード、仕様、プロパティ、証明を公開し、現在Windowsのインサイダービルドに導入されていることを明らかにした。
Microsoftは、SymCrypt (シンクリプト) がRust (ラスト)、Aeneas (エネアス)、Lean (リーン) を活用し、新しい検証済み暗号を開発していると説明した。これは、ポスト量子暗号を含む標準アルゴリズムが安全かつ正確に実装されていることを証明するもので、セキュリティ保証の向上を目的としている。同社は、SHA-3およびML-KEMの検証済みコード、仕様、プロパティ、および証明を初期リリースとして提供する。
形式検証は、現代のコンピューティングシステムにおける重要な保護を担う暗号コードの基礎を強化する。従来のテストや監査だけでは見過ごされがちな小さなミスが大きな影響を及ぼす可能性があるため、機械チェックされた証明を導入することで、すべての入力に対して正確な数学的仕様が満たされることを保証する。Microsoftは昨年6月にRustで記述されたSymCryptの新アルゴリズムを形式検証すると発表しており、これにはWindowsおよびAzureを含む製品やサービスで利用される暗号プロバイダが含まれる。
この手法では、Rustが広範なメモリ安全性のバグを排除し、Leanの証明が形式仕様に対する機能的正確性を確立する。これにより、開発者がコードを記述しながら検証を実施し、性能重視の実装選択を維持しつつ、進化するコードベースに対応できるスケーラブルな証明プロセスが実現する。Microsoftは、形式仕様と証明を含むSymCryptのブランチをオープンソースとして公開した。この最初のリリースには、現在Windowsのインサイダービルドで利用されているRust ML-KEMおよびSHA3コードの完全な証明が含まれる。
今後、SymCryptはRust、Lean、Aeneasに基づくワークフローをより多くのRustネイティブアルゴリズムに拡張し、WindowsおよびLinuxの製品バージョンに統合する計画である。これには、AES-GCM、FrodoKEM、ML-DSAなどの検証済みRustコードが含まれる。形式仕様はNISTやIETF RFCなどの公開標準から導かれ、Leanモデルは標準に忠実に記述されるため、レビュアーによる監査が容易になる。AeneasはRustの中間表現を純粋なLeanモデルに変換することで、既存のRustコードの検証を可能にしている。
参考: Microsoft Research Blog (アーカイブ) — 2026年7月14日 01:00 (JST)
原文ハイライト"verify code as developers write it, preserve performance-oriented implementation choices"