Introduction
The security of Bitcoin and other blockchains, such as Liquid, depends on the use of digital signature algorithms such as ECDSA and Schnorr signatures. The AC library called libsecp256k1, named after the elliptic curve on which the library operates, is used by both Bitcoin Core and Liquid to provide these digital signature algorithms. These algorithms use a mathematical calculation called a modular invertedwhich is a relatively expensive part of the calculation.
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, also called ‘safegcd’, was implemented for libsecp256k1 by Peter Dettman. As part of the vetting process for this new 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 indeed ends with the correct modular inverse result at 256 -bit inputs.
The gap between algorithm and implementation
The formalization efforts in 2021 have only shown 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 in the C programming language. For example, the mathematical description of the algorithm performs matrix multiplication of vectors that can be as wide as signed integers of 256 bits , but the C programming language only provides integers up to 64 bits (or 128 bits with some language extensions).
Implementing the safegcd algorithm requires programming the matrix multiplication and other calculations using C’s 64-bit integers. In addition, many other optimizations have been added to make the implementation fast. Ultimately, there are four separate implementations of the safegcd algorithm in libsecp256k1: two constant-time signature generation algorithms, one optimized for 32-bit systems and one optimized for 64-bit systems, and two variable-time signature verification algorithms, again one for 32 -bit systems and one for 64-bit systems.
Verifiable C
To verify that the C code correctly implements the safegcd algorithm, all implementation details must be checked. We use Verifiable C, part of the Verified Software Toolchain, to reason about C code using the Coq theorem prover.
Verification is accomplished by specifying pre- and post-conditions using separation logic for each function undergoing verification. Separation logic is a logic that specializes in reasoning about subroutines, memory allocations, concurrency, and more.
Once each function has been given a specification, verification continues by starting from a function’s precondition and establishing a new invariant after each statement in the function’s body, until finally establishing the postcondition at the end of the function. function text or at the end of each function. statement back. Most of the formalization effort is spent “between” the lines of code, using the invariants to translate the raw operations of each C expression into higher-level statements about what the data structures being manipulated mathematically represent. For example, what the C language considers an array of 64-bit integers may actually be a representation of a 256-bit integer.
The end result is a formal proof, verified by the Coq proof assistant, that libsecp256k1’s 64-bit variable time implementation of the safegcd modular inverse algorithm is functionally correct.
Limitations of authentication
There are some limitations to the proof of functional correctness. The separation logic used in Verifiable C implements what is known as partial correctness. That means it only proves that the C code returns with the correct result as it returns, but it does not prove the termination itself. We mitigate this limitation by using our previous Coq proof of the limits of the safegcd algorithm to prove that the loop counter value of the main loop is in fact never greater than 11 iterations.
Another problem is that the C language itself has no formal specification. Instead, the Verifiable C project uses the CompCert compiler project to provide a formal specification of a C language. This guarantees that when a verified C program is compiled with the CompCert compiler, the resulting assembly code will conform to the specification (subject to the above restriction). However, this does not guarantee that the code generated by GCC, clang or any other compiler will necessarily work. For example, C compilers are allowed to have different evaluation orders for arguments within a function call. And even if the C language had a formal specification, any compiler that hasn’t been formally verified itself could still compile programs incorrectly. This does happen in practice.
Finally, Verifiable C does not support passing structures, returning structures, or assigning structures. While in libsecp256k1 structures are always passed via a pointer (which is allowed in Verifiable C), there are a few cases where structure allocation is used. For the modular inverse correctness proof, there were 3 commands that had to be replaced by a specialized function call that performs the structure assignment field by field.
Summary
Blockstream Research has formally verified the correctness of libsecp256k1’s modular inverse function. This work provides further evidence that verification of C code is possible in practice. Using a general-purpose proofing assistant, we can verify software built on complex mathematical arguments.
Nothing prevents the rest of the functions implemented in libsecp256k1 from also being verified. Thus, it is possible for libsecp256k1 to obtain the highest possible guarantees of software correctness.
This is a guest post by Russell O’Connor and Andrew Poelstra. The opinions expressed are entirely their own and do not necessarily reflect those of BTC Inc or Bitcoin Magazine.