本ブログは 2026 年 4 月 7 日に公開された Amazon Science Blog “ Verifying and optimizing post-quantum cryptography at Amazon ” を翻訳したものです。 自動推論によって、セキュリティ、性能、保守性の要求をどのように両立させるか。 現在、安全なオンライン通信は 公開鍵暗号 によって実現されています。主に RSA と楕円曲線暗号 (ECC) が使われており、その安全性はある計算問題が困難であるという仮定に依存しています。しかし、これらの問題は 従来の コンピュータでは困難と考えられているものの、十分に大規模な量子コンピュータでは扱える可能性があります。「Store now, decrypt later」(今保存して後で復号) 攻撃は、暗号化された情報を傍受しておき、量子コンピュータで復号できるようになるまで保持する攻撃です。こうした攻撃が技術的に実現可能になるよりはるか前から、対策が必要となります。 ポスト量子暗号 (PQC) は、従来のコンピュータ上で動作しながら量子コンピューティングに対しても安全な暗号です。2024 年、米国国立標準技術研究所 (NIST) は 8 年にわたる標準化作業を経て、標準規格 FIPS-203 を公開しました。FIPS-203 では、量子コンピュータからの攻撃に対して安全と考えられている鍵共有メカニズムとして、Module-Lattice-Based Key Encapsulation Mechanism (ML-KEM) が規定されています。 本記事では、Amazon Automated Reasoning Group、AWS Cryptography、そしてオープンソースコミュニティが協力して、ML-KEM のオープンソースかつ形式的に検証された最適化実装をどのように作り上げ、お客様を「Store now, decrypt later」攻撃から最高の保証と最小のコストで保護しているかをご紹介します。 優れた暗号エンジニアリングとは何か? Amazon の Customer Obsession に従い、AWS は暗号ソリューションに取り組む際、次の 3 つの目標を優先します。 お客様のデータのセキュリティ : 暗号は安全に実装することが極めて難しく、わずかな欠陥でもお客様のプライバシーを危険にさらす可能性があるため、万全を期す必要があります お客様の体験 : 暗号には計算コストが伴います。AWS はこれを最小化し、お客様に最小のコストと最良の体験を提供します ソリューションを将来にわたって保守する能力 : 保守に費やす時間が少ないほど、お客様のためにより多くのイノベーションを生み出せます しかし、これらの目標の間にはトレードオフがあります。シンプルなコードは保守も安全な記述も最も簡単ですが、動作が遅くなりがちです。一方、高速なコードは監査が難しく、エラーが起きやすい傾向があります。 自動推論 によって、AWS はこのトレードオフを解消し、安全で、高速で、保守しやすい暗号ソリューションを同時にお客様に提供できます。 なぜ新たな ML-KEM 実装が必要なのか ML-KEM (旧称 Kyber) は実装の観点から十分に研究されています。一方では、 Kyber リファレンスコード が、長年精査されてきたクリーンな C 言語実装を提供しています。他方では、ML-KEM をさまざまな指標やプラットフォーム向けに最適化する方法を記述した数多くの研究論文があります。 2024 年に AWS Cryptography と Amazon Automated Reasoning Group が直面した課題は、リファレンス実装のシンプルさと、研究で明らかになった最適化の可能性を、本番環境で使える単一の実装に組み合わせることでした。 2024 年、AWS Cryptography と Amazon Automated Reasoning Group は、徹底的に精査された ML-KEM リファレンス実装のシンプルさと、研究で明らかになった最適化の可能性を、本番環境で使える単一の実装 mlkem-native にまとめるという課題に取り組みました。 同じ頃、AWS は Linux Foundation の Post-Quantum Cryptography Alliance (PQCA) の創設メンバーとなりました。PQCA は、「標準化過程にあるポスト量子暗号アルゴリズムの高保証ソフトウェア実装の構築を目指すオープンソースプロジェクトの集合」である Post-Quantum Cryptography Package (PQCP) を立ち上げました。 そこで AWS は独自にコードを開発するのではなく、チームメンバーが PQCP に参加し、まもなく mlkem-native を立ち上げました。これは、ML-KEM リファレンス実装と、最適化および形式的検証に関する研究を組み合わせることを目的とした、ML-KEM の高保証・高性能 C 言語実装です。 速く、そして慎重なコーディング mlkem-native のモジュラー設計は、ML-KEM の高レベルロジックをカバーする フロントエンド と、性能が重要なすべてのサブルーチンを担当する バックエンド を組み合わせています。各サブルーチン (SHA3 の基礎となる Keccak 置換や、高速な多項式演算の基礎となる数論変換 (NTT) を含む) には、特定のハードウェア向けにネイティブに記述された、高効率な複数の実装が用意されています。デフォルトの C 言語実装に加えて、mlkem-native は AArch64、x86_64、RISC-V64 向けのアセンブリ/組み込み関数バックエンドを提供しています。 mlkem-native のモジュラー設計は、ML-KEM の高レベルロジックをカバーするフロントエンドと、性能が重要なサブルーチンの複数のハードウェア固有実装からなるバックエンドを組み合わせています。 保守性のために重要なのは、フロントエンドとバックエンドの間のインターフェイスが固定されていることです。新しいターゲットアーキテクチャ向けの最適化を追加する開発者は、バックエンド仕様に従って選択したバックエンド機能を実装し、フロントエンドはそのまま維持します。バックエンド仕様の策定は、見かけほど単純ではないことが分かりました。これについては以下で説明します。 限界を知る メモリ安全性 C プログラミング言語のよく知られた課題は、バッファオーバーフローのリスクです。メモリ領域の指定された境界を超えて書き込むと、データ構造が破壊され、悪意を持って悪用されると非特権コードの実行につながる可能性があります。こうした問題の総称が メモリ安全性 です。Rust のようなメモリ安全な言語は、範囲外アクセスの影響を制限できます (たとえば、未定義動作を示す代わりにパニックする)。しかし、間違いそのものを防ぐわけではありません。 型安全性 もう一つのよく知られた課題は ML-KEM の実装に関するもので、整数オーバーフローのリスク、つまり 型安全性 の側面です。RSA や ECC と同様に、ML-KEM はモジュラー演算に依存しています。モジュラー演算では、演算の結果を特定の数 (ML-KEM の場合は素数 3,329 で、 MLKEM_Q または単に q と表記) で割り、その剰余だけが次に持ち越されます。剰余演算子はパーセント記号 % で表されます。 論理的には、ML-KEM で 2 つの数 x と y を加算または乗算する必要がある場合、( x + y ) % q および ( x * y ) % q を計算する必要があります。たとえば、(294 * 38) % q = 11,172 % q = 1,185 となります。このような「即時」のモジュラー q 演算は、データを「正規」範囲 {0, 1, 2, … , q -1} で表すために常にモジュラー還元を適用するもので、極めて遅くなります。 効率的な ML-KEM 実装では、代わりに「遅延」モジュラー q 演算を使用します。データはできるだけ長くモジュラー還元なしで操作され、最悪の場合のオーバーフローのリスクが生じたときにのみ還元が行われます。さらに、これにより Montgomery 還元のような不完全な還元アルゴリズムが使えるようになります。これは高速ですが、必ずしも完全に還元された出力を返すわけではありません。 ML-KEM の場合、モジュラー q = 3,329 のデータは通常、符号付き 16 ビット整数に格納されます。ML-KEM の数多くの算術ルーチン全体で遅延演算を扱う際には、データの最悪値の境界を追跡し、それらの境界が 16 ビット整数の限界を超える可能性のある箇所にモジュラー還元を挿入することが不可欠です。この領域での小さな間違いは、テストで見逃されることがあります。なぜなら、平均的な境界は最悪値の境界よりはるかに小さい傾向があるためです。そして、本番環境でランダムに表面化することがあります。 バッファ境界、特に算術境界の追跡は、時間がかかり、エラーが起きやすい作業です。たとえば、低レベルの算術関数の出力境界を弱めると、まったく別の関数で稀に算術オーバーフローが発生することがあります。これを手作業で確認するには、緻密なドキュメント作成と熟練した監査担当者が必要なだけでなく、開発が遅くなります。 mlkem-native では、C Bounded Model Checker (CBMC) というツールを使用して、C レベルでメモリ安全性と型安全性を自動的に検証しています。各関数について、機械可読かつ人間可読な契約をソースコードに追加してバッファと算術データの境界を指定し、CBMC にそれらの境界に対してバッファオーバーフローや算術オーバーフローが発生し得ないことを自動的に検証させます。 モジュラー還元の簡単な例を見てみましょう。 void mlk_poly_reduce_c(mlk_poly *r) __contract__( requires(memory_no_alias(r, sizeof(mlk_poly))) assigns(memory_slice(r, sizeof(mlk_poly))) ensures(array_bound(r->coeffs, 0, MLKEM_N, 0, MLKEM_Q))) { unsigned i; for (i = 0; i < MLKEM_N; i++) __loop__( invariant(i <= MLKEM_N) invariant(array_bound(r->coeffs, 0, i, 0, MLKEM_Q))) { /* Barrett reduction, giving signed canonical representative */ int16_t t = mlk_barrett_reduce(r->coeffs[i]); /* Conditional addition to get unsigned canonical representative */ r->coeffs[i] = mlk_scalar_signed_to_unsigned_q(t); } mlk_assert_bound(r, MLKEM_N, 0, MLKEM_Q); } 関連する部分を一つずつ見ていきましょう。まず、 __contract__( … ) に注目します。簡単に言うと、 memory_no_alias と memory_slice の行は、コードが読み書きできるメモリを指定しています。これはメモリ安全性に関連します。 ensures(array_bound(…)) 句は型安全性に関連しています。これは、関数が戻った時点でデータが区間 [0, 1, …, q ) 内にあることを 保証する ことを指定します。証明では、 __loop__(invariant(…)) があり、ループがこの境界を段階的にどう確立するかを指定しています。 i 番目のイテレーションでは、 i 番目の係数まで成立します。最後に、実装は実質的に mlk_barrett_reduce と mlk_scalar_signed_to_unsigned_q を組み合わせています。CBMC はこれらの内部を見ず、それらの契約に置き換えます。 int16_t mlk_barrett_reduce(int16_t a) __contract__( ensures(return_value > -MLKEM_Q_HALF && return_value < MLKEM_Q_HALF) { ... } int16_t mlk_scalar_signed_to_unsigned_q(int16_t c) __contract__( requires(c > -MLKEM_Q && c < MLKEM_Q) ensures(return_value >= 0 && return_value < MLKEM_Q) ensures(return_value == (int32_t)c + (((int32_t)c < 0) * MLKEM_Q)) { ... } mlk_barrett_reduce がまず対称的な出力区間 ( -q /2, …, q /2) を確立し、次に mlk_scalar_signed_to_unsigned_q がそれを [0,1, …, q ) にマッピングしているのが分かります。この例では、仕様が望ましい形で整合していることを目視で簡単に確認できますが、より複雑な例ではそれほど明確ではありません。いずれにせよ、CBMC が自動的にチェックしてくれます。 速く動かしながら安全を保つ 上述の CBMC 証明は、mlkem-native の C コードに対するメモリ安全性と型安全性を確立します。しかし、mlkem-native の最も性能が重要な部分 (Keccak 置換と数論変換) は、AArch64 と x86_64 向けに手作業で最適化されたアセンブリで実装されています。 mlkem-native のアセンブリ実装に対して、高い性能を維持しつつ保証を得るために、AWS は次の 3 つのコンポーネントを使用しています。アセンブリのスーパーオプティマイザーである SLOTHY、対話型定理証明器である HOL Light、そして HOL Light 上に構築されたアセンブリ用検証基盤である s2n-bignum です。これらを組み合わせることで、開発者がクリーンで保守しやすいアセンブリを記述しつつ、デプロイされるコードが正当性の形式的保証を伴ってピーク性能を達成するワークフローが可能になります。 高性能なアセンブリを手で書くと、根本的なトレードオフが生じます。計算を明確に表現するクリーンで監査可能なコードは遅く、高速なコードは密で、マイクロアーキテクチャ固有で、保守が困難です。SLOTHY はマイクロアーキテクチャ固有の最適化を自動化することで、このトレードオフを解消します。アセンブリプログラムを制約充足問題に変換し、制約ソルバーを使用して最適な命令スケジュールとレジスタ割り当てを見つけ、最適化されたアセンブリを出力します。開発者は計算のロジックを重視したクリーンなコードを書き、SLOTHY が高速なコードを生成します。 AWS は、すべての AArch64 および x86_64 アセンブリルーチンの機能的正当性を、HOL Light と s2n-bignum を使用して証明します。SLOTHY が使用される場所では、特定の命令順序やレジスタ割り当てに依存しないように証明が記述されます。したがって、証明を調整することなく、特定のマイクロアーキテクチャ向けにコードを再最適化できます。この「事後」検証アプローチは、アセンブリで表現された計算の数学的な正しさを、それがどのように生成されたかにかかわらず確立します。特に、SLOTHY は信頼できるコンピューティングベース (TCB) から除外されます。 誠実さを保つ 形式的検証は決して絶対的なものではありません。すべての証明は、形式的なオブジェクト (仕様とモデル) を非形式的な現実世界の要件とシステムに結び付けるものであり、これらの結び付きにはギャップが生じます。形式的仕様は実際に必要なものを捉えているか? 形式的モデルは実際のシステムを忠実に反映しているか? 証明基盤自体は健全か? お客様の信頼を獲得し維持するには、これらの限界について透明性を保つ必要があります。そこで AWS は、 SOUNDNESS.md と題したドキュメントを作成・公開しました。ここでは、mlkem-native で何が証明され、何が仮定され、残存リスクがどこにあるかを、HOL Light 証明で使用されるハードウェアモデルの忠実性、CBMC のより大きな TCB、2 つの検証スタック間の手動の橋渡しに至るまでマッピングしています。各ギャップについて、実施されている緩和策を説明し、今後の作業の概要を示しています。 AWS の目標は完璧を主張することではなく、透明性を通じて信頼を獲得することです。コミュニティの皆様には SOUNDNESS.md を批判的に読み、AWS の前提に異議を唱え、残存するギャップを埋めることにご協力いただければ幸いです。 本番環境への展開 mlkem-native は、AWS サービス全体の安全な通信を支える Amazon のオープンソース暗号ライブラリ AWS-LC に統合されています。この統合では、自動インポーターを使用して mlkem-native のソースコードをアップストリームリポジトリから直接取り込み、AWS-LC が最新の検証済み実装と同期し続けることを保証します。 この統合は手間を最小限に抑えるよう設計されています。mlkem-native のモジュラーアーキテクチャにより、AWS-LC はコアの ML-KEM ロジックをインポートしながら、プラットフォーム固有のコンポーネントには独自の実装を提供できます。たとえば、AWS-LC は mlkem-native の暗号プリミティブを既存の FIPS-202 (SHA-3) 実装にマッピングし、AWS-LC の乱数生成およびメモリゼロ化関数を使用し、必要な場合はペアワイズ一貫性テストなど FIPS モード機能を有効にします。これを可能にしているのは、検証済みコードを変更することなく mlkem-native の API を AWS-LC のインフラストラクチャに橋渡しする薄い互換性レイヤーです。 重要なのは、メモリ安全性と型安全性を証明する CBMC 契約が、インポートされたソースコード内に保持されていることです。プリプロセッサがコンパイルされたバイナリからこれらを削除しますが、ソース内には残り、コードの保証の機械チェック可能なドキュメントとして機能します。これは、実装と共に移動する一種の「生きた証明」です。 さらに、mlkem-native も AWS-LC もオープンソースで寛容なライセンスのため、その利点は AWS の枠を超えて広がります。誰でも mlkem-native を自社のシステムに統合し、同じ性能と保証の組み合わせを得ることができます。形式的検証成果物 (CBMC 契約と HOL Light 証明) はリポジトリの一部であり、関連するすべてのツールはオープンソースであり、セットアップと証明チェックのスクリプトが提供されているため、AWS のセキュリティ主張を独立に検証できます。 インパクト mlkem-native の開発は、自動推論を体系的に適用すれば、暗号エンジニアリングの 3 つの目標 (セキュリティ、性能、保守性) が衝突しないことを示しています。 CBMC は、複雑な算術全体で境界を手動で追跡する作業から AWS を解放し、テストでは見逃されて本番環境でランダムに表面化するエラーを捕捉しました。アノテーションはソースコード内に機械チェック可能なドキュメントとして残り、コードを同時により保守しやすく、より安全にします。HOL Light と s2n-bignum により、AWS は数学的な正当性の確実性を持って積極的なアセンブリ最適化をデプロイできました。SLOTHY により、特定のマイクロアーキテクチャ向けにピーク性能を達成しながら、クリーンで監査可能なコードを書くことができました。そして、証明は最適化に依存しないように記述されているため、検証をやり直すことなくコードのターゲットを変更できます。 その結果、従来の開発で達成できるものよりも、同時により安全で、より高速で、より保守しやすい実装が実現しました。AWS はお客様のセキュリティ、お客様の体験、そして革新する能力の間で妥協しませんでした。自動推論は 3 つすべてを実現したのです。 AWS-LC-FIPS リリース プラットフォーム 処理 3.1 4.0 改善倍率 c7i Keygen 30899 65146 2.1 Encaps 30623 61233 2.0 Decaps 25141 51545 2.0 c7g Keygen 29617 71134 2.4 Encaps 28482 66874 2.3 Decaps 23919 64765 2.3 Amazon の暗号ライブラリ AWS-LC で ML-KEM リファレンス実装から mlkem-native に切り替えた際の性能影響。ML-KEM-768 の性能は c7i および c7g EC2 インスタンスで測定されています。数値は 1 秒あたりの処理数を表します (高いほど良い)。ベースラインは ML-KEM の C リファレンス実装を含む AWS-LC-FIPS 3.1 リリースです。AWS-LC-FIPS 4 リリースは mlkem-native でビルドされています。プラットフォームは Intel(R) Xeon(R) Platinum 8488C を搭載した c7i と、Graviton 3 プロセッサを搭載した c7g です。 謝辞 同僚の John Harrison 氏 (Automated Reasoning Group の senior principal applied scientist) には、HOL Light での AArch64 アセンブリ証明の大部分を提供し、また HOL Light 対話型定理証明器および s2n-bignum 検証基盤の保守を担当いただいたことに感謝します。mlkem-native は AWS だけでなく、オープンソースコミュニティの多くのメンバーが関わる共同作業です。とりわけ、共同保守者である zeroRISC の Matthias Kannwischer 氏に感謝します。彼は AWS と共に mlkem-native を立ち上げ、以来プロジェクトの成功に重要な役割を果たしてきました。 著者について Hanno Becker Hanno Becker は Amazon の Automated Reasoning Group の principal applied scientist です。元 Mbed TLS の開発者で、Arm 上の高性能 (ポスト量子) 暗号に情熱を注いでいます。SLOTHY スーパーオプティマイザーの作者でもあります。 Rod Chapman Rod Chapman は Amazon Web Services (AWS) の senior principal scientist です。 Dusan Kostic Dusan Kostic は Amazon Web Services (AWS) の senior applied scientist です。 本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。

本ブログは 2026 年 3 月 20 日に公開された Amazon Science Blog “ Formally verified AES-XTS: The first AES algorithm to join s2n-bignum ” を翻訳したものです。 コア演算のアセンブリコードを単純化して明確化することで、自動最適化と検証が可能になりました。 暗号化アルゴリズムは、読み取り可能なデータをランダムなビットの並びのように見える暗号文に変換する数学的手続きです。暗号文は、対応する復号アルゴリズムと正しい鍵を使用したときにのみ復号できます。 保管中のデータ (ディスクやデータベースに保存される情報) に対しては、 AES-XTS のようなアルゴリズムが、ストレージに書き込まれる前に各ブロックを暗号化することで、物理的な盗難やストレージシステムへの不正アクセスから保護します。転送中のデータ (ネットワーク上を移動する情報) に対しては、TLS のようなプロトコルが複数のアルゴリズムを組み合わせて使用します。非対称暗号化アルゴリズム (RSA や楕円曲線) で安全な接続を確立し、高速な対称暗号化アルゴリズム (AES-GCM など) で実際のデータストリームを保護するとともに改ざんされていないことを検証します。Amazon Web Services (AWS) では、 EBS 、 Nitro Card 、DynamoDB などのサービスでお客様のデータを保護するために AES-XTS を使用しており、AES-GCM を用いた TLS によりサービス間およびお客様との通信を含むすべてのネットワーク通信を保護しています。 AWS は、AES-XTS 復号の最適化された Arm64 アセンブリ実装の形式的検証に挑戦しました。「形式的検証」とは、エンジニアリングされたシステムが特定の 仕様 を満たすことを数学的に証明するプロセスです。 本研究は、ブロック指向ストレージデバイスの暗号保護に関する IEEE 標準 1619 に従い、AES-XTS の AES-256-XTS バリアントに焦点を当てています。「256」は暗号化鍵のサイズを表します。 固定サイズのブロックを処理するアルゴリズムとは異なり、AES-XTS は 16 バイトから 16 メガバイトまでの可変長データを扱い、不完全なブロックには特別なロジックを使用します。検証されたアセンブリコードは 5 倍アンロール版で、ループが 5 つのレジスタ (それぞれが入力ブロックを格納) で並列実行されるように展開され、最新の CPU パイプライン向けに最適化されていました。エラーがあるとお客様データのセキュリティを損なう可能性がある重要なコードでありながら、手動レビューでは正当性を保証できないほど複雑でした。 Amazon Web Services の形式的に検証された大数演算ライブラリである s2n-bignum の一部として、AWS は改善された Arm64 アセンブリ実装による AES-XTS 暗号化と復号を提供するとともに、チームメンバー (John Harrison) が開発した HOL Light 対話型定理証明器を用いた仕様記述および形式的検証を行いました。 これは、入力長に応じて複数の経路を持つ大規模関数を対象とした証明駆動開発の実験でした。その結果、s2n-bignum ライブラリにおいてこれまでで最大規模の証明が完成しました。典型的な入力サイズである 512 バイトでは、アルゴリズムのパフォーマンスは元のコードと同等か、高度に最適化された Arm コアではわずかに向上しました。このアルゴリズムとその証明を s2n-bignum ライブラリに追加することで、より多くの AES ベースのアルゴリズムを追加する道が開かれます。 アルゴリズムの説明 AES は鍵付き置換を実装するブロック暗号です。つまり、平文ファイルをブロック (この場合は 128 ビットのブロック) に分けて処理し、任意の鍵に対して、各平文ブロックを一意の暗号文ブロックに対応付ける全単射 (一対一かつ可逆) 関数を定義します。この数学的性質により、復号によって元の平文を一意に復元できることが保証されます。 AES-XTS は、ストレージ暗号化のために特別に設計されたモードです。基盤となる構成要素として AES を使用しますが、ディスク暗号化の独自要件に対応するため、位置依存の tweak (調整値) と暗号文スティーリング (ciphertext stealing) (部分ブロックを処理する方法) を追加しています。ディスク暗号化では、任意のセクタへのランダムアクセスが必要であり、データサイズを正確に保つ必要があります。 AES-XTS は、2 つの鍵を使用するアプローチでストレージデータを暗号化します。各 128 ビットブロックとその位置依存の tweak は排他的論理和 (XOR、入力値が異なる場合のみ 1 を出力する二項演算) され、その結果が AES で暗号化され、再び tweak と XOR されます。これにより、ディスク上の異なる位置にある同一のデータが異なる暗号文を生成します。tweak は、セクタ番号を 2 番目の鍵で暗号化し、 ガロア体 で α のべき乗を掛けることで生成され、各ブロック位置に対して一意の値が作成されます。 最後のブロックが完全な 128 ビットでない場合、暗号文スティーリングが機能します。暗号文スティーリングは前のブロックからバイトを「借用」することで、パディングや無駄な領域なしに任意の長さのデータを暗号化できるようにします。これにより、各ブロックの暗号化を位置に基づいて行いながら、任意のセクタを独立して読み書きできます。これはディスク暗号化において重要な機能です。なぜなら、ディスク暗号化のセキュリティモデルでは、攻撃者が対象以外のセクタにアクセスし、それらを変更し、復号を要求することが許容されているためです。また、暗号文のサイズが平文と完全に同じになることも保証され、所定の場所に収まります。 XOR-暗号化-XOR (XEX) 構造を採用した AES-XTS 暗号化 暗号文スティーリングは、最後から 2 番目のブロックの出力を分割することで、暗号化中の部分ブロックを処理 対称復号プロセス 復号のための逆暗号文スティーリング アセンブリ実装の制御フロー AWS は、Amazon の AWS-LC 暗号ライブラリにある既存の AES-XTS 実装から開始しました。AES-XTS は平文を 128 ビットブロックでループ処理し、各ブロックの暗号化には 15 のステップが必要で、各ステップには暗号化鍵から導出された独自の「ラウンドキー」が使用されます。既存の実装は 5 倍アンロールされており、5 ブロックずつ並列で処理します。最後のブロックの長さが 128 ビット未満の場合、入力バッファの限界を超えて読み取る「バッファオーバーリード」のリスクがあります。 オーバーリードを回避するため、既存の実装では入力バッファ内の現在位置へのポインタに対して複雑な操作を行います。これには、追跡が困難な高度な制御フローが必要です。ループカウンタはループの前と途中で複数回インクリメントおよびデクリメントされ、ループには最終的なループバック分岐以外に 2 つの追加の出口点があります。 1 つの出口点は、ループの最終イテレーションで 4 ブロックが残っている場合のためのもので、もう 1 つの出口点は 1 ～ 3 ブロックが残っている場合のためのものです。ループのフローは、パイプラインの使用率を最大化するためにロード/ストア命令と AES および XOR 命令をインターリーブしています。ループ終了後、残りのブロックの処理は 4 から 1 までの長さに対して絡み合っており、最後に部分ブロックがある場合、アルゴリズムは暗号文スティーリング手順を実行します。さらに、15 個のラウンドキーのうち 7 つだけがレジスタに保持され、他の 8 つはループ内外でメモリから繰り返しロードされていました。 AWS はまず、Arm コード用のスーパーオプティマイザである SLOTHY に命令を再配置させてパイプラインの使用率を最大化することで、メインループのパフォーマンスを向上できるかを調査しました。SLOTHY には、さまざまな Arm マイクロアーキテクチャの簡略化されたモデルが含まれています。制約ソルバーを使用して、最適な命令スケジュール、レジスタリネーミング、および周期的なループインターリーブを提供します。 しかし、SLOTHY がループを識別して最適化するためには、ループは典型的なループの動作を示し、各イテレーションの最後にカウンタを減少させ、最初に戻る必要があります。SLOTHY はまた、8 つのラウンドキーをロードすることで作成されるネストされたループを処理できません。 これがループを「整理」し始める動機となりました。まず、すべてのラウンドキーを永続的に保持するためにレジスタを解放しました。これは、最適化された命令の順序が元のコードよりも少ない一時レジスタしか必要としなかったため可能でした。次に、複数の出口点と、残りのブロックを処理するためのループカウンタの操作を取り除きました。カウンタの値は常にバッファに残っている 5 ブロックチャンクの数を示し、SLOTHY の要件に適合します。ループは残りのブロックの処理の前に終了します。 ループが終了したら、1 から 4 までの残りブロック数のそれぞれを処理するための個別の処理ブランチを用意します。4 つのブランチはすべて暗号文スティーリングで終了します。これは、暗号化アルゴリズムと復号アルゴリズムの制御フローグラフ (下記参照) で確認できます。コード全体を通して、定数時間の設計思想を維持しました。つまり、分岐や特別な処理は秘密データではなく、入力バイト長などの公開値のみに基づいています。 AES-256-XTS 暗号化制御フローグラフ AES-256-XTS 復号制御フローグラフ パフォーマンス コードへの修正により、AWS は SLOTHY を使用して暗号化アルゴリズムを最適化できるようになりました。これにより AWS Graviton ファミリーの Arm プロセッサでわずかなパフォーマンス向上が得られましたが、最適化されたアウトオブオーダーパイプラインを持つより高度なチップでは、向上幅は小さくなりました。元の実装と比較して、アルゴリズムの実行を通じてラウンドキーをレジスタに保持しメモリからのロードを節約することで、AES 命令を他の命令とインターリーブしないことの影響を相殺できました。 ループ内の命令フローをよりクリーンにし、出口処理をモジュール化したことで、ループイテレーションのさまざまなアンロール係数を試すことができました。AWS は 3 倍、4 倍、6 倍の係数を実験し、さまざまなマイクロアーキテクチャにおいて 5 倍が依然として最良の選択であると結論付けました。 形式的検証による正当性の確保 最適化された暗号化コードを本番環境にデプロイするには、それが正しく動作することの数学的な確実性が必要です。ランダムテストでは単純なケースを素早くチェックできますが、AWS は AES-XTS 実装に対して最高レベルの保証を提供するために形式的検証を活用しています。 なぜ AES-XTS に HOL Light なのか? AWS の実装が IEEE 1619 仕様に一致することを証明するために、同僚の John Harrison が開発した対話型定理証明器である HOL Light を使用しています。HOL Light は、コードが書かれる際に検証される「構築による正当性」アプローチをソフトウェア開発に対して特に単純に実装したものです。HOL Light の信頼されたカーネルはわずか数百行のコードで、基本的な論理推論規則を実装しています。これは、証明戦術や自動化にバグがあったとしても、HOL Light が誤った証明を受け入れる原因にはなり得ないことを意味します。最悪の場合、バグによって証明を完了できなくなりますが、偽の命題を証明可能にすることはできません。 AWS が AES-XTS 検証に HOL Light を選んだ理由はいくつかあります。 アセンブリレベルの検証 : AWS はコンパイル済みコードに依存するのではなく、実装を直接アセンブリで記述しています。より困難ではありますが、これにより証明はあらゆるコンパイラから独立したものになります。HOL Light は CPU 命令仕様を使用してマシンコードバイトについて直接推論し、ソフトウェアスタックの最下層で保証を提供します。 既存の暗号インフラストラクチャ : s2n-bignum は、実行アーティファクトを取り除き純粋に数学的な問題を残すシンボリックシミュレーション、ワード演算用の特殊化された戦術、バイトリスト処理など、暗号検証のための広範なサポートをすでに提供しています。AWS は AES 演算に関する証明された補題を追加し、他の AES モードの証明にも再利用できるようにしました。 複雑な制御フローの処理 : 十分な説明なしに複雑な証明で失敗する可能性のある完全自動証明器とは異なり、HOL Light の対話型アプローチにより、5 倍アンロールされたループに必要な複雑なループ不変条件を経由して証明を導くことができ、任意の長さのデータブロックを処理し、可変長入力と部分ブロックに必要な複雑なメモリ推論を実行できます。 s2n-bignum フレームワーク s2n-bignum を AES-XTS の実装に使用することは、2 つの目的を果たします。これは x86-64 および Arm アーキテクチャでアセンブリコードを形式的に検証するためのフレームワークであり、暗号化のための高速で検証されたアセンブリ関数のコレクションでもあります。このライブラリには、特に大数の数学的演算 (これが名前の由来) に関する多数の暗号化アルゴリズムの検証済み実装がすでに含まれており、これらは公開鍵暗号プリミティブの基盤となっています。s2n-bignum の一部として公開鍵アルゴリズムを証明するために HOL Light がどのように使用されたかの詳細については、Amazon Science の以前のブログ記事「 Graviton での RSA の高速化: 形式的検証で正当性を証明し開発も加速 」および「 自動推論で「25519」楕円曲線暗号の高速化と正当性保証を実現 」を参照してください。 前述のとおり、AES-XTS は AES ブロック暗号のモードの 1 つです。AES は、換字操作 (S ボックスを使用した SubBytes)、転置操作 (ShiftRows、MixColumns)、および鍵混合を組み合わせた換字・転置ネットワーク (SPN) 構造に基づいています。s2n-bignum を Arm64 および x86_64 プロセッサにある AES 命令セットアーキテクチャ (ISA)、AES ブロック暗号の仕様、および AES-XTS 用の追加仕様を含むように拡張することで、より多くの AES ベースのアルゴリズムを同じ厳密な検証で扱う道を開いています。 仕様の開発とテスト AES およびそれに基づくモードの SPN の性質は、定理証明器が本来理解できる単純な数式 (公開鍵暗号の基本である剰余乗算など) では表現できません。データを処理するステップの記述を書く必要があります。これがアセンブリを検証する前に、HOL Light の仕様が IEEE 標準を正確に捉えているという確信が必要だった理由です。 AWS は、入出力にバイトリストを使用し、内部ブロック演算には 128 ビットワードを使用して、標準の構造を反映するように仕様を記述しました。次に、 変換 を開発しました。これは、評価が数学的に正しいという証明を生成しながら、具体的な入力で仕様を評価するために使用される HOL Light 関数です。 AWS は、さまざまな AES-XTS 暗号化/復号シナリオをカバーし、すべてのブロックの処理 (再帰を使用) と暗号文スティーリングを実行する単体テストを実施することで、仕様を検証しました。 これらのテストにより、より複雑なアセンブリ検証に取り組む前に、仕様が IEEE 標準と一致することが確認されました。この 2 段階のアプローチ (まずテストにより仕様が正しいことを保証し、次に実装が仕様と一致することを形式的に検証する) により、AWS は正しいことを証明しているという確信を得られました。 証明戦略 AWS の証明はコンポジショナル (合成的) であり、全体の問題を個別に証明できる部分問題に分解します。部分問題に応じて、部分証明は有界 (入力範囲に対してのみ真) または無界となります。 5 ブロック (復号の場合は 6 ブロック) 未満の入力に対しては、各ケースを網羅的に検証する有界証明を作成しました。5 ブロック (復号の場合は 6 ブロック) 以上の入力に対しては、ループ実行中に真であり続ける数学的命題であるループ不変条件を開発し、任意の長さの入力に対する正当性を証明しました。ループ不変条件は、ループ終了条件が満たされるまでに 3 つの重要な要素を追跡します。各イテレーションでのレジスタ状態、「tweak」(各ブロックの暗号化を一意にするもの) の進化、そしてブロックが処理されるにつれてのメモリ内容です。部分ブロック (末尾) 処理については、すべてのケースで再利用できる暗号文スティーリングの個別の定理を証明しました。 トップレベルの正当性定理はすべての証明を組み合わせ、次の命題を主張します。 もしプログラム、入力、出力、スタックが特定の互いに素な性質を満たし、 入力長 len が 16 <= len <= 2 24 を満たすならば、 初期マシン状態が適切なシンボリック値で設定されている場合、 プログラム全体が実行された後、出力バッファに格納された値は AES-XTS 仕様を満たさなければならない。 メモリ安全性と定数時間の証明 最近、s2n-bignum にはアセンブリ関数の定数時間およびメモリ安全性の特性を形式的に定義するための新しい関数と戦術が追加されました。これらのリソースにより、s2n-bignum の多くのアセンブリサブルーチンが定数時間でメモリ安全であることが検証されました。これには、楕円曲線のトップレベルのスカラー乗算関数、RSA の大整数演算、ML-KEM 暗号標準の Arm 実装 (Amazon Science で近日公開予定のブログ記事のテーマ) が含まれます。2025 年 10 月時点で AWS-LC で使用するために特定されたすべてのアセンブリサブルーチンは、定数時間でメモリ安全であることが形式的に検証されました。 AWS は、新しい戦術を AES-XTS など、その後追加されたアセンブリサブルーチンの検証に簡単に使用できるかを探っています。前述のとおり、AES-XTS は非常に複雑な制御フローを持っており、長く込み入った機能的正当性証明となりました。その複雑さは安全性証明にとっても課題です。プロセスは進行中ですが、復号および暗号化アルゴリズムの暗号文スティーリングサブルーチンの安全性特性はすでに証明されています。 これらの最初の証明は、バッファオーバーリードが起こりやすい重要なメモリアクセス手順に焦点を当てました。復号および暗号化アルゴリズムの残りの部分の証明は、同じ方法論を使用できます。定数時間およびメモリ安全性の証明は、機能的正当性の証明と同じ構造に従いますが、証明目標がより焦点を絞っているためより単純です。 正当性の継続的保証 AWS は形式的検証を s2n-bignum の継続的インテグレーション (CI) ワークフローに統合しました。これにより、AES-XTS 実装への変更は、形式的な正当性証明を成功裏に通過しなければコミットできないという保証が得られます。CI の一環として、CPU 命令モデリングは実際のハードウェアに対するランダム化テストによって検証され、不正確さを「ファジング」することで、仕様が正しく証明が実際に成立することを保証します。 さらに、証明では入力がシンボルとして表現されるため、すべての可能な入力に対する正当性が保証されます。これにより、コードのすべての経路をカバーできても、すべての入力値をカバーできない可能性があるカバレッジテストの典型的な欠点を克服します。たとえば、ここで使用されているような定数時間コードは、秘密値で分岐することなく記述されます。通常、秘密値はそれらから派生したマスクの使用により演算に組み込まれます。同じ命令が秘密値に関係なく実行されます。したがって、ライン (行) カバレッジの達成は通常開発者の手の届く範囲にありますが、値カバレッジの達成は正当性の形式的検証に委ねられます。 この同じ方法論により、AWS は数学的な正当性の保証を持つ最適化された暗号化実装をデプロイし、同時に大幅なパフォーマンス向上を達成できました。これにより、開発者やツールはバグの導入を心配することなくコードをさらに自由に最適化でき、バグは証明によって自動的に検出されます。AES-XTS での経験により、アセンブリコードの証明駆動開発が、証明可能な正当性を保ちつつ、より理解しやすく、レビューしやすく、保守しやすく、最適化しやすい制御フローを生み出すことが示されました。 著者について Yan Peng Yan Peng は Amazon Web Services (AWS) の applied scientist (応用科学者) です。暗号ライブラリと認可評価ライブラリの形式的検証に取り組んでいます。 Nevine Ebeid Nevine Ebeid は Amazon Web Services (AWS) の Cryptography グループの senior applied scientist (シニア応用科学者) であり、AWS 暗号ライブラリである AWS-LC のための最適化されたアルゴリズムの開発、検証、コンプライアンスに注力しています。AWS に入社する前は、自動車およびモバイルセキュリティアプリケーション向けの暗号ライブラリとプロトコルの研究開発を行っていました。 June Lee Juneyoung Lee は Amazon の Automated Reasoning Group の senior applied scientist (シニア応用科学者) です。 本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。

みなさんこんにちは！ワンキャリアで新卒採用サービス「ワンキャリア」の開発を担当している菅野(GitHub: sgasho ) です。 普段はWebアプリケーション開発を主戦場としていますが、業務の傍らOSSコントリビュートにも注力しています。