💻 computer science

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

This paper identifies and fixes two critical deviations in Go's extended GCD implementation that compromise RSA key generation, subsequently proving the corrected code's correctness and termination using the Gobra and Lean verification tools while demonstrating how AI agents can assist in refining formal proofs.

Original authors: Linard Arquint

Published 2026-06-05

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Linard Arquint

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are building a high-security digital vault (like the ones used for online banking or secure messaging). To lock and unlock this vault, you need a very specific, complex mathematical key. In the world of computer science, this key is generated using a recipe called the Extended Greatest Common Divisor (GCD) algorithm.

This paper is about a team of researchers who went into the "kitchen" of the Go programming language (a popular tool used to build software) to check if the recipe for this key was being followed correctly. They found that the recipe had been slightly altered, and they fixed it while proving mathematically that the new version works perfectly.

Here is the story of their discovery, broken down into simple parts:

1. The "Copy-Paste" Mistake

The Go developers wanted to update their software to meet strict government security standards. To do this, they took a recipe from a trusted, well-known source called BoringSSL (a secure library used by Google) and "ported" it (translated it) into Go.

Think of it like a famous chef giving you a secret recipe for a cake. You decide to rewrite the recipe in your own handwriting to make it easier to read. The paper claims that while rewriting it, the Go developers accidentally changed two important steps.

The Problem: The original recipe had a strict rule: "If you add these two numbers, and the result is too big, you must subtract a specific amount from both numbers at the exact same time." This keeps the cake from collapsing.
The Bug: The Go version did this "too big" check separately for each number. It was like checking the flour and the sugar independently. This broke the mathematical balance (the "invariants") that guarantees the key is correct.
The Surprise: Three different human experts reviewed the code and missed this mistake. It was so subtle that it slipped through the net.

2. The "Too Big" Ingredient

The second issue was about the size of the ingredients allowed.

The Rule: The original recipe said, "The first ingredient must always be smaller than the second."
The Change: The Go version allowed the first ingredient to be bigger than the second.
The Fix: The researchers didn't need to change the code for this one. Instead, they had to update the "proof" (the mathematical guarantee) to show that the recipe still works even with the bigger ingredients.

3. The Magic Detective (Gobra)

To prove they fixed the bugs, the researchers used a tool called Gobra.

The Analogy: Imagine a super-strict, hyper-attentive robot inspector. You feed it the code and a list of rules (specifications). The robot doesn't just run the code; it simulates every possible way the code could run, checking every single path to ensure it never breaks the rules.
The Result: The robot confirmed that once the "synchronization bug" was fixed, the code was 100% correct. In fact, because the fix removed unnecessary steps, the new code actually ran 24% faster than the buggy version.

4. The AI Assistant

The researchers didn't do all the heavy lifting alone. They used an AI agent (a smart computer program) to help them.

How it worked: The AI acted like a tireless apprentice. When the robot inspector (Gobra) said, "This part doesn't make sense," the AI would suggest changes to the rules or the code.
The Catch: The AI initially assumed the code was perfect and tried to force the math to fit. The human researchers had to tell the AI, "No, the code is actually wrong; look for the difference." Once the AI understood that, it became incredibly helpful, suggesting fixes and helping write the mathematical proofs.

5. The Takeaway

The paper concludes with three main lessons:

Even experts make subtle mistakes: Three human reviewers missed a critical bug that a formal proof tool found.
Formal verification is powerful: Using a tool like Gobra is like having a mathematical guarantee that your code works, rather than just hoping it works because it passed a few tests.
AI is a great partner: AI can help humans write these complex proofs, but humans still need to guide the AI to question the code rather than just accept it.

In short: The researchers found a hidden flaw in a critical security algorithm in Go's standard library, fixed it, proved mathematically that the fix works, and showed that the fix actually made the software faster. They did this using a combination of human insight, automated proof tools, and AI assistance.

Technical Summary: GCD: Garbled, Corrected, Demonstrandum

Problem Statement

The paper addresses the correctness and verification of the Extended Euclidean Algorithm (Extended GCD) implementation within Go's standard library (crypto/internal/fips140/bigmod). This implementation is critical for RSA key pair generation, a foundational component for TLS, SSH, and PGP. The Go implementation was introduced in Go 1.24 to natively support FIPS 140-3 compliance, replacing reliance on BoringSSL.

The authors identified a critical discrepancy: although the Go code was claimed to be a direct port of BoringSSL's implementation (which is formally verified in the Rocq proof assistant via Fiat Cryptography), the Go version contained subtle deviations. These deviations were not caught by three separate code reviews. The deviations broke the algorithm's mathematical invariants, potentially compromising the correctness of the modular inverse calculation required for RSA private keys. Furthermore, the Go implementation permitted a larger input domain than the proven BoringSSL version, invalidating the existing proof assumptions.

Methodology

The authors employed a deductive program verification approach using Gobra, a separation-logic-based verifier for Go. The methodology involved:

Formal Specification: The authors formalized the natural language specifications of the Go functions (extendedGCD, InverseVarTime, GCDVarTime) into Gobra specifications, including preconditions, postconditions, and loop invariants.
Deviation Analysis: By attempting to verify the existing Go code against the specifications derived from the BoringSSL proof, the authors identified two major classes of deviations:
- Unsynchronized Subtractions: The Go implementation updated Bézout coefficients ( $A, B, C, D$ ) independently based on local conditions, whereas the reference implementation required synchronized reductions to maintain loop invariants.
- Input Domain Expansion: The Go implementation allowed inputs where $a \ge n$ , violating the precondition $a < n$ required by the original proof.
Proof Construction:
- Code Fix: The authors proposed a fix for the unsynchronized subtractions to align the Go logic with the mathematical invariants.
- Proof Adaptation: They ported the existing BoringSSL proof from Rocq to Gobra. For the input domain deviation, they relaxed the invariants and postconditions to cover the case where $a \ge n$ , proving that the GCD value remains correct even if the modular inverse property does not hold in that specific case.
- Hybrid Verification: For non-linear arithmetic lemmata that the Z3 SMT solver (used by Gobra) could not handle, the authors used the Lean proof assistant to prove key lemmata and imported them into Gobra as trusted lemmata.
AI-Assisted Verification: The authors utilized an AI agent (Anthropic's Claude Code) to iteratively refine invariants and lemmata based on Gobra's error messages, significantly reducing manual effort in the proof construction process.

Key Contributions

Bug Discovery: The paper uncovers two subtle but critical deviations in Go's Extended GCD implementation that break algorithmic invariants. These bugs were present in code that had undergone multiple reviews and was claimed to be a direct port of a verified implementation.
Performance Optimization: The proposed fix for the unsynchronized subtraction deviation not only restores correctness but also results in an average 24% speedup (geometric mean) by eliminating unnecessary memory allocations and redundant operations in the loop body.
Formal Verification of Go Crypto: The authors successfully verify the fixed Go implementation, its termination, and its correctness against formal specifications using Gobra. This is the first formal verification of this specific component in Go's standard library.
Proof Porting and Generalization: They successfully ported a proof from Rocq (Fiat Cryptography) to Gobra and generalized it to cover the broader input domain permitted by the Go implementation.
AI in Verification: The work demonstrates the efficacy of AI agents in facilitating formal verification by autonomously iterating on specifications and identifying the root causes of proof failures (e.g., suggesting that independent coefficient reduction was the issue).

Results

Correctness: The fixed implementation was successfully verified in 16.9 seconds on a standard laptop. The verification covers the extendedGCD function and its clients InverseVarTime and GCDVarTime.
Performance: Benchmarks across various limb sizes (64 to 8192 bits) showed that the verified implementation is consistently faster than the original. The average speedup was 23.98%, with improvements ranging from 15.6% to 36% depending on input size. The speedup is attributed to in-place updates and the elimination of intermediate buffer allocations.
Disclosure and Impact: The authors disclosed the deviations to Go cryptography maintainers. The maintainers confirmed that while the deviations could theoretically lead to incorrect modular inverses, defensive checks in the RSA key generation code would catch these errors and return an error rather than an incorrect key, limiting the impact to availability rather than security compromise. The fixes are under review for inclusion in the Go standard library.
Continuous Integration: Due to the fast verification time, the proof has been integrated into the project's Continuous Integration (CI) workflow to automatically check for future deviations.

Significance and Claims

The paper claims that its work highlights three primary insights:

Subtle Bugs in Reviewed Code: Even well-reviewed code, especially when claimed to be a direct port of a verified implementation, can contain subtle bugs that break invariants.
Power of Formal Verification: Formal verification is a powerful tool for uncovering these types of bugs that testing and manual review might miss.
Role of AI Agents: AI agents can effectively facilitate the verification process by iteratively refining invariants and lemmata based on verifier feedback, though human oversight remains necessary for final cleanup and structural understanding.

The authors emphasize that their work closes the gap between the implementation and its proof. By verifying the Go code directly rather than relying on the existence of a proof for a different implementation (BoringSSL), they ensure that the specific code running in production is mathematically sound. They also note that while they rely on trusted functions for low-level bit operations, the overall correctness argument is broken down into small, reviewable components, increasing confidence in the system's reliability.