7 posts tagged with "Yul"

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 💪.

We present improvements we made to our tool coq-of-solidity to formally verify Solidity smart contracts for any advanced properties, relying on the proof assistant 🐓 Coq. The idea is to be able to prove the full absence of bugs ✨ in very complex contracts, like L1 verifiers for zero-knowledge L2s 🕵️, or contracts with very large amounts of money 💰 (in the billions).

In this blog post, we present how we developed an effect inference mechanism to translate optimized Yul code combining variable mutations and control flow with loops and nested premature returns (break, continue, and leave) to a clean 🧼 purely functional representation in the proof system Coq.

In this blog post we explain how we specify and formally verify a whole ERC-20 smart contract using our tool coq-of-solidity, which translates Solidity code to the proof assistant Coq 🐓.

The proofs are still tedious for now, as there are around 1,000 lines of proofs for 100 lines of Solidity. We plan to automate this work as much as possible in the subsequent iterations of the tool. One good thing about the interactive theorem prover Coq is that we know we can never be stuck, so we can always make progress in our proof techniques and verify complex properties even if it takes time ✨.

Formal verification with an interactive proof assistant is the strongest way to verify programs since:

• it covers all possible inputs and program states,
• it checks any kind of properties.

We continue to strengthen the security of smart contracts with our tool coq-of-solidity 🛠️. It checks for vulnerabilities or bugs in Solidity code. It uses formal verification with an interactive theorem prover (Coq 🐓) to make sure that we cover:

• all possible user inputs/storage states, even if there are infinite possibilities,
• for any security properties.

This is very important as a single bug can lead to the loss of millions of dollars in smart contracts, as we have regularly seen in the past, and we can never be sure that a human review of the code did not miss anything.

Our tool coq-of-solidity is one of the only tools using an interactive theorem prover for Solidity, together with Clear from Nethermind. This might be the most powerful approach to making code without bugs, as exemplified in this PLDI paper comparing the reliability of various C compilers. They found numerous bugs in each compiler except in the formally verified one!

In this blog post we show how we functionally specify and verify the _approve function of an ERC-20 smart contract. We will see how we prove that a refined version of the function is equivalent to the original one.

We continue to work on our open source formal verification tool for Solidity named coq-of-solidity 🛠️. Formal verification is the strongest form of code audits, as we verify that the code behaves correctly in all possible execution cases 🔍. We use the interactive theorem prover Coq to express and verify any kinds of properties.

We work by translating the Yul version of a smart contract to the formal language Coq 🐓, in which we then express the code specifications/security properties and formally verify them 🔄. The Yul language is an intermediate language used by the Solidity compiler and others to generate EVM bytecode. Yul is simpler than Solidity and at a higher level than the EVM bytecode, making it a good target for formal verification.

In this blog post we present the recent developments we made to simplify the reasoning 🧠 about Yul programs once translated in Coq.

Solidity is the most widely used smart contract language on the blockchain. As smart contracts are critical software handling a lot of money, there is a huge interest in finding all possible bugs before putting them into production.

Formal verification is a technique to test a program on all possible entries, even when there are infinitely many. This contrasts with the traditional test techniques, which can only execute a finite set of scenarios. As such, it appears to be an ideal way to bring more security to smart contract audits.

In this blog post, we present the formal verification tool coq-of-solidity that we are developing for Solidity. Its specificities are that:

1. It is open-source (GPL-3 for the translation, MIT for the proofs).
2. It uses an interactive theorem prover, the system Coq, to verify arbitrarily complex properties.

Here, we present how we translate Solidity code into Coq using the intermediate language Yul. We explain the semantics we use and what remains to be done.

The code is available in our fork of the Solidity compiler at github.com/formal-land/coq-of-solidity.