pith. sign in

arxiv: 2606.05796 · v2 · pith:DKPSGDPJnew · submitted 2026-06-04 · 💻 cs.CR

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

Linard Arquint This is my paper

Pith reviewed 2026-06-28 00:38 UTC · model grok-4.3

classification 💻 cs.CR
keywords extended GCDformal verificationGo standard libraryGobraBoringSSLRSA key generationdeductive verificationnon-linear arithmetic
0
0 comments X

The pith

Go's extended GCD implementation contained two invariant-breaking deviations from BoringSSL that were fixed and then formally proven correct and terminating.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that Go's extendedGCD in crypto/internal/fips140/bigmod deviates from its BoringSSL source in coefficient updates and permitted input sizes, each breaking the algorithm's required properties. Correcting the coefficient logic produces an average 24 percent speedup. The authors port the existing BoringSSL proof, extend it to the larger domain, and discharge the full correctness and termination argument in Gobra, a deductive verifier for Go, by importing selected Lean lemmas on non-linear arithmetic. The effort demonstrates that even heavily reviewed cryptographic code can harbor subtle bugs and that deductive verification combined with external arithmetic provers can locate and eliminate them.

Core claim

After repairing the coefficient-update deviation, the Go extendedGCD function satisfies its specification for the declared input domain; the repaired program is both partially correct and terminating. The argument is obtained by mechanically porting and extending a prior BoringSSL proof, with Gobra handling the imperative Go code and Lean supplying the necessary non-linear arithmetic facts.

What carries the argument

Gobra deductive verifier for Go together with the ported and extended BoringSSL extended-GCD proof and imported Lean lemmas on arithmetic.

If this is right

  • The repaired implementation can be used for RSA key-pair generation with a mechanically checked guarantee of correctness.
  • Termination of the fixed code is now established, eliminating the possibility of non-termination on any valid input.
  • The same port-and-extend strategy can be reused for other BoringSSL-derived cryptographic primitives in Go.
  • AI-assisted refinement of invariants, guided by Gobra error messages, can accelerate similar verification tasks.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Other language ports of the same BoringSSL GCD routine may contain analogous coefficient-update errors.
  • Embedding Gobra-style verification in the Go standard-library release process could catch future deviations before they ship.
  • The observed 24 percent speedup indicates that correctness fixes can also improve performance when they remove unnecessary operations.

Load-bearing premise

The two deviations identified in the paper are the only ones that break the algorithm invariants, and the BoringSSL proof can be ported and extended to the larger input domain without introducing new gaps.

What would settle it

An input pair inside the documented domain for which the repaired Go code returns coefficient pairs that fail the extended-GCD relation a*x + b*y = gcd would falsify the claim.

Figures

Figures reproduced from arXiv: 2606.05796 by Linard Arquint.

Figure 1
Figure 1. Figure 1: Proposed synchronized reduction for updating the [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Definition of the Nat struct that the Go standard library uses to represent arbitrary-length natural numbers and our invariant predicate. zero and smaller than 1 grants read-only access. Permission for a particular heap object can be split and combined, e.g., to share read access among multiple threads. Since permissions are non￾duplicable, a proof in separation logic guarantees memory safety and absence o… view at source ↗
Figure 4
Figure 4. Figure 4: Specification for the verified extendedGCD function. For presentation purposes, we use full instead of fractional permissions for a and n and omit that a and n remain unmod￾ified. gmax returns the maximum of its arguments. these functions are not called from any verified code, preventing unsound assumptions about their behavior from creeping into the proof of extendedGCD. 4.2 Specifications and Proofs Than… view at source ↗
Figure 5
Figure 5. Figure 5: Specifications for the verified InverseVarTime and GCDVarTime functions. We make similar presentation choices as in [PITH_FULL_IMAGE:figures/full_fig_p006_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Performance comparison between the original and [PITH_FULL_IMAGE:figures/full_fig_p007_6.png] view at source ↗
read the original 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 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper identifies two deviations between Go's extendedGCD implementation in crypto/internal/fips140/bigmod and the BoringSSL version from which it was ported: an incorrect update rule for the coefficients and an expanded input domain. The authors correct the coefficient update (yielding an average 24% speedup), port the existing BoringSSL proof, and extend it to the larger domain. They establish correctness and termination of the repaired Go code via a machine-checked proof in Gobra, importing auxiliary Lean lemmata for the non-linear arithmetic that arises from the domain extension. The work also reports three meta-insights on the ease with which subtle bugs enter reviewed code, the utility of formal verification, and the role of AI agents in invariant refinement.

Significance. If the machine-checked proof is sound, the contribution is significant: it supplies a verified, faster implementation of a core primitive used in RSA key generation, demonstrates that deductive verification (Gobra + Lean) can scale to non-linear arithmetic arising from realistic input domains, and furnishes concrete evidence that formal methods can detect deviations invisible to conventional review. The explicit reuse and extension of a prior BoringSSL proof, together with the machine-checked status of both the program and the supporting arithmetic lemmata, strengthens the result.

minor comments (2)
  1. [Abstract] Abstract: the claim that the two deviations are exhaustive would benefit from an explicit statement (in the body) that the authors performed a systematic comparison of the two code bases rather than relying solely on the two observed failures.
  2. The description of how the Lean lemmata are imported into Gobra (e.g., via trusted axioms or a verified embedding) is only sketched; a short paragraph or appendix entry would improve reproducibility.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our work on verifying and correcting Go's extendedGCD implementation, including the recognition of its significance for RSA key generation and the value of the machine-checked proof. We appreciate the recommendation to accept.

Circularity Check

0 steps flagged

No significant circularity; machine-checked proof against external spec

full rationale

The paper's central claim is a deductive verification of a fixed Go extendedGCD implementation using Gobra (with Lean lemmata for non-linear arithmetic). It ports and extends an existing BoringSSL proof to a larger input domain. This is self-contained against external benchmarks: the specification, BoringSSL reference, and proof tools are independent of the present manuscript. No step reduces by construction to a fitted parameter, self-defined quantity, or load-bearing self-citation chain. The two identified deviations and the fix are justified by direct comparison to the external BoringSSL code, not by internal redefinition.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The verification rests on the soundness of Gobra and Lean, standard properties of integer arithmetic, and the assumption that the BoringSSL proof is a valid base; no free parameters or invented entities are introduced.

axioms (2)
  • domain assumption Soundness of Gobra deductive verifier and Lean theorem prover for the imported lemmata
    Invoked when importing Lean facts into Gobra proofs (abstract).
  • standard math Standard properties of non-linear integer arithmetic
    Used for key lemmata proved in Lean (abstract).

pith-pipeline@v0.9.1-grok · 5744 in / 1365 out tokens · 31498 ms · 2026-06-28T00:38:47.261277+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

33 extracted references · 16 canonical work pages

  1. [1]

    José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub. 2017. Jasmin: High-Assurance and High-Speed Cryptography. InCCS. ACM, 1807–1823. doi:10.1145/3133956.3134078

    work page doi:10.1145/3133956.3134078 2017

  2. [2]

    José Bacelar Almeida, Denis Firsov, Tiago Oliveira, and Dominique Unruh. 2023. Schnorr Protocol in Jasmin. Cryptology ePrint Archive, Paper 2023/752. https: //eprint.iacr.org/2023/752

    2023

  3. [3]

    Linard Arquint. 2026. crypto/internal/fips140/bigmod: Fix ‘extendedGCD’ Imple- mentation Mismatch. https://go-review.googlesource.com/c/go/+/770380

    2026

  4. [4]

    Linard Arquint. 2026. Verification of extendedGCD. https://github.com/arquintl/ go-gcd

    2026

  5. [5]

    Linard Arquint. 2026. Verification of extendedGCD – Continuous Verification. https://github.com/arquintl/go-gcd/actions/workflows/verify-gcd.yml

    2026

  6. [6]

    Koenig, Joey Dodds, Daniel Kroening, and Peter Müller

    Linard Arquint, Samarth Kishor, Jason R. Koenig, Joey Dodds, Daniel Kroening, and Peter Müller. 2026. The Secrets Must Not Flow: Scaling Security Verification to Large Codebases. InS&P. IEEE, 492–511. doi:10.1109/SP63933.2026.00026 To appear

    work page doi:10.1109/sp63933.2026.00026 2026

  7. [7]

    Linard Arquint, Malte Schwerhoff, Vaibhav Mehta, and Peter Müller. 2023. A Generic Methodology for the Modular Verification of Security Protocol Imple- mentations. InCCS. ACM, 1377–1391. doi:10.1145/3576915.3623105

    work page doi:10.1145/3576915.3623105 2023

  8. [8]

    In: IEEE S&P (2023).https://doi.org/10.1109/SP46215.2023.10179435

    Linard Arquint, Felix A. Wolf, Joseph Lallemand, Ralf Sasse, Christoph Sprenger, Sven N. Wiesner, David A. Basin, and Peter Müller. 2023. Sound Verification of Security Protocols: From Design to Interoperable Implementations. InS&P. IEEE, 1077–1093. doi:10.1109/SP46215.2023.10179325

    work page doi:10.1109/sp46215.2023.10179325 2023

  9. [9]

    Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella-Béguelin

  10. [10]

    In CRYPTO (LNCS, Vol

    Computer-Aided Security Proofs for the Working Cryptographer. In CRYPTO (LNCS, Vol. 6841). Springer, 71–90. doi:10.1007/978-3-642-22792-9_5

    work page doi:10.1007/978-3-642-22792-9_5

  11. [11]

    David Benjamin. 2018. Add a Constant-Time Binary Extended GCD Algorithm. https://github.com/mit-plv/fiat-crypto/pull/333

    2018

  12. [12]

    Rustan M

    Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath T. V. Setty, and Laure Thompson. 2017. Vale: Verifying High-Performance Cryptographic Assembly Code. InUSENIX Security Symposium. USENIX Association, 917–934

    2017

  13. [13]

    John Boyland. 2003. Checking Interference with Fractional Permissions. InSAS (LNCS, Vol. 2694). Springer, 55–72. doi:10.1007/3-540-44898-5_4

    work page doi:10.1007/3-540-44898-5_4 2003

  14. [14]

    Cryspen. 2020. libcrux - A High-Assurance Cryptographic Library in Rust. https://github.com/cryspen/libcrux

    2020

  15. [15]

    Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala

  16. [16]

    Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises. InS&P. IEEE, 1202–1219. doi:10.1109/SP.2019.00005

    work page doi:10.1109/sp.2019.00005 2019

  17. [17]

    Go developers. 2026. testing.B.Loop Documentation. https://pkg.go.dev/testing# B.Loop

    2026

  18. [18]

    Secure two- party quantum evaluation of unitaries against specious adversaries,

    K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. InLPAR (Dakar) (LNCS). Springer, 348–370. doi:10.1007/978-3-642- 17511-4_20

    work page doi:10.1007/978-3-642- 2010

  19. [19]

    van Oorschot, and Scott A

    Alfred Menezes, Paul C. van Oorschot, and Scott A. Vanstone. 1996.Handbook of Applied Cryptography. CRC Press. doi:10.1201/9781439821916

    work page doi:10.1201/9781439821916 1996

  20. [20]

    Peter Müller, Malte Schwerhoff, and Alexander J. Summers. 2016. Viper: A Verification Infrastructure for Permission-Based Reasoning. InVMCAI (LNCS, Vol. 9583). Springer, 41–62. doi:10.1007/978-3-662-49122-5_2

    work page doi:10.1007/978-3-662-49122-5_2 2016

  21. [21]

    2019.FIPS PUB 140-3: Secu- rity Requirements for Cryptographic Modules

    National Institute of Standards and Technology. 2019.FIPS PUB 140-3: Secu- rity Requirements for Cryptographic Modules. Federal Information Processing Standards Publication 140-3. National Institute of Standards and Technology. doi:10.6028/NIST.FIPS.140-3

    work page doi:10.6028/nist.fips.140-3 2019

  22. [22]

    Pereira, Tobias Klenze, Sofia Giampietro, Markus Limbeck, Dionysios Spiliopoulos, Felix Wolf, Marco Eilers, Christoph Sprenger, David A

    João C. Pereira, Tobias Klenze, Sofia Giampietro, Markus Limbeck, Dionysios Spiliopoulos, Felix Wolf, Marco Eilers, Christoph Sprenger, David A. Basin, Peter Müller, and Adrian Perrig. 2025. Protocols to Code: Formal Verification of a Secure Next-Generation Internet Router. InCCS. ACM, 1469–1483. doi:10.1145/ 3719027.3765104

    arXiv 2025

  23. [23]

    Jade Philipoom. 2023. Add a Constant-Time Binary Extended GCD Algorithm. https://github.com/mit-plv/fiat-crypto/pull/1597

    2023

  24. [24]

    Flash boys 2.0: Frontrunning in decentralized exchanges, miner extractable value, and consensus instability

    Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, An- toine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, and Santiago Zanella Béguelin. 2020. EverCrypt: A Fast, Verified, Cross-...

    work page doi:10.1109/sp40000.2020.00114 2020

  25. [25]

    Reynolds

    John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. InLICS. IEEE, 55–74. doi:10.1109/LICS.2002.1029817

    work page doi:10.1109/lics.2002.1029817 2002

  26. [26]

    Junyang Shao. 2025. More Predictable Benchmarking with testing.B.Loop. https: //go.dev/blog/testing-b-loop

    2025

  27. [27]

    Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat- Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella Béguelin

  28. [28]

    Dependent Types and Multi-Monadic Effects in F*. InPOPL. ACM, 256–270. doi:10.1145/2837614.2837655

    work page doi:10.1145/2837614.2837655

  29. [29]

    The Formosa team. [n. d.]. Formosa Crypto. https://formosa-crypto.org

  30. [30]

    Filippo Valsorda. 2024. crypto/internal/fips140/bigmod: Add Nat.InverseVarTime. https://go-review.googlesource.com/c/go/+/632415

    2024

  31. [31]

    Filippo Valsorda. 2025. crypto/internal/fips140/bigmod: Explicitly Clear Expanded Limbs on Reset. https://go-review.googlesource.com/c/go/+/655056

    2025

  32. [32]

    Challenges in Survey Re- search

    Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, João Carlos Pereira, and Peter Müller. 2021. Gobra: Modular Specification and Verification of Go Programs. InCA V (LNCS, Vol. 12759). Springer, 367–379. doi:10.1007/978-3- 030-81685-8_17

    work page doi:10.1007/978-3- 2021

  33. [33]

    Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. 2017. HACL*: A Verified Modern Cryptographic Library. InCCS. ACM, 1789–1806. doi:10.1145/3133956.3134043 9

    work page doi:10.1145/3133956.3134043 2017