Certora verifica formalmente l'aggiornamento del P-Token di Solana come equivalente al token SPL

Il recente aggiornamento del P-Token di Solana rappresenta uno dei cambiamenti infrastrutturali più significativi nella storia della rete. L'aggiornamento riduce drasticamente le risorse di calcolo necessarie per le operazioni sui token, preservando al contempo la compatibilità con il programma SPL Token esistente.

Per convalidare questa affermazione, la Solana Foundation ha incaricato Certora di condurre una verifica formale per dimostrare l'equivalenza comportamentale tra l'implementazione del token SPL preesistente e il nuovo programma P-Token basato su Pinocchio. La società di ricerca e sviluppo Anza ha precedentemente descritto la verifica formale come "la più forte garanzia" dell'equivalenza di P-Token, e i risultati di Certora forniscono un'ulteriore convalida del ruolo di P-Token come sostituto "drop-in" di uno dei programmi più utilizzati da Solana.

Perché il programma Token è importante

Il programma SPL Token è al centro dell'economia dei token di Solana. Gestisce la creazione dei token, la gestione dei conti dei token, i trasferimenti, le masterizzazioni e le deleghe per la stragrande maggioranza degli asset della rete. Poiché quasi tutte le transazioni senza diritto di voto su Solana interagiscono in qualche modo con i token, qualsiasi modifica al programma di token comporta ampie implicazioni per l'ecosistema.

P-Token introduce una nuova implementazione basata sulla libreria Pinocchio Rust. L'aggiornamento offre miglioramenti sostanziali delle prestazioni, riducendo il consumo di calcolo di circa il 95-98% per molte operazioni comuni. I trasferimenti standard di token, ad esempio, passano da 4.645 unità di calcolo a solo 76, mentre le istruzioni transfer_checked scendono da 6.200 unità di calcolo a 105.

Questi guadagni di efficienza possono liberare circa il 12-13% dello spazio dei blocchi nella rete, creando capacità aggiuntiva senza aumentare i limiti dei blocchi.

La sfida di dimostrare una sostituzione "drop-in

Sebbene i miglioramenti delle prestazioni attirino l'attenzione, la compatibilità rimane il requisito più importante per un aggiornamento dell'infrastruttura di questa portata. I portafogli, le dApp, i protocolli e gli smart contract esistenti si basano sul comportamento del programma SPL Token. Qualsiasi deviazione imprevista potrebbe causare problemi di integrazione o rappresentare un rischio per gli sviluppatori e gli utenti.

P-Token non copia semplicemente la base di codice originale. La nuova implementazione adotta un'architettura diversa, che include l'accesso al conto senza copia, percorsi di esecuzione ottimizzati e funzionalità aggiuntive. Di conseguenza, gli sviluppatori non potevano affidarsi esclusivamente ai test convenzionali per stabilire la compatibilità.

Al contrario, Certora ha utilizzato tecniche di verifica formale per analizzare matematicamente se i due programmi si comportano allo stesso modo con tutti i possibili input all'interno dell'ambito di verifica definito.

Che cosa significa l'equivalenza per P-Token?

Il framework di verifica di Certora ha valutato tre categorie di risultati per ogni istruzione analizzata.

• In primo luogo, nessuno dei due programmi deve mai andare in panico durante l'esecuzione; cioè, il programma non deve mai bloccarsi o interrompersi a causa di un bug, di un caso limite, ecc.

• In secondo luogo, se il programma SPL Token elabora con successo un'istruzione e restituisce Ok(()), anche P-Token deve restituire Ok(()). In questi casi, entrambi i programmi devono lasciare i dati del conto in uno stato identico byte per byte dopo l'esecuzione.

• In terzo luogo, se P-Token restituisce un errore, il programma SPL Token deve restituire lo stesso errore nelle stesse condizioni.

Il framework di Certora garantisce che per ogni possibile stato del conto e istruzione in ingresso, il programma abbia successo (Ok(()) o fallisca con grazia (Err(e)), ma non si blocchi mai internamente. L'implementazione di P-Token è progettata come un superset delle funzionalità di SPL Token, il che significa che qualsiasi operazione accettata da SPL Token deve essere accettata anche da P-Token.

Il lavoro di verifica ha identificato diverse differenze intenzionali tra i due programmi. P-Token permette l'auto-revocazione del delegato, consentendo a quest'ultimo di revocare la propria autorità senza richiedere al proprietario del token di firmare la transazione. SPL Token richiede la firma del proprietario per la stessa azione.

P-Token espande anche il supporto per le autorità Token-2022 multisig. Mentre SPL Token rifiuta questi conti, P-Token li accetta.

Una terza differenza riguarda la gestione degli errori quando i dati dei conti malformati contengono tag COption non canonici. SPL Token rifiuta immediatamente tali conti con un errore InvalidAccountData. Il processo ottimizzato di caricamento dei conti di P-Token va più a fondo nella logica delle istruzioni prima di generare un errore, il che può produrre risultati diversi a seconda dell'istruzione in esecuzione.

Poiché queste differenze erano intenzionali e documentate, Certora ha incorporato delle ipotesi in alcune parti del processo di verifica per mantenere l'analisi focalizzata sul limite di compatibilità concordato.

Come ha funzionato la verifica

Il Prover di Certora analizza il codice sorgente dopo la compilazione in una rappresentazione intermedia di basso livello. Gli ingegneri scrivono quindi le specifiche formali utilizzando il Certora Verification Language for Rust, noto come CVLR.

L'imbracatura di verifica ha creato copie identiche delle informazioni sui conti e dei dati delle istruzioni, consentendo al Prover di confrontare entrambi i programmi nelle stesse condizioni. Utilizzando le tecniche di Modulo Satisfiability Theories, il sistema ha valutato tutti i possibili input simultaneamente, invece di affidarsi a un insieme limitato di casi di test.

Il campo di applicazione comprendeva tutte le istruzioni condivise tra SPL Token e P-Token, ad esclusione di AmountToUiAmount e UiAmountToAmount. La revisione ha escluso anche le tre nuove istruzioni specifiche del P-Token: batch, unwrap_lamports e withdraw_excess_lamports.

Nel corso del processo, il prover ha generato una prova di correttezza o ha prodotto controesempi concreti che evidenziavano le differenze comportamentali che richiedevano una revisione.

Risultati

Certora ha riferito che durante la verifica non sono emerse vulnerabilità sfruttabili. L'analisi ha confermato che le proprietà No Panics e Equivalence on Ok sono valide per tutte le istruzioni che rientrano nell'ambito di applicazione senza richiedere ulteriori assunzioni. Anche la proprietà Equivalence on Error è valida per il set di istruzioni condiviso, tenendo conto delle tre differenze comportamentali intenzionali precedentemente identificate.

Soprattutto, la verifica ha dimostrato che ogni volta che entrambi i programmi elaborano con successo lo stesso input, producono byte per byte stati di conto post-operazione identici. Il processo ha anche evidenziato come la verifica formale possa scoprire casi limite che i test tradizionali potrebbero ignorare.

Una pietra miliare significativa per l'infrastruttura Solana

I risultati della verifica sono arrivati poco dopo l'implementazione di P-Token nella mainnet, fornendo ulteriore fiducia in uno dei più importanti aggiornamenti dell'infrastruttura di Solana.

Combinando importanti risparmi di calcolo con un'equivalenza comportamentale formalmente verificata, l'aggiornamento mira a migliorare l'efficienza della rete senza interrompere le applicazioni e le attività che dipendono dal programma di token ogni giorno.

Per saperne di più su SolanaFloor

Solana finalmente si dota di abbonamenti nativi Onchain, sbloccando le buste paga, i budget degli agenti AI e le fatture ricorrenti
Noble Mobile dell'ex candidato alla presidenza degli Stati Uniti Andrew Yang acquisisce Helium Mobile - Cosa succederà a $HNT?

Che impatto avrà l'IPO da 2T di SpaceX sulle criptovalute?