Appleが量子耐性暗号コードをオープンソース化

Appleは量子耐性暗号コードと、そのコードの正確性を証明するために開発した数学的検証ツールを公開し、独立したレビューと業界全体での幅広い利用に向けて一般公開した。

今回のリリースには、量子安全アルゴリズムであるML-KEMとML-DSAの2つの実装と、その正確性を検証するためにAppleが作成した形式検証ライブラリおよびツールが含まれている。同社はまた、検証方法論の詳細なドキュメントも公開した。同社はこれを、これらのアルゴリズムの広く展開されている本番実装の中で、現在知られている最も強力な正確性の結果を達成したものと説明している。

量子安全アルゴリズムは、Appleのオペレーティングシステム全体で使用されている暗号ライブラリcorecryptoに統合されている。このライブラリは、25億台以上のアクティブデバイスで暗号化、復号、ハッシュ化、デジタル署名を処理している。Appleは2024年にiMessageで量子耐性暗号の展開を開始し、VPNサービスやTLSネットワークプロトコルにも技術を拡大している。

公開されたツールの1つは、暗号モデルを形式言語間で変換するCryptol-to-Isabelleトランスレーターと、結果を再現するために必要なサポートライブラリである。形式検証は数学的証明を使用して、あらゆる可能な入力に対してコードが正しく動作することを示す。AppleはコードをGaloisが開発した形式言語Cryptolに変換し、さらにケンブリッジ大学とミュンヘン工科大学の証明支援システムIsabelleに変換することで、両者が公式標準に一致することを証明した。Appleはハードウェア暗号コンポーネントの検証にIsabelleを以前から使用している。

検証プロセスにより、従来のテストでは見逃されていたエラーが発見された。研究者らはML-DSAコードに、デジタル署名を静かに破壊していたであろう計算ステップの欠落を発見した。このバグが本番環境に到達していた場合、iMessage内のメッセージが実際には認証されていないにもかかわらず、認証済みとして表示されていた可能性があり、ユーザーは自分の通信に適切なセキュリティが欠如していることに気づかなかったかもしれない。

これらのツールを使用しても、Appleは依然として従来の暗号テストと評価に依存しており、保証のために必要であると認めている。形式検証は従来のテストでは単純に見つけられないエラーを発見できる。テストは多くのシナリオを試すことで機能するが、複雑な暗号コードでは、網羅的にテストするには可能な入力の数が多すぎる。微妙なバグはテストケースの隙間に潜み、警告を引き起こさないことがある。一方、形式検証は数学を使用して、すべての可能な入力に対して一度に正確性を証明する。

しかしながら、Appleのチームは、利用可能なツールではコードのあらゆる側面を形式的に検証することはできなかったため、アプローチを組み合わせたと述べている。すなわち、中核となる数学的正確性には形式検証、形式的手法でカバーできない側面には従来のテスト、そしてすべての要素がどのように連携するかの慎重な評価である。Appleはこのハイブリッドアプローチが、重要な暗号ソフトウェアに対して最も堅牢なセキュリティを提供すると主張している。

詳細はAppleのcorecrypto GitHubページで確認できる。