Starting Date: June 2023
Prerequisites: Good programming skills; An interest in formal verification, security or distributed systems (blockchains)
Will results be assigned to University: Yes
In this project you will explore the world of formal verification and
blockchains, specifically the new Ethereum 2.0 ‘Proof-of-Stake’ blockchain [1]. This is a more energy-efficient replacement for the original Ethereum ‘Proof-of-Work’ blockchain. As in any blockchain, correctness of the
distributed ‘consensus’ protocol [2] used to maintain the chain and extend it with new blocks is critical. In Ethereum 2.0, this is the responsibility of
‘validator’ nodes, each of whom must deposit a monetary ‘stake’ of 32 ETH
(approx. $50,000) to participate. There are currently around 500,000 active validators and hence approximately $20B in total stake!
As part of the project, you will apply formal verification techniques to verify either (i) the correctness of parts of the Ethereum 2.0 consensus protocol (e.g. building on [3]) or (ii) of smart contract code that executes on the blockchain [4]. For example, a recent research project at Royal Holloway resulted in a new version of the Ethereum 2.0 consensus protocol that is more resilient to ransomware attacks against validators. Formally verifying the correctness of these changes would be an important contribution.
The project would suit a student interested in formal verification (e.g. participation in Royal Holloway’s Proofs and Programs Club would be great preparation!), security and/or distributed systems (blockchains). Contact Dr. Dan O’Keeffe or Dr. Julien Lange if you are potentially interested and would like to know more.
Related reading:
[1] The Ethereum 2.0 Beacon Chain
[2] Foundations of Distributed Consensus and Blockchains, E. Shi.
[3] Formal verification of Ethereum 2.0 Phase 0 release in Dafny