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

Abstract

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 of BoringSSL's implementation, we uncovered two deviations that each break the invariants of an existing proof for BoringSSL: (1) the Go implementation deviates in the way coefficients are updated, and (2) it permits a larger input domain. We prove correctness and termination of both the existing Go implementation and a fixed 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. For the existing implementation, we devise new invariants that accommodate the deviating coefficient updates; for the fixed implementation, we align the coefficient updates with BoringSSL's and port the existing proof. In both cases, we extend the proof to cover the larger input domain. Our fixed implementation updates coefficients in-place and, thus, reduces memory allocations, memory initializations, and memory copying operations resulting in an average speedup of 24% over the existing implementation. 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.