Verification of smart contracts

Dr. Lars Hupel

Dieser Artikel ist auch auf Deutsch verfügbar

Fatal flaws

In Ethereum a faulty smart contract became sadly notorious. From a so-called DAO (decentralized autonomous organization) an eight-figure USD amount was diverted. The historical background has already been described by Stefan Tilkov und Marc Jansing (in German). Basically, the DAO serves as an example of a contract, which, on the one hand, administers significant volumes of investments, but on the other hand was flawed and consequently led to severe financial losses.

There is no reason to assume that the series of spectacular bugs that have become known so far could not continue. In this article, I will not address the philosophical discussions of whether the code is sacrosanct and that such bugs are consequently merely features; this has already been discussed by others. However, it is important to note that, in contrast to paper-based contracts, there is no court that could interpret and correct a smart contract.

There are many other smart contracts that have high transaction volumes and/or a high account balance, making them especially attractive for attempted attacks.

For the first case, Blockspur has prepared a list. As of February 2019, this list shows a total of six smart contracts for which the average total of monthly incoming transactions exceeds USD 10 million. The largest contract has monthly revenues of just over 47 million; this is a contract for the Kraken exchange.

For the second case, a list of addresses can be viewed on Etherscan, showing the current highest account balance. In February 2019, this was by far the contract for the ERC-20 token Wrapped Ether; which currently controls over 2% of all existing ethers, corresponding to about USD 320 million. This can justifiably be called a contract that is too big to fail.

A contract that is rolled out in the blockchain is usually present in the source text (usually Solidity) only for the creator. The blockchain and all other participants see only the bytecode of EVM (Ethereum VM). Conceptually, this is comparable to Java code, which is compiled in JVM bytecode. Beyond this, Etherscan also offers the ability to publish the source text and check whether, after compilation, it is identical to the bytecode present in the blockchain. In the case of wrapped ether it can thus be seen that it is a contract with about 80 lines (plus license), which is similar to the official ERC-20 template.

In addition to ERC-20 tokens and exchanges, there is also a third type of frequently used contract: the so-called wallets. Parity is an example of a wallet that offers additional functions, such as administration of multiple authorized signatories.

Another analysis concludes that just 1% of all smart contracts received more than 100 calls. Nevertheless, somewhat more than one-third of all Ethereum transactions are contract calls.

Complete correctness

The problem is that a smart contract is carved in stone and that subsequent changes are impossible. As experience shows, software contains errors. Even worse: Usually, a specification is actually missing completely. When these factors are combined with the fact that a lot of money is handled with these contracts, it results in a particularly explosive mixture.

Luckily, software development knows a number of methods that can improve code quality. The simplest and most economical option for this purpose is testing. Alexey Novakov has already reported on the Truffle Framework, a framework that can be used not only to create and administer Ethereum contracts, but also test them. It is thus quite conceivable that popular approaches, such as TDD, could also be used for smart contracts. Even test coverage can be measured with Solidity.

Now let’s put the blockchain context aside for a moment. With tests, it is possible to show the absence of certain errors, but never the absence of all errors. As Edsger W. Dijkstra already said in 1972 in his ACM Turing Lecture:

Program testing can be a very effective way to show the presence of bugs, but is hopelessly inadequate for showing their absence.

So how can the absence of bugs be demonstrated? It has to be proven. For this purpose there are numerous methods that use mathematics and logic to ensure that a certain program code complies with a certain specification. That in itself is nothing new, because this concept is already known in various (object-oriented) programming languages as contract-based programming. The term contract here has nothing to do with smart contracts! Instead, in this context, it is about testing the correctness of functions, regardless of whether these functions run on the blockchain or a JVM.

There are systems for contract-based programming for numerous programming languages, including Ada and Eiffel as pioneers, but also Java, C#, and C++.

@Requires("x >= 0")
@Ensures("result >= 0")
static double sqrt(double x);

Most of these tools, however, are not really helpful for verification purposes, because, as a rule, only a runtime test is done. However, even before runtime, it is necessary to know that the specification has been complied with. I have already written about this principle and a particular tool elsewhere (in German). To put it briefly, it is possible, but it takes a bit more effort. In the case of Java, the situation is poor to middling. With the @Contract annotation, JetBrains includes its own primitive mechanism, but it permits only very limited conclusions regarding the program semantics:

The @Contract annotation lets you specify a set of rules (a contract) that a method must follow. If the contract is violated, IntelliJ IDEA reports a problem.

For smart contracts used to move around millions of euros, however, zero checks are inadequate. It’s time to roll out the heavy guns:

1. A completely specified business case
2. A smart contract programming language with defined semantics
3. A smart contract VM with defined semantics
4. A correct compiler for VM bytecode
5. Nodes that implement the VM correctly

Although such a stack does already exist in industrial applications, the blockchain world is still far away from that. Here, I would like to provide a brief summary of what already exists and prognosticate where the journey is likely to lead.

The EVM itself has already been formalized in a number of systems (Isabelle, Imandra, K). Simultaneously, however, some of these formalisms are executable, meaning that can be transformed into program code, which would be an implementation of item 5. At the present time, however, items 2 and 4 constitute the greatest weakness. Solidity, the most frequently used language for Ethereum contracts, is notoriously difficult to understand. This is also demonstrated by the list of known attack vectors. For a good language design, such lists should be very short. This is also the reason why web applications are not usually implemented in C, but in high-level languages.

However, this area is being worked on in academics. The third Workshop on Trusted Smart Contracts will take place in 2019. Runtime Verification is working on verification of ERC-20 tokens and a Solidity semantics prototype. These analyses have already revealed subtle errors in simple smart contracts, such as > instead of < or =+ instead of +=.

In the area of language design, there has also been progress. IOHK has selected a variant of standardized lambda calculus as the basis for its new smart contract language Plutus. This calculus is understood very well scientifically and, for the purposes of Plutus, was formalized in the Agda theorem-proving language. The high-level language itself is an embedded DSL in Haskell, which consciously dispenses with certain difficult-to-analyze constructs. There is still no toolchain for the verification of contracts; nevertheless, the selection of these technologies has laid the foundation for one.

The intermediate language Scilla, which is formalized with the theorem-proving system Coq, goes a step further. In this area there are already theorem-proving approaches for contracts. In the paper by Sergey, Kumar, and Hobor, a contract is developed for crowdfunding platforms that work in a manner similar to Kickstarter. To put it briefly, any number of backers should be able to make donations. If the campaign is successful, the owner gets all the donations. Otherwise, the backers can get their money back. In the theorem-proving language, this last requirement is formulated as follows:

Theorem can_claim_back id b d st bc:
  (* (a) The backer b has donated d, so the contract holds
     that record in its state *)
  donated b d st →
  (* (b) The campaign has not been funded. *)
  ¬funded (state st) →
  (* (c) Balance is small: not reached the goal. *)
  balance st < (get_goal (state st)) →
  (* (d) Block number exceeds the deadline. *)
  get_max_block (state st) < block_num bc →
  (* (conclusion) Backer b can get their donation back. *)
  ∃(m : message),
    sender m == b ∧
      out (step_prot c st bc m) = Some (Msg d id b 0 ok_msg)

Actually, this is merely a statement, not yet a proof, which the authors have unfortunately not made publicly available. And yet, they claim that it is only about ten lines long. Nevertheless, the problem is that proofs have to be carried out in a language to which programmers are unaccustomed. Furthermore, Scilla still does not have any realistic implementation of the language on a public blockchain.

Adequate effort?

The question remains open as to whether it is worth the effort. In industry, there are already isolated verification projects of a significant scope. A lighthouse project for the Isabelle system is the verification of the operating system kernel seL4. In their pioneering article from 2009 Klein et al. write:

Complete formal verification is the only known way to guarantee that a system is free of programming errors. We present our experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation. We assume correctness of compiler, assembly code, and hardware, and we used a unique design approach that fuses formal and operating systems techniques. […] Functional correctness means here that the implementation always strictly follows our high-level abstract specification of kernel behaviour. This encompasses traditional design and implementation safety properties such as the kernel will never crash, and it will never perform an unsafe operation. It also proves much more: we can predict precisely how the kernel will behave in every possible situation.

This high standard of assurances is also desirable when juggling great sums of money without any legal safety net. However, it has its price:

The cost of the proof is higher, in total about 20 [person years]. This includes significant research and about 9 py invested in formal language frameworks, proof tools, proof automation, theorem prover extensions and libraries. The total effort for the seL4-specific proof was 11 py.

The authors also state that the usual estimation rule for meeting the EAL6 common criteria is USD 10,000 per line of code. And yet EAL6 is a lower standard than formal verification with Isabelle, as was done in the seL4 project.

It is therefore necessary to consider carefully what is more expensive: the costly development of smart contracts secured through formal methods or the costly potential loss of great sums of money. In systems like seL4, which are used as microkernels in many devices, the considerations also have to include human life, which could be endangered by faulty software:

More than 30 years of research in theorem proving has addressed this issue, and we can now achieve a degree of trustworthiness of formal, machine-checked proof that far surpasses the confidence levels we rely on in engineering or mathematics for our daily survival.

Large parts of the paper can be followed without a knowledge of theoretical informatics, and they include some valuable information on the state of the art.

Meta-methods

Regardless of the considerations above, it is also conceivable that proofs could also be integrated in the blockchain itself. Like many other mathematical problems, proofs are difficult to execute but easy to test. Such problems are sometimes also referred to as one-way functions. For example, hash-algorithms are purposely designed so that the hash can be calculated simply from the text; but not conversely the text from the hash. With proofs the situation is similar: If there is a proof, it is possible to determine quickly whether a certain statement has been proven, but the reverse path is an undecidable problem.

In the past, therefore, there have already been attempts to offer rewards for proofs. One example of such a project was the Proof Market, where one could state a claim of some kind and attach a reward to it (Bitcoin). Anyone who successfully proved the claim got the reward. Unfortunately, essentially only faulty proofs were submitted, which utilized the known gaps in the checker. Accordingly, the page was closed in 2015.

Another project – Qeditas from IOHK – wanted to encourage the setup of a library of formalized mathematics. However, since the launch, not much has happened.

For now, therefore, the idea of uncoupling the development process of smart contracts from their verification – perhaps even doing the latter through crowdsourcing – remains just a vision.