21 posts tagged with "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/solidity.

In order to formally verify Python code in Coq our approach is the following:

1. Import Python code in Coq by running coq-of-python.
2. Write a purely functional simulation in Coq of the code.
3. Show that this simulation is equivalent to the translation.
4. Verify the simulation.

We will show in this article how we can merge the steps 2. and 3. to save time in the verification process. We do so by relying on the proof mode of Coq and unification.

Our mid-term goal is to formally specify the Ethereum Virtual Machine (EVM) and prove that this specification is correct according to reference implementation of the EVM in Python. This would ensure that it is always up-to-date and exhaustive. The code of this project is open-source and available on GitHub: formal-land/coq-of-python.

We are continuing to specify the Ethereum Virtual Machine (EVM) in the formal verification language Coq. We are working from the automatic translation in Coq of the reference implementation of the EVM, which is written in the language Python.

In this article, we will see how we specify the EVM in Coq by writing an interpreter that closely mimics the behavior of the Python code. We call that implementation a simulation as it aims to reproduce the behavior of the Python code, the reference.

In contrast to the automatic translation from Python, the simulation is a manual translation written in idiomatic Coq. We expect it to be ten times smaller in lines compared to the automatic translation, and of about the same size as the Python code. This is because the automatic translation needs to encode all the Python specific features in Coq, like variable mutations and the class system.

In the following article, we will show how we can prove that the simulation is correct, meaning that it behaves exactly as the automatic translation.

The code of this project is open-source and available on GitHub: formal-land/coq-of-python. This work follows a call from Vitalik Buterin for more formal verification of the Ethereum's code.

We are starting to work on a new product, coq-of-python. The idea of this tool is, as you can guess, to translate Python code to the proof system Coq.

We want to import specifications written in Python to a formal system like Coq. In particular, we are interested in the reference specification of Ethereum, which describes how EVM smart contracts run. Then, we will be able to use this specification to either formally verify the various implementations of the EVM or smart contracts.

All this effort follows a Tweet from Vitalik Buterin hoping for more formal verification of the Ethereum's code:

One application of AI that I am excited about is AI-assisted formal verification of code and bug finding.

Right now ethereum's biggest technical risk probably is bugs in code, and anything that could significantly change the game on that would be amazing.

— Vitalik Buterin

We will now describe the technical development of coq-of-python. For the curious, all the code is on GitHub: formal-land/coq-of-python.

We continue our work on formal verification of Rust programs with our tool coq-of-rust, to translate Rust code to the formal proof system Coq. One of the limitation we had was the handling of primitive constructs from the standard library of Rust, like Option::unwrap_or_default or all other primitive functions. For each of these functions, we had to make a Coq definition to represent its behavior. This is both tedious and error prone.

To solve this issue, we worked on the translation of the core and alloc crates of Rust using coq-of-rust. These are very large code bases, with a lot of unsafe or advanced Rust code. We present what we did to have a "best effort" translation of these crates. The resulting translation is in the following folders:

• CoqOfRust/alloc
• CoqOfRust/core

At Formal Land our mission is to reduce the cost of finding bugs in software. We use formal verification, that is to say mathematical reasoning on code, to make sure we find more bugs than with testing. As part of this effort, we are working on a tool coq-of-rust to translate Rust code to Coq, a proof assistant, to analyze Rust programs. Here we present a technical improvement we made in this tool.

One of the challenges of our translation from Rust to Coq is that the generated code is very verbose. The size increase is about ten folds in our examples. A reasons is that we use a monad to represent side effects in Coq, so we need to name each intermediate result and apply the bind operator. Here, we will present a monadic notation that prevents naming intermediate results to make the code more readable.

We explained how we started updating our translation tool coq-of-rust in our previous blog post, to support more of the Rust language. Our goal is to provide formal verification for the Rust 🦀 language, relying on the proof system Coq 🐓. We will see in this post how we continue implementing changes in coq-of-rust to:

1. remove the types from the translation,
2. be independent of the ordering of the definitions.

In our previous blog post, we stated our plan to improve our translation of Rust 🦀 to Coq 🐓 with coq-of-rust. We also provided a new definition for our Rust monad in Coq, and the definition of a unified type to represent any Rust values. We will now see how we modify the Rust implementation of coq-of-rust to make the generated code use these new definitions.

With this new translation strategy, to support more Rust code, we want:

1. to remove the types from the translation,
2. to avoid the need to order the definitions in the generated Coq code.

Our tool coq-of-rust is translating Rust 🦀 programs to the proof system Coq 🐓 to do formal verification on Rust programs. Even if we are able to verify realistic code, such as an ERC-20 smart contract, coq-of-rust still has some limitations:

• fragile trait handling
• difficulties in ordering the definitions, in their order of dependencies as required by Coq

We will present how we plan to improve our tool to address these limitations.

In this blog post, we present our development steps to build a tool to translate Go programs to the proof system Coq.

The goal is to formally verify Go programs to make them totally bug-free. It is actually possible to make a program totally bug-free, as formal verification can cover all execution cases and kinds of properties thanks to the use of mathematical methods. This corresponds to the highest level of the Evaluation Assurance Levels used for critical applications, such as the space industry.

All the code of our work is available on GitHub at github.com/formal-land/coq-of-go-experiment.