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

We verify and fix deviations in Go's standard library extended GCD implementation, which is critical for RSA key generation, by identifying subtle bugs that break algorithmic invariants and proposing fixes that improve performance.

Key Findings and Deviations

The verification effort uncovered two major deviations in the Go implementation of the extended GCD algorithm when compared to BoringSSL’s implementation: (1) the Go implementation deviates in the way coefficients are updated, which breaks the algorithm’s invariants, and (2) it permits a larger input domain. The paper notes that these deviations were subtle enough to slip through three code reviews.

Addressing Major Deviations

The first major deviation is the Unsynchronized Subtractions Deviation, concerning the updating of coefficients. BoringSSL and Fiat Cryptography consider whether the sum exceeds the modulus and reduce coefficients synchronously. The Go implementation performs "unsynchronized reductions by updating the coefficients as A ← if A + C < n then A + C else A + C − n end if instead of synchronized updates, which breaks the invariants (1) and (2)." The proposed fix involves using a single condition for both pairs of coefficients to ensure mathematical equivalence with the reference implementation.

The second major deviation is the Input Domain Deviation. The Go implementation "does not specify this requirement [that a < n must hold] for its GCDVarTime function, permitting inputs where a ≥ n." This breaks the invariants on which the proof relies. This deviation is addressed by extending the formal proof to cover the case where a ≥ n and adapting the postcondition of extendedGCD to reflect different guarantees in both cases.

Verification Methodology

The authors employed Gobra, a deductive program verifier for Go, to prove correctness and termination. Gobra translates annotated Go programs into Viper, which uses symbolic execution and Z3 SMT solver to discharge proof obligations. The verification process involves:

1. Verifying each function in isolation against its specification (preconditions and postconditions).

2. Using separation logic to reason about heap-allocated objects and memory safety.

3. Using trusted functions for bit-level operations, whose correctness is assumed based on manual review or Lean proofs, focusing the verification effort on extendedGCD.

Proof Structure and Key Lemmata

The proof relies on a set of key lemmata crucial for non-linear arithmetic, which are verified either by Gobra or by machine-checked Lean proofs. The paper mentions that Gobra verifies four of them, while we provide machine-checked Lean proofs for the other four lemmata. Two of the Lean-checked lemmata have a direct counterpart in Fiat Cryptography, while others state basic properties of modular arithmetic that Z3 cannot derive on its own. Termination is proven by showing that an expression involving the GCD value strictly decreases in each iteration.

Performance and Conclusion

The proposed fix for coefficient updates results in an on average 24 % speedup. Benchmarking showed a statistically significant, geometric mean performance improvement of 23.98 % across various limb sizes. The verification effort took approximately two person-weeks, significantly reduced by using an AI agent (Claude Code) to iteratively refine invariants and lemmata based on Gobra's error messages. The work concludes that formal verification is a powerful tool for uncovering subtle bugs.

Related Work Context

The work is situated near Fiat Cryptography, which also provides a verified extended GCD implementation, but the paper focuses on verifying the Go standard library implementation directly against the reference proof structure. Other related efforts include EverCrypt and libraries like HACL and libcrux, which offer modular inverse computations but lack the general extended GCD algorithm verification performed here. The paper emphasizes that reasoning about implementations on the code-level allows for verification without requiring implementers to exchange handwritten versions of algorithms.

Technical Details of Verification

The specification for the verified extendedGCD function includes invariants such as:

**(1) u = A **

a - B' n (where the proof notes this only holds if a < n.)

**(2) v = D **

n - C' a (where the proof notes this only holds if a < n.)

The loop invariants are adapted to handle the input domain deviation, and termination is measured by showing that u.Repr + v.Repr strictly decreases in each iteration and is bounded from below. The integration of Gobra into continuous integration allows for automatic checking on every code change.

AI Agent Utilization

The use of an AI agent was effective because Gobra produces insightful error messages that the agent could interpret and act upon, allowing it to autonomously iterate on both syntactic and semantic issues, such as refining preconditions and loop invariants.

Here are specific improvements for AI systems based on the findings in this research paper:

1. Develop a Formal Verification Agent that leverages deductive program verifiers like Gobra, specifically targeting complex, mathematically intensive algorithms (like Extended GCD) within standard library implementations (e.g., Go's crypto packages).

2. Improve AI system capabilities by enabling the agent to iteratively refine formal specifications (preconditions, postconditions, loop invariants) based on error messages from SMT solvers (Z3), effectively closing the gap between high-level natural language requirements and low-level implementation details.

3. Implement Trusted Function Verification modules that allow the AI to systematically verify small, crucial primitives (like bitwise operations or basic arithmetic) using Lean proofs, thereby reducing reliance on potentially unsound assumptions about external libraries or complex trusted functions.

4. Create an AI workflow that integrates continuous verification directly into CI/CD pipelines, allowing the system to automatically check for regressions in cryptographic implementations upon every code change, ensuring formal correctness is maintained throughout the development lifecycle.

5. Enhance agentic reasoning capabilities so they can autonomously compare implemented algorithms against established, formally proven reference proofs (like Fiat Cryptography), identifying subtle deviations in coefficient updates or input domain assumptions that human reviewers might miss.

6. Improve the AI's ability to handle and synthesize proof structures, enabling it to generate cleaner, more maintainable formal specifications by learning from successful automated proof attempts and iterative manual cleanup guided by the agent.

These improvements will result in AI systems capable of:

• Providing mathematically guaranteed correctness for complex software components (like cryptographic libraries).

• Automating the discovery of subtle, invariant-breaking bugs in high-assurance code.

• Reducing human verification effort by leveraging automated proof generation and refinement loops.

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.