Formal Modeling and Verification of Validator Voluntarily Exit in Ethereum 2.0 Beacon Chain

Abstract

The Ethereum 2.0 Beacon chain is a big step toward improving the security, scalability, and decentralization. It is based on the Proof of Stake (PoS) consensus protocol that maintains the validator status, attestation details, and many more. The term validator is introduced in the PoS consensus protocol and its work is to propose blocks and vote for them by becoming a committee member to add those blocks to the blockchain. We address the problem related to validator’s voluntary exit to vanish its active status and do its formal verification using the SPIN Model checker. There does not exist much research in this area as it was introduced recently in 2020. Further, this is the first work on formal verification of the beacon chain using the SPIN model checker. In this work, we formally specify the validator exit process of the Ethereum 2.0 Beacon Chain using the formal specification language, i.e., Process or Protocol Meta Language (PROMELA). We create a program graph for this process through the SPIN Model checker and describe safety and liveness properties using Linear temporal logic (LTL) in the form of a formula. The formal verification is performed to ensure correctness by giving the program graph and LTL formulas as input to the SPIN model checker whether the properties are satisfied with the program graph