A detailed grant document is provided here.
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.
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.
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.