Verification of the Incremental Merkle Tree Algorithm with Dafny

More precisely, the transactions are programmatically performed by programs called smart contracts. If there are real advantages having smart contracts act as third-parties to process transactions, there are also lots of risks that are inherent to computer programs: they can contain bugs. Bugs can trigger runtime errors like division by zero or array-out-of-bounds. In a networked environment these types of vulnerabilities can be exploited by malicious attackers over the network to disrupt or take control of the computer system. Other types of bugs can also compromise the business logic of a system, e.g., an implementation may contain subtle errors (e.g., using a += operator in C instead of =+) that make them deviate from the initial intended specifications.

Unfortunately it is extremely hard to guarantee that programs and henceforth smart contracts implement the correct business logics, that they are free of common runtime errors, or that they never run into a non-terminating computation.¹¹1In the Ethereum ecosystem, programs can only use a limited amount of resources, determined by the gas limit. So one could argue that non-terminating computations are not problematic as they cannot arise: when the gas limit is reached a computation is aborted and has no side effects. It follows that a non-terminating computation (say an infinite loop due to a programming error) combined with a finite gas limit will abort and will result in the system being unable to successfully process some or all valid transactions and this is a serious issue. There are notorious examples of smart contract vulnerabilities that have been exploited and publicly reported: in 2016, a reentrance vulnerability in the Decentralised Autonomous Organisation (DAO) smart contract was exploited to steal more than USD50 Million. There may be several non officially reported similar attacks that have resulted in the loss of assets.

The next generation of Ethereum-based networks, Ethereum 2.0, features a new proof-of-stake consensus protocol. Instead of miners used in Ethereum 1.x, the new protocol relies on validators to create and validate blocks of transactions that are added to the ledger. The protocol is designed to be fault-tolerant to up to $1/3$ of Byzantine (i.e., malicious or dishonest) validators. To discourage validators to deviate from an honest behaviour, they have to stake some assets in Ether (a crypto-currency), and if they are dishonest they can be slashed and lose (part of) their stake. The process of staking is handled by the Deposit Smart Contract (DSC): a validator sends a transaction (“stake some Ether”) by calling the DSC. The DSC has a state and can update/record the history of deposits that have occurred so far.

As a result the DSC is a mission-critical component of Ethereum 2.0, and any errors/crashes could result in inaccurate tracking of the deposits or downtime which in turn may compromise the integrity/availability of the whole system.

This could be mitigated if the DSC was a simple piece of code, but, for performance reasons, it relies on sophisticated data structures and algorithms to maintain the list of deposits so that they can be communicated over the network efficiently: the history of deposits is summarised as a unique number, a hash, computed using a Merkle (or Hash) tree. The tree is built incrementally using the incremental Merkle tree algorithm, and as stated in [21]:

“The efficient incremental algorithm leads to the DSC implementation being unintuitive, and makes it non-trivial to ensure its correctness.”

In this context, it is not surprising that substantial efforts, auditing, review [3], testing and formal verification [20, 21] has been invested to guarantee the reliability and integrity (e.g., resilience to potential attacks) of the DSC. The DSC has been the focus of an end-to-end analysis [21], including the bytecode²²2A limitation is that the bytecode is proved using a non-trusted manual specification. that is executed on the Ethereum Virtual Machine (EVM). However, the incremental Merkle tree algorithm has not been mechanically verified yet, even though a pen and paper proof has been proposed [20] and partially mechanised using the K-framework [5]. An example of the limitations of the mechanised part of the proof in [20] is that it does not contain a formal (K-)definition of Merkle trees. The mechanised sections (lemmas 7 and 9) pertain to some invariants of the algorithm but not to a proper correctness specification based on Merkle trees. The K-framework and KEVM, the formalisation of the EVM in K, has been used to analyse a number of other smart contracts [25]. There are several techniques and tools³³3https://github.com/leonardoalt/ethereum˙formal˙verification˙overview. e.g.,  [8, 9, 1, 6, 28], for auditing and analysing smart contracts written in Solidity (a popular language to write Ethereum smart contracts) or EVM bytecode, but they offer limited capabilities to verify complex functional requirements.

Interesting properties of incremental Merkle trees were established in [19] using the MONA prover. This work does not prove the algorithms in the DSC which are designed to minimise gas consumption and hence split into parts: insert a value in a tree, and compute the root hash. Moreover, some key lemmas in the proofs could not be discharged by MONA.

The gold standard in program correctness is a complete logical proof that can be mechanically checked by a prover. This is the problem we address in this paper: to design a machine-checkable proof for the DSC algorithms (not the bytecode) using the Dafny language and verifier. The DSC has been deployed in November 2020. To the best of our knowledge, our analysis, completed in October 2020, provided the first fully mechanised proof that the code logic was correct, and free of runtime errors. There seem to be few comparable case-studies of Dafny-verified (or other verification-aware programming languages like Whiley [23]) code bases. The most notorious and complex one is probably the IronFleet/IronClad [10] distributed system, along with some non-trivial algorithms like DPPL [2] or Red-Black trees [24], or operating systems, FreeRTOS scheduler [16], and ExpressOS [15]. Other proof assistants like Coq [22], Isabelle/HOL [18] or Lean [17] have also been extensively used to write machine-checkable proofs of algorithms [12, 27, 7, 26] and software systems [11, 14].

We present a thorough analysis of the incremental Merkle tree algorithm used in the DSC. Our results are available as software artefacts, written using the CAV-awarded Dafny⁴⁴4https://github.com/dafny-lang/dafny verification-aware programming language [13]. This provides a self-contained machine checkable and reproducible proof of the DSC algorithms. Our contribution is many-fold and includes:

• •

  a new original simple proof of the incremental Merkle tree algorithm. In contrast to the previous non-mechanised proof in [20] we do not attempt to directly prove the existing algorithm, but rather to design and refine it. Our proof is parametric in the height of the tree, and hash functions;

• •

  a logical specification using a formal definition of Merkle trees, and a new functional version of the algorithm that is proved correct against this specification; the functional version is used to specify the invariants for the proof of the imperative original version [4] of the algorithm;

• •

  a repository⁵⁵5https://github.com/ConsenSys/deposit-sc-dafny with the complete Dafny source code of the specification, the algorithms and the proofs, and comprehensive documentation;

• •

  some new provably correct simplifications/optimisations;

• •

  some reflections on the practicality of using a verification-aware programming language like Dafny and some lessons learned from this experience.

A complete (or perfect) binary tree is such that each non-leaf node has exactly two children, and the two children have the same height. An example of a complete binary tree is given in Figure 1. A Merkle (or hash) tree is a complete binary tree the nodes of which are decorated with hashes (fixed-size bit-vectors). The hash values of the leaves are given and the hash values of the internal (non-leaf) nodes are computed by combining the values of their children with a binary function $\mathbf{hash}$. It follows that a Merkle tree is a complete binary tree decorated with a synthesised attribute defined by a binary function.

Merkle trees are often used in distributed ledger systems to define a property of a collection of elements e.g., a list $L$ of values. This property can then be used instead of the collection itself to verify,⁶⁶6More precisely the verification result holds with high probability as the chosen hashing functions may (rarely) generate collisions. using a mechanism called Merkle proofs, that data received from a node in the distributed system is not corrupted. This is a crucial optimisation as the size of the collection is usually large (typically up to $2^{32}$) and using a compact representation is instrumental to obtain time and space efficient communication and a reasonable transactions’ processing throughput.

In this work, we are not concerned with Merkle proofs but rather with the (efficient) computation of the $\mathbf{hash}$ attribute on a Merkle tree.

The actual function used to compute the values of the internal nodes is not relevant in the incremental Merkle tree algorithms’ functional logics and without loss of generality we may treat it as a parameter i.e., a given binary function.⁷⁷7In the code base, the $\mathbf{hash}$ function is uninterpreted and its type is generic. In the sequel we assume that the decorations of the nodes are integers, and we use in the examples a simple function $\mathbf{hash}:\text{Int}\times\text{Int}\longrightarrow\text{Int}$ defined by $\mathbf{hash}(x,y)=x-y-1$ instead of an actual (e.g., sha256-based) hash function.

A complete binary tree of height⁸⁸8The height is the length of the longest path from the root to any leaf. $h$ has $2^{h}$ leaves and $2^{h+1}-1$ nodes. Given a list $L$ of integers (type Int) of size $|L|=2^{h}$, we let $T(L)$ be the Merkle tree for $L$: the values of the leaves of $T(L)$, from left to right, are the elements of $L$ and $T(L)$ is attributed with the $\mathbf{hash}$ function. The value of the attribute at the root of $T(L)$, the root hash, defines a property of the list $L$. It is straightforward to extend this definition to lists $L$ of size $|L|\leq 2^{h}$ by right-padding the list with zeroes (or any other default values.) Given a list $L$ of size $|L|\leq 2^{h}$, let $\overline{L}$ denote $L$ right-padded with $2^{h}-|L|$ default values. The Merkle tree associated with $L$ is $T(\overline{L})$, and the root hash of $L$ is the root hash of $T(\overline{L})$. Computing the root hash of a tree $T(\overline{L})$ requires to traverse all the nodes of the tree and thus is exponential in the height of the tree.

A typical use case of a Merkle tree in the context of Ethereum 2.0 is to represent properties of lists that grow monotonically. In the DSC, a Merkle tree is used to record the list of validators and their stakes or deposits. A compact representation of this list, as the root hash of a Merkle tree, is communicated to the nodes in the network rather than the tree (or list) itself. However, as mentioned before, each time a new deposit is appended to the list, computing the new root hash using a standard synthesised-attribute computation algorithm requires exponential time in $h$. This is clearly impractical in a distributed system like Ethereum in which the height of the tree is $32$ and the number of nodes is $2^{33}-1$.

Given (a tree height) $h>0$, $L$ a list with $|L|<2^{h}$, and $e$ a new element to add to $L$, the incremental Merkle tree problem (IMTP) is defined as follows:⁹⁹9Polynomial in the height of the tree $h$. The operator $+$ is list concatenation.

Can we find $\alpha(L)$ a polynomial-space abstraction of $T(L)$ such that we can compute in polynomial-time: 1) the root hash of $T(L)$ from $\alpha(L)$, and 2) the abstraction $\alpha(L+[e])$ from $\alpha(L)$ and $e$?

Linear-time/space algorithms to solve the IMTP were originally proposed by V. Buterin in [4]. However, the correctness of these algorithms is not obvious. In the next section, we analyse the IMTP, and we present the main properties that enable us to design polynomial-time recursive algorithms and to verify them.

A path $\pi$ from the root of a tree to a node can be defined as a sequence of bits (left or right) in $\{0,1\}^{*}$. In a Merkle tree of height $h$, the length, $|\pi|$, of $\pi$ is at most $h$. $\nu(\pi)$ is the node at the end of $\pi$. If $|\pi|=h$ then $\nu(\pi)$ is a leaf. For instance $\nu(\varepsilon)$ is the root of the tree, $\nu(0)$ in Figure 1 is the node carrying the value $-8$ and $\nu(1.0.0)$ is a leaf. The right sibling of a left node of the form $\nu(\pi.0)$ is the node $\nu(\pi.1)$. Left siblings are defined symmetrically. A node in a Merkle tree is associated with a level which is the distance from the node to a leaf in the tree. Leaves are at level $0$ and the root is at level $h$. In a Merkle tree, level $0$ has $2^{h}$ leaves that can be indexed left to right from $0$ to $2^{h}-1$. The $n$-th leaf of the tree for $0\leq n<2^{h}$ is the leaf at index $n$.

We first show that the root hash can be computed if we know the values of the siblings of the nodes on any path, and the value at the end of the path. For instance, If we know the values of the left and right siblings (shaded nodes) of the nodes on $\pi_{1}$ (green path in Figure 1), and the value at the end of $\pi_{1}$, we can compute the root hash of the tree by propagating upwards the attribute $\mathbf{hash}$. The value of the $\mathbf{hash}$ attribute at $\nu(1.0)$ is $\mathbf{hash}(4,\nu(1.0.1))=3$, at $\nu(1)$ it is $\mathbf{hash}(3,\nu(1.1))=3$ and at the root $\mathbf{hash}(\nu(0),\nu(1))=\mathbf{hash}(-8,3)=-12$.

Algorithm computeRootUp (Listing A.1) computes¹⁰¹⁰10For $l=l^{\prime}+x$, $\mathtt{last}(l)=x$, $\mathtt{init}(l)=l^{\prime}$, and for $l=x+l^{\prime}$, $\mathtt{first}(l)=x$, $\mathtt{tail}(l)=l^{\prime}$. bottom-up in time linear in $|\mathtt{p}|$ the root hash with left the list of values of the left siblings (top-down) on a path p (top-down), right the values of the right siblings (top-down) and seed the value at $\nu(\mathtt{p})$. The generic version (uninterpreted hash) of the algorithm is provided in the ComputeRootPath.dfy file.

For the green path $\mathtt{pi}_{1}=[1,0,0]$ in Figure 1, $\mathtt{left}=[-8,i_{1},i_{0}]$, $\mathtt{right}=[-1,-1,0]$ and the seed is $4$. The evaluation of computeRootUp returns $-12$.

Given a path $\pi$, if the leaves on the right of $\nu(\pi)$ all have the default value $0$, the values of the right siblings on the path $\pi$ only depend on the level of the sibling in the tree. For example, the leaves on the right of $\pi_{1}$ (orange in Figure 1) all have the default value $0$. The root hash of a tree in which all the leaves have the same default value only depends on the level of the root: $0$ at level $0$, $\mathbf{hash}(0,0)$ at level $1$, $\mathbf{hash}(\mathbf{hash}(0,0),\mathbf{hash}(0,0))$ at level $2$ and so on. Let $\mathbf{zero}^{l}$ be defined by: $\mathbf{zero}^{l}=0\text{ if $l=0$ else $\mathbf{hash}(\mathbf{zero}_{0}^{l-1},\mathbf{zero}_{0}^{l-1})$}$.

Given a path $\pi$, if all the leaves on the right of $\nu(\pi)$ have the default value, any right sibling value at level $l$ on $\pi$ is equal to $\mathbf{zero}^{l}$.

As an example in Figure 1, the right siblings on $\pi_{1}=1.0.0$ have values $0$ at level $0$, node $\nu(1.0.1)$, and $\mathbf{hash}(0,0)=\mathbf{zero}^{1}=-1$ at level $1$, node $\nu(1.1)$. If a path p leads to a node with the default value $0$ and all the leaves right of $\nu(\mathtt{p})$ have the default value $0$, the root hash depends only on the values of the left and default right siblings. Hence the root hash can be obtained by computeRootUp(p, left, right, 0). For the path $\mathtt{pi2}=[1,0,1]$ (Figure 1), $\mathtt{left}=[-8,i_{1},4]$, $\mathtt{right}=[-1,-1,0]$, computeRootUp(pi2, left, right, 0) returns $-12$.

As a result, to compute the root hash of a tree $T(\overline{L})$, we can use a compact abstraction $\alpha(L)$ of $T(\overline{L})$ composed of the left siblings vector $b$ and the right siblings default values $z$ (Figure 1) of the path to the $|L|$-th leaf in $T(\overline{L})$.

Assume $\pi_{1}$ is a path to the $n$-th leaf and $n<2^{h}-1$ (not the last leaf), where the next value $v$ is to be inserted. As we have shown before, if we have $b_{1}$ holding the values of left siblings of $\pi_{1}$, $z$ and $v$, we can compute the new attribute values of the nodes on $\pi_{1}$ and the new root hash after $v$ is inserted. Let $\pi_{2}$ be the path to the $n+1$-th leaf. If we can compute the values $b_{2}$ of the left siblings of $\pi_{2}$ as a function of $b_{1}$, $z$ and $v$, we have an efficient algorithm to incrementally compute the root hash of a Merkle tree: we keep track of the values of the left siblings $b$ on the path to the next available leaf, and iterate this process each time a new value is inserted.

As $\nu(\pi_{1})$ is not the last leaf, $\pi_{1}$ must contain at least one $0$, and has the form¹¹¹¹11$x^{k},x\in\{0,1\}$ denotes the sequence of $k$ $x$’s. $\pi_{1}=w.0.1^{k}$ with $w\in\{0,1\}^{*},k\geq 0$. Hence, the path $\pi_{2}$ to the $n+1$-th leaf is $w.1.0^{k}$, arithmetically $\pi_{2}=\pi_{1}+1$. An example of two consecutive paths is given in Figure 1 with $\pi_{1}$ (green) and $\pi_{2}$ (blue) to the leaves at indices $4$ and $5$.

The related forms of $\pi_{1}$ (a path) and $\pi_{2}$ (the successor path) are useful to figure out how to incrementally compute the left siblings vector $b_{2}$ for $\pi_{2}$:

• •

  as the initial prefix $w$ is the same in $\pi_{1}$ and $\pi_{2}$, the values of the left siblings on the nodes of $w$ are the same in $b_{1}$ and $b_{2}$;

• •

  all the nodes in the suffix $0^{k}$ of $\pi_{2}$ are left nodes and have right siblings. It follows that the corresponding $k$ values in $b_{2}$ are irrelevant as they correspond to right siblings, and we can re-use the corresponding $b_{1}$ values;

• •

  hence $b_{2}$ is equal to $b_{1}$ except possibly for the level of the node at $\nu(w.0)$.

We now illustrate how to compute the new value in the vector $b_{2}$ on the example of Figure 1. Let $\pi_{1}=w.0$ and $\pi_{2}=w.1$ with $w=1.0$ and $|w|=2$. For the top levels $2$ and $1$, $b_{2}$ is the same as $b_{1}$: $b_{2}[2]=b_{1}[2]=-8$ and $b_{2}[1]=b_{1}[1]=i_{1}$. For level $0$, the level of the node $\nu(w.0)$, the value at $\nu(w.0)=\nu(1.0.0)$ becomes the left sibling of the node $\nu(1.0.1)$ on $\pi_{2}$ at this level. So the new value of the left sibling on $\pi_{2}$ is exactly the new value, $4$, of the node $\nu(1.0.0)$ after $4$ is inserted.

More generally, when computing the new root hash bottom-up on $\pi_{1}$, the first time we encounter a left node, at level $d$, we update the corresponding value of $b$ with the computed value of the attribute on $\pi_{1}$ at level $d$. Algorithm¹²¹²12$+$ stands for list concatenation. insertValue in Listing A.2 computes, in linear-time, the list of values of the left siblings (top-down) of the path $\mathtt{p}+1$ using as input the list (top-down) of values left (resp. right) siblings left (resp. right) of p and seed the new value inserted at $\nu(\mathtt{p})$. The generic (non-interpreted hash) algorithm is provided in the NextPathInCompleteTreesLemmas.dfy file.

We illustrate how the algorithm insertValue works with the example of Figure 1. Assume we insert the seed $4$ at the end of the (green) path pi1 = [1,0,0]. The left (resp. right) siblings’ values are given by $\mathtt{left}=[-8,i_{1},i_{0}]$ (resp. $\mathtt{right}=[-1,-1,0]$). insertValue computes the values of the left siblings on the (blue) path pi2 = [1,0,1] after $4$ is inserted at the end of $\pi_{1}$: the first call terminates the algorithm and returns $[-8,i_{1},4]$ which is the list of left siblings that are needed on $\pi_{2}$.

In the next section we describe how to verify the recursive algorithms and the versions implemented in the DSC.

The (partial) correctness of our algorithms reduces to checking that they compute the same values as the ones obtained with a synthesised attribute on a Merkle tree. We have specified the data types Tree, MerkleTree and CompleteTrees and the relation between Merkle trees and lists of values (see trees folder.)

The root hash of a MerkleTree t is t.rootv. The (specification) function buildMerkle(h, L, $\mathbf{hash}$) returns a MerkleTree of height h, the leaves of which are given by the values (right-padded) $\overline{\mathtt{L}}$, and the values on the internal nodes agree with the definition of the synthesised attribute $\mathbf{hash}$, i.e., what we previously defined in Section 2 as $T(\overline{\texttt{L}})$. It follows that buildMerkle(h, L, $\mathbf{hash}$).rootv is the root hash of a Merkle tree with leaves $\overline{\mathtt{L}}$.

The total correctness proof for the computeRootUp function amounts to showing that 1) the algorithm always terminates and 2) the result of the computation is the same as the hash of the root of the tree. In Dafny, to prove termination, we need to provide a ranking function (strictly decreasing and bounded from below.) The length of the path p is a suitable ranking function (see the decreases clause in Listing A.1) and is enough for Dafny to prove termination of computeRootUp.

We establish property 2) by proving a lemma (Listing A.3): the pre-conditions (requires) of the lemma are the assumptions, and the post-conditions (ensures) the intended property. The body of the lemma (with a non-interpreted hash function) which provides the machine-checkable proof is available in the computeRootPath.dfy file. This lemma requires that the tree r is a Merkle tree, and that the lists left (resp. right) store the values of left (resp. right) siblings of the nodes on a path p. Moreover, the value at the end of p should be seed. Under these assumptions the conclusion (ensures) is that computeRootUp returns the value of the root hash of r.

Termination for insertValue is proved by using a ranking function (decreases clause in Listing ]A.2). The functional correctness of insertValue reduces to proving that, assuming left (resp. right) contains the values of the left (resp. right) siblings of the nodes on p, then insertValue(p, left, right, seed) returns the values of the nodes that are left siblings on the successor path. The specification of the corresponding lemma is given in Listing A.4. The code for this lemma is in the NextPathInCompleteTreesLemmas.dfy file. The main proof is based on several sub-lemmas that are not hard conceptually but cannot be easily discharged using solely the built-in Dafny induction strategies. They require some intermediate proof hints (verified calculations) to deal with all the nodes on the path p. Note that for this lemma, we require that the leaves are indexed (from left to right) to be able to uniquely identify each leaf of r.

The algorithms that implement the DSC do not use a bitvector to encode a path, but rather, a counter that records the number of values inserted so far and the height of the tree. In order to prove the algorithms actually implemented in the DSC, we first recast the computeRootUp and insertValue algorithms to use a counter and the height $h$ of a tree. In this step, we use a parameter k that is the index of the next available leaf where a new value can be inserted. The leaves are indexed left to right from $0$ to $2^{h}-1$ and hence $k$ is the number of values that have been inserted so far. It follows that the leaves with indices $k\leq i\leq 2^{h}-1$ have the default value. The correspondence between the bitvector encoding of the path to the leaf at index $k$ and the value $k$ is straightforward: the encoding of the path $p$ is the value of $k$ in binary over $h$ bits. We can rewrite left computeRootUp to use use $k$ and $h$ (computeRootUpWithIndex, Listing A.5) and prove it computes the same value as computeRootUp. A similar proof can be established for the insertValue algorithm. The index based algorithms and the proofs that they are equivalent (compute the same values as) to computeRootUp and insertValue are available in the IndexBasedAlgorithm.dfy file. Dafny can discharge the equivalence proofs with minimal proof hints using the builtin induction strategies.

In this section we present the final proof of (total) correctness for the algorithms implemented in the DSC (Solidity-like version.) Our proof establishes that the imperative versions, with while loops and dynamic memory allocation (for arrays) are correct, terminate and are memory safe.

The DSC is an object and has a state defined by a few variables: count is the number of inserted values (initially zero), branch is a vector that stores that value of the left siblings of the path leading to the leaf at index count, and zero_hashes is what we previously defined as $z$. The algorithm that computes the root hash of the Merkle tree in the DSC is get_deposit_root(). get_deposit_root() does not have any seed parameter as it computes the root hash using the default value ($0$). The correctness proof of get_deposit_root() uses the functional (proved correct) algorithm computeRootUpWithIndex as an invariant. Listing A.6 is a simplified version (for clarity) of the full code available in the DepositSmart.dfy file.

The algorithm that inserts a value v in the tree is deposit(v) in the implemented version of the DSC. Listing A.7 is an optimised version of the original algorithm. The simplification is explained in Section 5. The correctness of the algorithm is defined by ensuring that, if at the beginning of the computation the vectors branch (resp, zero_hashes) contain values of the left (resp. right) siblings of the path leading to the leaf at index count, then at the end of the computation, after v is inserted, this property still holds. The proof of this invariant requires a number of proof hints for Dafny to verify it. We use the functional version of the algorithm to specify a loop invariant (not provided in Listing A.7).

The termination proof is easy using size as the decreasing ranking function. However, a difficulty in this proof is memory safety, i.e. to guarantee that the index i used to access branch[i] is within the range of the indices of branch.

We have also proved the initialisation functions init_zero_hashes() and constructor. The full code of the imperative version of the DSC is available in the DepositSmart.dfy file.

In contrast to the previous attempts to analyse the DSC, we have adopted a textbook approach and used standard algorithms’ design techniques (e.g., dynamic programming, refinement, recursion.) This has several advantages over a direct proof (e.g., [20]) of the imperative code including:

• •

  the design of simple algorithms and proofs;

• •

  recursive and language-agnostic recursive versions of the algorithms;

• •

  new and provably correct simplifications/optimisations.

Our implementations and formal proofs have resulted in the identification of two previously unknown/unconfirmed optimisations. First, it is not necessary to initialise the vector of left siblings, b, and the algorithms are correct for any initial value of this vector.

Second, the original version of the deposit algorithm (which we have proved correct too) has the form¹³¹³13The complete Solidity source code is freely available on GitHub at https://github.com/ethereum/eth2.0-specs/blob/dev/solidity˙deposit˙contract/deposit˙contract.sol given in Listing A.8. Our formal machine-checkable proof revealed¹⁴¹⁴14This finding was not uncovered in any of the previous audits/analyses. that indeed the condition C1 is always true and the loop always terminates because C2 eventually becomes true. As witnessed by the comment after the loop in the Solidity code of the DSC, this property was expected but not confirmed, and the Solidity contract authors did not take the risk to simplify the code. Our result shows that the algorithm can be simplified to while not(C2) do ... od.

This is interesting not only from a safety and algorithmic perspectives, but also because it reduces the computation cost (in gas/Ether) of executing the deposit method. This simplification proposal is currently being discussed with the DSC developer, however the currently deployed version still uses the non-optimised code.

The verification effort for this project is 12 person-weeks resulting in $3500$ lines of code and $1000$ lines of documentation. This assumes familiarity with program verification, Hoare logic and Dafny. Table 1, page 1 provides some insights into the code base.

The filenames in green are the ones that require the less number of hints for Dafny to check a proof. In this set of files the hints mostly consist of simple verified calculations (e.g., empty sequence is a neutral element for lists [] + l == l + [] == l.) Most of the results on sequences (helpers package) and simplifications of sequences of bits (seqofbits package) are in this category and require very few hints. This also applies for the proofs¹⁵¹⁵15The file CommuteProof.dfy in this package is not needed for the main proof but was originally used and provides an interesting result, so it is still in code base. of the algorithms package, e.g., proving that the versions using the index of a leaf instead of the binary encoding of a path are equivalent.

The filenames in orange require some non-trivial proof hints beyond the implicit induction strategies built in Dafny. For instance in NextPathInCompleteTrees.dfy and PathInCompleteTrees.dfy, we had to provide several annotations and structure for the proofs. This is due to the fact that the proofs involve properties on a Merkle tree $t_{1}$ and its successor $t_{2}$ (after a value is inserted) which is a new tree, and on a path $\pi_{1}$ in $t_{1}$ and its successor $\pi_{2}$ in $t_{2}$.

The filenames in red require a lot of hints. For the files in the synthattribute package it is mostly calculation steps. Some steps are not absolutely necessary but adding them reduces the verification time by on order of magnitude (on our system configuration, MacBookPro 16GBRAM). The hardest proof is probably the correctness of the deposit method in DepositSmart.dfy. The proof requires non trivial lemmas and invariants. The difficulty stems from a combination of factors: first the while loop of the algorithm (Listing A.7) maintains a constraint between size and i, the latter being used to access the array elements in branch. Proving that there is no array-of-bounds error (i.e., $i$ is within the size of branch) requires to prove some arithmetic properties. Second, the proof of the main invariant (Listing A.7) using the functional specification computeLeftSiblingsOnNextpathWithIndex is complex and had to be structured around additional lemmas.

Overall, almost $90\%$ of the lines of code are (non-executable) proofs, and function definitions used in the proofs. The verified algorithms implemented in the DSC functional are provided in DepositSmart.dfy and account for less than $10\%$ of the code.

Considering the criticality of the DSC, 12 person-weeks can be considered a moderate effort well worth the investment: the result is an unparalleled level of trustworthiness that can inspire confidence in the Ethereum platform. According to our experts (ConsenSys Diligence) in the verification of Smart Contracts, the size of such an effort is realistic and practical considering the level of guarantees provided. The only downside is the level of verification expertise required to design the proofs.

The trust base in our work is composed of the Dafny verification engine (verification conditions generator) and the SMT-solver Z3.

Dafny is rather has excellent documentation, support for data structures, functional (side-effect free) and object-oriented programming. The automated verification engine has a lot of built-in strategies (e.g., induction, calculations) and a good number of specifications are proved fully automatically without providing any hints. The Dafny proof strategies and constructs that we mostly used are verified calculations and induction. The side-effect free proofs seem to be handled much more efficiently (time-wise) than the proofs using mutable data structures.

In the current version we have used the autocontracts attribute for the DSC object which is a convenient way of proving memory safety using a specific invariant (given by the Valid predicate). This could probably be optimised as Dafny has some support to specify precisely the side-effects using frames (based on dynamic framing.)

Overall, Dafny is a practical option for the verification of mission-critical smart contracts, and a possible avenue for adoption could be to extend the Dafny code generator engine to support Solidity, a popular language for writing smart contracts for the Ethereum network, or to automatically translate Solidity into Dafny. We are currently evaluating these options with our colleagues at ConsenSys Diligence, as well as the benefits of our technique to the analysis of other critical smart contracts.

The software artefacts including the implementations, proofs, documentation and a Docker container to reproduce the results are freely available as a GitHub repository at https://github.com/ConsenSys/deposit-sc-dafny.

I wish to thank Suhabe Bugrara, ConsenSys Mesh, for helpful discussions on the Deposit Smart Contract previous work and the anonymous reviewers of a preliminary version of this paper.