Enhancing Blockchain Security with Verified C Code
Bitcoin and other blockchains rely on digital signature algorithms like ECDSA and Schnorr signatures to ensure security. To implement these algorithms, a C library called libsecp256k1 is used by Bitcoin Core and Liquid. This library operates on the elliptic curve with the same name and includes mathematical computations like modular inversion, which can be resource-intensive.
In a recent development, a new modular inversion algorithm called “safegcd” was introduced by Daniel J. Bernstein and Bo-Yin Yang. This algorithm was implemented in libsecp256k1 by Peter Dettman in 2021. To validate the algorithm’s design, Blockstream Research conducted a formal verification using the Coq proof assistant to confirm its correctness on 256-bit inputs.
Addressing the Gap between Algorithm and Implementation
While the formal verification demonstrated the algorithm’s correctness, translating the mathematical description into C code presents challenges. The C programming language has limitations in handling wide integer operations like those required by the safegcd algorithm. Implementing the algorithm in libsecp256k1 involves optimizing matrix multiplication and other computations using 64-bit integers, along with additional optimizations for efficiency.
Verifying C Code with Verifiable C
To ensure that the C code accurately reflects the safegcd algorithm, Verifiable C, part of the Verified Software Toolchain, is utilized. This toolchain leverages separation logic to specify preconditions and postconditions for each function undergoing verification. By establishing invariants throughout the function’s body, the correctness of the implementation is validated.
The verification process involves translating C code operations into higher-level mathematical representations to confirm the algorithm’s functionality. The result is a formal proof, verified by the Coq proof assistant, that validates libsecp256k1’s 64-bit variable time implementation of the safegcd algorithm.
Limitations and Considerations
While the functional correctness of the C code is verified, certain limitations exist. The verification process focuses on partial correctness, confirming the algorithm’s result if it terminates. Additionally, the lack of a formal specification for the C language introduces uncertainties in the compilation process, requiring caution when using different compilers.
Despite these limitations, the formal verification of libsecp256k1’s modular inverse function showcases the potential for achieving high software correctness guarantees. With ongoing efforts, it is feasible to extend verification to other functions within libsecp256k1, further enhancing blockchain security.
Conclusion
By leveraging formal verification techniques, such as Verifiable C and the Coq proof assistant, the security and reliability of blockchain implementations can be significantly strengthened. The verification of libsecp256k1’s modular inverse function underscores the importance of rigorous testing and validation in critical software components. As the blockchain industry continues to evolve, ensuring the integrity of cryptographic algorithms through formal verification will be paramount.
This article was co-authored by Russell O’Connor and Andrew Poelstra. The views expressed are their own and do not necessarily reflect those of BTC Inc or Bitcoin Magazine.