Formally Verifying the Ethereum 2.0 Phase 0 Specifications
The Automated Verification team on ConsenSys R&D have been working on a formal specification and verification of the Beacon Chain for a few months. We are happy to report that lots of progress has been made and although not complete yet, we have managed to develop a solid and formally verified kernel of the Beacon Chain. For the first time, our work provides an unmatched level of trustworthiness to the core foundations of the Eth2.0 infrastructure.
Verification vs. Testing
We used the award-winning verification-aware programming language Dafny to write a formal (functional and logical) specification of each Beacon Chain function, an implementation of each function, and a proof that the implementation conforms to its specification. In other words, we have mathematically verified the absence of bugs. The implementations that we have eventually proved correct are based on the official Eth2.0 specifications with the caveat that we have fixed and reported some bugs and inconsistencies.
Our methodology is different to testing as we mathematically prove conformance of the functions to their specifications, for all inputs. Testing cannot range over infinitely many inputs, and as a consequence can discover bugs but not prove the absence of bugs.
And the best thing is that we do not need to publish a paper nor to review the proofs. The proofs are part of the code base and written as programs. Yes, in Dafny, you can write a proof as a developer-friendly program. Also, the proofs are mechanically checked by a theorem prover, leaving no room for incomplete or flawed proofs.
Properties We Have Proved
The properties range from the absence of arithmetic under/overflows and index out of bounds, the conformance of each function to logical (first-order logic) pre/post-conditions (merkelise example here), to more complex ones involving functions’ compositions. For example, we have the following property of the SSZ Serialise/Deserialise functions: for each object x, Deserialise(Serialise(x)) = x, i.e. deserialising a serialised object returns the original object. We have also established a number of invariants, and used them to prove that the core operations of the Beacon Chain and ForkChoice (state_transition, on_block) actually build a chain of blocks: for any block b in the store, the ancestors of b form a finite totally ordered sequence leading to the genesis block, which is the main property of a blockchain!
The Benefits of Formal Verification
Any formal methodist would insist that verification is a security best practice. Here’s exactly how this methodology ensures a secure and trustworthy infrastructure for Ethereum 2.0.
First, we have lifted the official Eth2.0 specifications to a formal logical and functional specification. For each function, we formally define what the function is expected to compute, not how. This provides language-agnostic developer-friendly reference specifications that can be used to develop more secure implementations, with less effort.
Second, our specifications, implementations and proof architecture are modular. As a result, we can easily experiment with new implementations (e.g. optimisations) and check their impact on the overall system. Think of a clever hack to implement a function? Change the implementation and ask Dafny to check that it still conforms to its specification. If it does, the proofs of the components that use this function are not impacted.
Third, our implementations are executable. We can compile and run a Dafny program. Even better, you can automatically generate code in some popular programming languages like C#, Go (and soon Java) from the Dafny code. This can be used to complement existing code bases or to generate certified tests. The implementation to be tested can use our proved-correct functions to compute the expected result of a test and check it against its own result.
Everything in a Single Language
Last but not least, our code base is self-contained. It contains the specifications, implementations, documentations, and proofs, all in a single, readable, simple and semantically well-defined programming language.
Questions and Considerations
What about the soundness of the verification engine?
You might be wondering, “what if the Dafny compiler/verifier is buggy?” We actually know Dafny is buggy (dafny repo issues), but we do not rely on the absence of bugs in Dafny. We rely on Dafny (and its verification engine) to be sound. Soundness means that when Dafny reports that proofs are correct, they are indeed correct.
What if the specification we have written is not the right one?
In this case, we would prove conformance to a wrong requirement. Yes, this can happen and there is no silver bullet to fix this problem. However, as we mentioned before, Dafny is executable. This enables us to run the code and get some confidence that our specifications are the right ones. And our specifications are written in first-order logic with no room for dispute about the meaning, so if you notice a problem, let us know and we will fix it.
What if Dafny cannot prove that an implementation conforms to a specification?
This can happen, but in this case Dafny has some feedback mechanisms to help investigate what steps of a proof cannot be verified. And until now, we have always managed to build proofs that Dafny can automatically check.
We welcome your feedback, so please check out our eth2.0-dafny repository. We’ve been excited to watch Ethereum 2.0 development reach its recent testnet milestones, and we look forward to working with teams across the ecosystem to ensure the next phase of the network is built on a rock solid foundation.
Acknowledgement: Thanks to my teammates Joanne Fuller, Roberto Saltini (Automated Verification team), Nicolas Liochon, and to Avery Erwin for comments on a preliminary version of this post.