We verify the 'extendedGCD' implementation in Go's standard library ('crypto/internal/fips140/bigmod'), which plays a crucial role in the generation of RSA key pairs. Even though the Go implementation is supposedly a direct port from BoringSSL's implementation, we uncovered two deviations that each break the algorithm's invariants: (1) the Go implementation deviates in the way coefficients are updated, and (2) it permits a larger input domain. We address both deviations; the first by fixing the Go implementation, which results in an on average 24% speedup, and the second deviation by porting an existing proof for BoringSSL and extending it to cover the larger input domain. We prove correctness and termination of the fixed Go implementation using Gobra, a deductive program verifier for Go. Where necessary, we used Lean to prove key lemmata on non-linear arithmetic, which we import into Gobra. Our verification effort reveals three key insights: subtle bugs can slip into even well-reviewed code with surprising ease; formal verification is a powerful tool for uncovering them; and AI agents can facilitate the verification process by iteratively refining invariants and lemmata based on Gobra's error messages.

翻译：我们验证了Go语言标准库（crypto/internal/fips140/bigmod）中'extendedGCD'的实现，该实现对于RSA密钥对生成起着关键作用。尽管Go实现据称是BoringSSL实现的直接移植，但我们发现了两处偏离，每处都破坏了算法的不变量：（1）Go实现在系数更新方式上存在偏差；（2）它允许更大的输入域。我们解决了这两处偏离：第一处通过修正Go实现，平均提速24%；第二处通过移植BoringSSL的现有证明并扩展以覆盖更大的输入域。我们使用Go语言演绎验证工具Gobra证明了修正后Go实现的正确性与终止性。必要时，我们使用Lean证明了非线性算术的关键引理，并将其导入Gobra。我们的验证工作揭示了三个关键见解：即使是经过严格审查的代码，细微缺陷也可能以惊人方式溜入；形式化验证是发现这些缺陷的强大工具；AI智能体可通过基于Gobra错误信息迭代优化不变量与引理来促进验证过程。