Safegcd’s Implementation Formally Verified

By Finance News On Nov 25, 2024

Introduction

The security of Bitcoin, and other blockchains, such as Liquid, hinges on the use of digital signatures algorithms such as ECDSA and Schnorr signatures. A C library called libsecp256k1, named after the elliptic curve that the library operates on, is used by both Bitcoin Core and Liquid, to provide these digital signature algorithms. These algorithms make use of a mathematical computation called a modular inverse, which is a relatively expensive component of the computation.

In “Fast constant-time gcd computation and modular inversion,” Daniel J. Bernstein and Bo-Yin Yang develop a new modular inversion algorithm. In 2021, this algorithm, referred to as “safegcd,” was implemented for libsecp256k1 by Peter Dettman. As part of the vetting process for this novel algorithm, Blockstream Research was the first to complete a formal verification of the algorithm’s design by using the Coq proof assistant to formally verify that the algorithm does indeed terminate with the correct modular inverse result on 256-bit inputs.

The Gap between Algorithm and Implementation

The formalization effort in 2021 only showed that the algorithm designed by Bernstein and Yang works correctly. However, using that algorithm in libsecp256k1 requires implementing the mathematical description of the safegcd algorithm within the C programming language. For example, the mathematical description of the algorithm performs matrix multiplication of vectors that can be as wide as 256 bit signed integers, however the C programming language will only natively provide integers up to 64 bits (or 128 bits with some language extensions).

Implementing the safegcd algorithm requires programming the matrix multiplication and other computations using C’s 64 bit integers. Additionally, many other optimizations have been added to make the implementation fast. In the end, there are four separate implementations of the safegcd algorithm in libsecp256k1: two constant time algorithms for signature generation, one optimized for 32-bit systems and one optimized for 64-bit systems, and two variable time algorithms for signature verification, again one for 32-bit systems and one for 64-bit systems.

Verifiable C

In order to verify the C code correctly implements the safegcd algorithm, all the implementation details must be checked. We use Verifiable C, part of the Verified Software Toolchain for reasoning about C code using the Coq theorem prover.

Verification proceeds by specifying preconditions and postconditions using separation logic for every function undergoing verification. Separation logic is a logic specialized for reasoning about subroutines, memory allocations, concurrency and more.

Once each function is given a specification, verification proceeds by starting from a function’s precondition, and establishing a new invariant after each statement in the body of the function, until finally establishing the post condition at the end of the function body or the end of each…