Narrowing the Gap Between Ethereum’s Specifications and Implementations via Model Checking

PI: Dr. Chenxiong Qian, HKU

Project Abstract: 

Ethereum has established itself as the most actively used blockchain network by providing integrity, resilience, capability, transparency, etc. These intrinsic features are specified by the official consensus protocol, which is implemented into programs called Ethereum clients. Nevertheless, as Ethereum is new and complex, not all developers have a systematic and comprehensive understanding of these properties, which widens the gap between the specifications and the implementations. In fact, there is an emerging trend for attackers to exploit implementation vulnerabilities in Ethereum clients to launch attacks with damaging consequences.

This project aims to narrow the gap between Ethereum’s specifications and implementations by building model checking systems to verify the consistency between different implementations and the correctness of the desired properties. Specifically, we will first build a system to map the code of different Ethereum clients that implements the same functionality. Then, we will build a system that uses bounded model checking to check the consistency of the mapped code and generate counterexamples for any inconsistencies. Furthermore, we will manually check the specifications to define the desired properties in a formal language and build a system to check the correctness of the properties for each Ethereum implementation.