量子セキュアな暗号の確保：Appleによるcorecryptoの形式検証のためのブループリント

量子セキュアな暗号への移行は、単にアルゴリズムを更新するだけの問題ではありません。それは実装の保証という課題です。量子コンピューティングが現在の暗号の基盤を脅かす中、ポスト量子アルゴリズム（PQA）を大規模に展開するには、従来のソフトウェアテストでは提供できないレベルの確実性が必要です。Appleのエコシステム全体で25億台以上の稼働デバイスを保護しているcorecryptoのようなライブラリにとって、たった一つの算術的なバグが、依存するすべてのアプリケーションのセキュリティを損なう可能性があります。

これに対処するため、AppleはML-KEM (FIPS 203) および ML-DSA (FIPS 204) の実装に関する包括的な形式検証のブループリントを開発しました。従来のテストを超えて、数学的な正当性の証明へと移行することで、Appleは、複雑な暗号プリミティブの初期導入時にしばしば発生する微妙なバグを排除することを目指しています。

corecryptoの高い基準

corecryptoに新しいアルゴリズムを追加するには、厳格な評価プロセスが必要です。Appleは、新しいプリミティブがセキュリティを向上させ、安全な設計を備えているだけでなく、高いパフォーマンスを維持し、ネットワーク遅延やメモリ使用量を最小限に抑えるためのコンパクトなパラメータを備えていることを要求します。

アルゴリズムが選択されると、実装は3つの重要な柱を満たさなければなりません：

セキュリティ: コードは、情報の漏洩、特にタイミング・サイドチャネル攻撃に対して強化されていなければなりません。
最適化: 実装は、基盤となるシリコンの効率を最大限に引き出さなければなりません。
正当性: コードは標準仕様を忠実に実装し、常に正しい出力を生成しなければなりません。

従来のテストの限界

シミュレーションや独立したレビューを含む従来のテストは不可欠ですが、高信頼性の暗号学においては不十分です。暗号のサブルーチンは、多項式や大きな数値といった大きなオペランドを伴う複雑な操作を伴うことが多く、操作のシーケンスの深い部分でキャリー（繰り上がり）やボロー（借り）が発生することがあります。

これらの「エッジケース」のバグは、捕らえるのが非常に困難です。コミュニティが指摘しているように、実装におけるステップの欠落がバグとして現れることがあります。周囲のコードが正しく見えるため、これらのエラーは手動のコードレビューを通過し、標準的なテストスイートでは発生する可能性が低い、極めて稀な入力によってのみトリガーされます。

カスタム形式検証パイプライン

既存のツールがARM64アセンブリのサポートを欠いていたり、既存の開発者ツールチェーンを放棄する必要があったりしたため、Appleはカスタムの検証パイプラインを設計しました。このアプローチは、高レベルのFIPS仕様と低レベルに最適化されたマシンコードの間のギャップを埋めるものです。

検証スタック

Appleは、信頼の連鎖を作成するために、専門的なツールの組み合わせを利用しています：

Cryptol & SAW: Appleは、ポータブルなC実装をCryptolに手動で翻訳します。次に、Software Analysis Workbench (SAW) を使用して、Cryptolモデルが実際のC実装と一致することを確認します。SAWはCに関する推論には優れていますが、FIPS仕様の全容を数学的に表現する能力が不足しています。
Isabelle: このギャップを埋めるため、Appleは（Galoisによって構築された）カスタムの翻訳機を使用して、CryptolモデルをIsabelle、つまり強力な証明アシスタントへと移動させます。FIPS仕様もIsabelleに手動で翻訳されます。
証明のプロセス: Isabelle内では、エンジニアは実装モデルと仕様の等価性を証明するために数学的な証明を記述します。ML-KEM および ML-DSA の場合、これは50,000ステップを超える証明ステップを伴いました。これをスケーラブルにするために、Appleは、異なるサブルーチンにわたってプロセスを簡列化するための再利用可能なIsabelleライブラリ（lemmas）を開発しました。

ARM64アセンブリの検証

corecryptoの最も困難な側面の一つは、タイミング・サイドチャネルを防ぎ、パフォーマンスを最大限に高めるために、手動で最適化されたARM64アセンブリを使用することです。アセンブリを直接、高レベルの仕様に対して証明することは、極めて複雑です。

その代わりに、Appleはリファインメント戦略を採用しています。彼らは、各ARM64アセンブリ・サブルーチンが、それが置き換える対応するCサブルーチンと等価であることを証明します。C実装がすでにFIPS仕様に対して等価であることが証明されているため、アセンブリの正当性は、その延長として確立されます。

実社会への影響と結果

これらの形式手法の適用は、具体的なセキュリティ向上をもたらしました。Appleは、初期のML-DSA実装におけるステップの欠落を、入力が期待される範囲を超えてしまう可能性があり、暗号計算を密かに破損させる可能性があることを特定しました。また、特定のパラメータ値に関する第三者の証明におけるエラーを修正しました。

限界の承認

Appleは、形式検証が万能薬ではないことを認めています。彼らの現在のアプローチは、命令を生成する際にコンパイラが正しいことを前提としています。さらに、SAWのいくつかの制限により、ML-DSAの特定のメッセージサイズについては、従来のテストによって検証する必要があります。

結論

形式検証と従来のシミュレーションおよびテストを組み合わせることで、Appleは、ポスト量子移行への高信頼性ベースラインを確立しました。彼らの形式検証ライブラリとcryptol-to-isabelle translator のリリースは、より広範な暗号学コミュニティへの重要な貢献であり、重要なセキュリティ・インフラストラクチャの数学的に証明された実装への移行を促すものです。