Riepilogo Tecnico: Verso la Verifica Formale Automatizzata di zkEVM tramite la Sintesi di Vincoli Guidata da LLM

1. Definizione del Problema

Le Zero-Knowledge Ethereum Virtual Machines (zkEVM) proteggono i rollup Layer-2 generando prove che verificano la correttezza dell'esecuzione off-chain. Tuttavia, la sicurezza di questa pipeline dipende da un'assunzione critica: l'implementazione sottostante in Rust della zkEVM deve realizzare fedelmente la semantica della macchina virtuale prevista. Bug implementativi sottili — come una contabilità del gas errata, aggiornamenti di stato mancanti o controlli dei limiti difettosi — possono consentire al sistema di generare prove crittografiche valide per stati semanticamente errati.

Sebbene i solver SMT possano teoricamente prevenire ciò tramite la verifica formale, la pratica attuale è limitata dalla sintesi delle specifiche. Esiste una mancanza di metodi automatizzati per tradurre gli handler degli opcode Rust a basso livello in modelli di verifica accurati e pronti per il solver. Gli workflow esistenti si affidano a specifiche manuali insostenibili e a test di mutazione creati artigianalmente, che non scalano con le frequenti ottimizzazioni e sono limitati ai comportamenti che gli sviluppatori anticipano esplicitamente. Al contrario, gli approcci diretti basati su Large Language Models (LLM) per il rilevamento di bug soffrono di allucinazioni e mancano di garanzie formali, poiché non possono produrre in modo affidabile i dettagliati modelli di transizione di stato eseguibili richiesti per la verifica delle zkEVM.

2. Metodologia: VeriSynth

Gli autori propongono VeriSynth, un framework che sintetizza modelli di verifica Python/Z3 eseguibili direttamente dal codice sorgente Rust della zkEVM. La filosofia di design centrale è un paradigma ibrido: l'LLM agisce strettamente come frontend di formalizzazione per tradurre il codice in candidati vincoli simbolici, mentre un solver SMT funge da arbitro della correttezza.

Il framework opera attraverso una pipeline a ciclo chiuso composta da tre meccanismi chiave:

A. Decomposizione Semantica

I file sorgente grezzi della zkEVM mescolano handler di opcode, routine helper e oggetti di stato. VeriSynth decompone prima l'input in unità di verifica semanticamente coerenti (ad esempio, un'unità simile a SSTORE che comprende letture dello storage, calcolo del gas e scritture). Ciò isola le transizioni di stato in unità modulari, rendendole trattabili per la modellazione pur preservando le dipendenze esplicite attraverso le interfacce delle unità.

B. Prompting Basato sul Recupero (Retrieval-Grounded Prompting)

Per stabilizzare la generazione dell'LLM, VeriSynth impiega il prompting aumentato dal recupero. Recupera esempi precedentemente validati da un database di riferimento basandosi sulla somiglianza semantica (famiglia di opcode, componenti di stato e pattern di modellazione). Questi esempi recuperati fungono da ancore semantiche, guidando l'LLM sul vocabolario simbolico, gli schemi di stato e le strutture di transizione senza copiarli come template. Ciò assicura che i modelli generati aderiscano alle decisioni di modellazione precedentemente verificate.

C. Sintesi dei Vincoli Guidata da LLM e Auto-Riparazione

L'LLM traduce ogni unità semantica in un modello SMT eseguibile (script Python/Z3) che codifica:

• Variabili di Stato: Pre-stato e post-stato per stack, memoria, storage, gas e contesto.
• Vincoli: Condizioni di guardia, relazioni di transizione di stato e contabilità delle risorse (gas/rimborso).
• Obblighi: Proprietà di sicurezza (ad esempio, limiti del gas, preservazione dell'altezza dello stack).

Il modello generato attraversa un processo di verifica in quattro fasi:

1. Parsing: Controllo di errori di sintassi e dichiarazioni mancanti.
2. Controllo dei Tipi (Sort Checking): Validazione della larghezza dei vettori di bit e dei tipi simbolici.
3. Esecuzione: Esecuzione della query del solver con un timeout limitato.
4. Controllo Semantico: Verifica se il modello soddisfa gli obblighi di sicurezza.

Se la verifica fallisce, il sistema entra in un ciclo di auto-riparazione. Le diagnosi del compilatore o i controesempi del solver vengono reimmessi nell'LLM come feedback strutturato per raffinare il modello. Questo ciclo continua finché il modello non passa o finché non viene esaurito un budget di riparazione (massimo 3 iterazioni).

3. Contributi Chiave

1. Framework VeriSynth: Il primo framework che sintetizza modelli di verifica Python/Z3 eseguibili dal codice sorgente Rust di una zkEVM, utilizzando un paradigma "l'LLM propone, il solver decide".
2. Benchmark a Livello Sorgente: La costruzione del primo benchmark di bug a livello sorgente per le implementazioni Rust di zkEVM, contenente 95 campioni difettosi iniettati attraverso cinque famiglie semantiche (aritmetica/bitwise, memoria/storage, gas/rimborso, percorsi call/create, ed environment/context).
3. Validazione Empirica: Una valutazione sistematica che dimostra come VeriSynth superi sostanzialmente i baseline diretti degli LLM e i flussi di lavoro di test di mutazione manuali industriali.

4. Risultati Sperimentali

Valutato sull'indice di 95 campioni, VeriSynth ha ottenuto i seguenti risultati:

• Tasso di Rilevamento Bug: VeriSynth ha rilevato 87 su 95 bug (91,6%).
  • Ha superato significativamente il baseline LLM-only (46,3%) e il baseline LLM conversazionale (61,1%), che manca del grounding di recupero e della riparazione strutturata.
  • Ha inoltre superato il workflow di test di mutazione Rust scritto a mano di Scroll, che ha esposto solo 55 bug (57,9%). VeriSynth ha rilevato 32 bug aggiuntivi che erano sfuggiti alle asserzioni manuali.
• Generalizzazione: Le prestazioni sono rimaste elevate in diverse famiglie di opcode, variando dal 95,5% (aritmetica/bitwise) all'85,7% (percorsi call/create), questi ultimi più complessi a causa dell'interazione tra i componenti.
• Studi di Ablazione:
  • Auto-Riparazione: Il componente più critico. Rimuovendolo, il tasso di rilevamento è sceso dal 91,6% al 66,3%, poiché molti modelli iniziali fallivano a causa di errori di sintassi o di tipo piuttosto che di incomprensioni semantiche.
  • Retrieval Grounding: Rimuovendolo, il rilevamento è sceso al 71,6%, confermando il suo ruolo di priorità di modellazione.
  • Decomposizione Semantica: Rimuovendola, il rilevamento è sceso al 75,8%, evidenziando la difficoltà di modellare effetti di stato dispersi nel codice grezzo.
  • Validazione del Solver: Rimuovendo la validazione Z3 (affidandosi solo al giudizio dell'LLM), il tasso di rilevamento è sceso al 47,4%, vicino al baseline LLM-only.
• Costo dei Token: Il costo medio è stato di circa 100K token per campione (totale ~9,5M per il benchmark), con una media di 1,8 round di riparazione per campione.

5. Significato e Rivendicazioni

L'articolo sostiene che VeriSynth affronti il divario critico tra la semantica implicita a livello sorgente e i requisiti di verifica formale nelle zkEVM. Trattando l'LLM come un frontend di formalizzazione piuttosto che come un oracolo di correttezza, il framework sfrutta la capacità dell'LLM di comprendere la struttura del codice pur affidandosi al solver SMT per la rigorosa validazione.

Gli autori sottolineano che VeriSynth integra piuttosto che sostituire i test manuali. Rileva difetti a livello di implementazione che spesso sfuggono ai test creati a mano perché sintetizza vincoli semantici espliciti invece di affidarsi a casi di test anticipati dagli sviluppatori. Il lavoro stabilisce un nuovo standard per valutare la sintesi automatizzata dei modelli di verifica a livello di infrastruttura, andando oltre l'analisi a livello di contratto o di bytecode per arrivare al livello del codice sorgente dove risiede la reale logica di esecuzione.

L'articolo conclude che, sebbene il costo dei token sia non trascurabile, esso è limitato e accettabile per la verifica offline della logica critica per la sicurezza, offrendo un compromesso pratico tra automazione e rigore della verifica. Il lavoro futuro è identificato nella stima sistematica dei falsi positivi sui campioni positivi e nella validazione cross-progetto.