mlkem-native 是 ML-KEM1 的一个安全、快速且可移植的 C902 实现。它是 ML-KEM 参考实现3 的一个分支。
mlkem/src/* 和 mlkem/src/fips202/* 中的所有 C 代码均已通过 CBMC4 证明为内存安全(无内存溢出)和类型安全(无整数溢出)。所有 AArch64 和 x86_64 汇编均已使用 HOL-Light5 证明其功能正确、内存安全且具有与秘密无关的时序(常数时间)。
mlkem-native 包含针对 Arm(64 位,Neon)、Intel/AMD(64 位,AVX2)、RISC-V(64 位,RVV)和 POWER(ppc64le,VSX)的原生后端。有关性能数据,请参阅基准测试。
mlkem-native 得到了后量子密码联盟的支持,该联盟隶属于Linux 基金会。
# 安装基础软件包
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 被用于以下项目:
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 代码通过适当的屏障和常数时间模式,针对编译器引入的时序侧信道(如 KyberSlash6 或 clangover7)进行了加固。
不存在依赖于秘密的分支、内存访问模式和可变延迟指令这一点也通过 valgrind 结合各种编译器及编译选项组合进行了测试。
其他攻击。 mlkem-native 仅以抵抗时序侧信道为目标。其他攻击类别,如功耗和电磁侧信道、微架构侧信道(例如推测执行)或故障注入攻击,目前不在范围内。
mlkem-native 分为一个_前端_和两个用于算术及 FIPS202 / SHA3 的_后端_。前端是固定的,用 C 编写,涵盖所有对性能不关键的例程。后端是灵活的,负责对性能敏感的例程,可以用 C 或原生代码(汇编/内联函数)实现;有关算术后端,请参阅 mlkem/src/native/api.h,有关 FIPS-202 后端,请参阅 mlkem/src/fips202/native/api.h。
mlkem-native 目前提供以下后端:
如果您想贡献新的后端,请与我们联系或直接提交 PR。
我们的 AArch64 汇编是使用 SLOTHY 超级优化器开发的,遵循 SLOTHY 论文8 中描述的方法:我们手工编写“干净”的汇编,并自动化微优化(例如,参见 clean 与 optimized AArch64 NTT 的对比)。更多详情请参阅 dev/README.md。
mlkem-native 针对所有官方 ACVP ML-KEM 测试向量9 和 Wycheproof10 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 客户端 运行 Wycheproof10 测试:
# 使用 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。
mlkem-native 依赖并附带一个 FIPS-20211 实现。如果您的库有自己的 FIPS-202 实现,您可以使用它来代替 mlkem-native 附带的实现。请参阅 FIPS202.md,以及使用 tiny_sha312 的示例 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。
不需要。虽然我们建议您考虑使用它,但 mlkem-native 在没有 CBMC 的情况下也能正常构建和运行——只需确保包含 cbmc.h 并保持 CBMC 未定义即可。特别是,您_不_需要从代码中删除所有函数契约和循环不变式;除非设置了 CBMC,否则它们将被忽略。
支持。安全级别是一个编译时参数,通过在 mlkem_native_config.h 中设置 MLK_CONFIG_PARAMETER_SET=512/768/1024 来配置。如果您的库/应用程序需要多个安全级别,您可以构建并链接三个 mlkem-native 实例,同时共享公共代码;这称为“多级别构建”,在 examples/multilevel_build 中进行了演示。另请参阅 mlkem。
可以,您可以为 ML-KEM 原生算术和/或 FIPS-202 添加更多后端。以现有后端为模板,或参阅 examples/custom_backend 了解如何注册自定义后端的最小示例。
如果您认为您在 mlkem-native 中发现了安全漏洞,请通过 Github 的私有漏洞报告报告该漏洞。请不要创建公开的 GitHub issue。
如果您有任何其他问题/与安全无关的问题/功能请求,请打开一个 GitHub issue。
如果您想帮助我们构建 mlkem-native,请与我们联系。您可以通过 PQCA Discord 联系 mlkem-native 团队。另请参阅 CONTRIBUTING.md。
美国国家标准与技术研究院:FIPS 203 基于模块格的密钥封装机制标准,https://csrc.nist.gov/pubs/fips/203/final ↩
严格来说,我们依赖 C90 + stdint.h + 64 位 unsigned long long。 ↩
Bos、Ducas、Kiltz、Lepoint、Lyubashevsky、Schanck、Schwabe、Seiler、Stehlé:CRYSTALS-Kyber C 参考实现,https://github.com/pq-crystals/kyber/tree/main/ref ↩
Diffblue、Amazon Web Services:C 有界模型检查器,https://github.com/diffblue/cbmc ↩
John Harrison:HOL-Light 定理证明器,https://hol-light.github.io/ ↩
Bernstein、Bhargavan、Bhasin、Chattopadhyay、Chia、Kannwischer、Kiefer、Paiva、Ravi、Tamvada:KyberSlash:利用 Kyber 实现中依赖秘密的除法时序,https://kyberslash.cr.yp.to/papers.html ↩
Antoon Purnal:clangover,https://github.com/antoonpurnal/clangover ↩
https://raw.githubusercontent.com/pq-code-package/mlkem-native/HEAD/Abdulrahman%E3%80%81Becker%E3%80%81Kannwischer%E3%80%81Klein%EF%BC%9A%E5%BF%AB%E9%80%9F%E4%B8%94%E5%B9%B2%E5%87%80%EF%BC%9A%E9%80%9A%E8%BF%87%E7%BA%A6%E6%9D%9F%E6%B1%82%E8%A7%A3%E5%AE%9E%E7%8E%B0%E5%8F%AF%E5%AE%A1%E8%AE%A1%E7%9A%84%E9%AB%98%E6%80%A7%E8%83%BD%E6%B1%87%E7%BC%96%EF%BC%8C%5Bhttps:/eprint.iacr.org/2022/1303%5D(https:/eprint.iacr.org/2022/1303) ↩
美国国家标准与技术研究院:自动化密码验证协议 (ACVP) 服务器,https://github.com/usnistgov/ACVP-Server ↩
社区密码学规范项目:Project Wycheproof,https://github.com/C2SP/wycheproof ↩ ↩2
美国国家标准与技术研究院:FIPS202 SHA-3 标准:基于置换的哈希和可扩展输出函数,https://csrc.nist.gov/pubs/fips/202/final ↩
Markku-Juhani O. Saarinen:tiny_sha3,https://github.com/mjosaarinen/tiny_sha3 ↩