形式的検証済み AES-XTS: s2n-bignum に加わった初の AES アルゴリズム

本ブログは 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 ビットでない場合、暗号文スティーリングが機能します。暗号文スティーリングは前のブロックからバイトを「借用」することで、パディングや無駄な領域なしに任意の長さのデータを暗号化できるようにします。これにより、各ブロックの暗号化を位置に基づいて行いながら、任意のセクタを独立して読み書きできます。これはディスク暗号化において重要な機能です。なぜなら、ディスク暗号化のセキュリティモデルでは、攻撃者が対象以外のセクタにアクセスし、それらを変更し、復号を要求することが許容されているためです。また、暗号文のサイズが平文と完全に同じになることも保証され、所定の場所に収まります。

アセンブリ実装の制御フロー

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 つのブランチはすべて暗号文スティーリングで終了します。これは、暗号化アルゴリズムと復号アルゴリズムの制御フローグラフ (下記参照) で確認できます。コード全体を通して、定数時間の設計思想を維持しました。つまり、分岐や特別な処理は秘密データではなく、入力バイト長などの公開値のみに基づいています。

パフォーマンス

コードへの修正により、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 <= 224 を満たすならば、
初期マシン状態が適切なシンボリック値で設定されている場合、
プログラム全体が実行された後、出力バッファに格納された値は 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 での経験により、アセンブリコードの証明駆動開発が、証明可能な正当性を保ちつつ、より理解しやすく、レビューしやすく、保守しやすく、最適化しやすい制御フローを生み出すことが示されました。