Formal Verification of the Safegcd Implementation

TL;DR

This paper presents a formal verification of the Safegcd implementation in libsecp256k1, ensuring correctness of the modular inverse algorithm used in Bitcoin's cryptography through machine-checked proofs.

Contribution

It provides the first computer-verified proof of correctness for a libsecp256k1 modular inverse implementation using Coq and Verifiable C, enhancing cryptographic reliability.

Findings

Verified the correctness of the Safegcd implementation

Reduced risk of cryptographic errors in Bitcoin's code

Established a formal foundation for cryptographic implementation correctness

Abstract

The modular inverse is an essential piece of computation required for elliptic curve operations used for digital signatures in Bitcoin and other applications. A novel approach to the extended Euclidean algorithm has been developed by Bernstein and Yang within the last few years and incorporated into the libsecp256k1 cryptographic library used by Bitcoin. However, novel algorithms introduce new risks of errors. To address this we have completed a computer verified proof of the correctness of (one of) libsecp256k1's modular inverse implementations with the Coq proof assistant using the Verifiable C's implementation of separation logic.