This is the start page about my efforts around smart contract verification.
The goal is to establish a method how to verify a smart contract so that no surprises happen after their deployment.
- gave a talk in DEVCON 1
- Berlin, 2016-11-1; gave a talk in Berlin Ethereum Meetup (video)
- Paris, EDCON, 2017-02-17 slide video
- Cambridge, ARM Research Summit, 2017-09-13 slide
- every update comes here: a gitter channel
- an Isabelle/HOL repo
- Solidity
- a Coq repo and a screen cast
- FP Ethereum community
- What are formal methods
- Verification of EVM bytecodes
- Verification of Solidity Programs
- A Safe Programming Language
- Dr-Y's contract analyzer
- Transaction visualization
- Resources
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?
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.
Coq proofs are currently lengthy.Isabelle/HOL made the proofs much shorter.- I believe Isabelle/HOL provides much easier user experience (because it has a well-polished machine word library). I've ported the Coq attempt into Isabelle/HOL.
- At the bytecode level, it's harder to see what the code is doing and what to expect.
- One solution is to make the Solidity compiler annotate the bytecode with the expected properties at specific code location.
- At the bytecode level, Solidity array access looks like storage access with Kaccek hashes, and somehow we need to assume no collisions. If I assume
∀ a, b. keccak(a) = keccak(b) -> a = b, using the pigeon hole argument, I can prove0 = 1and everything.- I can locally say
sorryoradmitto indicate that I give up proofs whenever I have to provekeccak(a) != keccak(b)becausea != b. Then the proofs would be incomplete and I cannot call my results "theorems", but I'm happy that way. Anyway the compiler assumes no hash collisions without logical justification (but empirical). - The module system of Coq provides a clever workaround.
- I can locally say
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)
choose Coq or Isabelle/HOL (overnight)I chose Isabelle/HOL over Coq.verifyThis is finished and there is a report.Deedand some other simple bytecode programs against simple properties (6-10 days)translate the definitions into Lem (2 weeks; almost done except the Keccak hash)done.develop a method how to verify assertions between opcodes (this is evmverif#5) (a week; there is a milestone for this item)cover all opcodes (3 days): this is already in progress. A milestone. mostly done,but LOGx does nothing right nowtest 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- ~~build a simple Hoare logic
- combine the Hoare logic with an invariant tracking technique
- develop Ethereum ABI
- implement the packaging ABI
- extend the model so that it can run state-tests
- implement verification-condition generation -- the desired post-condition and invariant annotations at JUMPDESTs would generate the formulas to prove.
- implement a wallet (might be between 8. and 9.)
- build decompilation of EVM bytecode into a recursive function in a theorem prover
- try to automate the process of verification / finding vulnerabilities
- My EVM in Isabelle/HOL says "your memory contents might change after you CALL another account", and I'm like "no, that's paranoid."
- The verification of Deed contract finishes. I break the contract to see what happens, then the proofs still work. I had a bug in my JUMPI implementation.
- I try to verify the Deed contract again, I cannot prove the safety property anymore, and I find that one precondition was missing about
activeflag. - I added gas to the EVM and run the Deed proofs again, it now takes overnight. I forgot to
timeit. - The OCaml extraction and the Isabelle/HOL extraction were using different endianness in the hash implementation.
Another way would be to verify Solidity sources somehow, not looking at the EVM bytecode.
- The only way to know the meaning of a Solidity program is to compile it into bytecodes.
- The Solidity compiler is changing fast and the verification tools would need to follow the changes
- The verification tools tend to believe a different behavior from that of actually deployed bytecode
The steps that have to be taken:
- 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*.
- Check the above against the reality. We need a big set of tests to compare the above translation against the bytecode.
- Translate the ML implementation into a proof assistant (or we rely on Why3, in that case we need to trust the SMT solvers)
- Try to assert properties in a shallow-embedded way and write proofs
- Automate the process, maybe by deep-embedding some kind of Hoare logic
- Vitalik's Casper with dynamic validator sets https://medium.com/@pirapira/a-mechanized-safety-proof-for-pos-with-dynamic-validators-17e9b45faff4#.94adc75cm
- Vlad's Casper until Consensus Safety https://medium.com/@pirapira/formal-methods-on-another-casper-8a75f6e02073#.qdps9277i
- Vitalik's Capser with static validator set https://medium.com/@pirapira/formal-methods-on-some-pos-stuff-e309775c2ab8#.vaaa77dut
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
- no loops or recursions
- this makes life much easier for static analyzers
- gas consumption is stabler
- users would need to call it again and again
- persistent program counter
- this discourages multiple workflows in a single contract
- reentrancy does not jump to far away in the source code, but reentrancy arrives around the last sentence executed
- protection against reentrancy
- explcit storage setting at every exit
It is inspired by an existing language but I will talk about it when it's actually working.
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.
A quick hack to visualize the dataflow in a transaction. This is useful after a surprise.
- Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
- most Ethereum transactions so far are "effectively call back free"