An Analysis of the Ethereum Proof of Stake Protocol

La tesi indaga il protocollo Gasper della blockchain Ethereum, utilizzando una versione estesa del model checker Prism per quanto riguarda la simulazione e la verifica. Gasper rappresenta un significativo passo avanti nell’evoluzione di Ethereum, introducendo un nuovo meccanismo di consenso e affrontando le sfide della scalabilità. Questo lavoro mira a modellare e a valutare il protocollo Gasper in modo sperimentale, verificandone la coerenza e la robustezza, alla ricerca di vulnerabilità rispetto a vari attacchi. Lo studio comprende un’analisi completa della transizione di Ethereum dalla Proof of Work (PoW) alla Proof of Stake (PoS), chiarendo le motivazioni e i vantaggi di questo cambiamento fondamentale. Inoltre, approfondisce le caratteristiche uniche di Gasper e i miglioramenti rispetto ai suoi predecessori, come Hybrid Casper, evidenziando il suo ruolo nel raggiungimento di maggiore sicurezza e scalabilità. Uno degli obiettivi principali della ricerca è la validazione del modello realizzato tramite Prism+ rispetto ai complessi requisiti di Gasper, garantendo che il modello simulato rifletta accuratamente il comportamento del protocollo. Attraverso test e verifiche, questo studio mira a fornire preziose informazioni sulla sua robustezza e affidabilità. Inoltre, la tesi esplora potenziali attacchi al protocollo Gasper in modo teorico e pratico, valutandone la resilienza rispetto alle strategie avversarie. Identificando vulnerabilità e punti deboli, la ricerca contribuisce a migliorare la sicurezza del protocollo e a guidarne l’ulteriore sviluppo. Questa tesi offre un esame del protocollo Gasper di Ethereum, combinando l’analisi teorica con la simulazione pratica utilizzando il model checker Prism+. Lo studio comprende la transizione da PoW a PoS, i progressi di Gasper, la convalida della coerenza del modello e l’analisi della sicurezza, contribuendo alla continua evoluzione della tecnologia blockchain di Ethereum.