2 posts tagged with "elliptic curves"

In this blog post, we detail the continuation of our work to formally verify the ⚈ Smoo.th library, which is an optimized implementation of elliptic curve operations in Solidity. We use our tool coq-of-solidity, representing any Solidity code in the generic proof assistant 🐓 Coq, to verify the code for any execution path.

In particular, we cover the changes we made to use unoptimized Yul code and how we made a functional representation of the loop to compute the most significant bit of the scalars.

In this blog post, we present the formal verification effort we started to show the absence of bugs in the ⚈ Smoo.th library, a library for optimized 〰️ elliptic curve operations in Solidity. We are using our tool coq-of-solidity to make this non-trivial verification using the generic proof assistant 🐓 Coq.

The Smoo.th library is interesting as elliptic curves are at the core of many cryptographic protocols, including authentication protocols, and having a generic and fast implementation simplifies the development of dApps in environments with missing pre-compiled (like L1s) or missing circuits (like zero-knowledge layers).

From a verification point of view, it is very challenging as it combines low-level operations (hand-optimized Yul code with bit shifts, inlined functions, ...) with higher-level reasoning on elliptic curves and arithmetic 💪.