pq-code-package/mlkem-native

# mlkem-native       [](https://www.apache.org/licenses/LICENSE-2.0) [](https://opensource.org/licenses/ISC) [](https://opensource.org/licenses/MIT) mlkem-native 是 ML-KEM[^FIPS203] 的一个安全、快速且可移植的 C90[^C90] 实现。 它是 ML-KEM 参考实现[^REF] 的一个分支。 [mlkem/src/*](mlkem) 和 [mlkem/src/fips202/*](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）的原生后端。有关性能数据，请参见 [基准测试](https://pq-code-package.github.io/mlkem-native/dev/bench/)。 mlkem-native 由 [Linux Foundation](https://linuxfoundation.org/) 旗下的 [Post-Quantum Cryptography Alliance](https://pqca.org/) 提供支持。 ## 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 # 构建并运行 tests make build make test # 使用 `tests`（`make` 的便捷封装）执行相同操作 ./scripts/tests all # 显示所有选项 ./scripts/tests --help ``` 更多信息请参见 [BUILDING.md](BUILDING.md)。 ## 应用 mlkem-native 被用于 - Open Quantum Safe 项目的 [libOQS](https://github.com/open-quantum-safe/liboqs/)，自 [0.13.0](https://github.com/open-quantum-safe/liboqs/releases/tag/0.13.0) 版本起（作为默认的 ML-KEM 实现） - AWS 的加密库 [AWS-LC](https://github.com/aws/aws-lc/)，自 [v1.50.0](https://github.com/aws/aws-lc/releases/tag/v1.50.0) 版本起 - Rust 编写的 TLS 库 [rustls](https://github.com/rustls/rustls)，自 [0.23.28](https://github.com/rustls/rustls/releases/tag/v%2F0.23.28) 版本起（通过 AWS-LC 作为默认加密提供者） - [zeroRISC's fork of OpenTitan](https://github.com/zerorisc/expo) —— 一个开源的硅信任根 ## 形式化验证 [mlkem/src/*](mlkem) 和 [mlkem/src/fips202/*](mlkem/src/fips202) 中的所有 C 代码均已证明是内存安全（无内存溢出）和类型安全（无整数溢出）的。 这使用了 [C Bounded Model Checker (CBMC)](https://github.com/diffblue/cbmc)，并基于源代码中的函数契约和循环不变量注解。详情请参见 [proofs/cbmc](proofs/cbmc)。 所有 AArch64 和 x86_64 汇编代码均在目标代码级别被证明是功能正确、内存安全的，并且具有秘密无关的时间特性（常量时间）。这使用了 [HOL-Light](https://github.com/jrh13/hol-light) 交互式定理证明器和 [s2n-bignum](https://github.com/awslabs/s2n-bignum/) 验证基础设施（其中包含 Arm 和 x86 架构相关部分的模型）。详情请参见 [proofs/hol_light](proofs/hol_light)。 **注意：** 形式化验证绝非绝对。关于 mlkem-native 形式化验证工作的范围、假设和风险的详细分析，请参见 [SOUNDNESS.md](SOUNDNESS.md)。 ## 安全性 mlkem-native 中的所有 AArch64 和 x86_64 汇编代码均在 [HOL Light](https://github.com/jrh13/hol-light) 中经过形式化证明，确信不存在依赖于秘密的控制流、内存访问模式和可变延迟指令，从而阻止了大多数时序侧信道攻击（详情请参见 [proofs/hol_light](proofs/hol_light)）。C 代码通过适当的屏障和常量时间模式，进行了加固以防止编译器引入的时序侧信道（例如 KyberSlash[^KyberSlash] 或 clangover[^clangover]）。 此外，还使用 `valgrind` 在各种编译器和编译选项组合下，测试了是否存在依赖于秘密的分支、内存访问模式和可变延迟指令。 ## 设计 mlkem-native 分为一个_前端_和两个用于算术与 FIPS202 / SHA3 的_后端_。前端是固定的，用 C 编写，涵盖所有对性能不敏感的例程。后端是灵活的，负责处理对性能敏感的例程，可以用 C 或原生代码（汇编/内建函数）实现；请参见 [mlkem/src/native/api.h](mlkem/src/native/api.h) 了解算术后端，以及 [mlkem/src/fips202/native/api.h](mlkem/src/fips202/native/api.h) 了解 FIPS-202 后端。 mlkem-native 目前提供以下后端： * 默认的可移植 C 后端 * 64位 Arm 后端（使用 Neon） * 64位 Intel/AMD 后端（使用 AVX2） * 64位 RISC-V 后端（使用 RVV） * 32位 Armv8.1-M 后端（使用 Helium/MVE）—— 参见 [#1501](https://github.com/pq-code-package/mlkem-native/issues/1501)。这仍处于实验阶段，默认禁用。 如果您想贡献新的后端，请联系我们或直接提交 PR。 我们的 AArch64 汇编代码是使用 [SLOTHY](https://github.com/slothy-optimizer/slothy) 超级优化器开发的，遵循 SLOTHY 论文[^SLOTHY_Paper] 中描述的方法： 我们手写“整洁”的汇编代码，并自动化微优化（例如，比较 AArch64 NTT 的 [整洁版](dev/aarch64_clean/src/ntt.S) 与 [优化版](dev/aarch64_opt/src/ntt.S)）。 更多详情请参见 [dev/README.md](dev/README.md)。 ## 测试向量 mlkem-native 已针对所有官方 ACVP ML-KEM 测试向量[^ACVP] 和 Wycheproof[^wycheproof] ML-KEM 测试向量进行了测试。 ### ACVP 您可以使用 [`tests`](./scripts/tests) 脚本或直接使用 [ACVP 客户端](./test/acvp/acvp_client.py) 运行 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`](./scripts/tests) 脚本或直接使用 [Wycheproof 客户端](./test/wycheproof/wycheproof_client.py) 运行 Wycheproof[^wycheproof] 测试： ``` # 使用 tests 脚本 ./scripts/tests wycheproof # 直接使用 Wycheproof 客户端 python3 ./test/wycheproof/wycheproof_client.py ``` ## 基准测试 您可以使用 [`tests`](./scripts/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 基准测试结果和历史性能数据，请参见 [基准测试页面](https://pq-code-package.github.io/mlkem-native/dev/bench/)。 ## 用法 如果您想使用 mlkem-native，请将 [mlkem](mlkem) 导入到您项目的源码树中，并使用您喜欢的构建系统进行构建。更多信息请参见 [mlkem](mlkem)，简单示例请参见 [examples/basic](examples/basic)。本仓库中提供的构建系统仅用于开发目的。 ### 我可以自带 FIPS-202 吗？ mlkem-native 依赖并附带了一个 FIPS-202[^FIPS202] 的实现。如果您的库有自己的 FIPS-202 实现，您可以代替 mlkem-native 附带的版本使用它。请参见 [FIPS202.md](FIPS202.md)，以及使用 tiny_sha3[^tiny_sha3] 的示例 [examples/bring_your_own_fips202](examples/bring_your_own_fips202)。 ### 我需要使用汇编后端吗？ 不需要。如果您想要纯 C 构建，只需在导入时省略 [mlkem/src/native](mlkem/src/native) 和/或 [mlkem/src/fips202/native](mlkem/src/fips202/native) 目录，并在您的 [mlkem_native_config.h](mlkem/mlkem_native_config.h) 中取消设置 `MLK_CONFIG_USE_NATIVE_BACKEND_ARITH` 和/或 `MLK_CONFIG_USE_NATIVE_BACKEND_FIPS202`。 ### 我需要设置 CBMC 才能使用 mlkem-native 吗？ 不需要。虽然我们建议您考虑使用它，但在没有 CBMC 的情况下，mlkem-native 也能正常构建和运行——只需确保包含 [cbmc.h](mlkem/src/cbmc.h) 并保持 `CBMC` 未定义。特别是，您_不需要_从代码中移除所有的函数契约和循环不变量；除非设置了 `CBMC`，否则它们将被忽略。 ### mlkem-native 支持 ML-KEM 的所有安全级别吗？ 是的。安全级别是一个编译时参数，通过在 [mlkem_native_config.h](mlkem/mlkem_native_config.h) 中设置 `MLK_CONFIG_PARAMETER_SET=512/768/1024` 来配置。如果您的库/应用程序需要多个安全级别，您可以构建并链接 mlkem-native 的三个实例，同时共享公共代码；这被称为“多级别构建”，并在 [examples/multilevel_build](examples/multilevel_build) 中进行了演示。另请参见 [mlkem](mlkem)。 ### 我可以自带后端吗？ 可以，您可以为 ML-KEM 原生算术和/或 FIPS-202 添加更多后端。请以现有后端为模板，或参阅 [examples/custom_backend](examples/custom_backend) 获取有关如何注册自定义后端的最小示例。 ## 有疑问？ 如果您认为在 mlkem-native 中发现了安全漏洞，请通过 Github 的 [私人漏洞报告](https://github.com/pq-code-package/mlkem-native/security) 进行报告。请**不要**创建公开的 GitHub issue。 如果您有任何其他问题 / 非安全问题 / 功能请求，请开启一个 GitHub issue。 ## 贡献 如果您想帮助我们构建 mlkem-native，请联系我们。您可以通过 [PQCA Discord](https://discord.com/invite/xyVnwzfg5R) 联系 mlkem-native 团队。另请参见 [CONTRIBUTING.md](CONTRIBUTING.md)。 [^C90]: 严格来说，我们依赖 C90 + `stdint.h` + 64位 `unsigned long long`。 [^ACVP]: National Institute of Standards and Technology: Automated Cryptographic Validation Protocol (ACVP) Server, [https://github.com/usnistgov/ACVP-Server](https://github.com/usnistgov/ACVP-Server) [^CBMC]: Diffblue, Amazon Web Services: C Bounded Model Checker, [https://github.com/diffblue/cbmc](https://github.com/diffblue/cbmc) [^FIPS202]: National Institute of Standards and Technology: FIPS202 SHA-3 Standard: Permutation-Based Hash and Extendable-Output Functions, [https://csrc.nist.gov/pubs/fips/202/final](https://csrc.nist.gov/pubs/fips/202/final) [^FIPS203]: National Institute of Standards and Technology: FIPS 203 Module-Lattice-Based Key-Encapsulation Mechanism Standard, [https://csrc.nist.gov/pubs/fips/203/final](https://csrc.nist.gov/pubs/fips/203/final) [^HOL-Light]: John Harrison: HOL-Light Theorem Prover, [https://hol-light.github.io/](https://hol-light.github.io/) [^HYBRID]: Becker, Kannwischer: Hybrid scalar/vector implementations of Keccak and SPHINCS+ on AArch64, [https://eprint.iacr.org/2022/1243](https://eprint.iacr.org/2022/1243) [^KyberSlash]: Bernstein, Bhargavan, Bhasin, Chattopadhyay, Chia, Kannwischer, Kiefer, Paiva, Ravi, Tamvada: KyberSlash: Exploiting secret-dependent division timings in Kyber implementations, [https://kyberslash.cr.yp.to/papers.html](https://kyberslash.cr.yp.to/papers.html) [^REF]: Bos, Ducas, Kiltz, Lepoint, Lyubashevsky, Schanck, Schwabe, Seiler, Stehlé: CRYSTALS-Kyber C reference implementation, [https://github.com/pq-crystals/kyber/tree/main/ref](https://github.com/pq-crystals/kyber/tree/main/ref) [^SLOTHY_Paper]: Abdulrahman, Becker, Kannwischer, Klein: Fast and Clean: Auditable high-performance assembly via constraint solving, [https://eprint.iacr.org/2022/1303](https://eprint.iacr.org/2022/1303) [^clangover]: Antoon Purnal: clangover, [https://github.com/antoonpurnal/clangover](https://github.com/antoonpurnal/clangover) [^tiny_sha3]: Markku-Juhani O. Saarinen: tiny_sha3, [https://github.com/mjosaarinen/tiny_sha3](https://github.com/mjosaarinen/tiny_sha3) [^wycheproof]: Community Cryptography Specification Project: Project Wycheproof, [https://github.com/C2SP/wycheproofhttps://github.com/C2SP/wycheproof)

标签：AArch64, ARM Neon, AVX2, C90, CBMC, FIPS 203, HOL-Light, KEM, Kyber, Linux Foundation, ML-KEM, PQC, PQCA, RISC-V, RVV, x86_64, 内存安全, 后量子密码学, 安全报告生成, 密码学库, 密钥封装机制, 嵌入式安全, 常量时间, 形式化验证, 格密码学, 网络安全, 逆向工具, 隐私保护, 高性能计算