Appleは、corecryptoにおけるポスト量子暗号の実装を、独立した専門家による評価のための数学的証明および検証ツールとともに公開し、外部の研究者が成果をレビューし、同社の分析を再現できるようにした。
ポスト量子暗号は、広く使われている公開鍵暗号アルゴリズムを破る可能性のある将来の量子コンピュータから、暗号化データを保護するために設計されている。
Apple corecryptoの形式検証に対する新たなアプローチ（出典：Apple）
AppleのOSおよびサービス全体で使用されている暗号ライブラリ「corecrypto」は、25億台以上のアクティブデバイスで暗号化、ハッシュ化、乱数生成、デジタル署名を提供している。同社は2024年、暗号化通信や機密データを扱うアプリケーション（iMessage、VPN、TLSネットワーキングなど）向けに、このライブラリへのポスト量子暗号サポートを追加した。
「corecryptoに重大なバグがあれば、それに依存するすべてのアプリや機能のセキュリティと信頼性を損なう可能性があります。そのため、私たちはライブラリへの新しいコードの追加に慎重であり、テストの網羅性について並外れた努力を重ねています」とAppleは述べた。
このライブラリはさまざまなAppleデバイスやチップ上で動作するため、Appleはすべてのプラットフォームで一貫した動作を確保するために、暗号コードを移植性の高いCで記述している。同社はタイミング攻撃への対策を適用し、攻撃を困難にするために一部の内部計算をランダム化する場合があると述べている。
検証システムの仕組み
形式検証は、定義された条件下でソフトウェアが意図通りに動作することを証明するために数学的手法を用いる。
NISTによって標準化されたポスト量子アルゴリズムであるML-KEMとML-DSAは、セキュリティ、パフォーマンス、コンパクトな鍵および暗号文サイズ、そして機能的正確性の観点から選定された。実装は、従来のテスト、シミュレーション、独立したレビュー、および形式検証を通じて検証された。
既存の検証ツールと検証済み実装を評価した後、Appleは複数のプログラミング言語、コードベース、および既存の開発者ワークフローをサポートするカスタムシステムを構築した。
このフレームワークは、既存ツールと新たに開発されたツールを組み合わせ、公式のFIPS標準に照らして実装を検証する。形式検証を専門とする研究・エンジニアリング企業のGaloisは、CryptolモデルからIsabelleの定理を生成し、移植性のあるCとCryptolを接続するツールの開発においてAppleと協力した。AppleはIsabelleライブラリおよび手動で最適化されたARM64アセンブリサブルーチンも開発した。
Cryptol-to-Isabelleトランスレータにより、CryptolモデルをIsabelleで再現して独立した分析を行うことが可能になる。
検証プロセスでは、従来のテストでは検出できなかったと思われる問題が発見された。一つの問題は、初期のML-DSA実装における手順の欠落であり、まれなケースで入力が想定範囲を超え、誤った出力を生じさせる可能性があった。この欠陥はデプロイ前に特定され、修正された。
「私たちは、形式検証と従来の手法を組み合わせ、エンドツーエンドの結果を批判的に評価することで、可能な限り最強の保証が得られると考えています」と同社は付け加えた。
翻訳元: https://www.helpnetsecurity.com/2026/05/27/apple-quantum-resistant-encryption-open-source/
