Formalizing Ethereum transactions

A new addition to the project of formalizing Ethereum and proving Ethereum contracts correct is the formalization of transactions. The definitions can be found at block.lem.

The Ethereum project has a set of tests called state tests at https://github.com/ethereum/tests/tree/develop/StateTests. These can be used to ensure that the new definitions agree with what is implemented in the clients. Quite many of the tests are working already. One part that is needed by some state tests are precompiled contracts. At least the ECDSA contract will have to be specified because it is useful in many situations. Now is the best time to refactor the definitions (because no proofs depend on them), so please take a look!

One trade-off is that the definitions must be efficient enough to execute. Some of the state tests seem to take too much time, or perhaps there are some bugs that cause infinite loops. Perhaps it could be useful to test using real transactions from the blockchain one day.

Motivation

There are several reasons why it is important to formalize Ethereum transactions. Perhaps the most obvious is that most applications use a combination of several contracts, and so the correctness of a contract depends on the specification of other contracts.

Even if there is only one contract, the semantics of calls have to be specified and this is difficult because of the re-entrance problem. Note that basically all contracts are affected by this issue. Re-entrance is perhaps even more complex when there are multiple contracts in the system that we want to prove correct. There are already valid reasoning principles that can be used to prove re-entrant programs correct, so I think it is now time to prove their correctness. Also different principles might be needed in different situations. Next I’ll try to sketch what could be the simplest way to prove correctness of re-entrant contracts.

Assume our contract is supposed to have invariant P. When we make a call, we need to assume that re-entrant calls preserve this invariant. To solve this problem, we can use induction, and assume that the invariant P will hold, if there is less than k gas left, where k is the gas we assume to have at the beginning of the transaction. The main result we need is that each call will return to environment so that they have only modified the storage of the called contract. Also the amount of gas must be lower after the call. Well there are many technical issues, but after resolving them we can then compose these triples, and get the desired result: the invariant will hold after the call, if it holds before it. We can also have parameterized invariant P(x), here the difference is that value of x can be different in the subcalls.

It should be quite straightforward to expand the definitions to cover multiple transactions and blocks. Then we can start proving properties such as that it is actually possible to get your ether back from a wallet, or that if a group owns majority of shares, their choice wins a vote. This kind of properties could perhaps be formalized as axiomatic principles, but it seems that there are some advantages for using multi-contract approach.

Consider first that a user wants to perform a transaction. Because the user cannot know that her transaction is the first one, this causes an additional level of non-determinism. This non-determinism can be removed by instead having a contract that will select the correct action for a given state.

Another problem is that even if we can mathematically prove that an agent has a good strategy, it might not be effective (maybe the strategy requires inverting a hash function etc.) We can use a contract to ensure that the strategy has low complexity.

So in general, the approach would be this: for each agent that is supposed to follow the strategy, have a surrogate contract that can be controlled by the strategy contract. We can assume that the strategy contract has only one method with no parameters, and that it is called once per block. Then the desired property just has to be proven to this contract as normal pre- and post-conditions. Note that for this to be completely reliable, the proof has to be constructive, in the sense that we must get an actual contract as the strategy.