Formal Modeling and Verification of Justification and Finalization of Checkpoints in Ethereum 2.0 Beacon Chain

Abstract

New to the Ethereum platform with version 2.0 is the Beacon chain. Validator status, attestation information, and many more are maintained via the proof-of-stake (PoS) consensus protocol, which is relied upon. The Ethereum 2.0 beacon chain relies on the validation and completion of checkpoints to validate and finish all the blocks associated with those checkpoints. By formally verifying it using the SPIN model checker, this research tackles the issue of the dependability and security of the Beacon Chain’s justification and finalization operations. Due of its novelty (launched in 2020), there is little any literature on the subject. Additionally, no previous study has formally verified the beacon chain using the SPIN model checker. The study makes use of PROMELA, a formal specification language, to formally outline the reasoning and finalization method of the Ethereum 2.0 Beacon Chain. Utilizing the SPIN Model Checker, a program graph is generated for this procedure, which formulaically expresses safety features via the use of linear temporal logic (LTL). To make sure everything is in order, we run the SPIN model checker with the program graph and LTL formulae as inputs to see whether the program graph satisfies the properties. This is the formal verification process.