自動推論で「25519」楕円曲線暗号の高速化と正当性保証を実現

本ブログは 2024 年 9 月 10 日に公開された Amazon Science Blog “Better-performing “25519” elliptic-curve cryptography” を翻訳したものです。

自動推論と CPU マイクロアーキテクチャ固有の最適化により、パフォーマンスと実装の正当性の保証がともに向上します。

暗号アルゴリズムはオンラインセキュリティに不可欠です。Amazon Web Services (AWS) では、Google の BoringSSL プロジェクトのコードをベースにしたオープンソースの暗号ライブラリ AWS LibCrypto (AWS-LC) に暗号アルゴリズムを実装しています。AWS-LC は、セキュリティと AWS ハードウェアへの最適化を両立した暗号アルゴリズムの実装をお客様に提供しています。

近年利用が広がっている暗号アルゴリズムに x25519 と Ed25519 があります。どちらも Curve25519 として知られる楕円曲線に基づいています。これらのアルゴリズムの実装をさらに改善するため、AWS では最近 AWS-LC における実装の見直しに取り組みました。本記事では以降、x25519 および Ed25519 をまとめて x/Ed25519 と表記します。

2023 年、AWS は AWS-LC における x/Ed25519 のアセンブリレベルの実装を複数リリースしました。自動推論と最先端の最適化技術を組み合わせることで、従来の AWS-LC 実装と比べてパフォーマンスが向上し、正当性の保証も強化されています。

具体的には、自動推論を用いて機能的正当性を証明するとともに、命令セットアーキテクチャ (ISA) の x86_64 および Arm64 において、特定の CPU マイクロアーキテクチャをターゲットとした最適化を行っています。また、実行時間の差異から秘密情報を推測するサイドチャネル攻撃を防ぐため、アルゴリズムの定数時間実行にも細心の注意を払っています。

本記事では、自動推論による正当性の証明プロセス、マイクロアーキテクチャ (μarch) の最適化技術、定数時間コードに関する考慮事項、パフォーマンス向上の定量的な評価など、この取り組みのさまざまな側面を紹介します。

楕円曲線暗号

楕円曲線暗号は、公開鍵と秘密鍵のペアを使用する公開鍵暗号の一手法です。最もよく知られた公開鍵暗号方式の 1 つが RSA で、その公開鍵は非常に大きな整数であり、対応する秘密鍵はその整数の素因数です。RSA はデータの暗号化/復号とデータの署名/検証の両方に使用できます。(2024 年 9 月に、AWS チームのメンバーが Amazon Science ブログにて、自動推論を活用した Amazon Graviton2 チップ上の RSA 実装の高速化とデプロイの容易化について紹介しています。)

楕円曲線は、公開鍵と秘密鍵を数学的に関連付ける別の手法です。この手法により、暗号方式をより効率的に実装できる場合があります。楕円曲線の数学理論は広範かつ奥深いものですが、暗号で使用される楕円曲線は通常、y² = x³ + ax² + bx + c (a、b、c は定数) の形の方程式で定義されます。この方程式を満たす点は 2 次元グラフ上にプロットできます。

楕円曲線には、2 点で曲線と交わる直線は他に高々もう 1 点でしか曲線と交わらないという性質があります。この性質を利用して曲線上の演算を定義します。例えば、曲線上の 2 点の加算は、最初の 2 点を通る直線が曲線と交わる第 3 の点そのものではなく、その第 3 の点を対称軸に関して反転した点として定義されます。

ここで、曲線上の点の座標をある整数を法としてとると、曲線は平面上の離散的な点の集合になります。しかし対称性は依然として保たれるため、加算演算は引き続き矛盾なく定義できます。Curve25519 は大きな素数 (具体的には 2²⁵⁵ – 19) にちなんで名付けられています。この素数を法とする数の集合と、同じ素数を法とする乗算などの基本算術演算を組み合わせることで、楕円曲線演算の基盤となる体 (field) が定義されます。

楕円曲線の加算を繰り返し行うことをスカラー倍算と呼び、スカラーは加算の回数を表します。暗号で使用される楕円曲線では、スカラー倍算の結果のみがわかっている場合、スカラーが十分に大きければ元のスカラーを復元することは計算上困難です。このスカラー倍算の結果が公開鍵の基礎となり、元のスカラーが秘密鍵の基礎となります。

x25519 と Ed25519 暗号アルゴリズム

x/Ed25519 の各アルゴリズムにはそれぞれ異なる目的があります。x25519 は鍵共有アルゴリズムであり、2 つのピア間で安全に共有シークレットを確立するために使用されます。一方、Ed25519 はデジタル署名アルゴリズムであり、データの署名と検証に使用されます。

x/Ed25519 アルゴリズムは TLS や SSH などのトランスポート層プロトコルで広く採用されています。2023 年には、NIST が Ed25519 の追加を含む FIPS 185-6 Digital Signature Standard の更新を発表しました。また、x25519 アルゴリズムはポスト量子暗号ソリューションにおいても重要な役割を果たしており、TLS 1.3 や SSH のポスト量子鍵共有ハイブリッド方式において、古典的アルゴリズムとして仕様に組み込まれています。

マイクロアーキテクチャの最適化

特定の CPU アーキテクチャ向けにアセンブリコードを記述する際には、その ISA を使用します。ISA は、利用可能なアセンブリ命令とそのセマンティクス、プログラマがアクセスできる CPU レジスタなどのリソースを定義するものです。ここで重要なのは、ISA はあくまで CPU の抽象的な定義であり、ハードウェアとしてどのように実現するかを規定するものではないという点です。

CPU のハードウェアレベルの詳細な実装はマイクロアーキテクチャと呼ばれ、各 μarch には固有の特性があります。例えば、AWS Graviton 2 CPU と AWS Graviton 3 CPU はどちらも Arm64 ISA に基づいていますが、μarch の実装は異なります。AWS では、この μarch の違いを活用することで、AWS-LC の既存実装よりもさらに高速な x/Ed25519 実装を実現できるのではないかと考えました。実際に、この仮説は正しいことが確認されました。

ここでは、μarch の違いをどのように活用したかを詳しく見ていきましょう。Curve25519 上にはさまざまな算術演算を定義でき、これらの演算を組み合わせて x/Ed25519 アルゴリズムが構成されます。概念的には、必要な算術演算は以下の 3 つのレベルに分けて考えることができます。

1. 体の演算: Curve25519 の素数 2²⁵⁵ – 19 で定義される体における演算
2. 楕円曲線群の演算: 2 点 P1 と P2 の加算など、曲線上の要素に対する演算
3. トップレベルの演算: スカラー倍算など、楕円曲線群の演算を繰り返し適用して実現される演算

各レベルにはそれぞれ独自の最適化の余地があります。AWS ではレベル 1 の演算に μarch 固有の最適化を集中させ、レベル 2 と 3 については既知の最先端技術を採用しており、異なる μarch 間でほぼ同一の実装となっています。以下に、x/Ed25519 の実装で採用した μarch 固有の選択の概要を示します。

• 最新の x86_64 μarch では、MULX、ADCX、ADOX 命令を使用しています。これらは、一般に BMI および ADX と呼ばれる命令セット拡張に含まれる命令で、標準アセンブリ命令 MUL (乗算) および ADC (キャリー付き加算) の変形です。これらの命令の特長は、組み合わせて使用することで 2 つのキャリーチェーンを並列に維持できる点にあり、最大 30% のパフォーマンス向上が確認されています。これらの命令セット拡張をサポートしない旧世代の x86_64 μarch では、従来のシングルキャリーチェーンを使用しています
• 整数乗算器が改良された AWS Graviton 3 などの Arm64 μarch では、比較的単純な筆算方式の乗算でも良好なパフォーマンスが得られます。一方、AWS Graviton 2 は乗算器が小さい Arm64 μarch であるため、乗算を再帰的に分解する減算形式のカラツバ乗算を採用しています。これは、この μarch では 128 ビットの結果を生成する 64×64 ビット乗算のスループットが他の演算と比べて大幅に低く、カラツバ最適化がより小さな数値サイズでも有効になるためです

すべての μarch に共通するレベル 1 の演算についても最適化を行いました。その一例が、バイナリ最大公約数 (GCD) アルゴリズムによるモジュラー逆元の計算です。AWS ではバイナリ GCD の「divstep」形式を採用しています。この形式は効率的な実装に適している一方、もう一つの目標である正当性の形式的な証明はより困難になります。

バイナリ GCD は 2 つの引数を持つ反復アルゴリズムで、最大公約数を求めたい数を初期値として使用します。各イテレーションで引数は明確に定義された方法で縮小され、いずれか一方がゼロになるとアルゴリズムは終了します。n ビットの 2 つの数に対しては、標準的な実装では各イテレーションで合計少なくとも 1 ビットが除去されるため、2n 回のイテレーションで十分です。

しかし divstep の場合、基底ケースに到達するために必要なイテレーション回数を解析的に決定するのは困難と考えられています。この上界に対する最も扱いやすい証明は、引数値に対応する点を含む 2 次元空間の領域を証明可能な形で過大近似する精巧な「stable hull」に基づいており、入念な帰納法の議論が展開されています。x25519 と Ed25519 の発明者の一人である Daniel Bernstein 氏は、本記事の著者の一人である John が開発した HOL Light 対話型定理証明器を使用して、この上界の形式的な正当性を証明しました。(HOL Light の詳細については、先述の RSA に関する記事をご覧ください。)

パフォーマンスの結果

ここでは、パフォーマンスの向上について紹介します。簡潔にするため、AWS Graviton 2、AWS Graviton 3、Intel Ice Lake の 3 つの μarch に焦点を当てます。パフォーマンスデータの収集には、各 CPU μarch に対応する EC2 インスタンス (それぞれ c6g.4xlarge、c7g.4xlarge、c6i.4xlarge) を使用しました。各アルゴリズムのベンチマークには AWS-LC speed tool を使用しました。

以下のグラフでは、単位はすべて 1 秒あたりの演算回数 (ops/sec) です。「before」列は AWS-LC の既存の x/Ed25519 実装のパフォーマンスを、「after」列は新しい実装のパフォーマンスを表しています。

最も大きな改善が見られたのは x25519 アルゴリズムです。なお、以下のグラフにおける x25519 の演算には、x25519 鍵共有に必要な 2 つの主要な演算である基底点乗算と可変点乗算の両方が含まれています。

AWS Graviton 2、AWS Graviton 3、Intel Ice Lake の 3 つの μarch 全体で、平均 86% のパフォーマンス向上を達成しました。

正当性の証明

AWS では、AWS-LC における x/Ed25519 実装のコア部分を s2n-bignum で開発しています。s2n-bignum は、暗号アプリケーション向けに設計された AWS が所有する整数演算ルーチンライブラリです。s2n-bignum ライブラリでは、HOL Light を使用して実装の機能的正当性も証明しています。HOL Light は、高階論理 (Higher-Order Logic、略して HOL) のための対話型定理証明器です。名前の「Light」が示すとおりシンプルさを重視して設計されており、構成による正しさ (correct by construction) のアプローチで証明を行います。このシンプルさにより、「証明された」とされるものが本当に厳密に証明されたものであり、証明器のバグによる誤りではないという高い確信が得られます。

実装をアセンブリで記述する際にも、同じシンプルさの原則に従っています。アセンブリでの記述はより困難ですが、正当性の証明においては明確な利点があります。コンパイラに依存しない証明が可能になるためです。

下の図は、x/Ed25519 の正当性の証明プロセスを示しています。このプロセスには 2 種類の入力が必要です。1 つ目は評価対象のアルゴリズム実装、2 つ目はアルゴリズムの正しい数学的挙動と CPU の挙動をモデル化した証明スクリプトです。証明は HOL Light 固有の関数列として記述され、証明戦略とその適用順序を定義します。証明の記述は自動化されておらず、開発者の創意工夫が求められます。

HOL Light は、アルゴリズム実装と証明スクリプトを入力として受け取り、実装が正しいと判定するか、判定できない場合は失敗を返します。HOL Light はアルゴリズム実装をマシンコードのバイト列として扱い、CPU 命令の仕様と証明スクリプト内に開発者が記述した戦略を用いて、実行の正当性を検証します。

正当性の証明のこのステップは自動化されており、s2n-bignum の継続的インテグレーション (CI) ワークフローにも組み込まれています。CI がカバーするワークフローは、図中の赤い点線で示されています。CI 統合により、正当性の形式的証明に合格しない限り、アルゴリズム実装コードの変更を s2n-bignum のコードリポジトリにコミットできないことが保証されます。

CPU 命令の仕様は、正当性の証明において最も重要な要素の 1 つです。証明が実際に正しいものであるためには、仕様が各命令の実際のセマンティクスを正確に捉えている必要があります。この信頼性を高めるため、AWS では実際のハードウェア上で命令仕様に対するランダム化テストを実施し、ファジングによって不正確さを検出しています。

定数時間

AWS では、セキュリティを最優先事項として実装と最適化を設計しました。暗号コードは、権限のないユーザーが秘密情報を抽出できるようなサイドチャネルを排除するよう努める必要があります。例えば、暗号コードの実行時間が秘密の値に依存する場合、攻撃者は実行時間からその値を推測できる可能性があります。同様に、CPU キャッシュの動作が秘密の値に依存する場合、キャッシュを共有する権限のないユーザーがその値を推測できる可能性があります。

x/Ed25519 の実装は、定数時間を念頭に置いて設計されています。入力値にかかわらずまったく同じ基本 CPU 命令シーケンスを実行し、データ依存のタイミングを持つ可能性のある CPU 命令は使用しません。

アプリケーションでの x/Ed25519 最適化の活用

AWS では、さまざまな AWS サービスのサブシステムにおける暗号処理に AWS-LC を広く使用しています。本記事で紹介した x/Ed25519 の最適化は、アプリケーションで AWS-LC を使用することで活用できます。アプリケーションへの AWS-LC の統合方法については、GitHub の AWS-LC をご覧ください。

開発者がより簡単に統合できるよう、AWS は AWS-LC から複数のプログラミング言語へのバインディングを作成しました。これらのバインディングは、明確に定義された API を通じて AWS-LC の暗号機能を提供するため、高水準プログラミング言語で暗号アルゴリズムを改めて実装する必要はありません。現在、AWS は Java 向けの Amazon Corretto Cryptographic Provider (ACCP) と Rust 向けの AWS-LC (aws-lc-rs) のバインディングをオープンソースとして公開しています。さらに、CPython が AWS-LC に対してビルドし、Python 標準ライブラリのすべての暗号処理に AWS-LC を使用できるようにするパッチも提供しています。以下に、暗号処理に AWS-LC を採用しているオープンソースプロジェクトの一部を紹介します。

取り組みはこれで終わりではありません。AWS は引き続き x/Ed25519 のパフォーマンス改善に取り組むとともに、s2n-bignum と AWS-LC がサポートする他の暗号アルゴリズムの最適化も推進しています。最新情報については、s2n-bignum と AWS-LC の GitHub リポジトリをご確認ください。