The objective of this project is to write a formal specification of the Eth2.0 specification in the verification-aware programming language Dafny.
More specifically, our goals in this project are many-fold:
- Write a formal (non-ambiguous and functional) specification of the Eth2.0 specification. This specification is written with pre/post-conditions using the Hoare logic style proof.
- Write an implementation for each function to demonstrate that the specification can be implemented, in other words, it is not inconsistent.
- Formally prove that our implementation satisfies the specification. The formal proof is provided in the form of mathematical proofs of lemmas written in Dafny.
To achieve this, we use the capabilities of the verification-aware programming language Dafny to write the specification, the implementation, and the proofs.
Dafny provides extensive support for automated reasoning leveraging the power of state-of-start automated reasoning engines (SMT-solvers). As a result, Dafny can assist in proving the lemmas that specify correctness. Moreover, as the lemmas are written as Dafny programs, they provide a non-ambiguous mathematical proof that the code is correct with respect to a specification. All the proofs can be mechanically verified using theorem provers.
We are gradually adding the Dafny specifications, implementations and proofs. Our current focus is on Phase 0 of the Eth2 specifications: SSZ, Merkleisation and Beacon chain.
An introduction (WIP) to the different components of Phase 0 is available in the Wiki section of this repo:
- Introduction to the Beacon Chain,
- Notes on SSZ specifications, implementations and proofs,
- Notes on Merkleisation specifications, implementations and proofs,
- Notes on Beacon Chain specifications, implementations and proofs.
Here is a recent youtube video with a presentation
The Eth2.0 specifications are subtle and sometimes complex. As a consequence, bugs, glitches or inconsistencies can creep into the specification and the implementation code.
Testing and code peer reviews can help keeping the bugs count low. However, testing can find some bugs but in general cannot guarantee the absence of bugs (Edsger W. Dijkstra).
These bugs remain uncovered ... until they manifest, resulting in crashes. Worse, they can be exploited as security vulnerabilities. An example of critical vulnerability is the OutOfBounds exception where a non-existent index in an array is accessed. This is one of the most common zero day attacks, and can occur in heavily tested code bases e.g. in the web browser Chromium.
You can read more about the specific case of the Beacon Chain in our Wiki section.
Runtime Verification Inc. have reported some work on:
- a formal semantics of Ethereum 2.0 Beacon Chain Phase 0 Specification using the K framework. This work presents a formal semantics of the Eth2.0 specifications in the K-framework. The semantics are executable and can be used for testing e.g. symbolic execution.
- the initial formal verification of the Casper protocol.
- the verification of the deposit smart contract
More recently, a security audit was performed by LeastAuthority. The code was manually reviewed and some potential security vulnerabilities highlighted.
Our work aims to complement the previous work by providing a thorough formal verification of the Eth2.0 phase 0 specifications.
- Eth2.0 resources resources, specifications and implementations.
- Dafny resources, install and learn.
- Coding practices and database of known vulnerabilities,
- Other resources, K-framework resources.
Pre-requisites:
- a working installation of Docker,
- a fork or clone of this repository.
A simple way to check the proofs is to use a pre-configured installation of Dafny on a Docker container.
On Unix-based system, cd to the root directory of your working copy of this repository.
/home/user1/ $ git clone [email protected]:PegaSysEng/eth2.0-dafny.git
/home/user1/ $ cd eth2.0-dafny
/home/user1/eth2.0-dafny $
The next commands will start a Docker container with Dafny pre-installed, and mount your local working directory as a volume in the Docker machine (this way you can access it from the running Docker machine):
/home/user1/eth2.0-dafny $ docker run -v /home/user1/eth2.0-dafny:/eth2.0-dafny -it franck44/linux-dafny /bin/bash
root@749938cb155d:/# cd eth2.0-dafny/
root@749938cb155d:/eth2.0-dafny# dafny /dafnyVerify:1 /compile:0 src/dafny/utils/MathHelpers.dfy
Dafny 2.3.0.10506
Dafny program verifier finished with 13 verified, 0 errors
root@749938cb155d:/eth2.0-dafny#
Pre-requisites:
- install Dafny, see our Dafny wiki.
- clone or fork this repository.
Assuming you have a running Dafny compiler, you may use the following command line to check a *.dfy file:
> dafny /dafnyVerify:1 /compile:0 /timeLimit:60 src/dafny/utils/MathHelpers.dfy
Dafny 2.3.0.10506
Dafny program verifier finished with 13 verified, 0 errors
The test folder contains some tests. The purpose of this directory is to demonstrate that we can extract an implementation and run it (indeed, once we have proved the code, there is no need to test it). To run the tests, you can issue the following command from the root directory (it collects all the files in the test folder, compile them and run them):
> ./scripts/runAllTests.sh
For an even better experience you may install VSCode and the Dafny plugin see our Dafny wiki.
To compile to Go:
dafny /compileTarget:go /spillTargetCode:1 src/dafny/ssz/BitListSeDes.dfyC# can be targeted by changing compileTarget to cs.