Home

Awesome

Formal Verification of Ethereum Contracts (Yoichi's attempts)

This is the start page about my efforts around smart contract verification.

Goal

The goal is to establish a method how to verify a smart contract so that no surprises happen after their deployment.

Talks

Links

The rest of the page

What are formal methods

What are formal methods? The word "formal" here is about looking at the shape, not at the meaning, of mathematical proofs.

For a long time, mathematical proofs were read, understood and then checked. In some cases you can do calculations like "a + b - b = a" by just looking at the form, saying something like "this cancels that". Still, in the usual practice of mathematics, you ought to be able to explain what is going on. You need to understand.

In the first half of 20th century, rigid languages appeared where proofs can be checked by machines. You can see examples here. Maybe the computers do not understand the meaning, but they can check the proofs.

When you translate mathematical texts into such machine-readable proofs, you are "formalizing" mathematics. Recent decades saw a tantalizing progress in this area. The Flyspeck project and CoqFiniteGroups formalized big results from the past centuries. The Homotopy Type Theory was formalized from its very early stages.

So far this was about mathematics. The take away is, you can obtain infinitely many truths at one shot. The equality "a + b - b = a" is true for any natural numbers. By the way, here we have a smart contract, whose input is actually only finitely many. Can we do something about this?

Path a: Verification of EVM bytecodes (currently followed)

One way is to look at the EVM bytecodes. They are executed on a simple virtual machine. The rules of the virtual machine is well understood by different Ethereum clients which usually match (otherwise they fix the difference with uttermost priority). The current attempt in Coq is in evmverif repository, and there is a screen cast.

Obstacles

Steps on Path a

  1. try Isabelle/HOL to see if proofs are really 5 times easier there (less than a week)
    • By the way, about the trustworthiness, I would put Isabelle/HOL at least as good as Coq because Isabelle/HOL is based on a simpler deduction system (a deduction system is not a piece of software; it is a bunch of inference rules usually written in LaTeX)
  2. choose Coq or Isabelle/HOL (overnight) I chose Isabelle/HOL over Coq.
  3. verify Deed and some other simple bytecode programs against simple properties (6-10 days) This is finished and there is a report.
  4. translate the definitions into Lem (2 weeks; almost done except the Keccak hash) done.
  5. develop a method how to verify assertions between opcodes (this is evmverif#5) (a week; there is a milestone for this item)
  6. cover all opcodes (3 days): this is already in progress. A milestone. mostly done, but LOGx does nothing right now
  7. test the new EVM against the standard VM tests (4 weeks; started, now parsing the tests) mostly done. but VM tests involving multiple contracts are still skipped
  8. ~~build a simple Hoare logic
  9. combine the Hoare logic with an invariant tracking technique
  10. develop Ethereum ABI
  11. implement the packaging ABI
  12. extend the model so that it can run state-tests
  13. implement verification-condition generation -- the desired post-condition and invariant annotations at JUMPDESTs would generate the formulas to prove.
  14. implement a wallet (might be between 8. and 9.)
  15. build decompilation of EVM bytecode into a recursive function in a theorem prover
  16. try to automate the process of verification / finding vulnerabilities

Personal Account of the Struggle

Path b: Verification of Solidity programs

Another way would be to verify Solidity sources somehow, not looking at the EVM bytecode.

Obstacles

Steps on this path

The steps that have to be taken:

  1. Know Solidity program's meaning without checking the bytecode. For this, one way is to write a Solidity interpreter in Coq or in an ML language. Another way is to compile a Solidity program into WhyML or F*.
  2. Check the above against the reality. We need a big set of tests to compare the above translation against the bytecode.
  3. Translate the ML implementation into a proof assistant (or we rely on Why3, in that case we need to trust the SMT solvers)
  4. Try to assert properties in a shallow-embedded way and write proofs
  5. Automate the process, maybe by deep-embedding some kind of Hoare logic

Related Projects

Sideway: Formal Verificaton of Proof-of-Stake Protocols

Sideway: a safe programming language

This alone does not verify smart contracts, but I have a chance to make it static analyzer friendly.

The bamboo compiler is now producing snippets of bytecode for the empty contract (still lots to be done).

The language has

It is inspired by an existing language but I will talk about it when it's actually working.

Sideway: Dr-Y's contract analyzer

The contract analyzer needs an overhaul in the functionality and the UX. I want to see the meaning of each basic block, and how the execution can jump around the basic blocks.

Sideway: transaction visualization

A quick hack to visualize the dataflow in a transaction. This is useful after a surprise.

Resources

An Incomplete List of Papers I Saw