Posted on September 4, 2017 by Grigore Rosu
The Ethereum Virtual Machine (EVM) has been recently given a complete formal semantics using the K framework, as part of the open source KEVM project. The effort is described in detail in the KEVM technical report. The aim of the KEVM project is to develop a suite of formal analysis tools for smart contracts based on the formal semantics of the EVM. In other words, the only trust base for these tools will be the public EVM semantics, which is the best we can hope for. The KEVM team currently consists of researchers and developers at Runtime Verification and in the Formal Systems Laboratory at the University of Illinois, and the project is being partially funded by IOHK.
While defining the formal semantics of EVM in K, there were moments when we asked ourselves "Why did they do it this way?" Also, while verifying smart contracts using the semantics, we found some of the design choices made by the EVM designers questionable; if nothing else, they make verification harder. We have decided to then collect our thoughts during the semantic definition process and during verification of smart contracts after. They were bundled together with the KEVM definition, under issues.md. Here we restate them so you can find them all in one place in order to express your thoughts. Maybe it is not too late to re-design the EVM, this time with formal semantics and mathematical rigor in mind. If the blockchain technology is here is stay, then we should better build it on the most solid foundation that we can.
Issues with description of EVM
Yellow paper - informal EVM semantics
These can be ambiguities/confusing wording in the Yellow Paper.
EXTCODECOPYexamples, though strangely enough
BALANCEdoes specify what to do. We think the community has reached agreement on this though, "non-existing accounts are empty accounts" or something along those lines.
More broadly, many features of the EVM seem to be poorly designed. These can be issues from simple "why did they do it that way?" to "this makes doing formal reasoning about EVM harder".
SHA3is done). Another (albeit unlikely problem) is that of address-space collisions.
In addition to the above mentioned issues, there are several things that could be improved about EVM in general as a distributed computation language. Here we mention some.
Deterministic vs. Nondeterministic (and Proof of Work and Scalability)
Because EVM is deterministic, it takes as long to verify a computation as it takes to run a computation. In both cases, the entire program must be executed; there is no choice about what the next step to take is.
In a nondeterministic language, execution is finding one execution path among many which "solves" the program. For example, any logical language where there are several possible next inference steps is nondeterministic (eg. Prolog, Maude, K, Coq). However, once a solution is found, presenting it is telling which choices were made at each nondeterministic step; verifying it is following that same sequence of steps. If at each step there are a choice from
M inference rules, and it takes
n steps to reach a solution, then the speedup in verifying is
One of the goals in a consensus-driven distributed store is scalability, which means as more resources are added to the network the network gets stronger. Using a deterministic language means that we lose at least one dimension of this scalability; everyone verifying the state of the world must do as much work as it took to compute the state of the world. Even many functional languages, by having evaluation strategies settled ahead of time, are deterministic (though they may have elegant ways of encoding nondeterministic systems).
On the other hand, what secures many of these blockchain-consensus systems is proof of work. Proof of work is the ultimate non-deterministic programming language; the programs are the blocks (before adding the nonce), and the solutions are the nonce added to the blocks so that it hashes low enough. When using a nonce of size
2^N, there are exactly
M = 2^N next "inference steps", and they all must be searched uniformly to find a solution. If instead the underlying programming language had some nondeterminism, some of the proof of work could be done just by executing the transactions going into the block. Perhaps the two can be used to augment each other, allowing for some of the proof of work to be provided via finding a solution to the program and the rest via hashing.
If such a system were implemented, it may be important to incentivize miners to supply solutions to programs/proofs on the blockchain. Perhaps a system where the time between when a specification/theorem is submitted to the blockchain and when it is solved determines the reward for the computation could be used. Natural incentive to place proofs of theorems on the blockchain would be provided in the form of the reward; this means it's against the miners interests to ignore transactions. The hard part is incentivizing placing theorems on the blockchain early (as it may be advantageous to hoard theorems so that you can submit solutions early to collect the reward).
The gas mechanic in EVM is designed to ensure that every program terminates so that users can't DOS the miners by submitting infinite computations. However, there is no such guarantee that the proof of work computation done by miners terminates; there may be no combination of ordering of transactions and a nonce that yields a solution (though this is incredibly improbable). Instead, we can leave it up to the miner to decide if pursuing a computation is worth the time lost in the pursuit. Indeed, this directly increases the amount of work possible behind a proof of work, as much more useless work has been added to the system (via computations that don't terminate).
In many sufficiently powerful nondeterministic languages, there will be plenty of execution search paths which do not terminate. However, automated provers (execution engines) for these languages don't throw up their hands, instead they design better search tactics for the language. It's not clear that leaving the burden of which transactions to attempt to the miner is entirely bad, especially when coupled with a system which rewards more for longer-standing transactions.
The problem with this, it turns out, is not that users may DOS miners, but that miners may DOS other miners (by presenting blocks that they purport terminate).
Language independence is difficult to achieve in a distributed system because everyone must agree on how programs are to be executed. Two approaches are the language-building language approach and the consensus-based approach.
In the language-building language approach, the underlying language of the blockchain is a language-building language. Thus, contracts are free to introduce new languages simply as specifications (programs) in the underlying language, and other contracts may use those languages by referring to the language definition contract. As a very simple example, if the underlying language was K, then you could submit a contract that is just a K definition giving semantics to the language you want to use in the future. Along this line, we should use a logical framework as the underlying language. Logical frameworks exhibit both non-determinism and language independence, making two improvements to EVM at the same time.
The consensus-based approach is more flexible in the interpretation of "correct" executions of programs. Essentially, everyone would vote on which execution is correct by rejecting ill-formed blocks (ill-formed here includes blocks which do not report a correct execution). This lets the definition of the underlying languages evolve out of band; major changes to the semantics would essentially require widespread network agreement or a fork. Indeed, the only thing that should be stored on the blockchain would be a hash of the program.
These two techniques could perhaps be combined.