Apple Corecrypto: 形式検証による量子耐性暗号化の実装と検証

導入と背景

Apple セキュリティ工学およびアーキテクチャ（SEAR）チーム、ならびにハードウェア技術における形式検証チームによって作成された本リリースは、以下の目的を達成するために行われています。

• 量子耐性暗号化への移行: 未来的な量子コンピュータによる脅威から Apple ユーザーを保護するため、iMessage などへの導入を加速。
• 高い信頼性の確保: 全てのプラットフォームでの展開に向け、実装の数学的正確性を厳格に証明する手法を開発。
• 透明性と評価: 今回リリースされる Corecryptoにおいて、ML-KEM および ML-DSA アルゴリズムの実装と、FIPS 203 および FIPS 204 仕様に忠実であることを保証するための数学的証明を公開。
• 技術の向上: 関連アルゴリズムのプロダクション実装において過去最高水準の正確性を達成するために開発した形式検証ライブラリおよびツールも併せて公開。

---

Corecrypto における量子耐性暗号化の進化

展開と利用

• Corecrypto の導入 (2024 年): Apple オペレーティングシステムの基盤となる暗号化ライブラリにポスト量子暗号化機能を追加。
  • 利便性の高い分野（iMessage, VPN, TLS ネットワークなど）で最初に行われた展開。
• Apple CryptoKit の強化: 昨年秋にリリースされた開発者向けライブラリに量子耐性 API を追加し、アプリ開発者が量子耐性暗号化を採用可能に。
• 規模と重要性: Corecrypto は現在、25 億台以上のアクティブデバイスで利用されており、以下のような機能を提供。
  • 暗号化・復号化
  • ハッシュ処理
  • 乱数生成
  • デジタル署名
  • 致命的なバグ防止: ライブラリへの新機能追加は慎重に行われ、テストの網羅性に例外的に高い努力を払っている。

アルゴリズム選定基準

Corecrypto へのアルゴリズム追加には、以下の厳格な基準を満たす必要があります。

1. セキュリティの向上
   • 新たな問題を解決するか、既存アルゴリズムのセキュリティを向上させる必要がある。
2. 堅牢な設計
   • 理論的な強固なセキュリティを持ち、全世界の研究コミュニティによる厳密かつ持続的な暗号解析に耐えること。
   • 実用面での安全な実装可能性も担保。
3. 高い性能
   • 各デバイスにおいて、遅延および電力消費の観点から極めて効率的であること。
4. コンパクトなパラメータ
   • キーサイズや署名サイズが、ネットワーク遅延への影響を最小限に抑え、デバイスのメモリ制約内に収まること。

採用アルゴリズム：ML-KEM と ML-DSA

• 短期間で基準を満たした 2 つのアルゴリズムが選定され、NIST によって標準化されました。
  • ML-KEM: 鍵生成・交換プロトコル（FIPS 203）。
  • ML-DSA: デジタル署名スキーム（FIPS 204）。
• 他の署名スキームも存在しましたが、上記 2 つが Apple の要件に最も合致していました。
• 暗号コミュニティによるリファレンス実装の確かな基盤の上に、独自の実装と改善を施すことになりました。

---

Apple Silicon における実装戦略

移植性とセキュリティ

Corecrypto は異なるマイクロアーキテクチャ（Apple Silicon など）に対応するため、移植性のある C コードを実装の基盤としています。

• 厳格なガイドライン:
  • 機密値の漏洩防止（タイミング攻撃対策）。
  • コンパイラによる保護の弱体化防止。
  • Apple プロセッサ機能の活用: Data Independent Timing (DIT) および Pointer Authentication (PAC) を利用し、サイドチャネル攻撃やメモリ破損型エクスプロイトを防ぐ。
• 脅威モデルの評価: 特定のユースケースに基づき、内部計算をランダム化する必要性も評価。

最適化と手動調整

リファレンス実装のレビューを通じて発見された改善点を適用しました。

• 数学的最適化: アルゴリズム変更せずに性能を向上させる処理を実行。
• サブルーチンの再書成: 業界最高水準のプロセッサの可能性をすべて活用した手動最適化を実施。
• タイミング制御: プロセッサの動作に対する正確な制御により、機密情報を暴露する可能性のあるtiming side-channel を防ぐ。

課題と対応

• 経験不足: ML-KEM/ML-DSA は比較的新しいアルゴリズムであり、業界全体での実装経験がまだ少ない状況でした。
• 過去の教訓: 早期の楕円曲線暗号化展開で遭遇した、巧妙かつ悪用可能なバグを引き起こさないよう強く動機付けられました。

最優先事項: 手動最適化（性能・セキュリティ強化）を備えた新しい実装が、機能上で正確であり安全であることを確保することです。

• 達成手段：深い従来のテスト、シミュレーション、独立レビューに加え、厳格な形式検証を組み合わせています。

---

Corecrypto における形式検証の要件

形式検証とは

• 数学的証明を用いて、システムやオブジェクトが定義された性質を満たしていることを示す手法。
• Apple はシリコン開発で形式検証を 15 年以上実施（2019 年から古典暗号化含む）。
• Corecrypto の目標: 従来のテストによる保証よりもはるかに高い信頼性を確保するため、数学的証明を用いる。

保証の内容

• 論理的整合性: 「実装の数学式が仕様のそれと同等であることを証明できれば、常に正しい出力を生成する」という理論的な保証を得られます。
• 従来テストとの違い: 一般的に従来のテストでは得られないほどの高い度合いの保証を提供します。

適用における課題

• リソース集約: 多大な時間と深い専門知識（数学的証明の作成、ツールのマスタリー）が必要です。
• モデル化の難しさ:
  • 実装と仕様が選択的に数学式で表現される必要があります。
  • 式が両者の振る舞いを正しくモデル化し、証明が単純な手順で記述可能である必要があります。
  • 十分な完全性（入力カバー）を持つ必要があります。
• 反復作業: 極めて大規模になり得る式を扱うため、証明戦略の構築には多くの反復が必要です。

検証の対象：ML-KEM と ML-DSA

これらのアルゴリズムは多項式や大きな数の演算を含み、従来型の専門サブルーチンのシーケンスによって実装されます。

• キャリー/バーロー（借記）処理: 計算中に発生し、数が多い・複雑なため従来のテストではチェック困難な部分。
• 互換性の確保: サブルーチンが個別に正しくても、出力が次のシーケンスと互換性がない場合のバグを検出する必要があります（例：中間値が範囲外）。

形式検証の 3 つの主要要件

アップル Corecrypto 向けの検証には以下の要件が設定されました。

1. 全体実装の検証
   • 個々のサブルーチンの正しさだけでなく、全体のアルゴリズム実装を検証できる必要があります。
   • サブルーチン連動して正しい最終結果を計算することを示す必要あり。
2. 幅広い製品サポート
   • 移植性のある C コードおよび ARM64 アセンブリ（Apple Silicon の命令言語）で記述された実装をサポートする必要がある。
3. 迅速な進化への対応
   • ソフトウェアの継続的な改善や新しいアプリケーションの導入に対応し、開発者ツールとの互換性を保ちつつ、検証労力を最小限に抑える必要がある。

---

Corecrypto 用のカスタムアプローチ

既存ツールの限界と独自開発

既存の検証ツールを評価しましたが、Apple の要件（多言語サポート、急速な進化への対応など）を満たすものはなかったため、独自の形を検証プロセスを開発しました。

• 高レベルのプロセス:
  • NIST 標準化された仕様と実装を形式的な数学に変換。
  • 最適化された C および ARM64 実装に関する増量的な証明を組み付けることで機能正確性を示す。

使用ツールチェーン

以下のオープンソースおよび独自開発ツールの組み合わせを採用しています。

ツール名	開発元/特徴	役割
Isabelle	フォーマル言語/証明アシスタント	複雑な数学的証明の検証（ハードウェア PKA 等にも使用）。
SAW (Software Analysis Workbench)	Galois	特定ドメイン言語（Cryptol）で記述した仕様に対し、ソフトウェアプログラムを形式的に検証。
Cryptol	Galois	SAW と連携する形式的な言語。仕様表現に使用。
cryptol-to-isabelle	Galois (Apple 仕様に基づく)	Cryptol のモデルを Isabelle に変換し、比較を可能にする翻訳器。

検証フローの詳細

1. C → Cryptol: 移植性のある C 実装を手動で Cryptol 言語に変換。
2. SAW による検証: SAW を使用し、Cryptol モデルと C 実装が一致するかを検証（C の推論能力活用）。
3. FIPS 仕様の Isabelle 変換: SAW でサポートできない高度な数学を含む FIPS 仕様を、Isabelle に徹底して手動で変換。
4. Cryptol → Isabelle ブリッジ: 専用翻訳器を使用し、Cryptol モデルを直接 Isabelle の実装モデルに変換（人的エラーリスク低減）。
5. 全体証明の記述: モデルと仕様がともに Isabelle にある状態で、両者の同等性を示す証明を書く。
   • サブルーチン多数、5 万を超える証明ステップを必要とするため、再利用可能な理論（レマ）を含む Isabele ライブラリスイートを構築して簡略化・拡張性を持たせた。

ARM64 アセンブリの検証戦略

CPU 命令シーケンスは数学的仕様から遠いため、直接的な同等性証明は複雑でした。以下の戦略を採用。

1. C 実装とアセンブリを比較: アセンブリ命令に対応する C 実装と比較する課題は管理可能。
2. 両者を Isabelle に翻訳: 両方の実装モデルを Isabelle で表現。
3. 置換の証明: 各 ARM64 サブルーチンが置換する C サブルーチンの同等性を証明。
   • C 実装内の全サブルーチンはすでに検証済みであるため、トップダウンでの追加検証なしに、最適化された ARM64 アセンブリ実装の正確性が保証される。

例：多項式の加算（C と Isabelle の比較）

以下は C で書かれた実装と、対応する Isabelle の仕様の違いを示す例です。

C 実装 (具体的なロジック) 16 ビット整数の範囲で表された係数をループして加算します。

void ccmlkem_poly_add(int16_t coeffs[CCMLKEM_N], const int16_t a[CCMLKEM_N], const int16_t b[CCMLKEM_N]) {
    for (unsigned i = 0; i < CCMLKEM_N; i++) {
        coeffs[i] = a[i] + b[i];
    }
}

Isabelle 仕様 (抽象的な定義) 係数の数やワードの正確なサイズを指定せず、ループではなく組み込みの

map2

操作で処理します。

definition poly_add :: "'a word list ⇒ 'a word list ⇒ 'a :: len word list" where
  "poly_add xs ys = map2 (+) xs ys"

---

結果と展望

検出された問題と修正

形式検証により、従来のテストでは検出されなかった以下の問題を発見・修正しました。

• ML-DSA の欠落したステップ: 稀なケースで入力が増加し範囲を超えて誤った出力を生成する問題を見出し、独立して修復。
• サードパーティの証明エラー: 外部ライブラリの不備を発見し、Apple の実装で使用される特定パラメータ値に対して修正。
• 潜在的なリスク: 欠落したステップの問題は、既存テストスイートからの警告なしに暗号計算を静かに破損させる可能性があります。

結論: 開発サイクルに形式検証を導入することで、「実装が正確であり、すべてのサブルーチンが連携して機能する」ことへの強い保証を得ました。

手法の限界と補完

• 仮定と制限:
  • コンプラーラ（C から CPU 命令を生成）が正しく動作することを仮定しています。
  • SAW の制限により ML-DSA のすべてのメッセージサイズを検証できなかったため、ブロックごとのコア置換サブルーチンを従来のテストで検証し補完しました。
• 総合的な評価: 形式手法と従来のテスト（シミュレーション含む）を組み合わせることで、エンドツーエンドの結果を厳密に評価可能と考えます。

公開とコミュニティ貢献

2026 年 5 月 22 日にリリースされる Corecrypto ソースコード最新版で、以下の成果を共有予定です。

• グローバルな暗号コミュニティとの共有: 形式検証適用における意味深い進歩を発表。
• オープンソース解放:
  • Galois が作成した Cryptol から Isabelle への翻訳器を利用可能に（分析の再現・独立利用をサポート）。
  • Corecrypto ソースアーカイブに含まれる Isabelle の理論（ARM64 モデル、リファインメントフレームワーク、SProp 分離代数ライブラリ、FIPS の形式化など）を公開。
    • プログラム推論のための強力なツール定義を提供。
    • 制限付き評価ライセンスおよびより許可的なライセンスの下で公開され、公共での使用が可能に。

今後の方向性

• 本アプローチにより、今日広く展開された ML-KEM および ML-DSA プロダクション実装における機能上正確性の最高レベルの保証を実現しました。
• 手動最適化されたコードを完全にサポートしつつ、検証済み実装の迅速な進化・最適化を可能にしつつ、常に正しい出力を生成するという強い保証を提供しています。