KEM-IND-CCA-Preserving Compilation of Jasmin's ML-KEM
本論文は、Signalで使用されている高度に最適化されたML-KEM実装に対して、新しいゲームベースのセキュリティフレームワーク、確率的計算をサポートするインタラクションツリー意味論、および関係的ホーア論理を通じて、Jasminコンパイラが機能的正当性とKEM-IND-CCAセキュリティの両方を保持することをRocqプローバーを用いて完全メカニズム化された証明によって提示するものである。
原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。 免責事項の全文を読む
デジタルセキュリティという極めて重要な世界において、暗号学は、プライベートなメッセージから金融取引に至るまで、あらゆるものを保護する「目に見えない鍵」として機能しています。数十年にわたり、専門家たちはこれらの鍵が破られないことを保証するために数学的証明に頼ってきましたが、紙の上の優雅な数学と、それを実行するコンピュータコードという混沌とした現実との間には、決定的な溝が存在し続けてきました。たとえ暗号スキームが理論的に安全であると証明されていても、その理論をコンピュータプロセッサが理解できる具体的な命令へと翻訳するプロセスにおいて、微妙なエラーが混入することがあります。これらのエラーは、多くの場合、翻訳を行うコンパイラによって導入され、攻撃者が悪用する脆弱性を生み出します。世界が将来の脅威に対抗するための新しい量子耐性暗号標準への移行準備を進める中で、これらの新しいシステムがマシンコードに至るまで安全であることを保証することは、もはや単なる理論的な懸念ではなく、グローバルな通信ネットワークの安全にとって不可欠な事項となっています。
研究チームは今、Signalのような人気のあるセキュアメッセージングアプリケーションですでに使用されている、ML-KEMとして知られる最も重要な新しい暗号標準の一つについて、この溝を埋めました。彼らの研究は、ハイレベルなセキュリティコードをマシン命令へと翻訳するために使用される特定のソフトウェアツールが、意図せずセキュリティの保証を壊すことがないことを実証しています。本質的に、彼らは、人間が読める元のコードに対して確立されたセキュリティ特性が、コンピュータが実際に実行する最適化されたアセンブリコードにおいても完全に保持されていることを証明したのです。この成果は、コンパイラを隠れたバグを含む可能性のある「ブラックボックス」として信頼する必要性を排除したという点で重要です。代わりに、コンパイラ自体が、抽象的なセキュリティ証明と物理的なハードウェアを結ぶ安全な架け橋であることが数学的に検証されました。
研究者たちが直面した課題は、現代の暗号の性質に特有のものでした。彼らが研究した特定のアルゴリズムであるML-KEMは、「リジェクション・サンプリング（拒絶サンプリング）」と呼ばれる手法に依存しています。これは、コンピュータが特定のパターンに適合するものが見つかるまで、ランダムな数字を繰り返し試行する手法です。このプロセスにより、プログラムは常に固定された時間で実行されるわけではありません。早く終了する場合もあれば、予想よりも多くの試行を要する場合もあります。コンパイラの検証手法の従来モデルは、予測可能で固定されたステップの順序で実行されるプログラム向けに設計されていました。そのため、コードが辿る経路が偶然性に依存する、このような確率的な挙動を扱うことが困難でした。もしコンパイラの検証ツールがこれらのランダムなループを考慮できない場合、最終的なマシンコードが元の設計と同じように動作することを保証できず、セキュリティチェーンに潜在的な穴を残してしまうことになります。
これを解決するために、研究者たちはこれらのプログラムがどのように振る舞うかを理解するための新しいフレームワークを構築しました。彼らはコードの実行を単純な命令のリストとしてではなく、あらゆるランダムな選択や外部との相互作用がツリーの枝となるような、「起こりうる相互作用のツリー」として扱いました。このアプローチにより、プログラムの「ほとんど確実に（almost sure）」終了すること、つまり、正確な時間は予測できなくても、確率1で最終的に終了するということをモデル化することができました。この新しいモデルを用いることで、彼らは確率的な設定におけるコンパイラの正当性の定義を導き出すことができました。彼らは、元のコードが辿りうるあらゆる経路に対して、コン compiled コードが一致する経路を辿り、結果の分布を正確に保持することを証明しました。
チームはこのフレームワークを、高信頼な暗号コードを記述するために特別に設計されたツールであるJasminコンパイラに適用しました。彼らは、数百万人のユーザーを持つメッセージングアプリ、Signalで使用されているML-KEMの実装に焦点を当てました。数学的な議論を絶対的な厳密さでチェックするソフトウェアツールである強力な証明助手（プルーフ・アシスタント）を使用して、コンパイラがソースコードをセキュリティ特性を変えることなくアセンブリ言語に正しく翻訳することを検証しました。彼らの証明は、初期の高レベルな記述から最終的なマシン命令に至るまでの、コンパイルプロセス全体をカバーしています。その結果、以前はソースコードに対してのみ証明されていた暗密の安全性は、ユーザーのデバイス上で実際に動作しているコードにおいても成立するという保証が得られました。
この研究は、将来の量子コンピュータによる攻撃に耐えうる暗号手法へのグローバルな移行である、ポスト量子移行への高いレベルの保証をもたらすための、より大きな取り組みの一環です。研究者たちは、攻撃者が計算にかかる時間や消費電力を観察することで秘密を学習する「サイドチャネル攻撃」をカバーするように、まだ証明を拡張してはいませんが、将来の研究のための必要な基礎を築きました。コンパイラがコアとなるセキュリティゲームを保持することを確立することで、彼らはより複雑なセキュリティ保証を構築するための強固な土台を作り上げました。この検証は完全に機械化されており、証明のすべてのステップがコンピュータによってチェックされているため、論理自体にヒューマンエラーが入り込む余地はありません。
この研究の意義は、単一のアルゴリズムにとどまりません。研究者が開発したフレームワークは、他の暗号スキームやセキュリティ特性にも適用できるほど汎用的です。彼らは、ゲームベースのセキュリティ（暗号の強さを定義する標準的な方法の一つ）を、コンパイラの正当性の観点から推論することが可能であることを示しました。これは、新しい暗号標準が開発・実装される際にも、同様の厳格な検証プロセスにかけられることを意味します。研究者たちは、他の専門家が彼らの研究を検査、検証、および発展させられるよう、ツールと証明をオープンソースとして公開しています。この透明性は、現代社会を支えるデジタルインフラへの信頼を維持するために極めて重要です。
結局のところ、この論文は、私たちのデータを守るデジタルな鍵が、設計した数学者たちが約束した通りの強さを持っていると確信できる未来に向けた、重要な一歩を表しています。抽象的なセキュリティ証明と、マシンコードという具体的な現実との間の溝を埋めることで、研究者たちは暗号サプライチェーンから主要な不確実性の源を取り除きました。彼らの研究は、ユーザーがセキュアなメッセージを送信するとき、その背後にあるセキュリティの保証が単なる理論的な理想ではなく、デバイス内のシリコンチップに至るまで数学的に保持された特性であることを保証するものです。このレベルの保証こそが、進化し続ける新たな脅威に直面しながらも、私たちを繋ぐテクノロジーを信頼することを可能にするのです。
自分の分野の論文に埋もれていませんか？
研究キーワードに一致する最新の論文のダイジェストを毎日受け取りましょう——技術要約付き、あなたの言語で。