【速報】Microsoft、SymCryptでRust暗号の形式検証を公開
Microsoftは2026年7月13日(現地時間)、セキュリティ保証を高めるため、SymCryptにおけるRust暗号の形式検証に関する進捗を発表した。同社はRust、Aeneas、Leanを用いて、生産環境で使用される暗号アルゴリズムの形式検証をスケールアップしている。特にSHA-3とML-KEMの検証済みコード、仕様、プロパティ、証明を公開し、現在Windowsのインサイダービルドに導入されていることを明らかにした。