introduction
The security of Bitcoin, and other blockchains, such as Liquid, relies on the use of digital signature algorithms such as ECDSA and Schnorr signatures. The AC library is called libsecp256k1, named after the elliptic curve on which the library operates, used by both Bitcoin Core and Liquid to provide the digital signature algorithm. These algorithms use a mathematical calculation called a Modular oppositewhich 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 was known as “safegcd”. applied For libsecp256k1 by Peter Dettmann. As part of the testing process for this novel algorithm, Blockstream Research first conducted a Formal verification The design of the algorithm using the Coq proof assistant to formally verify that the algorithm actually terminates with a correct modular inverse result on 256-bit inputs.
Difference between algorithm and implementation
Formalization efforts in 2021 only showed that the algorithm devised by Bernstein and Yang worked 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 an algorithm multiplying a matrix of vectors can be up to 256-bit signed integers wide, although the C programming language 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 calculations using C’s 64-bit integers. apart from, Many more customizations has been added for faster execution. Finally, libsecp256k1 has four different implementations of the safegcd algorithm: 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 a 32- bit systems and one for 64-bit systems.
Certified C
All implementation details should be checked to verify that the C code correctly implements the SafegCD algorithm. We use Certified CCoq is part of a proven software toolchain for reasoning about C code using theorem provers.
The verification process proceeds by assigning preconditions and postconditions using partition logic for each function under consideration. Reason for separation There is special logic for reasoning about subroutines, memory allocation, concurrency, and more.
Once each function is given a specification, verification proceeds by starting with a function precondition, and setting a new invariant after each statement in the body of the function, finally at the end of the function body or each until establishing the post condition at the end of return statement Most of the formalization effort is spent “between” the lines of code, using invariants to translate the raw operations of each C expression into high-level statements that mathematically represent what data structures are being manipulated. . For example, what the C language treats as an array of 64-bit integers may actually represent a 256-bit integer.
The end result is A formal proofAs verified by the Coq proof assistant, libsecp256k1’s 64-bit variable time implementation of the safegcd modular inverse algorithm is functionally correct.
Limitations of verification
Functional accuracy evidence has some limitations. Verifiable implements a different logic than that used in C called Partial purity. This means that it only proves that the C code returns with the correct result If It comes back, but it doesn’t prove itself to be the end. We reduce this limit by using Our previous Coq proof To prove the limits of the safegcd algorithm the loop counter value of the main loop never actually exceeds 11 iterations.
Another issue is that the C language itself has no formal specification. Instead it uses the Verifiable C project CompCert Compiler Project To provide a formal specification of a C language. This guarantees that when a certified C program is compiled with the CompCert compiler, the resulting assembly code will meet its specification (subject to the above limits). However this does not guarantee that code generated by GCC, clang, or any other compiler will necessarily work. For example, the C compiler allows arguments within a function call to have different evaluation orders. And even though the C language has a formal specification any compiler that is not itself formally certified can still compile programs incorrectly. It does happens 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 verifiably allowed in C), there are some instances where structure assignment is used. For the modular inverse correctness proof, there were 3 assignments that had to be replaced by a special function call that completes the assignment field by field of the structure.
summary
Blockstream research has formally confirmed 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 proof assistant allows us to verify software built on complex mathematical arguments.
Nothing prevents the rest of the functions implemented in libsecp256k1 from being validated as well. Thus it is possible to achieve the highest possible software correctness guarantee for libsecp256k1.
This is a guest post by Russell O’Connor and Andrew Poelstra. The views expressed are solely their own and do not necessarily reflect the views of BTC Inc or Bitcoin Magazine.
