mlkem-native

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）的原生后端。有关性能数据，请参阅基准测试。

mlkem-native 得到了后量子密码联盟的支持，该联盟隶属于Linux 基金会。

Ubuntu 快速入门

# 安装基础软件包
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

# 使用 `tests`（一个便捷的 make 包装脚本）执行相同操作
./scripts/tests all
# 显示所有选项
./scripts/tests --help

更多信息请参阅 BUILDING.md。

应用

mlkem-native 被用于以下项目：

• libOQS（Open Quantum Safe 项目），自 0.13.0 起（作为默认的 ML-KEM 实现）
• AWS 的密码学库 AWS-LC，自 v1.50.0 起
• 用 Rust 编写的 rustls TLS 库，自 0.23.28 起（通过 AWS-LC 作为默认密码学提供程序）
• Pavona —— 一个模块化、经流片验证且默认安全的开源硅片模块库

形式化验证

mlkem/src/* 和 mlkem/src/fips202/* 中的所有 C 代码均已证明为内存安全（无内存溢出）和类型安全（无整数溢出）。这使用了 C 有界模型检查器 (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 的_后端_。前端是固定的，用 C 编写，涵盖所有对性能不关键的例程。后端是灵活的，负责对性能敏感的例程，可以用 C 或原生代码（汇编/内联函数）实现；有关算术后端，请参阅 mlkem/src/native/api.h，有关 FIPS-202 后端，请参阅 mlkem/src/fips202/native/api.h。

mlkem-native 目前提供以下后端：

• 默认的可移植 C 后端
• 64 位 Arm 后端（使用 Neon）
• 64 位 Intel/AMD 后端（使用 AVX2）
• 64 位 RISC-V 后端（使用 RVV）
• 64 位 POWER 后端（ppc64le，使用 VSX；支持 POWER8 及以上版本）
• 32 位 Armv8.1-M 后端（使用 Helium/MVE）—— 参见 #1501。该后端仍处于实验阶段，默认禁用。

如果您想贡献新的后端，请与我们联系或直接提交 PR。

我们的 AArch64 汇编是使用 SLOTHY 超级优化器开发的，遵循 SLOTHY 论文[^SLOTHY_Paper] 中描述的方法：我们手工编写“干净”的汇编，并自动化微优化（例如，参见 clean 与 optimized AArch64 NTT 的对比）。更多详情请参阅 dev/README.md。

测试向量

mlkem-native 针对所有官方 ACVP ML-KEM 测试向量[^ACVP] 和 Wycheproof[^wycheproof] ML-KEM 测试向量进行了测试。

ACVP

您可以使用 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

Wycheproof

您可以使用 tests 脚本或直接使用 Wycheproof 客户端 运行 Wycheproof[^wycheproof] 测试：

# 使用 tests 脚本
./scripts/tests wycheproof

# 直接使用 Wycheproof 客户端
python3 ./test/wycheproof/wycheproof_client.py

基准测试

您可以使用 tests 脚本测量性能、内存使用和二进制大小：

# 速度基准测试（-c 选择周期计数器：NO、PMU、PERF 或 MAC）
# 注意：PERF/MAC 可能需要 -r 标志以使用 sudo 运行基准测试二进制文件
./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。

我可以使用自己的 FIPS-202 吗？

mlkem-native 依赖并附带一个 FIPS-202[^FIPS202] 实现。如果您的库有自己的 FIPS-202 实现，您可以使用它来代替 mlkem-native 附带的实现。请参阅 FIPS202.md，以及使用 tiny_sha3[^tiny_sha3] 的示例 examples/bring_your_own_fips202。

我需要使用汇编后端吗？

不需要。如果您想要纯 C 构建，只需在导入时省略目录 mlkem/src/native 和/或 mlkem/src/fips202/native，并在您的 mlkem_native_config.h 中取消设置 MLK_CONFIG_USE_NATIVE_BACKEND_ARITH 和/或 MLK_CONFIG_USE_NATIVE_BACKEND_FIPS202。

我需要设置 CBMC 才能使用 mlkem-native 吗？