Formal Verification of Justification and Finalization in Beacon Chain

In recent years, Beacon Chain known as the core of Ethereum 2.0, has gained considerable attention since its launch. Many validators have staked billions of Ether in the Proof of Stake (PoS) network. It is a mission critical system and its security and stability rely on the justification and finaliz...

Full description

Saved in:
Bibliographic Details
Published in:IEEE access 2024, Vol.12, p.55077-55102
Main Authors: Afzaal, Hamra, Zafar, Nazir Ahmad, Tehseen, Aqsa, Kousar, Shaheen, Imran, Muhammad
Format: Article
Language:English
Subjects:
Algorithms
Analytical models
beacon chain
Communication
Consensus protocol
Ethereum 2.0
Formal method
Formal specifications
Formal verification
justification and finalization
Model checking
PAT
Python
Scalability
Specification and description languages
Technological innovation
Temporal logic
Verification
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In recent years, Beacon Chain known as the core of Ethereum 2.0, has gained considerable attention since its launch. Many validators have staked billions of Ether in the Proof of Stake (PoS) network. It is a mission critical system and its security and stability rely on the justification and finalization of checkpoints. These are essential elements of the Casper FFG consensus algorithm utilized by the Beacon Chain. This process is critical for establishing a trustworthy foundation and finalizing proposed blocks by confirming agreed upon checkpoints. Hence, ensuring the correctness of checkpoints in the Beacon Chain has significant importance because any bug in it can cause serious implications. To address this challenge, we employ formal methods, a popular mathematical approach used for verifying the correctness of such critical systems. In this work, we have done formal verification of the processes of Beacon Chain state initialization, justification and finalization of checkpoints using the Process Analysis Toolkit (PAT) model checker. The adoption of model checking through the PAT model checker presents a novel contribution of our work, as this approach is not previously utilized in the formal verification of Beacon Chain. The presented work is specified through the Communicating Sequential Programs, formal specification language, and the properties are described through Linear Temporal Logic. The PAT model checker takes the specified formal model and properties as input to assess whether the properties are satisfied. The properties are analyzed with respect to the verification time, visited states, total transitions, and memory used. Through this research, we aim to increase confidence in the correctness and reliability of the Beacon Chain.
ISSN:2169-3536
2169-3536
DOI:10.1109/ACCESS.2024.3389551