introduction
The security of Bitcoin and other blockchains, such as Liquid, is based on the use of digital signature algorithms such as ECDSA and Schnorr signatures. An 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 Inverse unitswhich is a relatively expensive component of the computation.
in “Fast GCD calculation in constant time and standard inversion“, Daniel J. Bernstein and Bo Yin Yang developed a new standard reversal algorithm. In 2021, this algorithm was created, which is referred to as “safegcd”. outlet For libsecp256k1 by Peter Dettmann. As part of the vetting process for this new algorithm, Blockstream Research was the first to complete a vetting process Official verification To design the algorithm using Coq helper to formally verify that the algorithm actually ends with the correct normalized inverse result on the 256-bit input.
The gap between algorithm and implementation
Only a formalization effort in 2021 showed that the algorithm designed by Bernstein and Yang works properly. However, using that algorithm in libsecp256k1 requires implementing the mathematical description of the Safegcd algorithm within the programming language C. For example, the mathematical description of the algorithm performs matrix multiplication of vectors whose width can be up to 256-bit signed integers, yet the programming language C will only provide integers up to 64 bits (or 128 bits with some language extensions).
Implementing the Safegcd algorithm requires programming matrix multiplication and other arithmetic using 64-bit integers in C. In addition, Many other improvements Added to make implementation fast. Ultimately, there are four separate implementations of the Safegcd algorithm in libsecp256k1: two fixed-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 that the C code implements the Safegcd algorithm correctly, all implementation details must be verified. We use verifiable cpart of a series of verified software tools for reasoning C code using the Coq theorem prover.
Verification proceeds by specifying preconditions and postconditions using separation logic for each function subject to verification. The logic of separation It is a logic that specializes in thinking about subroutines, memory allocations, concurrency, and more.
Once a specification is given for each function, verification is done by starting at the precondition of the function, creating a new constant after each statement in the function body, until finally specifying the postcondition at the end of the function body or the end of each function. Return statement. Most formalization efforts are spent “between” the lines of code, using constants to translate the elementary operations of each C expression into higher-level statements about what the data structures being manipulated represent mathematically. For example, what C considers to be an array of 64-bit integers may actually be a representation of a 256-bit integer.
The end result is Official guide,Verified by Coq’s proof helper, that libsecp256k1’s 64-bit variable-time implementation of the Safegcd standard inverse algorithm is functionally correct.
Verification limits
There are some limitations to proving functional validity. The class logic used in Verifiable C implements what is known as Partial validity. This means that it only proves that the C code returns the correct result if It returns, but it does not prove itself terminated. We relax this limitation by using Our previous Coq guide One of the limitations of the Safegcd algorithm is to prove that the loop counter value of the main loop actually does not exceed 11 iterations.
Another problem is that the C language itself has no formal specifications. Instead, the Verifiable C project uses the extension CompCert compiler project To provide a formal specification for the C language. This ensures that when a verified C program is compiled using the CompCert compiler, the resulting assembly code will meet its specification (subject to the limitations mentioned above). However, this does not guarantee that code generated by gcc, clang, or any other compiler will necessarily work. For example, C compilers are allowed to have different evaluation commands for arguments within a function call. Even if C has a formal specification, any compiler that has not been formally verified could still miscompile programs. This does It is happening In practice.
Finally, Verifiable C does not support passing structures, returning structures, or assigning structures. While in libsecp256k1, structures are always passed by pointer (which is allowed in Verifiable C), there are a few occasions where structure mapping is used. For the standard cross-validation, there were 3 assignments that had to be replaced by calling a specialized function that performs the structure assignment field by field.
summary
Blockstream Research has officially validated the standard inverse function of libsecp256k1. This work provides further evidence that verification of C code is practically possible. Using a general-purpose proof helper allows us to verify programs built on complex mathematical arguments.
Nothing prevents checking the rest of the functions implemented in libsecp256k1 as well. It is therefore possible for libsecp256k1 to obtain the highest possible guarantees of program 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 the opinions of BTC Inc or Bitcoin Magazine.