
# ML-KEM / FIPS 203の安全、高速、ポータブルなC90実装
mlkem-native は、ML-KEM[^FIPS203] の安全で高速かつ移植性に優れた C90[^C90] 実装です。 これは ML-KEM リファレンス実装[^REF] のフォークです。
mlkem/src/* および mlkem/src/fips202/* 内のすべての C コードは、CBMC[^CBMC] を用いてメモリ安全性(メモリオーバーフローなし)と型安全性(整数オーバーフローなし)が証明されています。すべての AArch64 および x86_64 アセンブリは、HOL-Light[^HOL-Light] を用いて、機能的に正しく、メモリ安全であり、秘密情報に依存しないタイミング(定数時間)であることが証明されています。
mlkem-native には、Arm(64ビット、Neon)、Intel/AMD(64ビット、AVX2)、RISC-V(64ビット、RVV)、POWER(ppc64le、VSX)向けのネイティブバックエンドが含まれています。パフォーマンスデータについては benchmarks を参照してください。
mlkem-native は、Linux Foundation の一部である Post-Quantum Cryptography Alliance によって支援されています。
# 基本パッケージのインストール
sudo apt-get update
sudo apt-get install make gcc python3 git
# mlkem-native のクローン
git clone https://github.com/pq-code-package/mlkem-native.git
cd mlkem-native
# ビルドとテストの実行
make build
make test
# `make` の便利なラッパーである `tests` を使用する場合も同様
./scripts/tests all
# すべてのオプションを表示
./scripts/tests --help
詳細については BUILDING.md を参照してください。
mlkem-native は以下のプロジェクトで使用されています。
mlkem/src/* および mlkem/src/fips202/* 内のすべての C コードは、メモリ安全性(メモリオーバーフローなし)と型安全性(整数オーバーフローなし)が証明されています。 これは C Bounded Model Checker (CBMC) を使用し、ソースコード内の関数契約とループ不変条件の注釈に基づいています。詳細は proofs/cbmc を参照してください。
すべての AArch64 および x86_64 アセンブリは、オブジェクトコードレベルで、機能的に正しく、メモリ安全であり、秘密情報に依存しないタイミング(定数時間)を持つことが証明されています。これは HOL-Light 対話型定理証明器と s2n-bignum 検証インフラストラクチャ(Arm および x86 アーキテクチャの関連部分のモデルを含む)を使用します。詳細は proofs/hol_light を参照してください。
注記: 形式検証は決して絶対的なものではありません。mlkem-native に関する形式検証の範囲、前提、リスクの詳細な分析については SOUNDNESS.md を参照してください。
mlkem-native 内のすべての AArch64 および x86_64 アセンブリは、HOL Light において、秘密情報に依存する制御フロー、メモリアクセスパターン、および可変レイテンシ命令がないことが正式に証明されており、ほとんどのタイミングサイドチャネルを阻止します(詳細は proofs/hol_light を参照)。C コードは、適切なバリアと定数時間パターンを通じて、コンパイラによって導入されるタイミングサイドチャネル(KyberSlash[^KyberSlash] や clangover[^clangover] など)に対して強化されています。
秘密情報に依存する分岐、メモリアクセスパターン、可変レイテンシ命令がないことは、valgrind を使用し、さまざまなコンパイラとコンパイルオプションの組み合わせでもテストされています。
その他の攻撃。 mlkem-native はタイミングサイドチャネルへの耐性のみを対象としています。電力および電磁サイドチャネル、マイクロアーキテクチャサイドチャネル(例: 投機的実行)、フォールトインジェクション攻撃などの他の攻撃クラスは、現在のところ対象外です。
mlkem-native は、フロントエンド と、算術および FIPS202 / SHA3 用の 2 つの バックエンド に分割されています。フロントエンドは固定で、C で書かれており、パフォーマンスに重要でないすべてのルーチンをカバーしています。バックエンドは柔軟で、パフォーマンスに敏感なルーチンを担当し、C またはネイティブコード(アセンブリ/イントリンシクス)で実装できます。算術バックエンドについては mlkem/src/native/api.h、FIPS-202 バックエンドについては mlkem/src/fips202/native/api.h を参照してください。
mlkem-native は現在、以下のバックエンドを提供しています。
新しいバックエンドの提供を希望される場合は、ご連絡いただくか、PR をオープンしてください。
私たちの AArch64 アセンブリは、SLOTHY ペーパー[^SLOTHY_Paper] で説明されているアプローチに従い、SLOTHY スーパーオプティマイザを使用して開発されています。 「クリーンな」アセンブリを手書きし、マイクロ最適化を自動化します(例: clean と optimized AArch64 NTT を参照)。 詳細については dev/README.md を参照してください。
mlkem-native は、すべての公式 ACVP ML-KEM テストベクター[^ACVP] および Wycheproof[^wycheproof] ML-KEM テストベクターに対してテストされています。
tests スクリプトまたは ACVP クライアント を直接使用して ACVP テストを実行できます。
# tests スクリプトを使用
./scripts/tests acvp
# 特定の ACVP リリースを使用
./scripts/tests acvp --version v1.1.0.41
# ACVP クライアントを直接使用
python3 ./test/acvp/acvp_client.py
python3 ./test/acvp/acvp_client.py --version v1.1.0.41
# 特定の ACVP テストベクターファイルを使用(ACVP-Server からダウンロード)
# python3 ./test/acvp/acvp_client.py -p {PROMPT}.json -e {EXPECTED_RESULT}.json
# 例: 上記を実行したと仮定
python3 ./test/acvp/acvp_client.py \
-p ./test/acvp/.acvp-data/v1.1.0.41/files/ML-KEM-keyGen-FIPS203/prompt.json \
-e ./test/acvp/.acvp-data/v1.1.0.41/files/ML-KEM-keyGen-FIPS203/expectedResults.json
tests スクリプトまたは Wycheproof クライアント を直接使用して Wycheproof[^wycheproof] テストを実行できます。
# tests スクリプトを使用
./scripts/tests wycheproof
# Wycheproof クライアントを直接使用
python3 ./test/wycheproof/wycheproof_client.py
tests スクリプトを使用して、パフォーマンス、メモリ使用量、バイナリサイズを測定できます。
# 速度ベンチマーク(-c はサイクルカウンタを選択: NO、PMU、PERF、または MAC)
# 注: PERF/MAC は、ベンチマークバイナリを sudo で実行するために -r フラグが必要な場合があります
./scripts/tests bench -c PMU
./scripts/tests bench -c PERF -r
# スタック使用量の分析
./scripts/tests stack
# バイナリサイズの測定
./scripts/tests size
CI ベンチマーク結果と過去のパフォーマンスデータについては、ベンチマークページ を参照してください。
mlkem-native を使用する場合は、mlkem をプロジェクトのソースツリーにインポートし、お好みのビルドシステムでビルドしてください。詳細については mlkem を、簡単な例については examples/basic を参照してください。このリポジトリで提供されているビルドシステムは開発目的のみです。
戻り値、ポインタの有効性、エラー時の出力バッファの状態など、すべての公開関数に適用される規約については API-CONVENTIONS.md を参照してください。