论“高保证”密码学的承诺

关于“高保证”密码学的承诺

2026 年 2 月 5 日

软件密码学形式化验证

Cryspen 是一家将自己定位为提供“用于高保证软件的服务和软件，以便在你的关键系统中建立信任”的公司。他们的旗舰产品 libcrux 被宣传为一个“已经过形式化验证”的密码库，并提供“最高级别的保证”，这意味着可以安全使用且没有 bug。

在过去的 2 天里，我们在 Symbolic Software 向 Cryspen 的代码仓库提交了 4 个 pull request，以解决安全漏洞和实现缺陷。在此之前，2025 年末发生了一起事件，libcrux 在某些平台上产生了静默的错误密码学输出：Cryspen 静默地解决了这个 bug，没有任何公开披露，并且只是因为第三方主动提交了安全建议才收到了安全建议。

这一系列事件引发了对“高保证密码学”实际意义的反思，以及形式化验证社区是否已经养成了过度承诺和交付不足的习惯。

最初的事件：平台相关的密码学故障

2025 年 11 月，Filippo Valsorda 报告 说，libcrux-ml-dsa v0.0.3 根据执行环境产生不同的输出。与 Apple Silicon 上的 macOS 相比，在带有 Ampere Altra ARM64 硬件的 Alpine Linux 上，相同的种子输入生成了不同的公钥和签名。这不是错误处理中的边缘情况或性能衰退，而是核心密码学功能产生了不正确的结果。

该 bug 存在于 vxarq_u64 intrinsic 未经验证的 fallback 实现中。在缺少本机 SHA-3 指令支持的平台上，fallback 传递了不正确的参数，破坏了 SHA-3 摘要，并导致下游密码学操作静默失败。任何依赖此代码进行 ML-DSA 签名或 ML-KEM 密钥交换的系统都会遇到身份验证失败或密钥协商不匹配的情况，具体取决于哪个平台生成了密码学材料。

Cryspen 修复了这个 bug。但他们没有做的是发布任何公开披露、安全建议或承认他们的“形式化验证”库在生产环境中发布了一个导致静默密码学失败的缺陷。

掩盖

此漏洞的唯一安全建议不是由 Cryspen 发起的。而是由 Joe Birr-Pixton (ctz) 在 RustSec 建议数据库中提交的——这是第三方为 Rust 生态系统记录此漏洞的工作。在 Cryspen 提供了“refined wording”之后，该建议于 2025 年 12 月 4 日合并，该措辞强调该 bug 存在于“libcrux-intrinsics”中，而不是下游软件包中。

这种框架在技术上是准确的，但在实践中具有误导性。intrinsics crate 是 libcrux-ml-kem 和 libcrux-ml-dsa 的内部依赖项。这些库的用户经历了损坏的密码学操作。“intrinsic 层有一个 bug”和“密码库产生了错误的输出”之间的区别对 Cryspen 的营销叙事很重要，但对任何受到系统影响的人来说并不重要。

没有博客文章。没有安全公告。Cryspen 的任何沟通渠道上都没有任何公告。RustSec 建议（大多数开发人员除非主动运行 cargo audit，否则永远不会看到）代表了 Cryspen 对一个导致其形式化验证的密码库产生不正确输出的 bug 的完整披露姿态。

将其与其他密码库维护人员处理类似情况的方式进行比较。当 Kyber 参考实现于 2023 年底包含可变时间漏洞时，它成为了广泛公开讨论的主题、一个专门的跟踪网站（KyberSlash）以及受影响的下游实现的建议。当我们在自己的 Kyber-K2SO 实现中发现相同的漏洞时，我们在 24 小时内发布了公开安全公告；我们是最早这样做的公司之一。

Cryspen 的方法是修复 bug，避免任何公开承认，并等待其他人在一个晦涩的数据库中提交建议。

四个新发现

在 2026 年 2 月 3 日至 2 月 4 日期间，我们发现了 Cryspen 密码库中的另外四个问题。这些问题包括不符合规范、熵减少和潜在的 nonce 重用。

1. 缺少 X25519 全零验证 (hpke-rs)

Pull request #117 解决了 RFC 9180（HPKE 规范）要求的缺失验证。RFC 的 7.1.4 节规定，实现“必须检查 Diffie-Hellman 共享密钥是否为全零值，如果是，则中止”。

当给定某些低阶点（例如标识元素或小阶点）作为输入时，X25519 函数会产生全零输出。如果攻击者可以提供恶意公钥，他们可以强制共享密钥为零，从而使后续密钥派生具有确定性和可预测性。

此漏洞关系到规范中明确的要求，该实现声称遵循该规范。修复非常简单：DH 计算后进行一次比较。它的缺失表明要么没有仔细阅读规范，要么降低了对该要求的优先级。

2. 通过序列号溢出重用 Nonce (hpke-rs)

Pull request #118 解决了 HPKE 序列号管理中的缺陷。该库将序列号存储为 u32，其最大值约为 43 亿。RFC 9180 规定，对于标准 12 字节 nonce，必须针对 2^96 - 1 检查序列号。

原始代码中的溢出检查将 u32 与 u32 永远无法达到的值进行比较。在调试版本中，Rust 的溢出检查会在计数器回绕时导致 panic。在实际在生产环境中运行的发布版本中，计数器会静默地回绕为零，从而重用 nonce。

在身份验证加密中，nonce 重用是灾难性的。对于 AES-GCM，它可以恢复身份验证密钥和明文的 XOR。对于 ChaCha20-Poly1305，它可以直接通过 XOR 攻击恢复明文。任何使用相同的 HPKE 上下文加密超过 43 亿条消息的应用程序都容易受到攻击。

修复方法是一行代码：将 + 替换为 checked_add()。事实上，这还不是实现表明没有充分考虑密码学上下文中整数溢出的安全含义。

3. ECDSA 签名可延展性 (libcrux)

Pull request #1315 解决了 ECDSA P-256 实现中的签名可延展性。对于任何有效的 ECDSA 签名 (r, s)，都存在一个替代的有效签名 (r, n - s)，其中 n 是曲线阶数。如果没有 low-S 规范化（将 s 约束为最多 n/2），签名是可延展的：攻击者可以在不知道私钥的情况下生成替代的有效签名。

这在实践中很重要。Bitcoin 的 BIP 62 和 BIP 146 强制执行 low-S 规范化，因为签名可延展性可以更改交易标识符，从而可能导致盗窃和破坏交易链。更一般地说，任何使用签名进行重复数据删除、审计跟踪或缓存的系统都可能被可延展签名混淆。

libcrux 实现验证 r 和 s 是否为非零，但不将 s 与 n/2 进行比较或应用规范化。这是一个众所周知的要求，并且在过去十年中一直是 ECDSA 实现中的标准做法。

4. Ed25519 双重钳位 (libcrux)

Pull request #1316 解决了 Ed25519 密钥生成中不必要的熵减少问题。generate_key_pair 函数在哈希之前将标量钳位操作应用于原始种子：

根据 RFC 8032，钳位应在对种子进行 SHA-512 哈希处理后进行，而不是之前。对原始种子应用这些操作会删除 5 位熵（前一个字节中删除 3 位，最后一个字节中删除 2 位），从而将有效密钥空间从 256 位减少到 251 位。

虽然 251 位在计算上仍然可以防止暴力破解，但这种减少没有任何好处。无论输入模式如何，SHA-512 哈希都会产生均匀分布的输出；限制输入没有密码学目的。它只会减少熵，而不会提供任何补偿优势。

这不是一个微妙的问题。Ed25519 规范明确说明了何时进行钳位。不正确地实现它表明没有查阅规范或误解了其要求。

这告诉我们关于“高保证密码学”的什么？

形式化验证社区已经开发出一种用于营销的词汇，系统地夸大了验证实际完成的工作。当 Cryspen 声称他们的库“经过形式化验证”并且“没有 bug”时，他们正在发表与他们自己的 bug 历史相矛盾的声明。

2025 年 11 月的事件具有指导意义。该 bug 存在于 ARM SIMD intrinsic fallback 中——这恰恰是形式化验证工具无法推理的那种低级、特定于平台的代码。形式化验证在实践中意味着验证一个抽象模型，然后信任编译器、intrinsic、运行时和硬件都忠实地实现了该模型。

这不是用户理解的验证。它是验证 Rust 模型，外加希望 LLVM 生成正确的代码，外加希望 ARM 指令集按文档中的描述运行，外加希望每个 CPU 实现都没有勘误，外加希望操作系统、内存分配器和运行时环境没有引入任何可观察到的差异。

诚实的描述应该是：“我们已经使用 hax 工具链针对某些属性验证了我们 Rust 代码的一部分。已部署系统的实际安全性取决于你的编译器版本、目标架构、CPU 微码、操作系统以及我们无法验证的许多其他组件。” 但这卖不出去。它不会赢得资助。它不会吸引客户。

相反，我们得到“形式化验证”作为一个营销术语，一种声称优于依赖于广泛测试、模糊测试、跨平台验证和代码审查的库的方式——这些工程实践可能在平台相关的输出 bug 发布之前就已发现。

四个新发现加强了这种模式。它们都不涉及已验证代码和未验证代码之间的微妙交互。它们是直接的实现缺陷：

• 规范要求被忽略（X25519 零检查）。
• 整数类型对于其目的来说太小（序列号溢出）。
• 省略了规范化步骤（ECDSA low-S）。
• 在错误的时刻应用了钳位操作（Ed25519 双重钳位）。

这些不是形式化验证旨在发现的 bug。它们是仔细的代码审查、全面的测试和对规范的关注可以发现的 bug。它们表明开发过程优先考虑可验证的核心，而不是围绕它的工程基础。

验证剧场问题

形式化方法社区中存在一种模式，可以称为“验证剧场”：以一种营造严谨的外观但没有提供其实质的方式部署形式化方法。

一个“经过形式化验证”但发布时具有平台相关的不正确输出的密码库没有实现高保证。它实现了一个经过验证的核心，周围环绕着一个未验证的外围，这个外围可能会以使验证毫无意义的方式失败。

一家修复关键 bug 而不披露的公司没有表现出值得信赖。它表明营销问题的重要性超过了透明度义务。

一个缺乏基本规范合规性的代码库（检查全零 DH 输出、防止整数溢出、规范化签名）并不是以“最高级别保证”所暗示的谨慎方式开发的。

形式化验证社区需要开发更诚实的沟通方式。验证是有价值的。它可以发现测试无法发现的某些类别的 bug。但它不能替代工程纪律，声称相反会破坏形式化方法的信誉以及信任这些声明的用户的安全性。

当一个形式化验证的密码库为其核心原语产生平台相关的不正确输出，并且该库的维护人员掩盖了披露，同时继续将该库作为“没有 bug”进行销售时，我们必须问：没有哪些 bug？针对哪些属性进行了验证？以及值得谁信任？

在 Cryspen 的案例中，答案似乎是：不是重要的 bug，不是用户关心的属性，也不是任何密切关注的人。

想要一起工作吗？

选择 Symbolic Software 作为你值得信赖的合作伙伴，以增强数字生态系统中的安全性和促进完整性。

开始一个项目

• 原文链接： symbolic.software/blog/2...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～