Formal Verification of Capella Fork with Dafny

Overview

This project was built upon the eth2.0-dafny (ConsenSys R&D). Added Beacon Chain part in Capella Fork specifications.

Objectives

The objective of this project is to contribute a new formal specification of the Eth2.0 specification, specifically for the Capella Fork, in the verification-aware programming language Dafny.

Goals

• Write an implementation for each new function to demonstrate that the specification can be implemented, in other words, it is not inconsistent.

• Add a formal (non-ambiguous and functional) specification of the Capella Fork. This specification is also written with pre/post-conditions using the Hoare logic style proof.

• Formally prove that the implementation satisfies the specification.

Get started

Requirements (For Linux)

• Install .NET 6.0 as described above
• Install python3: e.g., sudo apt install python3 python3-pip
• If you intend to compile to PHP..., install PHP. (By parity of reasoning)

Installation

• install Dafny, see Dafny tutorial(Linux Version).
• clone or fork this repository.

How to check the proofs?

I have checked the proofs with Dafny 3.2.0 under Ubuntu 20.04 env.

Assuming you have a running Dafny compiler, you may use the following command line at the root of the repository to check a *.dfy file:

> dafny /dafnyVerify:1 /compile:3 /noCheating:1 src/dafny/beacon/Helpers.cap.dfy
Dafny 3.2.0.30713

Dafny program verifier finished with 3 verified, 0 errors
Compiled assembly into Helpers.cap.dll
Program compiled successfully

/dafnyVerify:1: This option controls whether the Dafny verifier is enabled or not. Setting it to 1 enables verification of Dafny assertions, lemmas, and proofs in your code.

/compile:3: This option typically means to verify and compile all specified Dafny files.

/noCheating:1: This option will increase the strictness of the verification process, potentially disallowing certain operations or constructs that could undermine the integrity of the verification.

For an even better experience, you may install VSCode and the Dafny plugin here, the latest adaptable plugin version is 2.3.0.

Beyond reproducing

Depending on your inclination you may use the verified code in different ways:

• you may contribute new code and proofs by either adding functions that have not been implemented yet or even testing that new ideas and optimisations do not break the proofs;

• you may use Dafny to generate target code (e.g. Go, Java, C#, JavaScript, PHP) and see how the automated generated code can replace or complement your code base;

• you may use the specifications to help in unit testing your own code. The specifications contain unambiguous pre and post-conditions that clearly specify the effect of a function/method. They can be used to write property-drive tests.

How to play with counterexamples if you find new errors?

$ git clone https://github.com/ethereum/consensus-specs.git
$ cd <consensus-root>
$ python3 -m venv .          # create a virtual env
$ source bin/activate        # activate the virtual env
$ make install_test          # install the necessary packages
$ python setup.py pyspecdev

Then, the executable Python code of spec will be generated. You can test it by simply running the following command:

python <your_test_file.py>

There is an example testing file under eth2.0-dafny/test/ called exec_spec_test.py; put it under consensus-specs/tests/core/pyspec, then run it.

My Contributions:

• scripts/call_graph.py [modified]
• scripts/countLines.py [modified]
• src/dafny/beacon/BeaconChainTypes.dfy [modified]
• src/dafny/beacon/Helpers.dfy [modified]
• src/dafny/beacon/Helpers.dfy [modified]
• src/dafny/beacon/statetransition/EpochProcessing.dfy [modified]
• src/dafny/beacon/statetransition/EpochProcessing.s.dfy [modified]
• src/dafny/beacon/statetransition/StateTransition.dfy [modified]
• src/dafny/beacon/validators/Validators.dfy [modified]
• src/dafny/ssz/Constants.dfy [modified]
• src/dafny/utils/Eth2Types.dfy [modified]
• test/dafny/merkle/third_party_implementations/PySszBitlistMerkleisation.py [modified]
• src/dafny/beacon/Helpers.cap.dfy [new]
• src/dafny/beacon/statetransition/stateTransition.cap.dfy [new]
• test/exe_spec_test.py [new]

How to complie to other languages

For example, compile to PHP

dafny /compileTarget:php /spillTargetCode:1 <YOUR_FILE.dfy>

For other languages, replace the parameter of /compileTarget.

For more information, please click here