💻 computer science

GCD: Garbled, Corrected, Demonstrandum -- Fixing and Proving Go's Extended GCD Implementation

本文识别并修复了 Go 语言扩展 GCD 实现中两个危及 RSA 密钥生成的关键偏差，随后利用 Gobra 和 Lean 验证工具证明了修正后代码的正确性与终止性，同时展示了 AI 智能体如何辅助完善形式化证明。

原作者： Linard Arquint

发布于 2026-06-05

📖 1 分钟阅读☕ 轻松阅读

原作者： Linard Arquint

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在建造一个高安全性的数字保险库（就像用于在线银行或加密消息的那些一样）。为了锁定和解锁这个保险库，你需要一个非常特定且复杂的数学密钥。在计算机科学的世界里，这个密钥是使用一种被称为扩展最大公约数 (Extended GCD) 算法的“配方”生成的。

这篇论文讲述了一组研究人员如何进入 Go 编程语言（一种用于构建软件的流行工具）的“厨房”，去检查这个密钥的配方是否被正确执行。他们发现这个配方被轻微篡改了，并在证明了新版本完美运行的同时修复了它。

以下是他们发现的过程，分为几个简单的部分：

1. “复制粘贴”错误

Go 的开发者想要更新他们的软件，以满足严格的政府安全标准。为此，他们从一个名为 BoringSSL（由 Google 使用的安全库）的可信知名来源中提取了一个配方，并将其“移植”（翻译）到了 Go 语言中。

你可以把这想象成一位著名的厨师给了你一个秘密蛋糕配方。你决定用自己的手写体重新书写这个配方，以便于阅读。论文声称，在重写过程中，Go 开发者不小心改变了两个重要的步骤。

问题所在： 原本的配方有一个严格的规则：“如果你把这两个数字相加，结果太大，你必须同时从两者中减去一个特定的数值。”这能保证蛋糕不会塌陷。
Bug（缺陷）： Go 版本对每个数字分别进行了这个“太大”的检查。这就像是分别检查面粉和糖一样。这破坏了保证密钥正确的数学平衡（“不变性”）。
令人惊讶的是： 三位不同的专家评审了这段代码，却都漏掉了这个错误。这个错误如此微妙，以至于它从人工审查的网中溜走了。

2. “过大”的原料

第二个问题是关于允许的原料大小。

规则： 原本的配方说：“第一个原料必须始终小于第二个原料。”
变化： Go 版本允许第一个原料比第二个更大。
修复方法： 研究人员并不需要为此修改代码。相反，他们需要更新“证明”（数学保证），以展示即使使用更大的原料，该配方依然有效。

3. 神奇的侦探 (Gobra)

为了证明他们修复了这些 Bug，研究人员使用了一个名为 Gobra 的工具。

类比： 想象一个超级严格、高度专注的机器人检查员。你把代码和一系列规则（规范）喂给它。这个机器人不仅仅是运行代码；它会模拟代码可能运行的每一种方式，检查每一条路径以确保它永远不会违反规则。
结果： 机器人确认，一旦修复了“同步 Bug”，代码就是

100% 正确的。事实上，由于修复程序移除了不必要的步骤，新代码的运行速度实际上比有 Bug 的版本快了 24%。

4. AI 助手

研究人员并不是独自完成所有繁重工作的。他们使用了一个 AI Agent（智能计算机程序）来提供帮助。

它是如何工作的： AI 扮演着勤奋学徒的角色。当机器人检查员（Gobra）说“这部分逻辑不通”时，AI 会建议修改规则或代码。
关键点： AI 最初假设代码是完美的，并试图强行让数学逻辑去适应代码。人类研究人员必须告诉 AI：“不，代码实际上是错的；请寻找其中的差异。”一旦 AI 理解了这一点，它就变得非常有帮助，能够提出修复方案并协助编写数学证明。

5. 总结

论文最后总结了三个主要教训：

即使是专家也会犯下微妙的错误： 三位人类评审员漏掉了一个关键 Bug，而一个形式化证明工具却发现了它。
形式化验证非常强大： 使用像 Gobra 这样的工具，就像拥有一个数学上的保证，证明你的代码确实有效，而不仅仅是希望它通过几次测试就能正常工作。
AI 是一个伟大的伙伴： AI 可以帮助人类编写这些复杂的证明，但人类仍然需要引导 AI 去质疑代码，而不是盲目接受它。

简而言之： 研究人员发现了 Go 标准库中一个隐藏的关键安全算法缺陷，修复了它，通过数学证明了修复方案的有效性，并展示了该修复实际上提高了软件的运行速度。他们结合了人类的洞察力、自动化证明工具以及 AI 的辅助完成了这项工作。

技术摘要：GCD：被扭曲、被修正、被证明 (Garbled, Corrected, Demonstrandum)

问题陈述

本文针对 Go 标准库（crypto/internal/fips140/bigmod）中扩展欧几里得算法（Extended GCD）实现的正确性与验证问题进行了研究。该实现对于 RSA 密钥对生成至关重要，而这是 TLS、SSH 和 PGP 等基础组件的核心组成部分。Go 的这一实现是在 Go 1.24 中引入的，旨在原生支持 FIPS 140-3 合规性，从而取代对 BoringSSL 的依赖。

作者发现了一个关键性的差异：尽管 Go 代码声称是 BoringSSL 实现（该实现已通过 Rocq 证明助手在 Fiat Cryptography 中进行了形式化验证）的直接移植版本，但 Go 版本包含了细微的偏差。这些偏差未被三次独立的代码审查所发现。这些偏差破坏了算法的数学不变性，可能危及 RSA 私钥生成所需的模逆计算的正确性。此外，Go 实现允许比经过证明的 BoringSSL 版本更大的输入定义域，这使得原有的证明假设失效。

方法论

作者采用了基于分离逻辑的 Go 验证器 Gobra，进行演绎程序验证。其方法论包括：

形式化规范： 作者将 Go 函数（extendedGCD、InverseVarTime、GCDVarTime）的自然语言规范转化为 Gobra 规范，包括前置条件、后置条件和循环不变性。
偏差分析： 通过尝试根据源自 BoringSSL 证明的规范来验证现有的 Go 代码，作者识别出两类主要的偏差：
- 不同步的减法： Go 实现根据局部条件独立地更新 Bézout 系数（ $A, B, C, D$ ），而参考实现则要求同步归约以维持循环不变性。
- 输入定义域扩张： Go 实现允许输入满足 $a \ge n$ ，这违反了原始证明所要求的 $a < n$ 前置条件。
证明构建：
- 代码修复： 作者提出了针对不同步减法的修复方案，以使 Go 逻辑与数学不变性保持一致。
- 证明适配： 他们将现有的 BoringSSL 证明从 Rocq 移植到 Gobra。针对输入定义域偏差，他们放宽了不变性和后置条件，以覆盖 $a \ge n$ 的情况，证明即使在特定情况下模逆属性不成立，GCD 值仍然保持正确。
- 混合验证： 对于 Z3 SMT 求解器（Gobra 使用）无法处理的非线性算术引理，作者使用 Lean 证明助手证明关键引理，并将其作为 trusted 引理导入 Gobra。
AI 辅助验证： 作者利用 AI 智能体（Anthropic 的 Claude Code）根据 Gobra 的错误信息迭代优化不变性和引理，显著减少了构建证明过程中的手动工作量。

核心贡献

缺陷发现： 本文揭示了 Go 扩展 GCD 实现中两个细微但关键的偏差，这些偏差破坏了算法不变性。这些缺陷存在于经过多次审查且声称是经过验证实现之直接移植的代码中。
性能优化： 针对不同步减法偏差提出的修复方案不仅恢复了正确性，还通过消除循环体中不必要的内存分配和冗余操作，实现了平均 24% 的加速（几何平均值）。
Go 加密算法的形式化验证： 作者成功使用 Gobra 验证了修复后的 Go 实现、其终止性以及针对形式化规范的正确性。这是 Go 标准库中该特定组件的首次形式化验证。
证明移植与泛化： 他们成功将证明从 Rocq (Fiat Cryptography) 移植到 Gobra，并将其泛化以覆盖 Go 实现所允许的更广泛输入定义域。
AI 在验证中的应用： 该工作展示了 AI 智能体在促进形式化验证方面的效能，即能够自主迭代规范并识别证明失败的根本原因（例如，建议独立系数归约是问题的症结所在）。

结果

正确性： 修复后的实现在标准笔记本电脑上用 16.9 秒 即可成功完成验证。验证涵盖了 extendedGCD 函数及其客户端 InverseVarTime 和 GCDVarTime。
性能： 在各种肢体大小（64 到 8192 位）下的基准测试显示，经过验证的实现始终比原始实现更快。平均加速比为 23.98%，根据输入规模的不同，提升幅度在 15.6% 到 36% 之间。加速归功于原地更新以及消除了中间缓冲区分配。
披露与影响： 作者向 Go 加密维护者披露了这些偏差。维护者确认，虽然这些偏差在理论上可能导致错误的模逆，但 RSA 密钥生成代码中的防御性检查会捕获这些错误并返回错误而非错误的密钥，从而将影响限制在可用性而非安全性破坏层面。修复方案目前正在评审中，以决定是否纳入 Go 标准库。
持续集成： 由于验证速度极快，该证明已集成到项目的持续集成 (CI) 工作流中，以自动检查未来的偏差。

意义与主张

论文声称其工作强调了三个主要洞察：

经过审查代码中的细微缺陷： 即便是经过充分审查的代码，特别是那些声称是经过验证实现的直接移植版本，也可能包含破坏不变性的细微 Bug。
形式化验证的力量： 形式化验证是发现此类测试和人工审查可能遗漏的缺陷的强大工具。
AI 智能体的角色： AI 智能体可以通过根据验证器反馈迭代优化不变性和引理，有效地促进验证过程，尽管最终的清理和结构理解仍需人工监督。

作者强调，他们的工作弥合了实现与证明之间的鸿沟。通过直接验证 Go 代码，而不是仅仅依赖于对另一个实现（BoringSSL）存在证明这一事实，他们确保了在生产环境中运行的具体代码在数学上是完备的。他们还指出，虽然他们在底层位运算上依赖 trusted 函数，但整体正确性论证被分解为小的、可审查的组件，从而提高了系统的可靠性。