Verifica formale dei meccanismi di consenso della blockchain utilizzando Event-B

Sommario

Questo studio presenta un quadro formale di verifica per i meccanismi di consenso blockchain e gli smart contract, utilizzando il metodo Event-B. Questo approccio combina astrazione dalla rappresentazione, dimostrazione basata su invarianti e verifica temporale del modello con controlli formali di sicurezza, vivacità e resistenza al doppio investimento prima della implementazione.

Abstract

Questo studio sviluppa un quadro di verifica formalmente fondato per i meccanismi di consenso blockchain e il comportamento degli smart contract utilizzando Event-B e la piattaforma Rodin. A differenza degli approcci precedenti che si basavano principalmente su simulazioni o validazioni basate su casi di contratti isolati, questo lavoro integra astrazione da Finite State Machine (FSM), dimostrazione guidata da invarianti, modellazione di raffinamento e verifica logica temporale per analizzare Proof of Work (PoW), Proof of Stake (PoS) e meccanismi per la prevenzione del doppio spesa. Gli smart contract Solidity vengono astratti in FSM e codificati come macchine Event-B, consentendo la specifica formale delle transizioni di stato e dei vincoli di sicurezza. Le proprietà di sicurezza — inclusa l'unicità delle transazioni, la coerenza dello stato, l'applicazione del controllo degli accessi e la conservazione invariante del registro — vengono verificate tramite obblighi di prova generati automaticamente in Rodin. Sono stati generati in totale 312 obblighi di prova, di cui 287 (92%) sono stati estinti automaticamente e 25 sono stati dimostrati in modo interattivo, con conseguente copertura completamente invariante. Le proprietà di vivacità sono state specificate in Computation Tree Logic (CTL) e validate tramite il model checking, confermando la libertà di deadlock e la eventuale selezione del validatore in condizioni PoS. La prevenzione della doppia spesa è stata formalmente applicata utilizzando modellazione del registro coerente nello stato, dove i vincoli di unicità sono stati dimostrati in tutti gli stati raggiungibili. La logica di consenso a livello di protocollo per PoW e PoS è stata affinata su tre livelli di astrazione, garantendo l'integrità del blocco e la correttezza del validatore attraverso un perfezionamento a passi. I risultati dimostrano che le dimostrazioni verificate da macchina forniscono garanzie di correttezza verificabili oltre la valutazione basata sulla simulazione, stabilendo una pipeline di verifica rigorosa e riproducibile che migliora la garanzia di correttezza e la robustezza a livello di protocollo nei sistemi blockchain.

Introduzione

La tecnologia blockchain si è evoluta in un paradigma di registro distribuito che consente la tenuta decentralizzata dei registri senza dipendere da autorità centralizzate. Replicando gli stati del registro tra i nodi partecipanti e raggiungendo un accordo tramite meccanismi di consenso, i sistemi blockchain offrono integrità, trasparenza e resistenza alla manomissione in ambienti aperti e conflittuali. Come descritto da Yaga et ^al.1, l'architettura blockchain combina primitive crittografiche, protocolli di consenso distribuiti e comunicazione peer-to-peer per garantire che le transazioni validate diventino computazionalmente impraticabili da modificare. Meccanismi di consenso fondamentali come la Proof of Work (PoW) e la Proof of Stake (PoS) regolano la selezione dei validatori, la validazione dei blocchi e la sincronizzazione del registro. Inoltre, gli smart contract estendono le capacità della blockchain integrando una logica programmabile che esegue autonomamente regole predefinite, abilitando applicazioni decentralizzate in settori come finanza, sanità e governance. Man mano che le tecnologie blockchain vengono sempre più impiegate in ambienti di alto valore e critici per la sicurezza, garantire la correttezza dei meccanismi di consenso e del comportamento degli smart contract è diventato essenziale per mantenere l'affidabilità^{operativa 2}.

Nonostante la loro natura decentralizzata, i sistemi blockchain rimangono vulnerabilità logiche e a livello protocollo. Gli attacchi di doppia spesa possono verificarsi quando i vincoli di coerenza del registro non sono applicati rigorosamente. Debolezze a livello di consenso, come una logica di selezione dei validatori errata o regole di validazione dei blocchi difettose, così come vulnerabilità degli smart contract, tra cui la rientranza e un controllo di accesso improprio, hanno portato a notevoli perdite finanziarie nelle piattaforme distribuite. Sebbene i framework di test empirici e simulazione siano ampiamente utilizzati per valutare il comportamento dei protocolli PoW e PoS, questi approcci forniscono solo osservazioni illustrative piuttosto che garanzie di correttezza complete. La validazione basata su simulazione non può dimostrare la preservazione invariante su tutti gli stati raggiungibili né garantire proprietà di sicurezza e vivacità su ogni percorso di esecuzione. Questa limitazione evidenzia la necessità di tecniche di verifica matematicamente fondate che possano ragionare rigorosamente sui sistemi blockchain oltre all'analisi osservativa.

I metodi formali offrono tale base abilitando la specifica e la verifica del sistema tramite logica^{matematica 3,4}. Evento-B estende questo paradigma attraverso un raffinamento a passo, rappresentando i sistemi come macchine a stati astratte in cui gli stati del sistema sono vincolati da invarianti e le transizioni sono modellate come eventi^{protetti 5}. La piattaforma Rodin genera automaticamente obblighi di prova e ne supporta la liberazione, consentendo la verifica controllata da macchina della conservazione invariante e la coerenza dello^{stato 6}. Tecniche classiche di specificazione come il B-Method⁷ e Z⁸ dimostrano come il ragionamento basato su invarianti e il raffinamento formale possano garantire la correttezza del sistema attraverso le diverse fasi di sviluppo. Questi metodi sono stati ampiamente applicati in sistemi mission-critical e safety critici per garantire la correttezza prima del^{dispiegamento} 9,10,11,12,13. Ulteriori estensioni come UML-B e i framework di raffinamento grafico dimostrano ulteriormente la scalabilità della modellazione basata sul raffinamento per sistemi industriali^complessi 14,15,16,17,18,19. Questi sviluppi illustrano che la modellazione formale basata sul raffinamento può gestire efficacemente la complessità del sistema mantenendo forti garanzie di correttezza.

Sono stati inoltre esplorati approcci formali di verifica per i sistemi blockchain. Le tecniche di verifica contrattuale basate su SMT verificano automaticamente le asserzioni all'interno dei programmi Solidity e possono produrre controesempi quando si verificano violazioni^{logiche 20}. Strumenti come VERISOL impiegano astrazioni a stati finiti per la verifica degli smart^{contract 2}, mentre gli approcci di dimostrazione di teoremi traducono i contratti in quadri di ragionamento formali come F*²¹. Inoltre, le formalizzazioni semantiche della Macchina Virtuale Ethereum consentono un ragionamento rigoroso sulla semantica dell'esecuzione e sul rilevamento^{delle vulnerabilità 22}. Analogamente, ambienti di dimostrazione di teoremi come Coq sono stati applicati per analizzare le proprietà di sicurezza legate al consenso e la correttezza^{transazionale 23}. Sebbene questi approcci forniscano preziose intuizioni, spesso si concentrano indipendentemente sulla correttezza a livello contrattuale o sulle proprietà a livello di consenso. Gli invarianti del registro a livello di sistema, le transizioni di stato di consenso e il comportamento degli smart contract sono raramente integrati all'interno di un framework unificato basato sul raffinamento che mantenga la tracciabilità tra i livelli di specifica e gli artefatti di verifica. Inoltre, molti approcci esistenti enfatizzano il rilevamento delle vulnerabilità o il controllo logico delle asserzioni piuttosto che la conservazione sistematica degli invarianti su più livelli di raffinamento.

Il presente studio affronta questa lacuna metodologica proponendo un quadro di verifica formale unificato che integra l'astrazione Finite State Machine (FSM) degli smart contract Solidity con la modellazione di raffinamento Event-B e il pagamento del dovere di prova verificato da macchina all'interno della piattaforma Rodin. Invece di trattare la verifica contrattuale e la modellazione del consenso come problemi separati, il framework proposto specifica formalmente le transizioni di stato a livello di protocollo per PoW e PoS, i vincoli di integrità del registro, le condizioni di unicità delle transazioni e l'evoluzione dello stato degli smart contract all'interno di un unico modello strutturato. Le proprietà di sicurezza — inclusa la conservazione invariante, l'unicità delle transazioni, le transizioni di stato controllate e la coerenza del registro — sono espresse come invarianti Event-B e verificate tramite obblighi di prova generati automaticamente. Le proprietà temporali e dipendenti dall'ordine di esecuzione sono specificate tramite la logica dell'albero di calcolo e verificate tramite il controllo dei modelli per garantire correttezza oltre gli invarianti statici. Un contributo metodologico chiave risiede nell'affermare una tracciabilità esplicita tra i livelli di astrazione: le funzioni di solidità sono astrstrate in transizioni FSM, le transizioni FSM sono codificate come eventi Event-B, e gli invarianti insieme alle specifiche temporali sono collegati direttamente agli obblighi di prova svolti e ai risultati del model-checking. Questa mappatura strutturata garantisce che ogni affermazione di correttezza sia supportata da prove verificate da macchina e distingua chiaramente le garanzie basate su prove dalle osservazioni basate su simulazioni.

L'ambito di questo lavoro è volutamente limitato per garantire precisione e chiarezza analitica. La modellazione si concentra sulle transizioni di stato a livello di protocollo per i meccanismi di consenso, i vincoli di integrità del registro, le proprietà di unicità delle transazioni e il comportamento dello stato degli smart contract. Aspetti a livello di rete come i ritardi nella propagazione dei messaggi, le strategie avversarie bizantine, i meccanismi di risoluzione dei fork e la semantica dettagliata del gas delle macchine virtuali Ethereum si spostano al di fuori dei confini di astrazione definiti. Definendo esplicitamente queste assunzioni di modellazione, il quadro garantisce che le affermazioni di verifica rimangano allineate con le prove formalmente verificate. Il resto di questo articolo presenta la metodologia di astrazione, il processo di modellazione e raffinamento Event-B, le procedure per la verifica invariante e temporale e i risultati di verifica. Fondando il protocollo blockchain e la verifica degli smart contract in modellazione formale basata sul raffinato e in dimostrazioni verificate da macchina, questo studio rafforza il rigore metodologico e migliora la garanzia di correttezza pre-implementazione per i sistemi di registro decentralizzati.

Protocollo

Input di studio
In questo studio, due smart contract Solidity sono stati utilizzati come input di verifica. Il primo era un contratto in stile Simple DAO utilizzato come caso di studio di rientranza. Il secondo era un contratto di bilancio semplificato/transizione di stato progettato per testare i vincoli a livello contrattuale contro la doppia spesa. Il codice sorgente originale di Solidity serviva come input ai processi di astrazione e verifica definiti in questo protocollo. Il processo generale di trasformazione utilizzato per tali contratti è illustrato nella Figura 1, che mostra la trasformazione graduale del codice sorgente Solidity nei modelli FSM, Event-B e SMV durante la verifica.

Modellazione del confine
La modellazione formale si concentra sulla logica controllo-flusso degli smart contract, inclusi il comportamento di ingresso e uscita delle funzioni, l'esecuzione interna e le transizioni di stato a livello contrattuale. La visibilità delle funzioni (pubblica, esterna, interna e privata) è stata rappresentata insieme al corrispondente comportamento della pila di chiamate rilevante per l'analisi della rientranza. I tipi di transizioni astratte (chiamata, invio, trasferimento) venivano trattati come operazioni per il trasferimento di etheri.

Gli invarianti a livello contrattuale sono stati definiti per garantire l'unicità delle transazioni e prevenire la doppia spesa all'interno del confine di astrazione. Per rappresentare i requisiti di selezione di validazione e integrità del blocco, il livello di astrazione logica del protocollo è stato definito in termini delle transizioni di stato a livello di protocollo sia di Proof of Work che di Proof of Stake.

Il confine di astrazione non includeva elementi a livello di rete, inclusi la programmazione dei messaggi da consegnare e i ritardi causati da un numero qualsiasi di salti, la risoluzione del fork, avversari di rete che impiegano strategie bizantine, la semantica della Macchina Virtuale Ethereum e la semantica del gas controllata dai nodi di rete, la propagazione delle eccezioni, le esecuzioni asincrone, il comportamento di fallback complesso e la finalità a livello di rete. Pertanto, i risultati della determinazione della doppia spesa si applicano solo agli invarianti a livello contrattuale e non costituiscono un accordo a livello di rete sulla finalità.

Strumenti e configurazione
La piattaforma Rodin veniva utilizzata per modellare, perfezionare, generare obblighi di prova e svolgere il modello Event-B (versione 3.7.0), che permetteva ai provatori PP, ML, SMT e Atelier-B di scaricare le prove automaticamente e in modo interattivo. nuXmv versione 2.0.0 veniva eseguita sui modelli SMV generati in modalità completa di esplorazione CTL per effettuare il controllo dei modelli CTL.

Tutte le esecuzioni di verifica venivano eseguite in un ambiente computazionale controllato utilizzando Ubuntu 22.04 LTS, OpenJDK 11 e Python 3.10.12. Web3 (7.6.0), NetworkX (3.4.2), Matplotlib (3.8.0), Graphviz (0.20.3), NumPy (1.26.4) e Pandas (2.2.2) sono stati utilizzati per implementare elementi di simulazione e visualizzazione. Questo progetto garantiva che i risultati formali di verifica e simulazione potessero essere riprodotti quando eseguiti nelle stesse condizioni di esecuzione.

Flusso di lavoro di trasformazione
Questo processo di verifica era composto da quattro fasi. I contratti di solidità furono inizialmente tradotti in una rappresentazione Finite State Machine (FSM-SC). Il modello FSM-SC fu successivamente codificato in Event-B, con invarianti e gradi di affinamento chiaramente specificati. L'astrazione FSM-SC è stata tradotta in un modello SMV in nuXmv. I risultati della verifica sono stati riportati come statistiche sull'addebitamento dell'obbligo di prova e sul controllo del modello CTL, e sono stati forniti controesempi come casi diversi.

Costruzione FSM
Ogni contratto è stato astrattato come una Macchina a Stati Finiti definita come:

Dove:
S = insieme degli stati
S₀ = stato iniziale
T = relazione di transizione
V = mappatura della visibilità
G = predicati di guardia
A = azioni/aggiornamenti di stato.

Algoritmo 1: Costruzione FSM da Solidity
Input: codice sorgente Solidity
Output: FSM-SC

1) Parsi l'albero sintattico astratto del contratto di Solidity.
2) Creare lo stato iniziale S₀ dalla definizione del costruttore.
3) Per ogni funzione di Solidity f, creare un S_f di stato di controllo distinto e registrare la visibilità V(f) ∈ {pubblico, esterno, interno, privato}.
4) Per ogni istruzione all'interno della funzione f, si deriva una transizione t estraendo predicati di guardia da condizioni di necessità/asserzione e azioni da aggiornamenti delle variabili di stato.
5) Aggiungere la transizione t a T.
6) Creare tipi di transizione espliciti per operazioni di trasferimento Ether (chiamata, invio, trasferimento), chiamate interne ed esterne, delegatecall, autodistruzione, uso di tx.origin, branch condizionali e costrutti di loop.
7) Restituire FSM-SC = (S, S₀, T, V, G, A).

E ogni funzione di solidità è associata a uno stato di controllo FSM diverso. Per la comprensione delle vulnerabilità, i flussi di esecuzione rilevanti per la vulnerabilità, ad esempio tali flussi con chiamate esterne seguite da aggiornamenti di bilanciamento, sono stati esplicitamente astratti in transizioni ordinate. La Figura 2 descrive un esempio di diagramma FSM-SC per il contratto in stile SimpleDAO, mostrando come gli stati di ingresso, le transizioni di chiamata esterna e le sequenze di aggiornamento di stato siano state astrstrate durante questa fase di costruzione.

Codifica di FSM in Evento-B
La transizione FSM era rappresentata come costrutti Event-B. Tutte le transizioni corrispondono a eventi dell'Evento-B, inclusi particolari guardie e azioni.

Algoritmo 2: FSM a codifica Event-B
Input: FSM-SC
Output: Macchina Event-B e contesto

1) Definire STATE_SET e FUNZIONE nel contesto contrattuale.
2) Dichiarare variabili che rappresentano lo stato di controllo FSM e lo stato a livello contrattuale.
3) Rappresentare ogni stato di controllo FSM s ∈ S usando current_state ∈ STATE_SET.
4) Per ogni transizione (s → s′, g, a), creare un evento Event-B E_t con:
5) DOVE current_state = s ∧ g
6) ALLORA current_state := s′ ∥ applicare(a)
7) Codificare i vincoli di visibilità usando guardie derivate da V(f).
8) Definire gli invarianti inv1–inv9 per catturare le proprietà di sicurezza e coerenza.
9) Definire l'INIZIALIZZAZIONE assegnando S₀ e valori predefiniti.

L'insieme degli stati, lo stato corrente, la visibilità della funzione, lo stack di chiamate, il timestamp della transazione, lo stato del trasferimento Ether, il flag di chiamata delegata, il flag di autodistruzione e la condizione di verifica sono alcune delle variabili catturate nel modello Event-B. Gli invarianti (inv1-inv9) e le azioni delle inizializzazioni (act1-act6) corrispondono a quelle della specifica formale. La Figura 3 fornisce anche una rappresentazione grafica di come gli eventi chiave rilevanti per le vulnerabilità, in particolare le transizioni legate alla reentranza, vengano mantenuti nella codifica Event-B. Questa figura spiega come i modelli strutturali del modello FSM-SC mostrati nella Figura 2 siano mappati in eventi Event-B verificabili.

Strategia di raffinamento
Furono implementati due livelli di perfezionamento. Il flusso di controllo contrattuale ad alto livello e gli invarianti core erano rappresentati a livello astratto. Il livello raffinato ha aggiunto restrizioni specifiche per contratto, tra cui restrizioni di call-stack, restrizioni di visibilità e condizioni di prevenzione del rientro.

Algoritmo 3: Raffinatezza e liberazione proof-obligation
Input: Macchina astratta e macchina raffinata
Output: Obblighi di prova espulsi e statistiche

1) Generare obblighi di dimostrazione per la macchina astratta in Rodin.
2) Eseguire i test automatici abilitati e registrare i risultati delle scarre.
3) Generare obblighi di rifinimento per la macchina raffinata.
4) Applicare i provers automatici agli obblighi di raffinamento.
5) Svolgere gli obblighi rimanenti in modo interattivo quando necessario.
6) Statistiche di prova di esportazione e rapporti di stato.

La segnalazione delle prove includeva il numero di invarianti, i livelli di raffinamento, gli obblighi di prova generati, il tasso di scarico automatico, il tasso di scarico interattivo e il tasso di scarico finale.

Specifica delle proprietà CTL e controllo dei modelli
L'astrazione FSM-SC è stata tradotta in un modello SMV per la verifica temporale in tempo di ramificazione in nuXmv.

Algoritmo 4: Controllo FSM a SMV e CTL
Output: risultato della verifica PASS/FAIL e tracce controesempi (se presenti)

1. Registrare gli stati di controllo FSM come uno stato di variabile SMV enumerato.
2. Convertire le transizioni FSM in assegnazioni protette (stato successivo).
3. Mantenere segnalazioni per condizioni rilevanti alla vulnerabilità, come chiamate esterne e aggiornamenti di bilanciamento.
4. Codificare le proprietà CTL in nuXmv ed eseguire il controllo dei modelli.
5. Se una proprietà fallisce, generare tracce controesempi che rappresentano sequenze di transizione FSM.

Il controllo CTL includeva requisiti per ordini di rientranza, la finalizzazione degli aggiornamenti di stato dopo le operazioni di trasferimento, la limitazione dell'ingresso ricorsivo non vincolato nelle sezioni critiche ed evitare blocchi.

Proprietà di sicurezza verificate
Il contratto in stile Simple DAO che impedisce la rientranza è stato confermato garantendo un ordine sicuro tra chiamate esterne e aggiornamenti di stato tramite invarianti e vincoli CTL. Quando consentito, queste guardie controllavano i vincoli di controllo degli accessi, assicurandosi che le transizioni non autorizzate fossero limitate da invarianti. Il modello del registro ridotto ha verificato gli invarianti dell'unicità delle transazioni e della coerenza del registro al livello di prevenzione all'interno del contratto.

Risultati riportati
La sezione Risultati fornisce report sulle metriche strutturali FSM, sulle metriche del modello Event-B e sulle statistiche per la verifica proof of obligation e CTL. I risultati della dimostrazione formale, e quelli del modello di verifica CTL, sono forniti separatamente per distinguere le prove di garanzie di correttezza da parte degli invarianti e le prove di una verifica temporale tramite la verifica temporale.

Risultati

I risultati di questo lavoro combinano i prodotti formali di verifica dei modelli Event-B e CTL con informazioni eseguibili provenienti dalla simulazione blockchain. La combinazione di questi output multilivello supporta la convalida dei comportamenti chiave negli smart contract, dei loro sistemi di consenso e delle limitazioni di solidità del registro all'interno della limitata esemplificazione del design.

Configurazione dell'ambiente e verifica delle...

Discussione

La verifica formale e basata su simulazione dimostra che il sistema di verifica multilivello utilizzato nella ricerca era in grado di verificare il comportamento degli smart contract, la correttezza dei meccanismi di consenso e la proprietà di integrità del registro secondo il ben definito confine di astrazione. L'evento-B fornisce una rappresentazione matematicamente fondata delle proprietà di sicurezza, un flusso di stato e una logica di prevenzione della rientranza in termini di invar...

Materiali

Elenco dei materiali utilizzati in questo articolo

Nome	Azienda	Numero di catalogo	Commenti
Piattaforma Rodin (v3.7.0)	Rodin Team / Eclipse Foundation	https://www.event-b.org/install.html	Modellazione evento-B, perfezionamento e generazione e scarico di obblighi di prova
Metodo Event-B	Università di Southampton / Comunità di Rodin	https://www.event-b.org/	Quadro di modellazione formale per la specifica e il raffinamento invarianti
nuXmv Model Checker (v2.0.0)	FBK (Fondazione Bruno Kessler)	https://nuxmv.fbk.eu/	Controllo simbolico del modello delle proprietà CTL
Graphviz (v0.20.3)	Graphviz Team	https://graphviz.org/	Visualizzazione FSM e rendering di grafici
Python (v3.10.12)	Python Software Foundation	https://www.python.org/downloads	Ambiente di simulazione ed esecuzione
Web3.py (v7.6.0)	Ethereum Foundation / Contributori	https://web3py.readthedocs.io/	Interazione con blockchain e simulazione delle transazioni
NetworkX (v3.4.2)	Sviluppatori NetworkX	https://networkx.org/	Modellazione a grafo di strutture blockchain e FSM
Matplotlib (v3.8.0)	Team di sviluppo Matplotlib	https://matplotlib.org/	Grafico del tempo di mining e delle distribuzioni dei validatori
NumPy (v1.26.4)	Sviluppatori NumPy	https://numpy.org/	Calcoli numerici
Pandas (v2.2.2)	Team di sviluppo Pandas	https://pandas.pydata.org/	Analisi e elaborazione dei dati
OpenJDK 11	Oracle / OpenJDK Community	https://openjdk.org/projects/jdk/11/	Tempo di esecuzione richiesto per la piattaforma Rodin
Ubuntu 22.04 LTS	Canonical Ltd.	https://ubuntu.com/download	Sistema operativo per tutti gli esperimenti
Solidità	Ethereum Foundation	https://soliditylang.org/	Linguaggio sorgente smart contract usato come input
Linguaggio di Input nuXmv (SMV)	FBK	https://nuxmv.fbk.eu/documentation.html	Rappresentazione intermedia del modello per la verifica CTL