2022 年 11 月事件：在 Python 的 GitHub 仓库中打开问题 99108，主张在 SHA3 实现中出现最近的 CVE 后，Python 应在其所有与哈希相关的基础设施中采用经过验证的代码。截至上周，该问题已关闭，Python 默认暴露的每个哈希和 HMAC 算法现在都由经过验证的加密库HACL*提供，功能无损失，过渡对 Python 用户完全透明，Python 现在从 HACL 引入 15,000 行经过验证的 C 代码，从上游 HACL 仓库拉取新版本是完全自动化的。

• 2.5 年工作成果：这是 2.5 年工作的成果，离不开Aymeric Fromherz的宝贵帮助，Son Ho早期有关键贡献，Python 方面 Gregory P. Smith、Bénédikt Tran 和后来的 Chris Eibl 也提供了很多帮助，HACS 系列研讨会创建了联系并提供了足够的动力。

幕后细节：

• 流 API 入门：许多加密算法是块算法，而流 API 更用户友好，能处理任意长度输入，但流 API 很难，因为要处理长期状态和复杂不变量，SHA3 的参考实现曾出现 CVE，流 API 也因底层块算法的差异而复杂，所以是验证的好候选，2021 年有相关研究论文。
• 完全通用的验证：论文的主要想法是用依赖类型捕获块算法是什么，然后对块算法的抽象定义编写和验证通用流构造，就像在 C++中实例化模板一样，将通用流构造应用于具体块 API 就得到该块算法的流 API，但实际与论文中的有差异，要考虑多种情况的通用性，如最终摘要长度、预输入、缓冲区管理等，最终对 HMAC 无需进一步调整。
• 无懈可击的构建：向 Python 提交 PR 的一个亮点是其基础设施的 CI 覆盖范围广，但也发现了一些棘手的角落情况，如处理 HMAC 时，在不同编译器下的编译问题，需要用“C 抽象结构”模式进行大量重构，因为从 F*到 C 的编译器 krml 要进行更精细的分析。
• 处理内存分配失败：F*中对 C 的原始建模允许对内存分配失败进行推理，但实际中没人这样做，对于 Python 要能传播内存分配失败，需要细化通用可变状态、块算法和通用流构造的定义，在源文件中插入option类型，在生成的 C 中编译为标记联合，也可以改变状态定义以包含has_failed运行时函数，但会增加复杂性和验证工作。
• 向上游 HACL传播更改到 Python：最初的 Python PR 包含一个 shell 脚本用于从上游 HACL仓库获取所需文件等操作，后来上游代码可维护且稳定，就删除了这些操作，现在任何人都可以在 Python 检查中运行 shell 脚本并整合最新改进。