Formal Verification of SSV Protocol

A detailed grant document is provided here.

Summary

The Secret Shared Validator (SSV) protocol has been designed by the Ethereum Foundation (in collaboration with others) to build redundancy in the Eth2 Client architecture by removing any possible single point of failure. It is therefore fundamental that the SSV protocol design is free from any security vulnerability to ensure that it functions as designed and does not potentially open up attack vectors to Eth2 Clients operated by honest staking accounts.

The grant work will be carried out by Roberto Saltini’s formal methods team at Consensys. Their previous experience include research on IBFT consensus and the design and formal verification of QBFT consensus.

Grant Details

This grant work proposes to provide the SSV protocol design with:

  • a formal specification and
  • a formal machine-checkable proof that the SSV protocol, as defined by the formal specification, provides the required properties.

The properties to be proven will include the following:

  • Provided that at least 1/3 of the SSVN-VC pairs are honest, then the Validator will never be slashed
  • The protocol never ends up in a deadlock state where no progress can be made
  • Assuming some level of network synchrony, a new attestation/block signature will always be eventually produced.

Grant Amount

This grant is co-funded by an equal split between 3 parties (incl. Ethereum Foundation). The total grant amount is USD 188k, which puts each party’s share at USD 62.7k.

2 Likes

一般投资者,怎么参与呢?能为提供什么服务

This is very important!

2 Likes

这是一定要重视的,必须严谨起来,这是对从业者得保护

1 Like

The grant for the spec was successfully voted on by the DAO.

2 Likes

Thank you ssv.network DAO for approving the grant.

Please use the following address for the grant payment.

0x48b356B7D93f6B0042b0c21E132f9Dc9aC9700a0

ETH is preferred over USDC if possible.

Thank you.

2 Likes

I can confirm Roberto sent me that address as well.

For the records:
The first version of the spec is now available on GitHub. Congrats, everyone!:tada:
ethereum/distributed-validator-specs: Ethereum Distributed Validator Specifications (github.com)

2 Likes