Jonathan Protzenko Microsoft Research, Seattle.jonathan.protzenko@ens-lyon.org BlogPublicationsResearchServiceSoftwareTalksTeaching

• protz
• protz

15000行经过验证的密码学代码现在进入 Python

2025年4月18日

在2022年11月，我在 Python 的 GitHub 仓库上提出了 issue 99108，认为在 SHA3 实现中出现了一个新的 CVE 之后，Python 应该在其所有与哈希相关的基础设施中采用经过验证的代码。

截至上周，这个问题已经关闭，并且 Python 默认公开的每一个哈希和 HMAC 算法现在都由经过验证的密码学库 HACL* 提供。功能上没有任何损失，并且这种转变对于 Python 用户来说是完全透明的。Python 现在 vendors（包含在其仓库中）来自 HACL* 的 15000 行经过验证的 C 代码。从上游 HACL* 仓库拉取新版本是完全自动化的，只需调用一个脚本即可完成。HACL* 能够成功地实现新功能，以满足 Python 的所有要求，例如：Blake2 算法系列的附加模式，覆盖所有 Keccak 变体的 SHA3 的新 API，用于处理构建系统难题的严格抽象模式，正确的错误管理（特别是，分配失败），以及用 HMAC 算法实例化 HACL 的通用“流式”功能，包括需要同时保持两个哈希状态的优化。

这是两年半工作的结晶，如果没有 Aymeric Fromherz 的宝贵帮助，这是不可能实现的，他承担了大量的实现负担。Son Ho 在早期做出了关键贡献，推广了 HACL 的“流式”功能，使其能够处理需要“预输入”的块算法。这种略微晦涩的推广实际上对于实现合适的、优化的 HMAC 至关重要，该 HMAC 在底层保持两个哈希状态。在 Python 方面，Gregory P. Smith、Bénédikt Tran 以及后来的 Chris Eibl 是重要的支持者并提供了很多帮助。最后，HACS 系列研讨会建立了联系（你好，Paul Kehrer！），并提供了足够的动力来实现这一目标。非常感谢 Python 和经过验证的密码学社区！

正如我经常喜欢做的那样，我将提供一些幕后花絮，并评论一些对于研究论文来说过于低级的更有趣的技术方面。

流式 API 入门

许多密码学算法是_块_算法，这意味着它们假定其输入是逐块提供的，并且对第一个和最后一个块进行特殊处理。众所周知的块算法包括哈希算法、MAC 算法（例如，Poly1305、HMAC）等等。实际上，块 API 并不易于使用：很少有人已经将数据分块；此外，计算结果（例如，哈希）会使块算法的状态无效，这使得例如计算 TLS 记录的中间哈希变得困难。

由于这些原因，密码学库通常公开_流式_ API，这意味着客户端可以提供任何长度的输入；然后，库负责缓冲输入，并在获得完整块后立即刷新缓冲区。流式 API 通常还允许提取中间哈希而不会使状态无效。

流式 API 很难，因为它们使用具有复杂不变性的长期存在的状态：SHA3 的（未经验证的）参考实现受到了 2022 年 一个糟糕的 CVE 的影响，Python “继承”了该漏洞，因为它 vendor 了完全相同的 SHA3 实现。

流式 API 也很难，因为底层块算法在无数不同的方面有所不同：所有哈希算法都接受一个空的最终块，除了 Blake2 之外；有些需要在运行时保留密钥 (Poly1305)，有些可以在初始化后丢弃它 (HMAC, optimized)；有些在处理密钥之前需要一些初始输入 (Blake2)，有些则不需要；等等。

鉴于这种固有的复杂性，流式算法是验证的良好候选者：我们在 2021 年撰写了一篇关于这个问题的 研究论文。

完全通用的验证

该论文的主要思想是，可以使用依赖类型来捕获块算法_是什么_。一旦完成，只需一次性地创作和验证通用的流式构造，并在块算法的抽象定义上进行创作和验证。然后，就像在 C++ 中实例化模板一样，将通用的流式构造应用于具体的块 API，然后就可以了——该块算法的流式 API，“免费”。

第一个障碍是，我们在论文（Listing 12）中提出的内容与 实际存在于存储库中的内容 之间存在相当大的差异。具体来说，捕获_任何_块算法都需要大量的通用性。

• 用户可以指定也可以不指定最终摘要的长度——例如，每个 SHA3 哈希都有一个固定的输出长度，但 Shake 变体产生的结果的长度由用户提供。
• 块算法可能希望在数据块之前接收预输入。例如，对于 SHA2，预输入为空，但对于密钥哈希模式下的 Blake2，预输入是密钥块。
• 无法急切地处理块，因为某些算法 (Blake2) 不允许最终块为空——这大大复杂了缓冲区管理，并与预输入相互作用。
• 某些算法需要保留额外的状态：例如，Blake2 的密钥长度可以在初始化时进行调整，但需要保留在长期存在的状态中。
• 为了避免在中间摘要提取时使块状态无效，我们的流式 API 在底层复制状态——在某些情况下，更容易堆栈分配此副本，但在其他情况下，堆分配副本更有意义。
• 在某些情况下，我们希望每个算法都有一个 API（我们有四个用于 SHA2-{224,256,384,512} 的 API）；在其他情况下，我们希望每个算法族有一个 API（我们有一个涵盖所有 6 个 Keccak 算法的 API：SHA3 的 4 个变体和 Shake 的 2 个变体）。

达到这种通用性水平需要多轮迭代，这由 Python 的连续需求驱动。最终，对于 HMAC（我们最终在 Python 中实现的算法），我们意识到我们的证明和定义足够通用，我们不需要对“实例化”我们的通用流式 API 进行任何进一步的调整。

防弹构建

向 Python 提交 PR 的一个亮点是，他们的基础设施具有比我们可能梦想的更多的 CI 覆盖率：Python 的完整构建在 50 多个工具链和架构上运行。不利的一面？我们发现了一些非常烦人的极端情况。

在处理 HMAC 时，出现了一个特别棘手的构建问题。提醒一下，HMAC 是一种通用构造，给定一个哈希算法，它提供一个密钥消息身份验证代码——简而言之，有一个高级 HMAC 代码片段，它将大部分工作推迟到各个哈希算法。每个哈希算法本身可能具有多种_实现_：例如，HMAC-Blake2b 由 HMAC-Blake2b-32（常规实现）和 HMAC-Blake2b-256 (AVX2 宽向量实现) 实现。

这已经导致了一些问题：如果 Python 在具有 AVX2 的机器上运行，HMAC.c 可能会调用 Blake2b_256.c 中的函数。但是，只有 Blake2b_256.c 可以使用 -mavx2 进行编译：来自 HMAC.c 的代码将在所有机器上执行，即使是那些没有 AVX2 的机器，这意味着它_不能_使用 -mavx2 进行编译。到目前为止，一切顺利，这是我们以前做过的事情。

问题在于 HMAC.c 为 Blake2b_256.c 创建初始状态：

#include <immintrin.h>
// ...
 __m256i *blake2b_256_state = aligned_malloc(sizeof(__m256i)*4);
// ...

大多数工具链都对这段代码感到满意——immintrin.h 定义了类型 __m256i，即使 HMAC.c 不能假定 AVX2 指令可用，编译器也不难在不使用 AVX2 指令的情况下将 blake2b_256_state 零初始化……除了，一些较旧的编译器拒绝处理 immintrin.h 标头，除非使用了 -mavx2，这破坏了整个目的。

这需要大量的重构才能使用众所周知的“C 抽象结构”模式，该模式本质上是在 C 中定义一个抽象类型。

// Blake2b_256.h
typedef struct blake2b_256_st_s blake2b_256_st;
blake2b_256_st *blake2b_256_malloc();
// Blake2b_256.c
#include <immintrin.h>typedef struct blake2b_256_st_s {
  __m256i contents[4];
} blake2b_256_st;
// HMAC.c
blake2b_256_st *blake2b_256_state = blake2b_256_malloc();

使这变得格外困难的是，C 代码是从 F* 自动生成的，F* 对抽象的概念_非常_不同。从 F* 到 C 的编译器 krml 必须进行大修，以执行更细粒度的分析，即使在存在此类“抽象结构”的情况下，也能处理各种可见性级别（公共函数、库内部函数、翻译单元内部函数）。

处理内存分配失败

虽然我们最初在 F* 中对 C 的建模允许推理内存分配失败，但实际上没有人费心这样做。对于 Python，最好能够传播内存分配失败。这意味着我们必须改进我们对通用、可变状态（例如块状态）的定义；我们对块算法（例如 SHA2-256）的定义；以及我们通用的流式构造，以便都能够将内存分配失败一直传播到调用者。值得庆幸的是，这并没有变成一件大事：我们沿途插入了 option 类型，并且因为我们有一个通用的流式构造，所以实现和证明只需要为流式 API 的 15 多个具体实例更新一次。

源代码中 option 类型的存在会编译为生成的 C 中的标记联合；这有点冗长，我们可能会更改我们对状态的定义，以包含一个 has_failed 运行时函数，该函数可以评估内存分配是否失败，但代价是更多的复杂性和验证工作。

将更改从上游 HACL* 传播到 Python

我的初始 Python PR 包含一个 shell 脚本，该脚本将从上游 HACL* 存储库中获取所需的文件；通过精心设计的 sed 调用在标头中删除一堆多余的定义；并就地调整一些包含路径，也使用我最喜欢的重构工具（是的，sed）。好处是，初始 PR 简洁明了。

后来，一旦清楚上游代码是可维护的并且非常稳定，那一堆 sed 就被消除了，理由是如果标头包含一些额外的定义，这不是世界末日，并且所有这些都使维护更容易。

现在，任何希望刷新 HACL* 的人都可以运行 Python 结帐中的 shell 脚本，并提供他们调整 Python 的 SBOM（软件物料清单）中预期的哈希，他们就可以开始了，并且可以集成最新的改进。

结论

我很高兴看到在一个像 Python 这样的旗舰项目中如此大规模地集成经过验证的密码学代码。这表明经过验证的密码学不仅从学术角度来看是准备就绪的，而且还足够成熟，可以集成到实际软件中，同时满足所有工程期望。感谢一路上帮助过的所有人！