The security of Bitcoin and other blockchains, such as Liquid, depends on digital signature algorithms like ECDSA and Schnorr signatures. A C library called libsecp256k1 provides these algorithms and is used by both Bitcoin Core and Liquid. These algorithms use a computation called a modular inverse, which is an expensive part of the process.
In “Fast constant-time gcd computation and modular inversion,” Daniel J. Bernstein and Bo-Yin Yang created a new modular inversion algorithm called “safegcd.” This algorithm was implemented for libsecp256k1 by Peter Dettman in 2021. Blockstream Research formally verified the algorithm’s design using the Coq proof assistant, showing that it correctly computes the modular inverse for 256-bit inputs.
However, implementing the safegcd algorithm required adapting the mathematical description to fit within the C programming language, which only natively supports integers up to 64 bits. Several optimizations were added to make the implementation fast, resulting in four separate implementations of the safegcd algorithm in libsecp256k1.
To ensure that the C code correctly implements the safegcd algorithm, Verifiable C, part of the Verified Software Toolchain, was used with the Coq theorem prover. This involved specifying preconditions and postconditions for every function undergoing verification using separation logic. The verification process then started from the function’s precondition and established a new invariant after each statement in the function body, until the postcondition was reached at the end of the function body or return statements.
Most of the formalization effort was spent translating the raw operations of each C expression into higher-level statements about what the data structures being manipulated represent mathematically. The verification resulted in 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.
However, there are some limitations to the functional correctness proof. The separation logic used in Verifiable C only proves partial correctness, meaning it only shows that the C code returns the correct result if it returns, but it doesn’t prove termination itself. To address this, a previous Coq proof of the bounds on the safegcd algorithm was used to prove that the loop counter value of the main loop never exceeds 11 iterations.
Another limitation 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 the C language. This guarantees that when a verified C program is compiled with the CompCert compiler, the resulting assembly code will meet its specification, but it does not guarantee that the code generated by other compilers will necessarily work.
Additionally, Verifiable C does not support passing, returning, or assigning structures. In libsecp256k1, structures are always passed by pointer, which is allowed in Verifiable C, but there are a few occasions where structure assignment is used. In summary, Blockstream Research has formally verified the correctness of libsecp256k1’s modular inverse function, providing further evidence that verification of C code is possible in practice.
This work also highlights that the rest of the functions implemented in libsecp256k1 could be verified as well, allowing the library to achieve the highest possible software correctness guarantees.
Source
<p>The post How Digital Signatures Make Bitcoin Secure! first appeared on CoinBuzzFeed.</p>
